From a0f226c179235948cc9549c9261926909bec60e2 Mon Sep 17 00:00:00 2001 From: StefaniaEmiliaValoti <96013980+StefaniaEmiliaValoti@users.noreply.github.com> Date: Fri, 24 Dec 2021 03:15:49 +0100 Subject: [PATCH] Stefania_Valoti_CEC --- .../mockturtle/algorithms/simulation_cec.hpp | 96 +++++++++++++----- mockturtle.cbp | 36 +++++++ mockturtle.layout | 5 + obj/Debug/experiments/exact_mc_synthesis.o | Bin 0 -> 24240 bytes 4 files changed, 109 insertions(+), 28 deletions(-) create mode 100644 mockturtle.cbp create mode 100644 mockturtle.layout create mode 100644 obj/Debug/experiments/exact_mc_synthesis.o diff --git a/include/mockturtle/algorithms/simulation_cec.hpp b/include/mockturtle/algorithms/simulation_cec.hpp index 2b8cce16c..ec39bb597 100644 --- a/include/mockturtle/algorithms/simulation_cec.hpp +++ b/include/mockturtle/algorithms/simulation_cec.hpp @@ -26,36 +26,69 @@ /*! \file simulation_cec.hpp \brief Simulation-based CEC - EPFL CS-472 2021 Final Project Option 2 */ - #pragma once - #include #include #include - #include "../utils/node_map.hpp" #include "miter.hpp" #include "simulation.hpp" - namespace mockturtle { - /* Statistics to be reported */ struct simulation_cec_stats { /*! \brief Split variable (simulation size). */ uint32_t split_var{ 0 }; - /*! \brief Number of simulation rounds. */ + uint32_t round{ 0 }; uint32_t rounds{ 0 }; }; - namespace detail { - +/////////////// +class new_simulator +{ +public: + new_simulator() = delete; + new_simulator(uint32_t num_var, uint32_t split_variable, uint32_t turni) : + num_vars(num_vars), split_variable(split_variable), turni(turni) {} + //already in the normal code + kitty::dynamic_truth_table compute_constant( bool value ) const + { + kitty::dynamic_truth_table tt( split_variable); + return value ? ~tt : tt; // depending if the value of value is true or false we have tt or tt negated bitwise. + } + kitty::dynamic_truth_table compute_pi( uint32_t index ) const + { + kitty::dynamic_truth_table tt(split_variable); + if(index < split_variable) { + kitty::create_nth_var(tt,index);} + else { + if (!((turni >> (index - split_variable)) & 1)) + tt=~tt; + } + return tt; + } + kitty::dynamic_truth_table compute_not( kitty::dynamic_truth_table const & value ) const + { + return ~value; + } +//up already in the normal code except the if-else-if +protected: + uint32_t num_vars; + uint32_t split_variable; + uint32_t turni; +}; +/*! \brief Simulates truth tables. + * + * This simulator simulates truth tables. Each primary input is assigned the + * projection function according to the index. The number of variables must be + * known at compile time. + */ +////////////// template class simulation_cec_impl { @@ -63,33 +96,49 @@ class simulation_cec_impl using pattern_t = unordered_node_map; using node = typename Ntk::node; using signal = typename Ntk::signal; - public: explicit simulation_cec_impl( Ntk& ntk, simulation_cec_stats& st ) : _ntk( ntk ), _st( st ) { } - bool run() { - /* TODO: write your implementation here */ - return false; + if (_ntk.num_pis() <= 6) { + _st.split_var = _ntk.num_pis(); + } else { + uint32_t m = 7; + for(; ; m++) { + if (!(m < _ntk.num_pis() && (32 +(pow(2,(m-2))))*_ntk.size() <= pow(2, 29))) + break; + } + _st.split_var = m; + } + _st.rounds = pow(2,_ntk.num_pis() -_st.split_var); + _st.round = _st.rounds; + bool Solution = sim(); + return Solution; } - private: /* you can add additional methods here */ - + bool sim() { + for(int k = 0; k < _st.round; k++){ + new_simulator new_simulator(_ntk.num_pis(),_st.split_var, k); + const auto tts = simulate(_ntk, new_simulator); + for(auto& po : tts) { + if(!kitty::is_const0(po)) + return false; + } + } + return true; + } private: Ntk& _ntk; simulation_cec_stats& _st; /* you can add other attributes here */ }; - } // namespace detail - /* Entry point for users to call */ - /*! \brief Simulation-based CEC. * * This function implements a simulation-based combinational equivalence checker. @@ -99,8 +148,7 @@ class simulation_cec_impl * if the network has more than 40 inputs. */ template -std::optional simulation_cec( Ntk const& ntk1, Ntk const& ntk2, simulation_cec_stats* pst = nullptr ) -{ +std::optional simulation_cec( Ntk const& ntk1, Ntk const& ntk2, simulation_cec_stats* pst = nullptr ){ static_assert( is_network_type_v, "Ntk is not a network type" ); static_assert( has_num_pis_v, "Ntk does not implement the num_pis method" ); static_assert( has_size_v, "Ntk does not implement the size method" ); @@ -109,26 +157,18 @@ std::optional simulation_cec( Ntk const& ntk1, Ntk const& ntk2, simulation static_assert( has_foreach_po_v, "Ntk does not implement the foreach_po method" ); static_assert( has_foreach_node_v, "Ntk does not implement the foreach_node method" ); static_assert( has_is_complemented_v, "Ntk does not implement the is_complemented method" ); - simulation_cec_stats st; - bool result = false; - if ( ntk1.num_pis() > 40 ) return std::nullopt; - auto ntk_miter = miter( ntk1, ntk2 ); - if ( ntk_miter.has_value() ) { detail::simulation_cec_impl p( *ntk_miter, st ); result = p.run(); } - if ( pst ) *pst = st; - return result; } - } // namespace mockturtle diff --git a/mockturtle.cbp b/mockturtle.cbp new file mode 100644 index 000000000..4f95a9207 --- /dev/null +++ b/mockturtle.cbp @@ -0,0 +1,36 @@ + + + + + + diff --git a/mockturtle.layout b/mockturtle.layout new file mode 100644 index 000000000..593c06eda --- /dev/null +++ b/mockturtle.layout @@ -0,0 +1,5 @@ + + + + + diff --git a/obj/Debug/experiments/exact_mc_synthesis.o b/obj/Debug/experiments/exact_mc_synthesis.o new file mode 100644 index 0000000000000000000000000000000000000000..c25f1046262935aa4f07cf404e63134a354e4b16 GIT binary patch literal 24240 zcmcJ13wT^*wf46snRGf|GMy%EIx}rbn%-%fThp{nnl^13lJo*;(-x?O&15o@PCJN903)p2uQ2QT~H7F-~|gJAOZ(PydZG!;8A&wM?8-Tdi4B)`uraMBg+4-wf5dK zlQfv)@t^0Jz1Ci9ed}A_`Y!vsti6X$`W5{=7b&%#u~Jo^i%#Sim&=0yH@TF0VZYpK zfLhgmS^ZEr7Z%dA*G|>{mHNSKwopKFETkxPHOXa)6_VV}l43dN>#UzBmTQE_fhls0 zo%QLda@RnvZ9sIE19U3LMRKW3frTE>zX-W6SaJr-b$+FxMbg>V-)&dwNyt5E$&oKQ zm48P=Q>!h)u%=9@Gu=fbky}re=YMqf!fvHbUMMuUT;y6dh(zVF%EOTK2O?7bl`eX5vs?Oy-22LtbWx8E3D@}74G-hNxD(LkX*@JHT$`)yV| zDead@`f)Pn7Y{(h;+|5O=;fpFOf*}2nEhaQO5C32(h>u{p9xO(x6uVZf(P-Zwn^|b z{s9Y~0bFL`0P2nHN}(y>=P`QDKUmwfW=&H|?WX#s`o`LIBe~IJv?G$rM4NFF&P0xO zBvX-8GF-cESe16Q9XXhdX0k`Jxo9kWG)2f0E%X`eBB*>Yp;aO;@a<^tbDJhIi=87~ZL`WO$dp z-GYxY{Dl4i!%ylzF#MDbtfut$=xq$|(@_h)pW$cpXBd7?e~01c^=}wHsOO$b=^oOp z48NccGJII)7=BUT#PAXQFvCancNspWOV?1kFX_b$AJ<(BzpRfkd_v#A@JanN!>9DC z44>8&Ybo7V^#+E|=mQMDrY9Iat3S^0>-rgn-_So~_)V?WQMzyGA$0w1D2I|jOtyC%r>e|Fyb|;?_wli_{hexl7)tk zoLN?~*zl3}%1V|PK5|=G$#TOd$yXRYNxstXQSwX%7{Q<_OnQ$ly?JgZShsX|snl?<**R;M!JuK`W zQ?t?g=ixv51t{>dmbu6xJT#Pv#+3VD`HXaJc9NjfN1$%dR;fr^CYp$bvr*+fG&6Ng zjrl}S_yCkW>?o`RZ#arVUsM6xb`RwKQbAiK0Tfa3{tJqf8wGxuJXXaXyKL5sN-1^P zj>OwZ0eQ?)FgRlc`*#mCn##Bu3a+!2_+QCuiq2Tm&ZIKF2^B9pYOX^2undaNSj`1& zkH1W*h4@P|_zl@J?~k~+$7ZG|JkTvA`%fe_E`_GJqm4@^+OC+fHa3fueHMxyb(FDb z^RFyw$;$nnnd#lho$@Uxn>EWS>+IHZP|W$+@o-wXubG*e7LxAX&yMSZq64-vKN+m5 zQ+UXQF(0fQOr;XaeTw?y4BBaAY!GeqPvpS6q48eQ%8hgZJ-@;Q-9C3Bjm~r%Svv#0 z&5dVEkF2~6$f^vDMzT@fdoT*Q-F^P0)R5fn%^@NLGEo`R9G@$9w}(crrj1ir7z6)O zckEWwPW_}>1(TzR1co{@r}S@YUPaMER5ml7jHQ(KG~^b>ley?{CY&%a@yO=F$=nw5 z>e|{^IFXHRh5g;-pPjALqOovdG^)ya*11utnocM$>s?3AtaPdaGlI6Zch=X|#(GTl zaM`Z8mWMY^N!2&FXRxumTk7lwFmykRxCsB*e&nwfzexsMu;?$QPoN$s`DrA*#YujS zc_7U#q1H5|N#FtU$#-%`E;DL*<4fMZfj3y)f6Ez7wliKsDNNW9#ea77jGaO0$r+UV zE+oCjNj}vXhVniLu_dNSJuw{~OhnD0Xf7O2WL4Sd?201BcszGB&;8o$iiM^b&!UN; zT}3ln5~<{H?NDkII?$SCT~*$ym8zRnnyteq@t*RvxLbNZDpM)8;~4euVhx3fvqg#H zlM?@F&6LEkL@Jz>M`Sm3{c%vkkx zGG)H8O@X?mra*6ktr_)00?*0hrQ755ejt?mb zDJ(=Jl|G@oho{p)>_Qy_XVGykH;ch(RM^d;KXM|%X58$k;G$4lQ0IoJc^sQYMN@Mw zWlCeivjVjn=jQc2Qgl7aqgH*Nl2;o`sII(3KX*4#($gtyf2Xp(28mT`qN$kjPE4a^J-8VCDC5;w6qqdhchd;dvVkPH?3Co6 z?5xz#sxi-USe`*K0S>t>CEG{mrj#1(j&^aGkU8GY zrb%DWnMsLs<^^++_g!QFUy3{P{nKd5cjj^K%=>L6c4vNgnuK;|9+%EcS>9@=mCnpQ zT`isYnd!7hXCCk0J$^#n10DZLItVE&gmmU_Pp3mVb6!Vnd6(Rhh2o%z-26i({QN9`H#5IoU&3&U{t&|s{TRb- z`ok>Osb7Jk-Q_#<)2zQs|Cr%Utyr#GFJaiD|G=AP8Ozy5d1uVRCK5e0QuwCW!by<(&OGhh&lgQ0jVM&sBUi=H7#-&OiF z_DJ2ntMv;EPwG3cx$X8{uODG}gMN|WhxKa=Z`6Nccv_!_y&AXgCOydTX8m^zZ_~Fi zyj?%W@DBYWh9B1kHpAV%zt_td-mBL${9n44;eC3T;r;qLhM(3CGW@K5j^XF@8w}s9 zp5XldPj%ly()asnANH`_zCTp2W%z%qPci(j>TZUAtUku@t?Dxb=M3tBlq%?dl??rF@_0!J;M=whG9~_$nbLgYlazJjjdz% zoUCqVnA7iKII6E?IHvDmIH8|nctU@V;g$MzhF9sg7`{(0XeT|_=q85m*ZmAn>KMZh z=&KoiP~XAuTK#o~AJVTgyiS*Gq4YQC1q^T0O$<-zeuk&@7{ia~n;AY{{UpOLSO1jZ z6V;v$O8;c_N`_BW4*;%9#B*4dV};=Ngyt<=fNkMyE)!1qIdL%kz z@{$Lu-FQk>4!P#hDi{u_+OMx9hg1#d<(L?`s}9J%chwPnis@1P5W}PTWrlJ6AApT0 zYCK}5;H_wQgckv8Yk4VMFyWWALG4y`G@$Zxkd_}K-&&f{O;TdbKhC1Zo|!<^!?r3K z0a?{A=j2tzXJ*eIY$Y@&nqrTwWJdOM1+AhL+Y_{usCge+LMH1-JgHn;DrtvgJ>irt zXt__#yJ5*v7D|ogl&gcKT2PTWbrfPc63t|kYpX@38zCoB!^*YIBGV0#gIMixrKovd zSV{%e3;fNNK92b!sBHO=AVD4n<{U1sPU{GLC6@z4PbF0l|AV96i!E;P-u62s84!R|6N zZLnhnno4KY{H5Amz1Bxl33v56-zVnr$~%eEr3@OREJ~eqJm&A1&Mw$kK6jx~8?S~T z3)&WTpq+0_65cL2ok=g)7Nk9*jSmvu86cUpF9GMBK)3H(T88Uav<%Zf)iO-~Ov~{6 znwH`D=URsCUuYVpHx0$dl<#{bSd4FW9Izh5Zuo%|o`6|?dVui-!_yfp!`6dZhOLLR z3|n8&GHgApY1qP6!=wW9jseE4E%w&If}wKvB9vz?m1mgCvysbrOv-tZ=*NW)R4qv4 z%gnn9?~sSHw}DKK{k56c+aA*uq<9MkIsNlro0GjeGbyK{y`Iq|?Mp<5YMmC-Rg-Tq z_hYQFTMXmx)M7qLQ?sewv$Lb|QQG9a1v%V=Helz#_&epmE4k@&$R15)a`}Rklj^If zirW@GiaCRw4dd^W&8H!(&~D$!Z(K``&+KfzTTmLt-zghv{y3lZnC9SUJdukh&9N{Z zzu6qGSlf*<@|f~cq3zXcVCh;~y|#O1asGTMtU++xc@E4|Udkm1O!k!nTbD9nG*8*h zDlvM}l3xXm1-uvn+Fi56n?>5a#0ri_cvl*-$3?c(%{kGC(OxR~6JbjlJLS>vP$GqK z7(3X3`;ApG$aHuTxNdcr;Y5`97`(Abr!F%BPa6K%5~a4)2A(mzuR^vHDj=l-Uo-SR zYGs|{Hsx8vcOfXA?RSG5_`2a8!JWTz+?fyrz9F=L5|O8jSv<6LCL-7x9EzsH!%+MW zhM%@LONE+9gmc(9Osl}tLiZ5;XgE1UMtsFs^ghUz6D>ZZ0$(-!58!?or$xfyROW;V zeAB3W3e?^mlusgl90|WAS$m8fBZFpSG-Hm0Csg1$p_UtvOeM!?2v6kaGl6d#9xjs2 zMx!j?J}=yW%^ksEX};($2)EYas=$lJ+^d#h6>03?I&3PC{YQ~)v{@?fl2P@32yZfW zq*+=8zGDQh1ErHFi4mL;1^&qhoCc+rD5FeySt$LKrare?1;Q5osve&ti`XtyFChU4h4plHWmlhlhG^hll1!=u+0iN_pwN!y_GLR#6w* zNuwzJyQ!nQ(V?WP7YTVuU?fARJjl@TAa+Jmd zC8vV*(vy6-qp8s>T6WgVM$;uit#dUaU z`FcO9uHEoB)i2M4TR`nHO}mG2R9=VY0ZPHunMhXZUDD&40oY=zFmZ*cpQ=HPy*e!Qvw{AcRtqK*P_d z&;g-%h%z!1KA}Pfg;LIx6cQa0f}aQ{qIf2UE)>ca#t@1trledfv;s_TH8gM@7oRR|&6)G>8M-N4c)AAF-$wjg!mL6ptZqY$8Tz(pk3fWLmQNji-AvRyE ze2zl2CpI1*LLJ{OMpM`qrxq)FW8-P;B;?Rg`dn@@oZ`VmfHd_fNMs}7Bm|a=00oK_ z3iMdzoFz6={Fs=xiy1U63VDRrGcuULQIZN>@2?`4?7p~ z;@%r10R^FnlP0Bt<}5GeLU%|xSCJ%Lpz1wvEeWtLxa-5B?69MZu|g9_dynP&*cN45*MvO6gpPAnF83a^fN6e1@)&fD^L*7o-t@izs~Nv(=N z&uG%}xR#75vd&M9Pu$)+makJ&R8W{$zRLWxu2m#vRqQsAqKLf7QoAptqO50gDN-+A z6wxC5h0LcIv`NLWvvSJRBw10AU%pJXl+zSrB1N%mB4t@@8@x&Q6dG8-?-`GvhDQcf z=tikv3K{g%6jbVsn-_#oYINeDo4Xx_6Xpx0m_3qKp@q_nD9SKzsIXIsgbHmEK1Cl+ z=HnPLv`Dm5P~v3m*)%#pjaW#*ij$JZXd0$MQ4#pFqrhn*exjjO)7VMoa)(+h;uP%2 z`k0gCg4T*D6#tkv#ZT%iAu8??DGmik=ItpIqC(Y)CW@RqnFkOXB2Mv_`K(nh*tyh@3cXrdNsDm$3wzdDSl;d_mGwOwL4&40H_v zpnsuwX(?|xaIU%3aTQu6WufTKd|50us`r1F`gdS3q@d5d8f#!@%SIveMrn}db`%kM zHlc}FW<-TrrFaxBn$O7bY%Yc7dRm-Mk)+&@Va7;wBtrFav#=<*RI(t~*{Mm0>g5(G z3q_tz%>qJvAQ!q#q$n=+tWsG7CWdYjAqrX*A%5C$W9fCe=K<+{6w%5?;UQu7%#g4s z$kk$Tk2;EHK*(K3HAQi+QWR3n9#0QuP$SEPPw}w%qB0-R+ep7$_!K8QDLqyRDzsAA z6h2#&oSa0-KPG(IwaX{BJxOgXfyVZ$(gm~+Lw^yH#^x{Ob-LB!s6-G)1Gv+@k{0N+ z@0S-ZZY7ZVxVw>-2NX*?S*pWBp|yKF9Uh7)>+n#R>|VZ}kGXh)mhP*pIJ4F20v6iK z*LK6j5qe(QAn)+piF6$v3MT9DP!LtSe->tM$y`(OrdoS8ikWGdwSC0%(ssYwmO(0t zt?BA`6`s3_=rxYrh7g6aP6?J zLOFxuMB3Nbgz3|wrSqGhGf2A{e7`J6Gh|{nwGw~1pXP|n7s84lZ)HGWeKQHH^wC6x z1%$9_UKVYMG_C(2=T4jcIbG_6wIbVN`J65?VCxq~+J5W~BybeUglh%eKej{>5`a zv`D<~v3Q?NN>eVpA+dOWkoF@Wmd@E*5{n0dv?Br9a3VDrPDq}#4j9d<#Ru4PU<#R* zT$q^+sl^9v2F*z0oJ_Jfw2C&pciSblsNG++Ypx)Kt83OCVg;8~N?Ui(N?Yn$5l~Z+FWTocI zL`PIz2j7&cporFObw?q&&`j7#J1gn5+e*6KOAl5hNq6uKl3KELUGBRfx|1sWS3r1o zg#3{`ku`Ck!yB%3pIh-m@PwG8W1hMPmXXbeY`29o!x2>%G}vQ>)G<|8V^nQzq4MqI zE9K-!j3XgLmKfDxX42?yGo#6|cm@m1x|O29rjI*}wUW$cq=!f7O^CW?qmr_+$>TPC zqcOiwe=3{CMrJI9IYZqRBlr_GfI6X_FqIvPLfv-Z*;MQVGx@wJ(!e zh6QAD4;IQ3I9IFtkiiR63U2WK9_^Mm2qmk#!Qe?91v~KikLht$cS__b_#sbEsJf3} zvkw(a!4MXGFpIT)h3h=QtPJR3K?TaQqjs5wX5nrZtxI9F&9?$fRKOQ1FQ?9SWzr zcuy6JySiUXS?Gi_zqnI9+$vSwQ?BLIgz4O~;K-7i9VTpb-*T;@Mog!nR^C!Nu$~nb z9gt48TwH)~e^vK&R};3XhTHd`~QrNFiXOrpv{CqktKkLy?v>yM#^wG!8wJK@YFlEgTA|u{p8C zX!fY8*&`eZvava6>k(D6R~Qs^Q^3IUS=C%1tdlm&PZ)X@J+65(3o`p$+)*eRGD)HyZ2Z%9Z_T~Jq0pwhXVl>gLhvzI)O^DzkP; zh9m=uqmrgW?E)*ytYv@}KE+q%jqX#sXcwEdzH6SB`tAV%#Z)yfNL!=;ELNyw;|yMZ z(JDW2@(mOlVzw`_id46H4(nz0 zj>34S#}@tpmes~3MbRZuJA0b~Szzm;U$Ch9|n!Pmvby*k469 z=7VyYp?XrBgB?=S7wg8tiVmsqvRyir#Cz&Zjos>vg*a_7XRKuCtV#|nLj0LAb1l)c zYWW9f*;zHIK-2qiqTb%@Q{4?$x1Rsl8Ed8tnY5WS@;UE~3MqVjWkO$p2^4AzB6^1GP8FxOm zU8#t(l%*Fo(#mKy3>r~gr-_9jE=4QU0F)o1!c!Ovo73{ z&laK%JcV_zsL)B|*94?$klLyi^2=h*#Hpve1I}rHT9T-3WMmPXyd>W^@Rnq$u~lo` zSCy~yrK_Nu1efLOlr%2#QqIe*)Tn5TsE)B{TU4r*jv*jW1rc$TWh_W!%4)|WEJLbE z>fGX_HhE3GLKCDaccihZL9u+KYn|1?z(YePHT8M>xal`=)3;iCBU+$kR1=}>XQXXL zS(=N@%GdjPs{$ZrH|!S4e=+>Aq1Z_XLCu>)_H0CIr>3M^Y;tn4dW$$ZgCUkyRFKwOGmezg@vH5w%xLe6%k=ak%Swe z8dX-4+-Vqn+zY#xpcghk_PoMEOQCw4La|0EQg6KsN(H380LHUjg_TM*t<-LaI)0MW zd#G^ONB3K0Jii?VDRsdP>%PB5^`L0`oSfk|yV>k_aav;XY5?-T`*BsC?BOFmkZ4_q{1e~u@P}o=fQH5oU1ncrU>m-4%O7WY$)*AyN zlSRmBIvlrBu;;-*JEo0;B1tqJ9FWA~!{DR);n;ErM_{a2&MX)O70uB`@!}0KmKSGW zI~t{xEAQUXCOo#5AYs2CBwUn@zdIp}*!U2MAWCm2iZ{UVS`Xfd5J42(l!Fv}WdtM) z5XCDRp&^n3NhuA+3b9pi_MxCz>p;3bo=lLKl+NPO8$^P#VS=VJsYohG8zsLmJoVpKu2Q2cMvO9WPT7oH?!B&Rj7O7~b4m!ZC~9g{XZaKY zmgClUnSd3152WBNaW!T;P8Gh4F3NGm2PWj0m?&5_*sCyPSkz$g-8btsE_~>NzhGiZ zs)83$twu?Uck>WS(IG6i74v|!bH^O}YbUE#D;w=l@+}5scA;?}P(58;ZMCbczKHF& z_{6$w^ys=wbgXf0?GB2}uN^#5%VX@i3tL-iQRDQPsnzmbIJY%8t4;n2PhYzfm^F_=-46DkgFWS79p!e42?slX2n*42i-UdN z!G7UjE9Tg8FFTkQ)gWoR9c)RZO&fBszjv@l9PD=vb~hT8XgP!`6wGw6PdeCV9PD)m zd&9w+FxQi`Z4UNI$fo_w!QOPRw;ara{v>H%aIjY#>}L-4rh~oZU`=RjlD5Oa`W)<_ zgM}UJ4hOr>!5((7rycBh2lJvqN*>h?R_9>#4%X&i2?v{SuxlLbl!M*rVBdAHA3NBu z9PB?GtOWZ!mY*H$JO|tFV3#`BF$a4RdpMHz#}0M}x}(q@bFdf&7onYWu=1@kmKdsO zyWLll4)zrX`!@%po{VZjU$sXILmk4fLZg6zKi*V!ux7^KaE0Rmq^QMJKB?8?1M+&}Z%pNnSriy=sUo*yF3q6g+0=O&uk}#WO%m_^e;8C3Cl^G(7;bXPstMNcrw*+I*JD zyJ8lOJ*?N#rT;7|GFYq=rCZfTnFAwWE?&UUWwx2z(mZSmjP%KbmCI&yI$ z+c&csj~qaKZ!qbzXE=`;NF}n}{pal;NDY|XOvn{~CSzw4K7&PqljvPS$9E0>+DbxF HuK524d>+ev literal 0 HcmV?d00001