From feb96f950db355e850a449838e6e2a50c1c5de6e Mon Sep 17 00:00:00 2001 From: Mikulas Patocka Date: Sat, 18 Jan 2025 21:06:09 +0100 Subject: [PATCH] rework the verifier to prepare for loop cutting --- builtin.pcd | Bin 6359828 -> 6357264 bytes newlib/compiler/optimize/defs.ajla | 6 + {stdlib => newlib}/compiler/optimize/verify.ajla | 185 ++++++++++------------- newlib/z3.ajla | 2 +- stdlib/compiler/optimize/defs.ajla | 6 + stdlib/compiler/optimize/verify.ajla | 185 ++++++++++------------- stdlib/z3.ajla | 2 +- 7 files changed, 172 insertions(+), 214 deletions(-) copy {stdlib => newlib}/compiler/optimize/verify.ajla (61%) diff --git a/builtin.pcd b/builtin.pcd index 71d52b7fb23e1af82bd62940cce10b3dadb2e35c..22081fb24b1a446ef9e3db71eb73f8589474b811 100644 GIT binary patch delta 70038 zcwW@K4_s7L`agc}+&ge*?j5Yi1^M*kOvc0SseQn65&JU6$N|%LHTKl!Z zMb(Bpk*c1Llc;){C{p{Fp%OKGZSYcFO0qIk%zBXQ>im{?X-cKVX@?VrAQuk#!DwW61 z6Uk?aR;cy<6p2c1AFt5SvAjyIEu&QO4YG)&zOJE0o&~(T!i&_jT#~5logp?#jR1kx zOL9chV06i-cZv(ZXiJ+3#n<>$;n}?~5?r#l#Luv#lfBNH(KWbs&;dAXJSFOBsKNWh4NZw6%@{i0PnDO>vOV8z$mePETZ(E`L-J1yk+9Oa-y5dWnzopj z#wWiw{F0}Z>l2;i%l1oDe9WLyWr-0|`xm5J{-dGLlp5-wm6AtWlBnSZvqJ69<|MaX2f0*a=7E0a;X(}P zYic^RG{xDda-@(>Rp%_RQQluvTaebV4RN*_w{SRSVTku3T+iQmWF3WmoUb3K?z|Xr z0_$RWuOi{@5ASuY2p<6-cdu)U8cRnB**w*KW&nfrCO>t_#u?;$Znk8dgZs?jO!&;i zX9OLw3R5XnS_V$L;R=}QWGv!>-iEbSh|h5t5UatAsUUQnXD#9L8SWL*whz?=Dwz-u zm5qv!D1ZKV2bFsSAMLv`HY;shh_gANx-NV~eCCC&v-^W7qs48f%4_US@@Bxo3u7Zx zD)uav=)hPQc3B3fWqqb*ky31x;^u@{2$Nb6I(li_2C$-Rwy2zNwj{|T#d>vS}aoe-y=QxjT!j(>D95q80wCUS86f^H#t{X zC4LfFlV)nxS)t0aLeyu`kxao(wT~9T=dE&y%yDz)gbK}|HKRsFTvid`5`WIidF0InyELTqcFCO$rq3(#Rzz zE990i9Ll#b3ROK;q)^$iEQvN|2@aD#L}v;;mL<%kw#kB&I1=a4TyS_8Jqe$@P`O!@ zJA9c&?r{*<)X=p&${ivxGcR1}zoz%(5?SlK>E<+Ew^^>P9~n{Le(h9pi2@iUtXS`o9H zDWT&FwA!{fi4NAKC{$}(tkis{O5_~{PW-jOnhWY88;?1(Gc{79vfrB(aB<`v`w(h)*dS3;j-cw|VufbXrg@^4 z$Yi^oNiTHS*Ne@mv}dtdqvq!zv!5U?2bKLj5dm32jBJ@8C`Mfbw8^&E-i!0ixzIi5 zM8O#sW+5-sY)|tA6NQmyZnhf~a?~lGAl)BGlhANti)9 zmRsFaH_Z$eSp4rqNE$g;6SP^g@x!QlKx@r7n@OK9v!_|05wT z-)0a^)43pe-~-lpZA%sGsp{NpgofXsqX$QhPP!d%P>b>##H zG<&izi;i6qlSOS88BgDL_J_XLSre!!4_Kknqlmqv&~_C(PzLR}AW0+N6gWy<4EY>G zP|02)AvxT*FGQ=a2x4i|R1AfGCSp?k6v27M?(@^>b9f=W-%V|npk4G)_(1VKg$}-G zIOV3UQ%!e6RqEGI3)%VFbdz3AqQi|vfWbwI!q1`g&kxr6F)f{#_f3%KqvGv=7WW|ROt3J0G1ilakHxN(`e^%Nt?iM*Y{997Im3BVCO7$ zGZ#HJG`3pk+I%huZT0ac>vUn*sA-|oX;ll7JI;(}OK;=V{g|QbCqMk|C62#ksrGi@Xi-{tYl{pntIM~aS zak&pomk3S_jdg{|PSrPH)S61*=!#I~M9Dd{>D+}{O{w5A>Y#)6lp5hZ$1f1cTMCuW z`69n};nk(WNK00T1>Gj8;6ExlhO(xtP_ZoPC>89zYOS9*6_DW)fPJ+ET(~Ym&x!_H zZM}51qH@!z8GECW7kC__F9$fa6bTra;EDE(R^bu8|ABzVKBY0x@` z$8^MGru7F>G$S*PJW9SoNPzd+bZ3E`HvSu6zNHk-E`5cd!p2G?k#$I~MJYNyn-Ln$ z8G+n;H7foOkm2$_%(9W|PQgRo*NP;|NUq0#77%|8k_6u>VFoDe|0qkN_B$clst=F_ zH>?sI{5<;eDq*B`UZ_&oc<0f)Dj~thXsA@05`p~TN+BO({(6;=L_01W)>n6_^-9NI>j$EzP^hwg>Fv5f@DGU8a`FsI zvGq$&=g(C!5dMBbhrKrrgdn)gqt=%r73#WC4+m$bJmV%|#ZMyoLZnLm@h}xNMw9v@ z-?-~$;h>>^`b-L5Qh$l`zdwd`QPlo&AfgzUY`1Sfj?^zLT>>Sy_Ak-KUAGFp0eCv* zKs}@`i%=}Day=RDSlV`*Fp|%qT!%b_d?kWv$qC(NP9=vd82-BQHUh>^aF%S|r1^B&ME$?*1B4XIZx>ua2T9Edi2xBh&~U@;!bUiqotvTn zitm6Rn1{5wxRX(H8u4Qp(1wS!?BjZn~_Qbp^^G8&}w;L0JH|y$sobDy3mN9onRM(?9G;}0aA57_`jf9{7`?L zC(mPoFHl#~zqT-fjb+;fr_eved}>``7#K;a+7SYEXQkLbKG2DEJ~ogJ50Jg1j|ASv>6>5EIph;nE+Z2^r zpFyx009pUD=$@~ke@klI+#rbj07>?r7wDWeKNE73{|$=bE+OY9Par#}X|_wL`Mpad zTMj^nF9y`RY>090se;5NX-*xmaln4v-o=g}Id6$oXC+k4`-gc_plmF{^mE{(u3~{m zyWSRUR9=yYM0FJ}1t)EPI-mN?ZR;*wt*ki^ME|S?oR=y8hskxlO$W7Y3{8E7g}=g- zblTwzv=GK?Q3SLMob4C0$IVs>^vBRUe5INr^Y+1Q)mc z!$grbE?AVa*&)hyyg%3Fj2t`~>kU$jM{?$0bvs=UpJV%Noi?(J+5 zyb}$UT`&#<5`k~ZXR|>`6d{LNw*L7*j!5--gR5m5sn4c})HXu&)$A~cHGjzlm(`0< zeflJYd~I1yYAEtz?A}6y?S`pfe2&BU|`(7~oqqPMZg1 zI>_B>NT<$Ri-Q^-RUA|viyPISz!g<{&0?S(V_jb81)CRUyBfV?#L8nvw%Tu^BRf=$ zT&stOq^3g++J_lSsQf*X67VF8)cmVdsnMTqtjy8(26#EPH^5qIOrWDB#u7H2#*MtK zpwx&@L}Ni|EWNsV}43sOxAn{;dLDZQEu5TRwnjVfP@NvGD-1W4*iukZ5B7axUvw42`)5vZ;JIR-v{3iL@CrSrSbdadE$3 z%hqL^d{Sd^S7du6Mrrb~$Ru4@BXnUUFE2`>ebHd0`dFlBvT?z`_}~rK#mHdy9*cD9 z6MW&Dw#HA6McyqM*-SG>+qxqY_?X5m-$!aZA48A*5P3J1B+p_g|6HZf|6`<|C-oUf z)zbmfsxwM3nARBdVuw!(RC`2f`O+e7X_Z?0l&X;>IILRqtCg23b)8Pvb^2U`^b4w< zkS3xxdkj(n6&5lO{UMD1m;uxsH_pcp3Q{^X9fg0{I*A#p5WcaZ=Y}9TgV&k`DJys_ z@6I^2Q4yt$y?AZ}H*N#E_IjjbC-37%m3CikhFxB>Sf#^zW7V2sUTSnplDkhwi>Sm0 zr|UOM?qK9|KA((gcNns$eT*tnxhx@so29Z-d+rE|(6>QSZu7_zKBh*GY<9>ur@tU@ z>r@Ovx4?~u!|&uoZY7S@5h6ERg6|(Da#IW(SML!ygaPibSL6zC?w%=fzY{r5Jy+y9 zP=0fX$Q9$hxJu;ClR2*ZUXeQ<$#F$5iku(!w>FF1{Shetp2!(+?)XsTZWOqiIpuSa zyBmb^eiXSEF(6q6Blju_ zir{GZmlF3LDzq9*T+vW)T5IC=vilF1xHoXDcrbX}{jiC98OL2aOx%@Li2C0q-9MMd znzY41)FI7HA1NJZJ~pzj+>e>O+wB|c7YI`)^ zL3Q7m^DXSQrjrGRp>5Yr)Tli*4hGw8t|xI=gh~zf!A#q`&D#SN&qzjAHih=@GicN{ z5~A@9ngoBc(g7i9h?O1#Kv-D=%-;12#JLrp!n^rzQAIwHR(C8-z@c;)uaWZyGrDA4 zAko1W03oWg5Qn69CN|jgQX5|lNTg}#SDtW##xvBLBv-1S2R=r2bH>M>}^&x|U z)S+-NbuviQ!4K6RU4|xqL?>I{Fp7c7XGAI-f`C!^Bm71mmdm9DF6#Oo(8`_4V)2<+ zZkMzzPT4_6YvNQocFsK8mLfR^H#*iw+Hu%(L9|9yRiIG(QJ%Wxpsea*GE(V9i?teF z&OeoP#MMjF;D&g)F3>qeB8NfFp`7W6iNywF4&9f#B;G+g{n2)+o(sl3w=RLobs#KO zkK@HabB7cZOuIq$oK7&Rhxz&+&q17?386G3Mg~PhC4!tzzIo_!)g!YdDjE_Ege}NE zJub12l}e))*{M8g5s>IcC-iyD68u{UDsB;V^=rqz&s2NeD7nijQg?Z#q7UNXKP*u! zZ0D7}>41?%L^BVe<|l^%q`ZwVUduv4yC^GsY@lGIMjIcQt&lXzqEg)rFhfSbln^3- zDEH)2J9#dPSAwEYi+~mUe*yw@wF370?_|40jf@s$44S0%8rkNd5OEuBnb@w!N{;Os z=x|4A`YDUS!)bNXKwXzUP|cNwlLg8~My~Oty$~80fxhr3S?R zz*HO6JsizIrH0gLDGIMqKHXj!3k43R| z6`~05d}ZQb<(a$EXp=|Mc$M~irD}ohwTRibGqy)0Dm23?yMrT;cOH1J#wpy+wtpvR z)M}NB@O^l+{KN^%L8t<{>4=ukqpB%T(440M8T=a5qTzBAd;5))m4BEeQoa+ad6*UUCMURP?@D}ACrEJNd7x6UV-^%V$_{%;16*(Y zMiNcTJeb-3K)K&bN!0elJQ(W+r1cf|0G7LML0ssb<5a0LeUdHU--Da8*%%c}6)nBB z!$~_+Od1^}5pMmju=T19CV=N@iE5zw33Mk$Rw1X){{+Og?{eH(em!!S+QD#XE{7d{ z^IoZOM~vLUK;%xvoIvF!yTnIOL7|XD4Hu+}RO?NXXvU(5kQjC)K@4Trv)PQnOi1HR zQlsLK+jwfa1AK3M6O?;=t?$)Lq_LIWW(y3;vvQM3jwVq z0mAQ!hXGbQP7?m|r2;%*f}BsSZwXS(y%1uZg}Fp0#-r;k=F_$>RH^kcj6&xXa4CmZ z!xAEC&&pZ$8s@*t$Hj`Y-6eadGQAkC!-;Pd3G8(KVzH)z>F)h8$mZt5UVN!?RHGsSttl^9VGHsZM*jJY*H|t^9M%GiC9!Eh)iU3ZW#2^~ND39Qp4x*@wPv{spfyZhz>W)#1T!Y$(vr<&Kz7GdT4 zpToG<&6p$7hQ>4pbtb_PT4~R#mLcT306ww{1822{{T&xv;8UsKQL9E}>m*0O{~r4F z>LNsjTqu5pORnwBz9$*J;zWB?X+`!>nJi0zmS@q|Ba6}O$BUswwN4o7UUaGI0r=_s z^PmLch=kw>>dmL0)clbLVTkIFsu)lYAo!(VnCw*g>xBt555r4I8=wFiX3PbMSO9#r zHU)i3Aie`JWCe3uox70ivG@>49e0Zf)P5AOtCj{M1N#mMa^1C&03u$at(Q8K72w~Y z)v^=nFe)L|PPRy6FMWU)p68S^gQI+cNX-xo#TirsH7tqY8fVuFe;X1GF-=}hM{|%j zxegg1!!&tE9J7YXkOLUrTRwsP4`>19fI_Z_oHki~k6YpHtz%%#l%C0Lu0>ZEqJoEjw1{0XFX z=!)4ks!u@OmcvliGf;NW#!(Pz-lUr`h`O-mJjeUU{SUVPNuZs|S-Q(*J z^-8V+yeX1J1t_H;n}sUlVrWN@Wxaz-Js-}g!+&`tr{YCRnt>v|bUm3I==3|0H8QhgWxRbLC> z+`blyTDfUFe9FC=+E_JJUe2E+nuy+_(Vs%;{1va%Oi5uA(0K}ZH)N$#$$P-7Wx2>> zTBe22RmMpo-IELPl%+=~bnq!>s8YKh+US@D=lU}>2hw9gJ5_yDYQGf?bSA~ZR-*Cm zbe7a`6qu@f29xlGNY-6hr&_zp?)oPuxBKoOY#iv&Pnc%;GOHfnR{9eYG&iC zq|pLg`YSYXIwIxgAY+cCP1lKba{DY8vva^|$^EloC9gz^_lyA)eIKGMtGC0y%!EXK zjyxM?p4JkBqO6GnhV{*oPm$!Qiga4XL}lBBkY`i#b=Y03Fcx{_9^UPmn?Y7hPkrG$Yv;b%C#U{ zIfnBX3wMUOjRaC}PE%`UL4xJ^Ck?@XdAN`dE*RI$lMhpKyX7qPn_q{zx0=le8M}w5 zYS!*f+vLHUZAi`-yb5S|9yG<%+% zwqDGhg4unJ6mY$Zym$c`DL)83KK3#ozMeWQUmzC;XF(rxp#zf>6x#YV8ZYl$g0Wrz zl(YNINlIXCwL*#?p`!Mt!GMsLOoHdWPXHK9h(cWOV?3K58Yj_ae<SESge~vY5zA7cB=b)9uo9MSVi5G zJe3ZZ5qzpMd0@T*@KF-WyHBtH2``jweWoPW-eQaTqqayX0m6#SiQp{1sw0HI>#dMqb&B|Jfbeg{AaSE z!z(jI@@7U!7N&>n!@`=0_AipBlKMM?5-6W81tr-18pB70OiP9c{h2_I`m`QX5C=;Z zn&^syi=yaIAu{`8zd9Fg;0DpnCd(=t4=k2_Je8A#g6}M_otYNU8Je4n_+9<`><}{3 z6|#P*>?Tz)4@jZUNJUrc>LNG=--|{R{taMYa}lUCUl=)X$_@1ZgVkR~Is(4idsDAC zm+{Efo(D?lj69YsWBA}4`She*E8+NBCz^WEtFiMTUl=ChXjIRWl}i@p#GAPXV6?kj zX6{A|{f-nfXM^z`8*Szu$9Y|bnR7w|)rn^A?`(Z3*UX*c=D4+An7K#eInH*z%1$8Nu2VvFl~?32m9@C0*U-P|HS}-nxo`a& zKbQ8bQng?q{jqVq5c|f@4?a;|&KM{+vS)rqFlYM_yh-JYf|58dWQ;?(o+s4(;cK*i zAIR1&l0xj2e`ph_{tvPgJWc;&qGFmG5=I)WSF@9-=_}Z9$yX48^Fows&j&MZp57k;*%18LpbbxJB7ex9vSUk+nES}m}-{XG?f6R3I#E^I%z0My?r zfGxZNrLW7wXzkPRTddRk1X{hlNTUsZksYT{oTO9Kds}HnAawjAU)71}e6#K_ z)WLSxuz<&gF@+}oRUUKNZe{D;vVJ7nEh#6}7cwN; zkTa>I<+Q~!K8#L)8M58t(a->00-gsHk+!}8bM<@&&+dp{tWxdrS@6tnFqHkzd1Bhp zUXO*cCn=mE-dLkY!vjZrt2`uT2p8O8#6-j1v%q>fm^xk-?7^LZRcxy|lhYQ@Vh3&g z7FfUgxCYTBqFMIx1b!MNx5%3HXdi``L_5DMNw6|49};4LEt(IfBY!g4YhFnP@cJDF z)wftv_~DehA6kB*KZ&fg)Qe%}Aj4KPNoU;Jm+_Ib^C8gaVY)Nh<)H1qi*k}{INV0X zApok*22tXDw5iFgQ8nA(=5PSFU(F!?y|NOhLL#k>87flCui4JKFHAPt`v7oI*H{!? za}&f{oUsV7XaVjPpT~A_KVlH6nPo(5wS`Jb0rA`i;DH(%3=H8UBN@m<-DBg~BKQyh z|AwO`CzU@j1Xyj9qy+r$u}PM|+KU0FrYuNjj}^n;Opv6SXV~h*mGhB7`KCCH4vwwL z<^E>M5c2yIkWN%sY*hSg0=(Llhyko$)c&POrMf1t(7S8t@Q^sGssiw2n(d%H4~SZ@ zOTMEfHK1IsQsH@Q^X*UWOx@5)uE1`u*LkQa-l5uBRhA zR~hW&o5E(KUq{SpzabaQ+@7oiT8&cjH(ZZ3F_T~kO?v6oS6_0~8dv(NE7!QF;Bl)) zyH^RSC6@~V&QzT&{~A);&O|6>E_KXFf`_aS9Vg6<*>(yQc;O>+)?rlhwk!l*9ILn} z|6N|PP7CQ*Vn|~XDft~)qms9w9o6fQBls+$WH}ZhX4Ffpe_Ng!#|pE*GZ5%x1nNFj zf;$))vqOnLDBDfp2gFRY({6y@zKXZ;g;Y@I(`fC2R3~-aV9261bK+Es7OKeJH^9^W z=X{yuKgX`dOb<~=47JQ~#aPyA0{PxZLVP~zP|2$T$W@5L9l?Z8@kJ;BhT(i|kbLLw zjG;Zh6~A?2*lsi{JrATwR}EFkF)7wT&JX2a3Cnj}k1&VQxOe60Iv4y|xL7mPu7=3p zWL8Z*((8CPBt2H^Y~lwZMnb*SC|SPedLG|Pp)1~#M^f9rP(pn@Po#VYo5WjXRGmY) zp2zsucYRUk($bY>mn@%1%~v2{&wJgV=n;t$5V3Hx5Dn zsO4HD<9a-n+GS@9(;?;<-#U6nE2%4gEap(htmle0b!xg=nAL@dCdyzz47fljRbRZZ;)+a`2LF#>~ z7C(f4t@tXa!`*ImL3C|4~Y3C@|WXZE=RNp4+&5Z>Ry4tK*!|$eIFVbS~ri!5CRkJi| zyBM6NCn5K7ZBmd`&4Z;S(f;hYxK%V)v4-D~#NO@1Von?-e*$pc{A~%M-zLR9A?%{K z(2-Rb#s%M+!gMz=q>2pJ>2Zz=PVk#(+tVrbn2)%gdH=DY?+At80j(bWbF^ytnCo#` zZo1-g*{&OZjGOE6jA7U7rc#;h_G9MJe5YNcrn}$;*=e6}x1Z!tv7-0okT=O+fGn=; z-PtzEzip`!s5?&zlw6=t$@v)K;ujHxD<(=?4nv4_I=@ z*J^-kcz-6csKGG&=1t?Fa`B@@DqB5jdsP1nfn)$UtEuvWs zG;D!xT?Zp;c>*k`_qjp*{9O3`%h+@@+sBe1iM&XA4#8KpUl<|ME;ADSll0q0b+dgU zDfvPW=P0yoC?Cc-{{(b%z6*n?95F&X@zw~o^?L>t6d6JE?`Dx7Ona_J14;thNOv!~ zzUEvWI8BWNRviuh*ty0m@d>p4T_B6HDGMdayBTyV??o*yJ5sQBry&;u)C-*IdMw8h?wZUHwM3!sKGOcbs)S6y=nmA*SW32rA=v3zk7 z$&SL*z9eaRkp!Agvgaf^W||zmXr`P*GxtYJ5*6Pcr&x}1J-BEn?H{Kk7@6LRWPNR> zR#VHw@iFULwX7z(dzEG1SsZYsPoCmRFI}~q3aSAdcHb3J))W?OdTW0;r0eTR!5X92 ziSZ|brRq4z075l}T!G_@WERdKqo*EgSiIBMsXutXWa~)JZQWOIv zAD=NS1?m&dOqm)U6X6QH@F1YW9z=qe(30bfL9X@}E`>itJM*k|{Q(RQ9Z5|~qNY3q z7+3yK_=Gp36p6i0koj}+&okP{TZ$1-kC~99BrQ>Ue7ecS1&s`Df35~#mN!TIpZoUD zxHJ0p<&uV+xl~k7;Q#-nbLUO8M?rq4yZ5puW-Iz8=z|YQYQU$meGg7?ODCLck87{` z5Cc%>bYUpoJr^UE93yRM=Jk+p&rD=4$5IjLFR>su%Y}wK$z~wNWg>_?3b6fCH2~hS z5QT+)m~j;R!%M1c{cLIYCqAC2GF0XWcGFo zhC0vejY4~J&cwBsy?^ZIV%C;#pc@At%K~Gsu$*ND)b~_a3N|i5gmE8}6+W_8wBE~B z+A5}4q5KP@QTx~+iP{gasZNGLw{I7nRKJ;}E4hnoz2Il+DA{(;OE{Tg4FXU7m1H^= z)b}w{pwGXFABjeJkxC|h~{UkJF z(rDTfF)4{!>a$c@QMfF$X}*%lsO=Vq8mP9aHLKkKW^^9lr* z<{vO>E%zm=iD5%d3>`1J=t3P81mp6y>ErFZmsZobY(j{U61`lHYYI;j>N7feD@SAn z8SKy;k@h)r5S6mhRLVQZb}0>p-Mc(!{?HTIZiAJln_f+eO->0>8*w^n9E;rBDj_tM zn3>pp=Io-VG%g>Qdkhd!^YCE+R-5A?QiIt^`|<_Fa)9fdzNc3ZeO{0;}G+YVXtIANux&&BJ z<>*Nwt^Ho!NC%S5>ExTjzptcI$vg1>{;^Ia z(A32qBwh$7{#LS$%KxLRrOL%<$G332Xk=>_3hmsUGL`Cvjt;Jl1Xer?Ptyf6apf(7 z+kZI4LtP)jBh_V@k#9XX5C2jCsy!bW*z?*j2A2o1+B0W}Nd70riBvQh>EGVbMlY2_ zC5Uw3sYn|wXWNH8zrko#J78yrjrmDdwqdn1ywm=u#c2eY3_~&Wf4QUC~aPKfN(9kMUdGQ=T|I|WA_UL?tx~^ck zPW?Q5Tfv@|y$w`y-e02DoQK}HRv;+0i|}8aBN0Y@{{&;r_W+nQ49=JI$A|;XPe^oZ zJM)TLQK3g9yMA0~qlTfNdqOU}g^o<{0+(A0QD~T~BnEKe5Vv=Um=YC=Tw{~As&|CKbUW`q@{s-n&6C*Tk&|FBRAv~2@J!_oVO z%=s9%!BGzVNr=<6Qobz(f_gyV8>v)@O`tp@bZg`A@d^)^HH^0#cXRso^Oul7bzR3E zskfl1mX)*6_vhe6w|)zha;%b9jK4cw!Or~*gT9$5*4)KbVOil7H}MMp0`VpALPw2? zgR<5SQUm_V;5;hxkx~#RmFNFaw##K>|X; zUG<)i0H|hyCEexJN1B&+cx&&8Ht z_fIw_P|24_R_jnrcV1MzH51M@lFh-t6%W%YX36QV*q-6%X2IrS;GV@uC5JZu#sJNT z$O4W!I9Q_c!{><9UXv)&jyvMv172oNUw<$dmhmLat@=m75meWbH!!4K`7jxM(^&O! zkv-v$ZvUT0*b!hV<9TH!JUb)N{uW!b{$;92n9L@Vu-h4 z$Xto4uFbYlyE`V8s#d^+x;_LTliq@`)Z=48VHu3B-H))`oRtP|a%4Ul|Klu?Y~?w& zo&d=Yq9gt^J2j=`putl7la`~$zFT=mIBe3|<$zWts}o#Qce@i#dGc%kkr(GHgA5`4 z(0?@GLR$6YxS@3LPwf3^lZC7;Eg18LtDpyMDZ`*|y(O_^0+vALT&#)G$|a7kIu!1q@qU<_M6UtproXOE8}wG_Hg zzYKS!YXKE2#z2rQv*4_|-m^f;H^D{jXlKta#anDO>L_UBT^1)b{2pcZ6|#xbhs1R9 zSzt4sNAb_Q5Bzu4foAo53%vVUrs3Bmq*D7W7%R^XwomEWA*nSRhA08oCAOMB3^mbR zo8qGab+KUl?;30}0~%kE5u?=Pj~6YMU9#rF8!|5h&RJD@1??PbTpE1+#<7>s72j)V zY_m^hI@Rsr(=l)h%gFycOk#Vf=%W>T5f*(HAgUG59q-h_E`Z}sKqpEn9v4IP)5oKu z7qg9uuVv$(HrYdEk1($~6j8SFN~n_h7Hm}4i~Ltc1(6c6rra$l2`8z-&WA?zRt4`a zXl5Q2rc>psU^J^3E=srT5?M)wZg;#SCy;s@djh2{5%%^vzNs(Ewtyp^y)|T(!d}Xp zrr60pZMMpct+Cyr?B%KUFl1bPS2jF%`WRFe#4Pe{Gf6e7a)_M&0m|NI#>gB~l{`vM z9j;KmRVm{q(C@6u+q88|3|ksjO87~%hgpTHDSN5<2uyG9Af$YiYzN4r<6y8h#UI2H ztw(Xw&wDXqmmc{*=2x-1Pr&k<*+W#-)7j4bhg5hN56g8jkg9k-!`;ds;DU=|+2eQC zY$Q=L;oH0)WI_w)JH&t=p*uewG+ULJ>VQXZ)O5l4mw&CQyn%8b8Zw63ciI5}x?)1; zWUUS6{iy1s=2FP4Ar+3O_G0$T>;u^zs$DqVN#%?G^2E}i&a6NRA$g6?U9F5Y?$#v42 z>J-%&oPR1!nVLjZe}jd!J#CPJm~;kjTUQ~;HEua!0u{4UyOUVOj4=tJm^o` z5=G$!;uF{_;2U9Pz9;~_`bvPZk}na}t70Z0@GpWUHC$#(rMjq?GTO0JQ7onquyLhN zcEwP^&`BB;JiT@?RHapgLn-+Yrn6zJ;-(fW6L+&y3>5znzHD#=^!FV2Y4;;+ z`}{3wO2A*Il5aF1NW-s@1^adZymhhnqqGiUdq)>WDgn2F{5}eRFem?D=nL3P`zsH4Yrj_2i0WbBpm(&#^#^)@C zF1CDuXrNxeUJ;NVYopE;i(wGcG=Ram=h~<#7ICYR?U3?*J0J4dGY5)059JzWEP?f~ zQQ_f*-`QMR#YF`FmuXeywmc&ei%mrX@$HVb#mZW!)q?@3FP;bYYz2(>9%C;SC+WN6LOK|}uWw+Yj+fa>09fwi{4x&d`4zJiOZX>4f+aE}tDWi(u*mF!&uIRQ zEE-t}o;K}s+PBo=hJPho0V_O?wk5(9R9&h_G2vG?vq`w{x{{lACYdzKU&7wPbQ^ot z|2_{iv`Q7@!s|+G)4}mxTWoTvU@HJ)`t$`h%0J{lCiw>Z-tL<~AwM}$f`=>}39&mL z1Yl@7qOv(Qgf-=Li)6|P^)!h}uZTmo&7SP7nh#~px+D%JbR45ombe6TRw@!(Ea2Fx zGy6>ya*Y#g7B($0DkO?5+B8GaOruYnmL{Q}JGLWn@$Cl!Yd&U!DeI})_a({%eMTc( z7N38IR-~Db*vedZM-;pF&(LBo>##(7N(8NDF-)}SpHTItuic8icY>`5haZ|OppN@y zYA0Sk8y+niZ95*FKyB@8_ii;R`=^eu@nZtX>~|dQibMz$;Rw{*kpC>C@mt)cp|byy^g(-5hQQkZOt%_5DX|xqzu2`$Zx%Sw|uW zcP#+Eay~m)(zoHIQOD(iW@M6FPy6qYH52>FeluY%ZF(Sb2(|O<4QCVJU;M3%4ff*L zwpEegmF?H&Imr30UEwbyzBo21Pz&trP>qW5L5@uu9q}TCsd#BFDmGe~R%K*gQqepvoSbIBU=Q>1~H8X}|bPNk5+wEM> zuTimgZR;yUo`fPB6{iA;`Th*_v2PFJar^WIBF#unR54(>M)~s~yY3su|J1Rxj1B1x z8%qauOpevaHByl*cW^xmt7B>P*Ml_bx*Pzi*MORsGG2$zwL#BPvM$L%t()W6k1#-5 z4Qv5;V}`Y7IBDZs(F$aqd@*FMdw}9vzL%(?P7;;XnxqA#RGTmqUS@rQ7#|i6+dSUe zNpFIVTq_Nw_9Wo8@&fR=ch5Xk7nA;)I+02r8*HciJv1h?mN^`O*#s}g^{nv5)BXht+ud6L+^)+k zooAazxBWw~lbbz;)cuAC{M4=(hv7y>Aa|J-d<}Y2m#VP0k2@pafp$UJ9QV7RGaED6 zoAI2IiA^a7-+q(3C)Q4f-irxNAl9&LWbTMb61BG=J1_bBT%>#VOn`;mFN>5_XS30< z<=MULfZ5pm>juRJj%5MV-o6;R(a2!w=(v!@R9y>C?SFfm7;uhOER4+&q28tk`%%>a zUsC>otQX*i(Y$?TbnZBN>a2XJKE$GNJ;xvm|65rz*5T^|kUk=4`&IKL!~GmR|1Wtc zHT@#&K9|=PIRd`1(3v7$G2Y3sS@@j-uTfnqdr!^lL*dINAwX2QqaDG7qrDXgNyWWL zgFO?J9Ah=A+#TqsN8-CMQ;iA#>dJ)Bk?FgMjvUvt9#tW)akxZX#^EAAHc)^>rfY(t zzZOObz8=4<)E@Mp`UZEzn(GaAl0F7-c76b5c29-YdqzS3yG9|w*tjQIiDN&<)>}~@ z<$glI?`@lG>A)J)*W&VQg&#}%r<~$nGYnC^{cG_y_^bAp9Z>hR5y4HLq+Gl7RD;Yo zUl|h2WAr^|IyT)p@!XJxlsz^Je)LL%#7f>M*!y_mO13l5U1;pz*IM3SZwBP5jk+05%TyEr0 zk;GyoU7?m%SKIAp5=4mimRHREb6hGo`gT_j4Ba~nj^W$69&hdEPW}ZWe`x5~`*$RI zeX25@n!Rq33P;7b$aO6`BQ1+nbZKs6_H^7ngM<@A9)lUA`PSJ`!690)**Kd!2&vZqz*DjY{ zF2SESvi-t4P;2W;yvk<;3WoP%{QH(KRE$jQ4$7#r*=g;eB`3Er`5iT6{U<>Z+fOk3 zj&ivlP3!5mYnIE_AHl$;2ke#&T#v(;MWuh8lRypK>0(UynHIKi+2aJQ@fr|H$LF#} z)qjRxsBbr^w67cPyPE~R&d(u~vLk4ww!;*f3oqM<42q3WiO{=0`v%M?dpzk(n%uNnK##dItCtaWjHdlP5x@ zPOB`L*v->|8pq#|clO|!@cSYO+H|}(h(Vj=iFPee z{&+~V`FY0P6Be~A=E6Q%?j@!7hBv$8=QDV-#|nSnBQ2JFlXs`AntCS6_OppJ}XGp(B2l_P#k6Im7RxAl?^!fSUKl z18U9|B)%h%I|eZMw^qe+71!e%X3(C&aS8kkvKWi(@QCY2X_gGGC%+#-+uBVUxo;gL zQONH=Ey-J+E2c9Py%gz8v?^s)xsh(n>f-ZLumDOr5S}R zbvEMJnqWK&$J%$`MasI_YR6)XNbP4~Bdd4MQ3HiC(dzG)jy&-I zA%l{ihNi5-z{5 zm?w#wA4LT>0B`64<0PDO7jNemQAf3`#Z+=ZYi6WEcnDMJFxuO^2-kU{O`cg2y?+NxIiro=G#xue#NWEL&f)kVv^}6N` zUE5B%cSR=j5*qt~`MyG9OQJn(x3OmPljBdD%JkJm7WegGDNjYf*0r){*6{FUO7KU4 z`_=f>mmoDCKvOyr(ZzUjQ#>@}J81}YJ^Syo!F44Dqo=tsJ*j@t)N&L z$uHCW!U=Ji`-qE4;L$$fV%K)`Rjy^+smiq$^6F8pT6Lj=+!tH_OQNd2c1Zuq#h2Sp zJH7GKB&Gj&W8F(^8`^b4kZIk*degEb=(S8?(M8j?Pmv=RKZh{f$N8NX^ddRiVnWWZ z`+oM`nelldwO)u+M_Lrs#|3J=$AMN)jO^x$5FIHMb); z=@LKq5qo_~32eIi{A^YCB8lM!Y<&iry_xngDrl26BP%kBO7EJlnZkD-?=#%|`N19) z&4>#1sJN6hqYd13oJriY`ML-jwQgZM+%AG_+O5mZKDSfyUmN1eyOM$CUocAi1-ez} zIE?*^=_4#=1y67%=W*x^t8>Uw+smeO$pP-gScpVeqzIr@GHG~8Z;RK2Ak zMVTDkOFB%NvAv|}34NaIUz+UmR3B;b7Y6n4Sh72)hg+Ox2ym3*_!-?ejqGZ66{x|P zyR*%qz7h9xHSp9XmEbSRkIYl3p<{|j<&PVs+!C&5B_=G*@En7^k2KjHfT#ONa}@2r z!k(ZnBD32KwDTR=9?Piqjc`*Y_lj_i#|r@V<}4hLFnh3RTQOw8`U6C|`Ug`|zq+^S z>o_~P_9y%t37%-|gz#$W^5KaR6~~fN?qsuN8#s1yJ@5SK{fM$VbpIKyC;2EnjesUk zVFDUVWo772-Z`cL`a5{;yJMuD@Ktlg0HD$5K4rj)rHjAm?vo9%c^WELdL7DHQi_wu zju{m-T`^8MW#%T3oCyc9>Ss9!_iAe>M;Q~$QFJ_g(wy#!-|QS>#H89Nkxms8u0;Qh6aDIA-%bUdNx6U4jf6^_jq z7C)tMci~vwpy=x{wa+NrMQAK_x1xKlb{yHH+4kQl9NQRG{({0S;<%f+rWX}Go|eC) zaB-+`;13E{%o^USaOa|{JN7I3+nBb#sc>ny?|xh1*0L_Yujp%aD?U`X`&k1W3dd&c zc6_XGgHg}brEtd~3aMM+QkZBs3pWHur_sVag5xgP!hOXr=eUiUh5IX@Y4cDE*8l>Q z!!6tkjIi6nX&|&K$D;pW*S@J1?gt#3XIZ%BNE|P@3C;5 zsGnbB;r@i{D;{h7b(3Z6DD$CbEL=MR-12vCd+i?u*kPw{UmjMq$Jt z?&e&M^D9wY5?XF?L~-n?`)X$tmyNEJrA2Y6IChVU;=Z;(RF_0?_ae&rDx$bT9IH1) zamRth*LFm48xc0Peiy|>8rkn#s@&_ScQ{_fH#`^71N*T(cE!VJUTPj(1!eIU161l(cFGq_b-m- zzQr-?++YJ0#nF04x=N$DHB1dIi{?BKYGrvem&@v3!^&a2Th`tde_J#@T4Vfewri_z zF1sSQt-SeP2&PMZXc;}*Mg&paT?dAa9rmKjnTQ8D_f=MvO9FO z#@)>rxk2ODs+RK>jk7VmxFKxYkHKTpK8@Rq_BrJ*8h40Q{HvzpUNl z277e)Lru5seV=IDdr;6U-p0AX&>@peAHx++>M zqM@F8Dk^e^q8@tS2`8L*DhlXHCmq*!E_WK>jC)cejn-{%kb>@&Z1=6Rl(-JPA;<9vD35#Db$(3>iK>wKhlFI3?^ zb*U5QS9>>$f)wUi&0M7gP{9S1Np8|2Lt5@$bT9f*kfRmb(4XAwy^L+16`<2Q1+>TUR0X1w;AXU#lUt09a7KJmOl-Yr-ugh^rwHWu+V=z zEx&*toOkVN9JRFGHFC(^19X>Gl6v$Imp)@y;4g`a@*S zx#MYr9)0cOxfdDZ#`7p!>Ksq+D!C+KM{?SD^*2HNO{`B&GhV;Y*SKmtjhm|cRVP9*>7O3Nh^=~X=8HShU}6r_4w_Zt)GPraqL>41t*2?`HQ zq>EJ3D<&FgiYm}Q-bnB0Mb5YGxa@wT`kPdL+5MBR>GU-g8YxLVqjY_2q){q?;cp{1 zyWpZpe04JppG0Ggs>WL;(GMzoFnQ zL@(*yl^4W|?0WKp_{&Mw+k-HveMb=AQ&cMIc^hXz5I^B`E9xhlvTZ^9QqQ>^>{Zk+ z&B}a1^m;VE*wc+K-7;1EO;dl<)n9OZ>6RIl@B1n*pUO8bcJEX^NxLw2(^NiL;1!T- zu7K>iaw?6{UHa;&r01UdvZvA`+QipR<-x5tXDTnx@4Id)k6Cp$Po=+w>LJ5N{f|$jNNvhzrt+Os^RrWFxgJ~gP30f_G`@-o)Ct|MfxU{!ism|1 zv6U)c>okhc>OMY=c5hG>SQ1RzmMbl-nL*Q)FL|$@LGzR=7$2QMvsJl`yJk=mU8)Xt z&!9K;b>+hu6s^aaPiD{-WmiMT46aD<=^6BkDxljhgvTJ~h!ASh923G1lg(p8=&(xH zH#LNx-}|SB&_krx+H1A%Qfl|BZwn9U95tlFRKGtqWb*tWev$Q`TobbMlE~mqA#_~% zXf{TOs?d^|jZA@M7kyS3~&a z=zy@~wGcL^`E{`Ib%eX?LfCwL!qPWD>ziPkqSk6oeF*zjU<1Nyh3*3g?^m3o??)@% z3SsASy$ue&jRMLWktTLi)ibq$_(5w7d^CzmI(04&r0$0UEd z>uV`MSaL!N=#&D4Ip0YBlagQPI>k1o{!@_4xrvEzeR-cJFr3M=@y%I zL$3H9besV@g#|x=K|NrjF!L-pD6IHV@}HCZ=XSjoW(r{?44#)XKTDcENh2)yMb7c7 zoI{xTo18;f(T_Sie}~*9Ec^rE=0CxfKM|fiAWHE63jx)_#J|BFVevo6Xc>guItV%U zU(oO$!t4Hn?D-$GuP@YEt`a6*0QM^K=sv`U1IJKAbPa`E><3yeM0op!kPC)E4!#I% z7H0b+K5#hXIz?Tfv=Lzc2!xl91RViL-|Y)PK=CL!;b=MGXgT4774VIT_38Uy-` z1*?Sd6H5W=bFA9 zHnw(#iM+bzCKGQ72nem;9%dJLKhrqqC2#_z(fT)-$E1Jtk@WBqNj8PVoanL2gb*l zC`DftOO~4`M@2YRfW0eC{4xKsBojXpl&v=LqVRkdD&SpX;?L5!k`Zpb1mQ+E!u{5o z_;Q_<0yd|b_+r(v&cqin*Lr9`&x&3}^>eaJ=`&NT8%%s7l7Fd*ukF^2CZ5FTxXeWP ziVa?5D!al&ar$=dCKElUukE*+NdNk&ZM%slGX{i>z8y#JH>p2!{n7hFZ=B}qDKzmI zTXZLCoqd;yc4)cC#G55*?*TjSg<1{8Cc0PAazE5oSz@9q6vG}e@%?(4kRC?46+(L{ z*e=X{gdM|2hMnR;JK-UjkHTZ9403fDWY=Rz*Q@xjK4H0uo>VO?d)ma0?*q@7=oS^; zR%N356#Ms@cygm^AIw!%W8%A{p8Y1ihxELrHL9*6fpsRjP6af-VdCi=TRjT!95Cr< zN_$&5oH{}CyKtzY_h16c2Vi@%iS)}S*GDGWqS$u`4%YRta!{2o?TCr=mjTU3O+4+> zd(6a>T-C=F^$D`RG?D(LhsF*QFRKgu8q7Lj;>|q8oiIV&Hzxj)dFM&cuM4!CM!e@+ zn9%VZDsKNCzG3*mMAs@d^_WPnByIZ<6>REN>2!+<&ztBb-GV+*v9RP9*edK-uvzH+ z4IC7f_k*_Ik*{5t_XolQ|CC|vPZ`z*5Z*Un^5Fvimz?NtInm!TO#K6y2E~~M5$^aG z?EDwu`Tv>t@vTbTkd^2P3^8-xuJ$vt&3lJ|*5PK-8~cnS&78ksqz?z40B}H9J_@vt z20MiL7lXz?Gwz53A*YQ2`-Np=5pNv_whFTiX4XW&c%-ZG$$@JE*efiVh!%J!fwn22 z|5P)NV*S(1Y}3kM&=rFCU^Cbs3bxEL^WALUY|v;ib1&%&H?xoUdgtSyCjuE77eH=U z2-Zb|wTr--Sk;o@YC!j*Mcu-}O{jSA6_6VhH);)JnK7Lu_ z$k-_?xCRWm7Hkw|=9u|9P=1}6H!_;Hnt2#4$~BW-Q_^#TnZ8rZyV*8xV$ z9cDVAHL~4Id-N0cgJvpL-LmpgGu<#mH7V;UGaXb9i=H|&ty2*-2h225CG7anOykrO zvH7H#-Y4D7%=D`oV*C5eG*!iCUl2+M6*B`vX`{;D78**S7pd}=h4RysWpyb1p(iCT z4W&<2e*0yiJTg`(>h3;xc_{rfN}aIw>QH)CJ*wMw*MGD>^p6Qwv{!}V$>RA?x?Hhq zZz$zy8&rdZ`$E}>o|;g;f@JOwM?%%#%=&#tW}P49Yi>qD>xZFy@vT(kN7j!* zF{*zAIprKShFqBghc+ z8BWk3Olt%C+7Ms*Ib_RGutk`445W6HSKbcUb{uRI=6r#8zc00{yrl9=L^wJS(JsvS zDwKP4;Mb6=h0YU5-+2NRD(Hl4{01$n`3C9YPeSfE35{f*f;@N%>C3y6tUI3NG$NXW zY2TuNUSZL92sd^^uI+{#|Gk_*m~%!<^aEHX4C?_Kh3>Opx1x_#|04=EoC9lw@x5TD zFz+WY;5=A$9tGKd23v*RKCr(J=}LY1mP7z+fYfT$eQp2`-R09f2$`V2re2th7K_JWg6*kQNBz z$4di*ITNG-6Qu#dFr!oq^pSg#)J&K^84Q>r6%*Qmz!qWVRIpE2Gz~OP2Wy1RU^J*h zm^%X+3J95r{$Cw}fOykPwtcq=a-kV=a46(Pp=Tz-2NboB6wgAz!C_#7&^=okHe1S@ z0|w1S{zk=Fy8nADGx204tPDp2=R9QS6z0zd4OXyL=!yV)ghi2H@B)<6v;gI1*=F){ zR^UQ}*DCU3zB_6r-;fVPAz?){=(K~~!s11sB?fGZLB9N0sh9%=*9p@WgZ+yUUm6G5 zx&#_(Su#_e_nnCFUy6cjmO^$dQyF)?{OzoXKCQ{-c$DK^0S*ewS3=X41nC^Y%tXWw zBqF{f2@GB(mJ+&GgFV7R7ie6AYBa2wiE%0|83ptR3ob!IgBz?7#;?VRyMzTPk}ehb zs#765({O?=Vc|N&8`8zX>C(B@`=ocR7bo^0LtuuOGD8w>kaWVFOQjcPqQDBFeIpdz zxlvr}GO^(0(hy<1R~q8;qM*D@hzPg>thxdToL7pkUWxF$EJ?Q+;nl+UtE50-!PTHK z8?4I~*VzKOZwo5wE4u~()@zZV?OMn=IYjpGz z;0EL`yHN((o8a5+H_gP|Yw>V&RaQZ$rHCc5y19=ML%p zci@Co1&|ZBfxX-GFr&tag6+r<ogRK5%0ndKlof$&P9b2r$vTQv5h zG`M0WrXyP_5RmhfINj6GK*Q5w%V)rWXAoae2|AwzyPt*66g($hzel`&k7%q)G$t&2 zUNp8>Y~8U}RQ7`O*J>FkgsvCC9%0cwF!&{~@g-4hjcDLy(ZI{NmRa{BUF&}79j_qX zZ%i#BDiuTZ6V2%zpY+U9e_`rxw)&e>|4Gl>%Wm^^pPa?d6Yf*9s9e|V^eo!1nB6^# z=gQK)pGC(Nt9xeg4?fkMokj7A%|FhfG~J@!S^ToOw{I40@mKwJY#7bGNZsnq2YXh7 zW!Yi0Nzr(37=Ncj?9A33#His8%g6y|_Hf>k( z;4@(Vdk8N$Ih#z1{{PJ86%%cf=Fn1APJ7%Os#0>+#yOm>_cq7{<#Q<4U-c8mTZm}> zLI)@t49wwz0>{tg@bZYcESrDjp39R+ zO`pu=$)cXab16})(En2eSdYx5wTgM4&E@4(g-7SINxItSQnq@GEj&4wEb2tof98@y zG1zFK+q6caEOf78P@08?T%fpT$y0n zMhmY<$h^WrbxO8uwvbK9gIg@*&^Eo^!e1_GxWU5fvGQ&Ntv7+aiaT@zZn4l0idDB+ zcx74jHn8SSi+(!xsiBMyDDxiBw!?yrKE)P_(k(1T0R<%%>QM|Th1~F{g=Y>jcS*h{ zEc}}ZVY|VgCoS}!qTv|}FZgMH&cbuEB~@VjUW@7u%EsO5K+hPLya?KAEW9M5V?S8% zDi~ac_?9=p+ykJo5o~$~%zh6HYz7-X0=*xD{;go`5mhcvU4D*$!DC?67dTrf41(&OXxbAI@*42S1rg|l;nO$9A8!r8WdCa}{C*3ArOA1R&{&OYJ|gKV1(IbaUtE=9c? zxp6M?m4%11Zxqi13+DU6*-7#igtL>_qQmiW-VRp9g!7mg9~;gp?p+L)Im5ARW;xio z0xV2KeAsHRZ4H?327^<|X_k>DU`i8A^84 zg!5n%|7tj|!%BP;biEzUOVSPRfSpZX)dz^LZh@S87_=V&>2s!!T8<&0^b64QRXE+K zG6tUtr`r_$z7OZ+NO?bo^U^oJzHnZYm;XCt|9_CL?O&)nkLK~U)_B1@mK%qH-eI8M zaIkvhJf&`*epa8y3&m{XK%)^H3bYQv70g`-rp18vC16lINJ(J#8n7h= ztXZ$9SE`j}A|P)Q=(!4XTnh&0f_^uHJ-30a+riqq!Ls6c6r))1Aegmt9>prUcY%(I zd3yaV6+bnPCwzOJo`=Du>X~`GGb5`KG(S5J3wRavc7&>`dF&(Jm*%mLwA9RFA1Qoo z9{Y&?5TY z`w(Co3w9X5f{9@8?0iq=ChAD-=5DtGSD=i zeWc}s`RpT>kLR<|cfS(Z`*blkm53uqtFnbWR{tq0uAOfcL z^F^?e6px5tC&>wnU?=GuAHhD6GbMrtlCEILxigW`K05+86>}rlM+z;F&GW&Q2r$P6 z21ZA)k2EZbfXU*(Lf>*6WF>-$Yd}j17`PtnzZC57f{mNO%4@))tzdQ@=(-KGZU+r_ zg9AIj&Jxhq^au{B9tVq`1am4u_w%4_A83399DF^3eWSYpY&{skzR~bLSam3ZeWb4? zf_=pONd)^sz~Kn?jaJa7E((Z9{4|1{B%m#VouuW92zC-{M+Eyw&o>e5BMn^<>?1*E zBG^aF=RivzX!{)|8vGM%{u?a$H-denbVwx2o(nZq{}1*@K+g!Ub`+Q&2s+0_(oHI3 zz@$jJU7KQBBnA?5BnFb%k?bSc^CM}q){G7LnxiAx_SrF!>>~lOk?aF?ixKW|M&jXO za2WzBS0F)RVkCTE4H%dL_NRj#mx7I6uyQk4bPbrj6?El+*4seC_DD9>;9X$%j!5#c z?MjfK_7Sk`aU>{s60)}vjDH^CmVKb%6)Es_#CJ77ZaE0nz7Lik0t;Is**9`N2R&az zMzNDreHqD4;`db~`$CfYV-bY6Sq zQwzwYTlCxlUfiGg(gOOKwAU}7x?##kK33r>KJf@xeRKg`I#e&d=~}=WH(I`5Ko=|e z{RleGFW?2(<-aVT3UwlXe;do*kv3jD(>B^h#VWkd4A~oInoh zFKx?I8%3!2{>yDNsMx*LMpOLiQy#Fr*5NC<)5dD-zRSi-jDm`6{JOgQ9vi()dPdR4 zp6PnP#$74sAsaoT<4bM)wmNvHjaU4am)U5E_Jb#E6s+z1w2kgo46d^Asu1^H8!zOd zYOwZ2n_fHNQ|jUa@_!ku+m8fUwV>fOu=#Z`?+wsg54JaeMQ?$&MzH%JSoSW;b-o9= z?|rbcS%>@d(jf#49zjIb~%En8UJg32c@4%*R zFz<|wx3vVGwei}BydQ169=fI%>^^U!xk@vozu72V?_Tcdx6wLfPsfObl&#n~eIcz^ zv@cvp8QLLNEu=LnL)#_w`!_GV{>T;mmoB6_714a-LOQSe-0chLxLz`T&qBIph@P!o zNY5(I8+>sg_4ug*4lbm(Mk*Ecs&EzW|K~#5u5IzxLK>^mC60;W2YdU3DDqeFo@w>l zZBb*#h1AW7q9xi`bE7arI4_D$=_W)((T93Dwxj;Fgs3?e&1qR2#Z!v5IIvPtFM=p^ zM)7isj-^q&%r0|z{jf`-A}{rsS48n_W}V^3YJm+Xl zj$*g0xg?5>mAMuSNR8s9HMVt8SU0vF<@P9gb&WH?o()lysOX=`Tt;CVqiBX|Ld|A0 zvHGegUa3}{9mPv+s;-HmT}pSfEsDbRW|I4&=rN@u|I#QL>8C$2{>WcZQ+9Q{6%tnO zcquApl`rtwD1J>*CA2>WwhFy_qIkk~Kv-G@hCL59J&$y0d%+%I!3&5tRD(6b_!kl1 z@gmDU%H4+u|CbO^@e*WP4cJ;E6?qx#7Z&dagI+q14)`FeF+*d)r*TC}Ekly;b zmVLU5BEnM#_SPXm(Hl{i;(in1b;87YIe{>@K~8W0`6>=Tw!Q_qMd*DSGqOcDUUGfoV zJ_I%j(^|k@VbRB6&?ll;q3bZ%Ei7mi3x6ur62>2i^6^3E5d`FY1_rc6@k@<5Mg6+i z`#BhJ6z#1R#vcQ_jv-%uI~aHz;WfwQL|;fcVZoPDp$;DcYCE8T_^%}4S5n~DQs4=& z`h=Xg6LM##SoRx)2b_%JiMN`Qa^h2vyM;wv;wh)WMxQ#+H$vWTLBH=1QTZJ-kl2la zy1G$7;rEb@XOO<}4AOgkKzN_9xCi0pvq;x+7WuP(1pUt;zP|LYDCc!4%|ByYv-U;t z&|Gq1G&SmdDS^>6LyrPOQQ@`W(KJqRaA7n(twxPJM>MsoQKWfwG;bVi zO|K8RI{N-CF^-MVG|XSQ&bDaG%ik5vi^2Ntj;5_DL(L=6{3fAcXEZI+7pEtq>B?bh z(0F6VnYL*4XIFoV)L)GHi&cLP^|x64#i_p~>d&eEma4yH>TkLFi&uXu>d&;TT$bgd zL(#msH(OB;ngb$xTOju-M(UG)9L=vWIzK^WdJaePLNrfnH2S%sR$9rY(fm^l&Lh#h z7S{Y(H2;8RtM$>81-Vn{J21|a8rY98#$WFIks79== z33mEPC!B1jE&2)=Z0GgOc_DTxRjf1Hd7*XKEW6&bM)7m(yw0&L+)nyu1naDJ(!V=c zw!qGJMS)Rv`dHDn2o-(=?%o(*|+UUk@fi=A(~`tw2a z9bnovu*hd8pFXI&69L_KgNA#-_+l{cez2+pY<~#!djzySYUkCx`H$Io`D5`eu>1*B zr0Pkq_9=unJ!9t!cF(hRA0Gr(*?H35?|E=Q*t-|(dcn?1PlH|rJ^So@qgwhBPTc;o zoj3SfYa!>o2Dz;cvY{Sw?g3P!;B8dA=AaJ;o$rDH@7pOsG3*07J7Jfi{#1eCBhg3; znDsqWmiGf#bQUZ- zhxp2$z?z>C-uMgTmfyhk-x1#ZC)ocN!f6n)FYrGc1gqYvX&nMO{XqAyMRbp@h(DM= zVi7y5ee@!|k(LZ&!M^c}XoPZ754PE`yKI3>@= zu&-3_h1~K&4386zeKGtBE&in#_Mt&V{cze)6GQJP*1i(MJ4yy>V`#3P$E$iHhF<{p zycxr0J z%`to*UGY&2kBIJ%WBBtHou9^#Pk$#P_h<}XNR7v0ur|Fth8h*Sz69I8j-d%EUD&A@ zdR?*q`xr`7j6WB{537Yg$M8;c`aOmwD`x+tsGmhHh@}A~*A9=RW?kU`uQ~{F z6JvceT|cb`$MTkSYgjA|>IX(^EDxFaF|kyx*byH~4#k!=vGl2mA54p-Kt)Fe(pxsg z@{W$4D`I)4N5fUIJk(mZ#PZ8V+jX(r5OZ!UjaPDhUMv+TQ)l1ri)CBoJ`l@qo&z3^ z3u4eK2a>LjHMRE>OHaiych6%EUi&= z?u{j{Zutwbe6cEdF_te*RWHTzqfD^xWz@WLe=I+8bkxT3#mDe^EZ++RHN^4 zQrQK1>t`$-Rx}@ur8A0+M`LM$9{W$k@_ zZfyHKmRGL(?0?4c-AV1gv6QUXGsMBOR33i^Urwusg99TR+#*YWgFe(PyV${+C>rD7 z)&BkC9Ne;i2}tLh=-?B3jSgC`D%3c`!7m?6Lma$&Ajr)0QFW+;UeL~DanMQKq6H4V z(de={=x-&rI2`nhj$iJevH`3V|$l%xj240Hzo=YJ&W=e}Tf?1b=_RGNlFW4ol z+XNP0;ov1Uc~?3pM%z3y%fb89;y0rO1HziCK=0KK9!QMYV4JXbi-Q-C)LsJ-Q0IO zc*H9$a&R~6zX!5y2Q*Mrj0$JohX(oIk8+ysM~f>Skd~J?cmsCWgFa-ShrkYD?ZaSk zDO!;E2xQw%FyK+~8DV1?SoRp0^Eg`S*#*Xzqs5jdP@!&Ng>N?w(w+nZD$wGN3beTT zDYUTXX|&i?3AyB12VV=ip2GY zHhhGLUSabgu%ZRb`xtb60-6t_rGc&BU@KbO{i)dYh?w>>F>M>z+=d31ey$p<`@i=n zT3C4uE%rMu8u$V&F8>lI%KzxICI!y zZn5Q}#oXc?|Ha(kw&9QieIplRt7*VuKA~e2Xc&!xT7^XyBRn&3F-EpA2yas4k!>uP zKW;HbHUrYrc(6lQI{_@72>QH69M~s;fs?@=Vbc__JP6F43Qc5A0~4o%wqR7KS6DRz z%nVt~K43IK6FtHPGi$&{1EEk!=B&l+1C?RWNdIh{uyqbtHCGC>fQE2{_l83wq=;(C_#K65ws;qfx@a)2rpO- zjfA-n-sOTO8rOj3$5j zi^{VR9s*rLU!bWh8yI>!sZ*nikrZ^ zJkWJBXuf4Je^<$HD>Om*;xoQ{vE6Or-M5Q(-vN!Z-2qKh7J#|ippn|`i}@|Lu@D-` zyb~I!y-O;7H|Q-wIYIZJ-1d7AUUM%r;`8i4L|`#m+AD0i4;sn8U%dVS@%j?+`Uk-d zMLo3EJOsJuVKB24v^^pw*a>zE8y{s2sQdpisG{sK46Ox^i|uxacMGe^MMFvk&34vcRme`SS!U@pA~0)7Uh&br>WQR?U9yMK_%@~NKo=TG?Bd*jDG3;#~TdTpU7r}ykVA@Ndr3UnS8SE6+?FUO(lsDH@E2J6 zw-oq~sC*FN9fQzF(Z2|H{0B`K{|EN}4;rbWI8I-10hl%h+|E(jszP5;$XT_VAyD|OHpg2;^H`^37=lO6~`)ZjEQ5F z6pW4Ip|yKl9BU+Od>m_}V1m?qB4{z9pdKR%uACIdZ$tto$MN)A=9D-(sOX*+$KS>% z2#({=oAl0zV~x8_akNqQ|7LR>f2qMfGmgsj42LC-KfYTL30B&1qRd60F$Qc`d{ePz zaU6ep)3Gd$=Z^B@!Mc@TUm_aVloUtPR62Vy!t>m56@$~j?DROi09zl& z(`Ex1N+Uzm#pKF3{x)adRdM_xqUxGB{_EE?|yt9HcEj0^NNBaZaX zPq|7}`Fg7MX=pI#nK&Q6Byv|mh5pa7Q&6|C>A5(*CRFc(98FLs3Vs>!gTjve zD6sYwu(%fVzKU{=9PJ4|+a;%?-_9o1&iIEBz33e-y_HPI_D7_$^u9 zC+G#o16X_M5;j?R<`TTN+qi^H7I+ondxb4mb9p|h%tpcaTR`_U zDA@m6ut}Jo16r>GdxVwOgPyHmU@q7qEW81<-w5^zt8da&{m+|+0OQSIo3Qv6(0Qx0 zR9Kr2X5R(|-wt*NOYZ;^3zlH$-3B%(^5V4ZpwqX6UeNu&^Uft~v#h(9u&vxhpyQq; zY^#8K!A?bOv%)8qu*v*hS;8jEd>1CO9*4>D&%$JRflgdx#yIgktg%jLPEnhnd7KmT zf0YI&=4!?}*=E%foOpvj5eb8h;Ghu&wod|UCWA#&P_QEi>=)Kd1+%7sLDRu@VM(wP z_y6%T5HKjL3juRXpxF#|3d=%4*G$lF7T74v3j-~)!ERy2958Jz7+~??pxFWzggfyd zG7s!m)V8Xd59V2&Sl6|{$tEkeIoVW23&GqdC!5L{4F=ksY_hslPBxj{>!dMCF35FK zu96+Td!1~vqTNnA{Zdpa%VJVh!&Y6w+CJDUZRk?AS%+~ccQfnkrQFT@mMmqHxl)&MH%q*IDXTR2j-~jG z@`9z%oT4^C`8F_b`%*Sprf(^~;3zCq9CYqN!U17zIl^o|bZ-0SBL1>f?ik%B5_p{AWS?b4%G~?Nv+JW|@1J@;#pGg{5pe zd-YPx6TAp^C~A`xG^+I4L`Pw=%x_^b>i|raAFvD~t*xdpwYIBrVmpEuUSTK zE1I*HQTYf}!?tw~AfXY_7Q_JZe#h?Sr={Ln5UppcUKTC$;@ibf&kQEwFBNR)P#?xmiyd^W9PtBcFhGH@nCu83NkAC2J&#=d2j`P&9PN+idOMM zE9fSrLchut^rMn%_N*X}a@K&CSI{s;^BXI8HH@=C#$uB4rMA;FZD^ym<+p_Tl$t90f{el?pDwvx=MB7@GA^n{}K(v@UY49;80rmZMh zNi($k{7U|STfhq|X_M~%rPV8Go+>c$)s_6Jwf)VN{H4b7dN8wLB|Bx%ft9>Xy7%Bp z+N{zS9$HDyE7@>lCGAob&Fx&tLvTy?N;<6?;u=^|SI=8tOyKd1X{0X zY)#;;wQZj!;QNN3CGg(g&d(G0<#S@YO0Nnm`YM6nH8-AwMyMN%Kbyb{pi0jrVAu2c z1oowdz64sK;#+@Dpo2s7rsYKXaEN-=Y9E=%Ym!SwC(_1|>cEjmlNGbGcZ|LxQT-*U zzg6|4?^qpm&}Y3Nk&Y_6pqGS!GTpteD_qgI*FGVT3k#YHMWuNz6CuZQTxOG*5|nf754|7b+n;UrqDKY38xo5V}%j6WrDA20d|6$m~L zHY)0c*L8iWAl>4A$c8_X_!+)g@ljQwz%i@%L!516SJ6VPk%_D5IXx&vuA=AFpw;AF zMO#%x3O1~w&qpcwkyUh=zSFfox{9B4Ysyyf(#eWvR?%)%fZyI#d|Qq8 z(#YVn)wE@->H*oSX|!G~pX*yqCe_rzDLay5T=mH@YlfWlgZ-Ng$AoiQ$6&+g}NVU4uVvKVXk+s8M_vOlKJP;8m1=m!kO0T$-MZoAS9WdP)+EvB=epC+k#~Nt)SLL z$#j>#iY!T{c9qV&Jefk&32IW4X|YOQnVHPLsL*yrGA+=9^3}*m`?a9=3fnI-| z%u9!AyOQyW;M-(gBGmn3GT%J4olB;jD^&OpH$JzcsCAz?)Xl~mP}B=#D*X^1e<4%3 z>4nHpJPZlV7eQ_oX89w7|8U6F!o(2>?-iDgM1D&EJXIw1t8l!h)HI51Iuw3NypNL1D#gslXhxxLa5<7bgs}Ail+d271HY zKCHc;Cn}r=P1xs)287vG#QR5}z}g76jHO^-B+?Zx0E2A^Z?d5QSqmZiMWG^k_0ZazhSYD;g7eQxHBVEKil*l?D^FfY<_Gy@FV05%Cdmx6u5;!N?0jbMY&eVIP5>VLhLA)x4TFvyDvHFzcACdj?Q;wxmJ zx)Sk?!n7=e_hre6H$xL)S0TLlDuicV4fbp5{$G-f0P_|pP?&ZN*efi$Rw|eS)(KtL z;RHR`K`y)=G;WptE_CO@Wc|YO8&v;io7{*5Z8st!?sP9 z_{;~uL19ISj1vz^%Y_9G$$5MaqkvkWt5hmf3c2tRFleV}NSOAhINPJ*Y-QqB!v)A^2s`vLE3s!mL+hM64AJ2_3J39j}VBy(TAmT~746I9r{VR#@P5Aj~@~8fX;_2pyk_ z2820BL<66R286aY(SR`PbJ4)((*MhjiUy8}29CjYS?yx;;}{96k3&xU0yggc0&>xp zpt%EV?m)cvE0j0z738w7LF);GxA^41+lh!lVfi3p2k3 z`-LUnf#z=MjzVAN_i__?1~sn~I)4DWgoQmwXFdzIoJDx{kD&iK6j*gm?t*)fu1{F@ z6KFpVcAn?EXCD>+j11O3x#Q`RJDy)a^RIHkUm@rI2HDULHuR$cp5Gx43M>CW`ourw z4(m_IWdmY@zoh@S{)K?-zmYKD9~nsg5nB(+*e@*p7wIhjL2ec1{14%Qv=-k56?!iK z{fDgObk&MFoonb?{M=RVPz03vA%XQm$n6&*W5F=cd=cWC71_D`A=7Zk6+-(6gm;X9 zoHr8X83Vw^0EBx+t;O}fe-tv5jRtKOgYCk+K+rG-tP`em#8CT5_Vh8e!Ke8b=hSdnx>> zp_)S}{FALkpQlijZa{kqZ#{B+i4z8%Nufj)Z~Zxi!d3e2-*!y%OI3eq>Tg~BG{5wy z3w$|$r||CEc15kd?0-`DO-=A%3eU7w{+B{Us*qa$RGv4<8=1;m$PA-Wc?P%eV#vW` zQmIYRYe?m(#*zuC^rM~ynU=~MIC>QI%wbn>DzB*t4oRiMdJJ)ert%V!&ahO7wL6vKhv?Ubsq~Gm@L(#PRdffWkz<$|g+tRgJ)9AcUIiR~DjRI6bg;iTSpfTS0?&%UHvN;r9bxImi~X&@$Vit4^8K9 ziq!e1vnyAOOsBJ|MCbH$`e~?syPi&0YE{_NX^&D(z)k7A9kBS0bd1{tV4E;+TRLto zwx{zJ(ZF5L?pZ&#zT>g<#F>kFA4tctst0j0ducj%z=lWDd0O7`cshNd`_HrKyss?h z#dQ9`;4vtqs4=}FJ*wihbpDR2-y7*XzgTx5ou1HdHd@l@X@8~UAJh3APtULEG)J-Y zAJu}PyPn>&eqMdixb@8sr<4s}&pm|#*3(v1LgSeAY#u+udM-I!ENZkKOg^@{IXAJaL{EJaHKprsUc@ z{L$S&yNBwv*<(DkQmjdli@MuAynL;Cn}=U>R2F(DSdAIM<1=XH5Iwh*K|kxB z7MelJRD%j4>-R0s_;tb9o<$jO=(r5JMEOPYmG%2?&Da~csQhaRRBiW}4Du+G#`|yJ{!ut) z$L=K?)ZeA*FSCC4l8x8DHKKdr2D+i)0m1K&B>gU{{jmU^4Q{CnAU)+B_Ub4eTN_V};`B|M0_kE!PsbR3 zmuM&$OEVNpMvdp~e_b=jlb~E1O;;=^G;u|p&xG>DqT%gO8l@}H9LgsyJ35PY=rP=5 z;f6Il5>Cas{F9NCrpID;p^bu70Bu-^C7pAkP{86SQhq=k@ljlJTV<54vASc8;%jni zW;CC;`lD!479{iB1lp^|+|3D`zHe(Hzvpt!bK%3+laiTbImxUsi#LUO_0H>tt@;(U z{whuiDNm)Qzfveb(f!Xl{*r=IjVZc9L26jgng~*zTQgquMO}gJ1s<+InsRw9mn#p~ x8geTq)#=>I*K~Y=awDw~zrKxZy6gZie;|w8%4sx<|MPOqn-vokmtK>z>HnAim?8iG delta 69967 zcwXGS4_s7b_CJ2_+&gfGdq?gt12e!V!yk22)Iks_F$c9o1sx0(jdCn4D@rUY+Nj2| zvW<4J(K)tJjhmGfZrEDbMup{W?k**oTh`KkaJMbnXv5ajTCCsuxibR;`G@`YdVOC% zUa#RY_dd^g&U2n~-sha>&!zsZb;8ELI>EP&->ED3iYoVABvE~4nMj?Fjuol;{E-7s*+M;6;je}Tb5&|@9%`qimsN>^6^kTldXpEa;g5>6sYOuqX7FUE z4IfN4Q}^E{qt!xQBH!;oUHjG9rBnSrRPeoO28S!+BuwohC;s2Od{EeGZj+x0-C8Wv-s8X#AfMRokvG2kLm3EJmM2(U-i-{T}enX_ON7B zy6!vObjtc(=WOoyPFKZ~Z>*@IrzV9QALL7$s)TAo1`6u6!fUUKGgH$yI<&L{40Vqa z(X|7)V15|b?S2o;*XJ)n53U^wG4g_oe2)}J{?<5DxP^6y7mktdkC1k`DA=0obwVpo zu1u5IjPEOX@~oaIl9({tN$R_kMC#HDUHngJhfA2+Y>O3KJQdFH*qfJ2LX(asO8;6n zx!EHNEkdb{=eYI9b=>1%Q~XB9<>C9mQ#$SmeD`t!cNeZJbpp2(*N+8(E5+5O7r5(j zZI2PS;kYi36}U~Pmqdq?PCIc>u)~=nCMje7dqH3q0 z@D-F(%$unv#$cg(r%=OROgmmv&D8ZC8`Np&x@(kRp$hy$*|nntt*k`rM+q3ZQ9>cL z-8Dxtjs|UAcvKeCepU=^6p~}K5TwnYEmo*)v>=75?j4P)T~Ehi1V#%Es=CNzp(Ct) z&oStVdkmg3np8dpPi=oHw@~3M6CMOTP-lYGLcwgoNz!h7ZTbk>?%Nm- z%70p9A)nbQQRQq?9<}dQomBNrqMfS83hN9Phr60dyA1|2b-t-8{AIM`P1VdVq?~br zdDOzNKt^$WKa24Z@X3z4SKfTxIAIbGEYN$%bAwn-9*mW74jv7|$AHgFTILd_vw_)O zY^GfsN>S?`XVh{MJf-|Ueg0P6{ zl0d0$8EkHA#sXE(o=l;l3-qZ}n4G3i#Wk`**`v}V$rG+mP2MC6Rh>+hsKOyA#tXs? z7HTwC=L*ve?AC?&l+mlX!g%9_;hO9!(6Ud5TS?6mEQaDRCxvwM+g!7`I83NGTpU-r z^XSk-+Wcj*GL}8LC|n{!kbTeOLI5#5ij50t|3(a~`_dRGaAY{tHAOE`dmdCXxHwVb z3+ZsJXeMtSl!?(cMrdkn(Aqq~Y$yyjQAjzw6*|%ljqKcL5H+II^*2y$d zH&L(|%EAPu(w2$B9KM*om?)$gW`*w-lPO1n+sHspsZti`8@)?PEr%oov?QW$^Z`RG^WWWh!yjnEeRvuwcL1#8NF9>3ne zU+tq)6mm~Ok-B$acfk$QU|#!}I9Of#%Yx$H{7aPmTQ)kBo@}SRlLVJxMpy*J#1{yY z^z3T^neKq(JOzSEEAJQV{A{|tK*$_AHO%O2E@U&zPNs&hzoKQG@m78+tt|qs*f&<7 z?d##HdJ3RCbHWu_VLk0WR-DR808t(rhF&~S4jnsBQ29Bu`+A+3YR?0^4Y$R>=%3Wt zsMw1Bww?!rD+;qZ6Ca5->=Lv+y*Es{9J*nnk=Zv?(ope3U@jp1h;=njydoQL)#|&IwLDhlZ8SaBmdK} z=0KsKq_YnBxR5PG(_{CU4}FD>ey^KKSt&rbmS^TkdL~GL_Cs}{-n$DS>61*~EmH+m z@8Xzc-o8B6stJmjTnWb_lhUcs&_1o&?TlesRW?O1Yx>ag{BV_gQ$VI82}hMIttY-$9Kx^MISg9d-j;eLf;hwXRoa)VYxq7FZP9dZk{vs;Nqq@)N$`c%2= zUT9ZU50Ieb?V(ZR{L*CTT2TZm22{}0UaK{biCL+GVInw<_2f*1J5H8H)7&*X)#k4Q zj228*R4SM*G*DX}#Jl;Au&HfdCo73sq>9fxe2kICY03-+qca34XL|S^yGGngJmfRIJ*djX1SAl5*peI_%_Scb49c#9;F<9_&=ZdX2ou`d!0)_}bP z@lZJ;v^wW(0NApyqVu$R!aOVW++$Rzdl`t;T$!jE=7f7Uhl*x1M^ud{+jY5Mr-RM~ zDs_#Yr_f6F^~h3tbm7BWQV=a)4!@Ke?$sRHf4PuLRgALNexXQ(SJ)L(Z;kLZm$u|V zC?!{5DEA&Kjvn6jKhHskeFgp+(ESj4hGpP<=noP)dh~W65nSQjI`aTEX|7)`RPtx0 z(fyF%rl$YnCH@T>^>9U|UItrvwB<@fQL|~sD2T{CB}PhTdUz(k^CNs-KfT{czLg6F z3_`fq9CtRIZo4Yta$3KzD$OUa5*qdVg|ub#A_Q~S;n}*C29-XZ2%&Ct#HiH0eoiPx zNbcnNVy)gt2cJ0FeP_N|&tkS&lyf}*G;2~ClC}jpiJwVDFAgzN!PSDQMNRo({$hw< zXg2r8DVnzXiykqfLfI#=a}sBUZ;pvP#K%LXn}w0&StZN>!@KKXHhVoopl_=L8$Xvm zSS5_WonK6pLjs^Qy zj}U3=b3-i6g{y^X>8$!bMRth(npH<7HfbK<)F zY@7_TJ0*9VgGe5Ee2B?>fiw4}{7zxzxoKpdsebbwpKwTb_MZ5=??803?p(cTT=$=e zWam9X_F3x}p1BkE3huKYiPpBmm8gvRHP@GMU5(Evxa)|{v+t2)Z6a-2FO1` zCUs0lzT07tCFA698D_(iiN9a4(m{g^x0RzRRQp#|qCE*lq`(a6duxHrvH~F$pjDI& z&}w-KnL_==Ch?5XGMgx9Jwvpd{ph@NM9bP>RQ)&tS9L!Yg3Rt8PCz2`Km@1`=D}Qt z)8X}VLg^8$$0I$1CpT?LM2n61&JV;Ta(*^kIUUw;VYvWnu7PinPbdY7U9C$!`-m=o=xmk({}qg4+1UvE^a z>E3vb&Y#gHL-jqI&RoC5AM~DGT7KmNg}ed5btV$tGgeQ?Zfjad_dg3Zd~HgzAq&ZT=h7s5SVX_m0}Pz)7Byh~2M>K)MAi zQ1ze7Fw`gh>m)r}&)L<^t>+p@?~{UEI0u#L=g#FDea}SH@oYq#RQ;@AIXk7!XV2NG zbF{dQ!jKQpUmgYfbuVaAzfdiqf;2s8m9&&prJ4xxLH)K;FIQr#vI5%@3B-Tw+X zdrOl#8TpGf6`u{=m)kWkyrOe%DQ=jTLF3CM_>P{IzVRK_eeLoQA&^n8I0o zjip5KS4~i;a0wV#c_Y&JhL@lW|2})6Ik@2ileKfP8Pd{b=5YVhsZouI>MRh=Zi`nE zBODY(b3kQ(N&X?Mz5K8H`($UhGcV(_afra}K^t3#3*1}HyI&TB>#23NMWRmcOo~Au@W`?B zdWk&i%p!Syt!HbEyhN^Md~MH5l&IknR6FuIi zD@&oyas&$1|BW3LXPv zEFmDJCR5S+PKOT7L>~n-gWdv)UX(;?d|h^gTJ_v)2k$R}y88qC>Uv#9HaZ&;2=4CJ zsqR0a1HqdhAKzHfL+wXE#qj~^w#Ty-*vAYaHDne^)N`xZLD^qPs1bzVT1I=|)_$i# z{8xa3?p;af-Z+R*n&?oe=|csbKi`f7`lJ$C!u8kvOff_z#tgKjaGIIa*M@7$p*He; zF#+VR!?3o#A1C@%J%su|CVG(v?r>jZ>!&tqnF%ozrxaWK_1Qp~chR2rVl-d)Ycn$3 z3(>LmoifJqXo`#6Uqf2e=kbU!cE&2?TRz)Ct*=`kDA@=VqTDPB?puVBnTc|p$0ue{ z{jrqL3Ud9+yx8385?7woXK38=S5HLNF-l+MSC2tFPfS#3?|D|GxqXy=O@X%3%jQQ^ zD!p8P+kNeq>+y+cZofRX{m1-J+EFfzByS7MD(mkUr;b{-0=W}BXzPyJTBq+)D2DsX z$s)CO$BOjvD$!0QpPD5qIBaxK`=tvk7)m3C<2VZ2H|Qlkoi_YEmMFM61&FahZz0D+ zdhIVL;tL6&{UuuQT#)4;&zlfX@FD#=awQp^fizVLP<$RND$e5XK_0cMrUYK+eb&SR zfMM_vz>30;l=uwd`H^Ni(hcc#ZY!-Mb+W$NU+ol|4;_u|jOCMPtvA<7?cc;ong~W~ zA~^g_?07sfeH%N6e2-%sZM#svEWotq8^a=DXN5TBpuao1Ndsiac-GG*ur+pNn~#6Vc^Rk(%y|g~m zyJmDJTL+=sZjh{0_&uP~a$#>?xEO57}9Ow9_z~uwCPkt|OSL52C7r9vy zQuz@g=g`47jTgCiNUV0U$d%!H>kN^58L9EsMIv_?<(*4Kt`g5TSBcyuGP35MiQKob z9M^?H9z4%}UF05v(6)Xcayoo({7B?(7q~mQ;O8RuQxNJnC33GosC(g*evJYhv3f2Q z1d6ltTs^+8AFb!U#kG2Zo@)ZbuAB7S3Y6b-vtFB-{P-3Dq67c=VZ}nU*I<)g|dhTh^@f_8259;pZxOM;3b1~D=Dsf$G9jE4VRAeGQDsg{A1&KFs6(cxq<K7u_M7k)eLGJ(||#B42W94j?1Ikd3fb~_P((F4P=M?;f`xM&wP24f6%!>y&jT0@DHOgXd?))~+!&B|004q;VoT9gZ zQxh%giJKn&^BMdJBwl;9&Pw$?XiYiQTWrU#Vy)Eu7zh@ginG8J%1*^yVPMZJ+VfXW z#qFc5)8b(i8xd&RCHR1br@>gucX9RpwqJtbXD=4X(ufkBdvzl1+G$Yy?jB(4_i=V| z=j4f$H)Xg=ZLb3uvzyrFjBDc&EL}TXp^oq49Ax*fd9bYu;M)q|YET263+e$!Pf6k? zJDfz*0l2ZYLWbAJXR9P#RG|hOayI$WCaasa0U{#oCNP#a?Ur*9nt{Cfsh6Rt?C9fj z`AMDXuTD}1@Y*EGHh*v_%$P_2&d9X#BnIdZFJ~FqtRNR|RZlzK9APDgPA;Ivtte4& zZ3R4Ae3D3ObcjB@cQdc{Gq{9G4VL0;$DNv? zk}80Qc2SmoAgk1X9&NPCYFJ(_J%X49cd7&)mz~t5l5%_re578^)BH>p$NbFhCyL>F zo+w6~@!TAQ2S&jC$sb|Nj_GA*?>&(!jsY5L+kvLtW8sYo7nN($mG}f&w%u*zvuMj^ zi#gPh?r-5LJ)MZ28k5-Q$6zEX%HtG&jty7vnhr)90cCG-a|0g z-d2Jzq!M9B_ZCD(onKuP!h7<@f>OutVVncU8=*idLaatsp#Aj(*nomkHJOPDpG?c1 z0p&__89Eh<@U4Ere3ABUU7&>26oyd9Tm40s!`nz0cXBuInSdz`(qKbt?X}$f*(NjjY7y7^;-H1)iflpUs})$s#_98+5_dwal|{(6S{1no zk5(Jyr4*bt2afA^u}Wb7d}xG+MZQb3PaDv5uGjSyo7y(Xiof=jz6ew$lOxp{`1^(6ZS*{hT7q0iZEpZo zY7=CIkEg@e$Y$#HNmAfmsC`p{oMp0vEsiOnsC97JI+K;EZ_W_u*gT+*YL<(mWLjmG z3m_%amk?*`cNj6BL57W(AyeG7$j<>0cdv%quV?|Yofdfp)po#mod?TQDog|$CR)2* zk4R+}`msDw&gO^EhD13Rmo1Omtt5V8K+JdNVj%c*wx{qUY&Pgl6-m6(hIqbB68&C> zUxhixnSwO)?GD^-Y*3X|l?(%BkqkGNZvv zB@e?L`I=d*cag06>z|XF>#cGdPb*(Suvj%F2C}>Z<9_fico^@EZb=`aF?Ng?l7{|L ze6OUUhXrehPQ3%7t=}U^&Bv1E4xTELkq2!1+F;Wxj@(Og70udIyC&AMYo+kO71(7j zd8`t&|8Zc(R=ey#F7#`=Jd!*s(lKU3;3e0uN5ZJJ%c76vetxDkupD{0Yp9$@?)*44 zus)q_=Y$lLv9r{`-ynXkST6dHy{j4`VdoIqKU5x1-S-T`01cCuQ~OdIFzdc_mDPl^ zU6U(P@pizK>#uA}==})z?K9w%T8GIiLxsDbj}#ms+qJ@sdZ<|K3?~0<;B9+)C7k+5 zhNo$Ajpkt!sqAaW-0Q&2KEc0{TIgQ-6!O7L%4fL&k0oi-^5NKBqKNMdx}||| zv@!wsy{*F)rUROXY69n%K|eh2C5ZmuBaq%2XmiiqkXMHV4!`>PIT-YXY~V1)CT1bd zeheMXgr!tofh4m;HxwF~1(m8|zw(|&ex~_@R5BIXfD@1ECH({@6IeUTB+B89e5|Mz zORRhfG+Ne)QsCu9B8>NNKG<)=x*_e$q-KiG6dgH=CQ9pYNn2zrBHAS zM9_6GQQ}qq(Ra;J>U8*)L@TXfLm$y87clhE;ec07TV|Y?tVWSMn||e?;-w=Z70;q( z5W_yJNbAz%5<~^E4G>l~QhuFkhr~*n2uJl3;qGgtG%9v7&8stq1jiyFK9(MI%Bj6E z3_^ZnW&8Jli#8`l^Z!wk@{W;Rp~0+8L9L!wphd0e1*m^Tj4kl64T4SvU}aV zd~$4vYpRp2h?bI}{XM5n-|E)q7F(!xyj(#$e+>j`94==?QR-NN2ZT+4+b&vE?}^`jhl=Kq^& zr&7r$kZye*!ULcqhGG;#wYrJP3U%eNeR8KkZASs9u)_Y%-y)&!(b)CXds>jVC&`%~-L8^wc5^orlH7SY6?5lwi$o3o&w?m56S78E{R8_MXQ7u>BjFN;;|RVZE8$kLyLG7-d2Ht!_i) zYx^3IQ~5AL!|)^ie1rA~1Gz0rp_Mi1EU4iN;Xpk6s`Xi!uLQFzmB;hs6`ki<4!zy$n>EG72FDJtz{J!mV;w@}p@bot0NkeuBOObn(j zii)e@wvN6&2g#n#tOULnLXO?9e5_ETTehpL-hst z<=GBx>%4oY((EmgYj~~yde;9Ky88a)G^!k9P(yvTPiM7%Qfi^5DS#NyblFWU)>w%J zQhW|Qx<1(o1Rf@ZAaC#Vu-wVhFguiIdfzgLff=avZ>WU(F~I$v87%)gylvgbQTO@LsMk45-Z>aacrO?}5N6$TSlL45TqAK#N&0K24q`NHA$RdZjUeUj z$+ol42q4pk2wsgO{I|c8WR%2BMV?4T>^;MSHcOqR!l^VVI#!h zIbr;WpwkZ~G&I*=G#6p=x#uV}j=a;MA?_D3zFns@fc%i3QJm6ig=5>O(ebXqvCf0~=)1n!JUKWpWxn#Bci0x{+nM z!{GjBoR?>#m1S~eC_kxwWs;3ro>wJ3qnAV*S|*$QHT7U|J~D$Lv|}erxXi`S(9C%J znh$I%n<~*}{GrWSp^T|nGV{r_<2&R`g}F$VjHrW?tk>d)m9^n8QbOl1F>~eS<8|_a= z!xEcDq@b7&qOYM1U%4ET66O7IfeOAh{38-$$UB#yYPK7ut!#ss zo34x*42P~upm+^0m)Zh7z)bIwehM7C1Odb!`N7aRdrv#wSbQ2l0Q5~^8zU}91k|5g zz{*E4)7(=jXRTOVZHwa`hr)Lai{oy`xOO_?I13EPH8zfW7T*tzkK^pf>5B{ExIeI^ znyGQzh1nd})E&odhViMF$lNaALicu=%SFAGU&&kr%2~COu(an5Im=WQw$aGvVfy9` zd7r_}g?`d$|FbYH$E0jgJE+QEM7u|`Gpx@d;`jaE7?HYc^X=sOTLL=s_qo8zi(v;% zi%SqaCuc+b_Ml7JqEEY4xc93gbu?15%QG0owU=j@sp^Zl60N^H0|2r>3jek3xeCP1 zEo=sYJymzjMx9akTE7PY40((-(`h z^(|V9abi>kLuZrVFpZ==E^ zF#oO-BPCO0pD^2R!?qdg=;%7pOzpqTPy$Y#jVsnHU2($=t8O6QcR)k?+p?3NK{-p$x02d} z^n3kvu-y&`1H1P&=6;VYatvql@DdkV&|$~W*dF)Dxskl^bs}weM@}8e*kk^VwKy(Z zEH_*=hRTMhR*g@7B#nJXw(@B->tk;w*)K6Ee)}jXaa6bk*277W7BtGqV+K%Wk0;_Y zigI2QtW+^XRYRo5(5VpV#C`Jk#DUfFHHzuHni^fje|S8rv3;LBk}sg6fAyM;{W?oq zGG>@*<2$nL2YeK8At7YZ{>znAs{O1)iSV(yUE^cNC*B|OF-hZNwKWC#;dzkuk>ggC zvOo1^lV{Uh(KN7VF6G!3rjn;UK{POxU=wj^v~0hen>bM9;o?D1uD*<&3wszw61*9f z-F6?^@YKMnKHkrE8I8ycFMzcE3P^101~A(XfS2sLxfUwNFMbl09*{E=9UysLxUUnq z(8hc_72Tv{Qq`@{mzvK?LXxBc+h_oIC#<*Y#fy>Syv8j0%0x7=G*RL&pbt*YO{G0= zvx5!q$`%t-Uq+n0%7UH09!}}=%|NjGK~z1!_I)*`!>m*!lpEiTW_f5tC)xE_luk0u zDbTn!i37MENxR2k*u8&XyE_@%UC-)Oa&JVBTXrJ2aE=xWsQy}g9yto~0Y5{4E55&= z{dNlypr)@OsG8p_fWuvxf#5kdgQd|&zcyIOnkw<3S+kp#C6pp1 zK5odP)?)^BQzx6IU&D40t<8tHADkyq@ilI?NS)E%DTnBw{6G4Uy>RSAA zWaTP>Yh{a`Eslo!A+qxug>#csI`|!%k|<&VNI|f*=Zid*f*(Rj)bAlJ*I&*Tsrm@Q z*Q(LbSCg+w|Lum4|MX_!G3l8#^_$Xj;4w2>ncwqAfDF4_N|KJSaL1y*;Ge zJqfAoz$hHvl7&dzs^Y?Z4D!6`FqKBQka}}dG+_+wQxa>oDYBDRwe%R{=_%KgVb?p-J!tRvfkc~1O$e_a? z%2uj90iP+xIRUsgz)9A2SupH6#X{8uQ;SU=uJ6DK``b+Ww-%WB(X``_^5n$GS)NE5 z!Lpw5ti4ozJRNqU*%r31wDwP`jlB26jdmum7h!D43ddzF%$T%2wLSN+vqbA5;Jt4l z2yS?|jF}CvEfcF>9$^j{SDsu*85~zGySi${^7E-$Z?aL%YQ17$ zhj5vxbF}}26E3_KDP7jiX$W+5dNFW4^wax~coFcvg{}OQUjQuJ^?n+rc^$Iwmc-8;RRNIp+j!=F}#Cv(PhB|iI* zwVlLu2iPI&%P=ldO_D9JJxwLwJs8)XH5jjwcBHnxr=ZpDozVJ~m*8Hbp+cp-hgnYb z+z^GFJ4?b$S3FVP$ExOCsf-=}s+pw>tfkHCv|kP#vR{doy^ZljgVC#3Fv|I&L-5mOn$`wXfPTeb+xG{@Y!Knce{YI;x<-XH@dGJ48VFEpRlN z2s)mDYHQUhnN|i7W?RdHq7>k* z5*5A{D+P|oir%6b1^-*4l?pFGo2{3zobwKdrtKj7L+76qNzb;-eM?(zF11qj9q^Tf z&%ia>cY)W25hjTrO8n=u;HeVI6$9%L)5P=Xu(-rbCGa%Vbp&a82`_}8nOf#&BV&4g zq^N<&6fOiFZ2E^`faXJJ!*3=70r&7y;66!8W)vgS%;Ur5nVR|Nqgn+xd|WT3^ZXC- zB;r)qJ6`lu_HwZ~a7!Grtm^?zB_|MhG(H6L`1k|aHHxvqetv*wXJ*YG{6wVshtNUS zQUo>jOugjaHkBs{-x*gE&y@HJfQnj#YRa6>Z71Qj;1d@-A9C zpEpx|7pk{?l%XVw1BOV_nB0*z)Jki9tf*9Z2TaA8C@TJ1u-uen69f0El7T@q+dFKd zA|FCqXbN)5l_=Wr`uwoER1D#jGipi_9lp@xkATu(0LeIrst4DYzEdS;^zW zl#sX^J}m~T9|9AzZ$v)dGF!1z-J7#vrn_PRbY*ZCBQ&1*I}@!&*4CL++0d&ibX0FL zCuW9uOAGVHqIheFuaoym>Tqd*XjnN-d%3>Z!|}8%5pJ`sK3ARM2$!84zDBg2`67Mz z?}$5NWgPwJLG-s2p?ILg78qw3L}QNgauL=} z91fWdn~h+25<|C)7(9Ivq#chzQ0i^{oKJRJsY>k!DkP)AM~ixy3`6Q2g5lvoj+Quh zMD@F8Dde6$f3VW{*BNBe+0?+ZBe3iYmS2|q6_8ce9qa@{8nmZ!Z?fbsSf)@tTT}L~ zi5)C2XBwFSjr+6N8&z(CdJUeMh1^e1ME9mkryFeT++5(F31SpP+w$O*PsB13v4iEk z`%ZXLO_-Vp&lsFE{wdaWuCM}Z7ndsj&M)CN-eITpZb=dca9#3-^^CBM7$QM@2nZIe zl~jM{Pfpuy`*$)1-=8c}?Okk=O^UPiMkgTnn+2#o5jkZ2ci<^F1U}I@sZgcr_hrP> zmrhoxWe)PijlUOF?R_J$l>Ta-nYPJ70Ug|gK%?Xvb}Hq2R8}8h=b6|^t${ zIS-VGv~Ig-4`hsj{Qr7BG-fDg*vWE6U$t+Ne6Jh(j*e5$w4SAHlY)$d&)QMHe8 zK4G}D$?ZfxlK3pYXP9X0_4XV~W^Z4Wkrp_atdhGPbqC*Y6GJiY%lgx_j^KM*=AgzH zxBtp!_D`cKFCfzk9)njZ{P<#(j>IVIDQo#+XW*p8Nxu4g>Z?9OT)rDA0tsQ10h3o+oF1E-?%Web1#mTP0392`*=Y9Cl^~nlb}cLW=HjkQUL0SiihfU zv6<;RU`e&_SnPC+y5=7t4V?Yk3%Filp)~l#&OWK_Peq~UZ4$=6*DTE-x=(tu1HCVq`u#lIKAt)Jko4@-d+#dqq^ZZT;EG<{5_2Jnn zXvYIsn6|rbzW@}RX6S%viKVx;gVYpQwY_+uqzQ_u<01LFn{y?!Z%2MSl1B_Q+aqEu z*IplQ_Ir23+bx2opInK+oxOaFI`*(-vPyKlGhR`Q!Lavd6BaR4CMaoS8)Jst9)zD? zlLJDY$0d=fWZvelP8X@XFB}djZoP7JSgEmjBMvOv~%YqG|)B))tmgl>h@RRp}b4LTg^Re2}zzC?tAr5 zb(T%_kUSgRe$w0I5eF+h*wXd6FdTQHL_PliG;|8%Fsf!{Iqmu8d>6S#AT_Rj$?7Dp z&f=l!6Q)|K4o(7t6YSwbvF)SKT2(C6%v&+ZzM%@`rzWbDm4QIln*`%7V4I-S1H&YL zRfZIJUMB`#XK0(GhyfkqrJcW+ZKvQCqn)ZYLcWgQu$>0Cr?Q1`7+seUnPAVbRB&5? z#_~Qg=26RJq(T!RmiDAl;J|iZigu>8akR)bftz6)qvPPQJ{p7mOk%Hj{eo@pU{9MG z@*&M+)Uf}E6<)0ZY^#l;o*9sjHv9sapZ8S@RASl%D!J~;#z>ZCh_v|{45D;10_&0m zfRWbCh^bp*Ahi1F=xfuWa#+ZXNV#1Pg8PDd**2BNv+=tN+45dqpo*!;rmB2fmC~EK$)^LU=}4=${y+-rif%2 z4uI^=)r+RcYqfOYPX^_TQywQ@9>Rkl^045W@N7G)p~-DsY~k)O6jePm3_7$5o$Fx7 zvMQ=shZjP--F|ql89pR<>fH#JT#W{&whBkxr<_m_w(h1a!};!J@pc2--?%x&5wKi{ zhhCV7YIaJ2p+No?R~2!#F_pw0y)N zqF6w|3D9825-E=wR|*n8fr=`G=~UC2o=x84Q1}*;UD8j`oWSaGvzZR1=Bd=PN|1)K zr71R@

XRWHpOT-H-K~eqkl`M(9KEeKvvdCXiy+@7XJkvP>4Lyq#(Em#V1k3SrOJvam&cIPN|2Ie~WuEO5{y{aFYt7vP0A}!m*4xntD z+qbB~I;6dtkB07=XeIX?#Pzl4HSH{Cj*G2(luU|KERhZM?1xRqv9|+LeL-9uz^KyixxMl|8n4O2$3>e1!@9-by;SqqDqBJYwL zM;kJSnJJ5)quzHB+-+{oh75*fL!FkhIYIUY@{+nqxYvMA=e^1f5RQ%!^^E8Q+LGcx z`cnkmZe`nej<6xBzEBbUSpZqje)b-Mn_=VZFp~Bv;YdPdrPYndqL|F2F=G`yTXUM=&xtov>vFVe%Z*X^k(Bc#)9~L*Ds{X9 zbj!Xb6I{++5+13}d}u}GEVkq7RrVF^)5=XS&z@I82PQ4NYvAlbu=1{Yg zzAE2L-tt8fRbD3{*_)+j+gaeo>u!isOiQ@F83eX47)#5Z2cPvv7mHKao1dQ>@LUZK zjgRYFf{5O5&C0NPjkG&1H??{D$UU%UliO;3OZ7MnvlGueJL2fDG9?dJO(+r8ZiS?~Nh)t1b<7pbgry(>cCX>Dwx6`{n2Zh1V_ z$*ROpB>t93snqm9Jdk}0J8+A~-C4{xE{2yZo<0P4&OE0k@v2V}Ed0;t=rF}fO-b{R zH9n9gQPn1-e7?8f4GUj{J(oPn_R5L8vPnfoUbVYa30wvLxN<#8DJN#bUAzr2Z+ITs zU3^LiQT7)CT?^`mK{0N_t?Ij#FfnZ+`v(*O*7dmGbu~*VmjW}h8(0!?G1Ry2c&S7u z-vej>rKDt6r2A1Ldo4cK(BW3W8ihTL9Y&RotrFBIoXCC^J~JC+w3lSFUkoJJh%<$` zoa>u%Vm2QEld&Plh#&~7)*mv`*$Mpia-Ha}d>t^2Mn*+L4y!N_Ge(Eo92>%nJws%* z7j!n)7elar9RpnSAl`16ihK5yMT*JIgNu{69cdK=PEzIhA2qd?6E3(HZwZGzdtPuNuKQ)Vsf;d zvov*VxEnFVH^^on)@r`OOpUi?_AS{B>$B^jk?NNcy@b!uYbs zT6+y!yxwF>%8KeZ`#WUcG$b!3h0mg8U&0qR&dQRs<6>xfR+gFN4X~px%_={PayBA2 zs`zodlGrOfF4~4SJQHuFinr&hp$wv7SG;6k(F7Y}iB{*8LSX6aRBsjAqS&g7w&%S& zAbTgDG|=k0-bzN7ir7(xMOGVC|6LaSK4?_!I2diogk+n)aVKociEp;i2Be=k>4P!m z+Itn-=_qDTOwNj;xRR~I#v#Hf--8sS;A`Bgyu%P)x$SvTj;g!_5Gs zNH7rzTwWZm26iHhU^|{DScss_eid6*n}WZB)8R?7p90b{Yv|p(5Q-`GzcL^8nF>Vd z%z)s6$$(k)It=nz)RB2e@=cp0@)P_=F9_))enRSUc;Im`Ix-!;jn8yMWfpHp;sL@%l;`PfOOyDxXH_=R;#_ zA4F$-cczHF?k1Ube}Dj?Ae$v?U&tbD?3S}NH8VxjjP-)qo`H(e;b*H4%tqYyHy~!8 zrqzsvM(x_SXrM~8utPx&Z-cXS_DP|E)j~J6>7#dGY1x`#W`9XiD17mE$f_ywmQl9e zt-WP5^wMdkK1q>ga3P>07lZDW%@Nr~dUgy^Lb?`-2%~k4z2LZpHoR@H`uD~wCNtN!FHLh0#Fs&C8?RK< z^pxNVW#3y z&{;P2Dx0c3@ULH^gkpU6vvSBH`E`{3B@2G;PZTv<9?SK& z<;_fnWKt7G_Kx<2;gOA@vT<{*)LsSVPUpXD-EyH5JB(SJXfU_whvruru|z$R?lTglD|9_ zH10%x(p{3Ik^;;(MDQq)a^6l%rK+DIyLGU4fE;;_O(qN(q3}PU9oNZel>G;t#Q$_K z&Wu+7))GRGq4iwc5Q^&*^*J*qVkI8;1VqrHs;z=ZPWz zRND}vlI;&{W5fT!jw;96SYDmlha9OPBm3bJTs=uiHOWCvn{oPI7lTFt{ z9?cmu2YwUn|B+-R@1YT*-;*Tu7KCZNP^|b1f1>zZGeuHQ%ofky*7}g4O!E$WL0}vyFwq8DbvaIlpQEG)ocgws!}3bQjInvrZ+oi z?GZICbe5#?2pnEZt!WT);CIme8P+uFyvqTZJiz|BKsJ!NZJeoqTp#j->0RBaB-@#L z=5w%pZj4CF9zc<&oV|XHQ3}3h7pd(;Ig-bjdZmwC!HNoGv%fTCAz)VQw5yCw*(?E1 zuC~;(Nbp~7r!G}iPNP00I+HCbu&8dBD-A-5xB54zR&5%AjR*S)O(T$V%zP!eUosFb z!?dSlS2uw=A=h42bVGcU0Bxpd{`}+1{*ZZ-SB%gH9hjUDN1v%;-Zs4 z{ywC4)tAL12U!c3Q?UND>4BCR9QjEp{#XG7Pjw7t*emWoeX7x$yc}VNQ?=J}sNYP8 z8uiX~zy{yA7^yEIK^>KRnIwu2G`Fr~3UQm{2l1m7z0Pq6WSvo-Kwi zF-JPUR@y=xu$l(a&Hh56)@vhb+dJh!C3#jwi_AK<3yQyLHz=%9!sAstcamy|jE<9z z&VyGy^a`5_Y0FnaGjP79Qa~TCKm80GdyP+WB#33h&2fDjV^n(ZO2s-flRJGZdkCKo z=xBV5mFn)AW$`pYA&(rGxmP+TiAk`ABxfXt0>>D?MdjJehS$L!w+Z1@3Mg zn^W_>I**&1FFRI}zXaXE8eeALB1O zKZ-;BG)9`r_83w%&ioB^(5LO}Z42z3$sO#xQh(9u`w=r;XeRZjIf_~88LcRCgv%RN zTo>YUn-2<;y#`$F-M2WZ+hZ9`DVio1+PnWq)IDeTUIVQ@V9g9SvnivmnPt~64>i-p zTG(}u>2wZ8vk+)E+iz|U@>G}eo_A6iWfM5HN7)x~qb?cB2r-ykGYeVZ~E$y80A{~t-lcU`7R!2^qt^Zp`c zpgl%j&=kU-vKL2~$y05JUdWmmEeA^f$P$6I$Dt+O+aZGTgoOiP&D@V{&L!++9c-Ij zFIjsr*XQ+^c$pC|zxu{CS6_d{n!walJJmU2ZQ3SZ+Vy*56x-T7hGoEjvH{#eyjL-6 z>z<>i=pDgqh&=gu->@2I_3O@-%T3|#^xT1-C^goz>-$;7&5xn|cPeRv7}B2S?EgVK zp<(Ub427>A#v&ku+MAR`DE3fH2nX0Kgce&w7C9nvV*l{<2{IKZRz57F?C{;KAsK0b zRQ9A~#W=g4pboEvbCIT|TB!1|GWPE(5o)P7DgRmzx?2&8)HJfQ*-O|Pq~hR@*VnMa zNmfA&+^q~IPH(vRKN+Hs=z`ltb_yKa*Pfh!yy@U#ks9md&~$fFl*qEfVtn!kB4c-- z8Yr?k{X~{?Uc_G)&l$?zy9QftF2 z`@>=+8n?1^I?`a}ga2Zj)Xw%nYaMYegdpm^V-qwNCQ1XX<0t9BtTxBvO0SwHIdC^&TJopAwzRGAyC5^{aKT#V;pIbmZuyaBbxz;<=`! zF!}nL5|Lbg01s%?68g6jNA>{7s@SGO@83Z=I2z4s|A0ben+aW0vZDT51+SwGkEEEX za1vOqY)D6)KP+%k{q3mO9vADN`qo5%!k>+j{|NYKy~rj}XLUM6_vj>v95O;aFZ=7{ z5w_P)0Dw3QfQWAP4=g%|0j#=D#Npoi3oOP|uJ30onNG%;$u}czIdwlFRg!1EQ`Jha z#e6n>l0`e7wvM5VThc?D|NMK?5C`0AlLAW@id5|q@@VUM@hbI9#}Ia0nZdRoLbyFw z0~UL(cdFz#fWI75MK`VgDmIU*3emx)&lic5{avhuE$_0oJyiZ0(S?22#S-tNWo1cb zZI_nunJ{iMyf#sKIs)x>wk@^$n^ILfu+)1*$??rZkxEVp06-PPVl7t!`LO`(;c-&n zFbeiu$o8vTU@nHRYi$OQtg~ z^y5@fubsK47Z=7%;z!U1kHJcABYVB!-E+b6J4uT6azGYnOrxTg;?hDJd)d)vs^{$@ zb$-KUyh~=Y|4*{vt8y!Cyp&hTxsPqWz20P@!s-PMa;-8-d=Wi(&4M&)nxcwS`5ii5 z#ikXya+yjw*@i3TKOJrHVa^>X88Gn_K{Bv;H*H;z%A{N~)i*&!U5~rju>q@Hd$V8Y zsIT^-A@UuU+(hFM0md#@?PhZG~&!lN?vD=&s#*O&Pbx{R=B}2e$f{rcT=A=k=Mt1NR82dN z+)Bw|L9mx71%8WL?95SUEPq+ffC%MVe`0b*)db|L{-#ar%x;`WA3tQXQ%M=DB=|1c zc3c}T(%!ES10Tto3(I?02iCtp4_)&x7_Co~Aq06mR?)QCy=Eq|)~j?j?XBh1xd-~T zgAPBEJe9mMFB#eUHgdvxVWOO6ajE1f5>={a{|7?3L{Q0ob26-WKYL#|JHuLSVa9R_ z-D$s~#7^$yNh)~{q$5Q6t_lCZ-rMk@MP97E-MV!_B?^tQk=qQbu&>TxeIvRCkkS~tPh?8V3` zU&c$wN>(=jWu$AFN(eRsZF$g!bo;jO9^e={T0GQBUEeN-G}t@+v*#wLfvY`|R+}n* zUS=m(4?7AF$hBz4!tHKZ;r~FUoB33#KQ9AbFTKba#Y4vkHlx3+6b^w`EZW;oxbR45 zZ^@vw+r>0;uVSgkR=ADUyV4>4u?9kWm?((6n@qozAmn%`d60$E4*x9VkimIbw0_Y-jLtTu(5ZQ- zlYrpgC0H%IOhp@bbKny=x|1(RAL&j!D z4L}`P75?SWA$#9(I3jIZRqz!IV&w#&QvJS#HtI@ZZ(zO|oj7&?HcN*AXwf}tNT*^$JZN#X08oxT`vsY2Rio&ijqNvxV66p4K5zS<8M(*Gk zZOaNV-1I&$UHhjB1uJqL{?_*#QM@)BSPWn-gezHjGS*IZ1@zV(k@45#DU$Y5b|W1g z0-}Wv3@Bljr*>Gp9k&ez5M-K48C!b(P%AL73 zYJI~N2Kd5N`HHs9OtW1sv_~Y8$7Rs!%pqp#`UiXO)3^~LHN6B^qJcT=4bJOevIGUp zxfdLDu{~lXY(}Ed08v#* zD&K{uD<988B=K0PWK56PHG2gPt<9bfoJq`8=-8#~s5;|B+nj>Gq$r*`pMaZagT8q; z0VjQbidW8TlOFaDCECX!Ch6E`RH>bv>>ZSk>i7^H?|GK(L~hOin7lDjv_ukPM|kj^ zt8Q=v?gzXVe#&Bx8xWJU^5(N}!w|x+&XoFeLSwD+9`*u?!En{`;>2?R(0@k$BJ`ul zIx7lK&j@mwqjtXtN9)*)(5-bSMz(v^f~2Dbi8h@BIXp*fvvcm6qJq;-PD_1~J&n-G*KpEHwNIxB#+izjM<}9J8cI5eVP1>(Q zlcO*;t?3nrKDN!xBS!#Xu39o%Jj*CeWNU2)TV>9HM6djm%)NzpzgkkX*Fd%#6>bZz zva|8Up5RSGYHEbvG&6e_StqLE+f(hRzp4&uf3Fa4Q)AzNl#10(QNmaM$4K z-KB63;=1uy3U@cI!4`$P9E~~OP_)-Le2go@h;45w+Rn8#dlc?sj=Pg<{k5WPLSM62 z;gV6|P@BS4vWDMLxW%x%#y=|BKR#^eP`KfE?mDb+HMpvuDjeZ{)n^L#7;E5jg}VXQ z#xE3Z80uwxt8m{!R7#AI%Ru>!aYil^S4X^&dkWWGiAL^g9$ly#YUJL5Y433vwM`G} za*f=t7~y;)X9l5N(~R2xjcc1_{I|jJ8^djN$h)FIrRP=WHKcrFdxv}eR~N12>Q#B-CFCXA2gvRDRK5YHWl(>Sy$ zo_hrNI^*7Wt{m5mkHmA|nlWyl$8+mr*uURXxmeuam8^1aqh42*%6$usIp|TjmYC3T z-W422p9YmF1eTQh)?cnRufN>Xe$&`(RVr7<+W5K3wSgDu1(oxH*7~-hX@{;oWL!^wetUK>HOoOsJcIXQc_YZf>l>t71>2m7g=$I z6;@nzg~gB%R(=>378V(OqoTqda;Ye(sK_YEsE3M*jEs_mii(N~i;N133JsMEiqi43NP73-G<)6J@Or7MC-^(Gp+Ay}8=qr&1~ z*5kl!!StZ6NLeuH)omda!DP@*RuxQzinb?JI>q|u6_uew-U=p*w&T0Ol&Ki-Q852H zv9=?a^ot{okHM}_g6aPh%Rdd~X?sf-*!D#*RjK1s;GtmZ*BN_)`KqV(TVZc7{i+Ji z>qmrq$-zjf(Of-;HRcIjC!1gSdW?;<>&N8t6hs*}fS3Do#BZ~~QU#0I_ zhV~T$A1I<-T&PI6Wr3QLW70`V(3eLICz!h@dWT54W zwp$IXi3*>ARw-7M8F-)`zQ;gDmCw5q<#g`?y-yg(w^i+oK8=8qdT{h51Dm919}4Vh zL3rxhVAuNwYF2Fc*ucNnEc?tr`YRUIUmHkI3^~6w&>xD1BL@1&Usdd!$yB7riHVc> zx0+=^lWFxi{MfU3eBk77rcBS7KAH5?R)-@0Cv(nZ`a;n%zxnLk$#cyM@)l2~5tYEb zbTVz!BlD`s+?hf3{Naqf_Y>Jz76Im0h*?<*8&+qwl~wQ|V74Gqu03B2$MsdH}Ljnn8yeTjJIG&-Vx!?}MNpGO?8Poov;a^AjbI+^qjN;giY zI8~#{Yo^l-m45V=>9j?KS3WeIPAfV2sp)i^vXtxn>Gb;qiX+46>GZYIXW<{yX@WNG zKVaLq8T22;hQJw=qS!xe2IXkqGS8rAlxq7{?%2L*hT2TKwr`qw%r|t^40={osBG&D z{=H}EwKMpPTKIo6=qqjT>t|4f?i{zwApPA)cgYOuRpCv(88l6u4~zpdXu()*q8XH+ z;(Pv@K|57LLIO;5T#W(^W)nHo@hhw*(%;z|v6<*eJ!-_6=p(&&up-_>Yn07uZ!yt} zx-)GzQMlsZ9VSXs2eOx$_;a}acbWJaqfSvjsB+(J;`^TgMg7#TdWVUhXSvJ4Aw~U^ zulgPn?TguUq&6U7N5y3`)iz6Qv(*;TTyfc)+V^~QSI^|D80XfRSoJ0>x@IOH$xr~f zu>f-FwKM5L-F>g0Nm)uBzF{Wm_4$sQX7WHbbn{I9?DFs}GkJV!@y(>aluBwIp2;tm zls+<(Pi)4=XX@d>M}aQGphrw-p>xOi>Jf zTU9JU<@;(DE!MjJeirTCs49>YLbt6}D$1Ngvz7DY70;nXs#}vN_aoag^nn zP&%Z%viROmbv{?;fX74WUajgULTR3MhNnYml0GTz38l*vNB1?~+Zej%8eh*Fq5R@q z{+prvy{J)PWoszgGW;#D?Jb0R-wtKl4GXK@0qt#Ix1v^Q;k%*iRfhKv-X!$CkMI%2 z1^UXgwmp>HF7*SDK12aEA0naaBUGSASlEI1fCEV1dH@CIe2nz;3DQ*yZJl68C-UWe z3VHNXEvvI)^+8Ga84`4UhJp&aqy?WNzCq~z0_+tQeTfPfx}~K;?;+9DA(UJB6=d7j zV3(#(AE*Zbf!~0Q!qjiUAz|frQb4a1AS^sA`Hx6`Ve0piUs%~E`HxC|MIRS%ObR$I z1qf67r2t{&4^qGhDL`2GqvRiu{KC|eY-1WZ3Ay?w(D5@g+xv6quE^QuIqTVOrx95z zbPa)h!qQ*Ckl(;IVeT1_h9$q|uBT?3r*hju{*>gx+!0Csmn0Xu&dTA0rT>$|jY@uD z?%$ICAIbj@+T#8fa=);Q%s!3?KgZ1MRMZg#W59s1V1qE(4;&O$oQr(6age*lK`t5( z8vPO8;tx6JJToiXZvy1{2|ny3PXvc1B0+Tk=$eG^{z;H4&Ij!mAiU=S$fbdhEf<0v z!h#^g8-gLX1fxP(25`h@Kt#=C&@}}a2Btu+m?{S}$^ngXz-e;8>2kp7C@_Bp=x+k+ zg`SzM0KGcnNfjyvuMr&dDw#VRbkC{&oLhx7u2-S zOu4$|5oWqYF)*_E)^PJ)o3A0tOnPcGWQmzB)+O7`d=B+rYUatz;-!cmRE$;Zjy98C zCgbNY^9jhg%*^k%j>ek#eZD}anO|-hU2f(VT?SW}=_bXtm1fdQMD1=f>CawzJZ4JM zXTZvJW-3q-u8YB;R5PzasZKZZrGE7WGk@{CBm))5%QW+MA5*gsZqG)zX(Ph@FER6} zIX?&N*ktAtQ|D!7K4GP9h6ePN*_G5hccVFDZkj#M%vT>g-eOw_j!E*^AzMGZibg zZbhc*0yD+yYqi_V^t3*Ymzha_;L=fU=2?tUVcR`B4wjnLW@$cH8g|1h-{8Gw9#YHi zL#+!c%(O$x512`>krPWhk~CGt&k|LqC}RgPD>PD^9=!EkBw`uSo100R4XgZ9gMEXAmZI z{ep@+Ps2Biznb~u6Yam5)mW-DG>i(i|Dn?97L|>d=|nPYE%=;Up zf4~}{<6q?K5f-btb-4*7%ZJ`Y+qVatTO;ibcKeJG zsmkxn595)sUQu^<+8Rc`=z*o_`Y?J*-G@8s!gz*5PkQKq;cpRN^&MneFW4!}KMeXEL3uStAUnPX zyM={)i1$CLW#vM3M-kyVhKL?v;qfr;?uLHI4MO)1NZ(tno*r^9(@l z9e_p(PC}-ikiJGSO!rFL&xmLjW(}f%Az}G12sfRA+;j@E=d>I^SU4mm`W37eT7LuE zgx)jYfTE98Ka7Hnzk`iJ&mUl)u=r0fa0IL$K|#*Hz%F6lS#abm(pCNsEw+wAZXbo_ z^8OCPDTMw(MD;&XV%FN(t;V%0+X~rSTR#tFiTn>^vsq92n$1`0du4QLTjj04D^xLEHx9BSirzAshH3) z7wi<~&I5;q<>8=dKG-O9FF=EOg+&XYp+M_g^#2Ac0z470{XhidvPFDXD5rfn%FU0T%Qs<$6$o!q!r5{bJGw%nuhqwbRTvsUa_6fy8#>&mSupZOc_`*Wnjrd{y|}B zHqse4f{jAYB}m^dEX|R0zD>y3un7U~OL2gHVcBJfH|C1XbEUg&mhQG$y!vvaH(VjM zy+YFENjhQS7U`B(qC8)%>^QH2YWuDdXUi9xUM(#VdbUbSwxXcoYY-k-0M-{E-hHh& z@3jao{y#}~9l{$xA9)I;Kw;_ipy>v%BJhLAKw7`0kq^7v79`!!3{- zZxLTA28W8}9I#DO^*_h0GU5sI|AUr|{s#qAm&nk28@#>eHWW~@9SrdyzD1Z?DhCo) z-Y!mi2iPMlxpOY&JxyieRKlFQWIVVV2duvva`FyvXa@$K(sHB^xkm;RVeY*k-6!LT z&{H9ru7F&Azv};b$NB&=bP5X|l`=OHQJAt_)dXnk1nKa2_&RUzE?h>Qoq ztVd-$5LWM+i@8B(H3E8tC69ro-6*JSx3uhWX<3c5Oz3$6928bQDJuW3s9ac5E9E{V z8h^@%h}@?^zh@9pCv?|={dLmfXQjo@NsFI@T=={=T|G3=S}&%20UUh+@wIzE_lw|w z??pIGX@hwEOXBq}iOTkh%7oP~BcroXG$t&0MY`*&GEN9n_kn}L@+Q#o8o0LYHBs$; z(Ll3kpczhPZ$ZMY7U>HD9bcYJtcp4!6IHeYQEnm;_U@X~F*fq{8^ zgW)|nkH6N{^z%I0t5|Sq9?z_0ot{UB6dQh<#~*5IIWv#kiXFrA_r1>0PdJSa%^7*t~$+QO?`2^vm1M|tO7;x?aUN_NgUO+2VIX#{QRHx+ps}^v& zp*ta$KD|I)PpS^?YDYvzpAJwq7_*QIGR$7c;WcrP!?VDqBGB~^*!dEe_3=VFq3SjC zDOmpbLe^N-7hvs|3wg?^y?Y@~Ee#%8NFM#VUBK4}u=gw^{rleHZx-^ZtFqpOY?A&X z3n^dSxRwnpB&#}*{ahB~y_qRNJxGO8b=9`X4JV)haFl?YDtLiaT_rORe;y zV*Q;~(*L1q*a0@)XVtgJJ~e#t4&^=wIv%p}bKQWQR{n2V|4tN8`lyu#6hn4HZhgYa za|^joNxo;S{Hq~r9T@VgmHtsQzF_5LKRpdrp1rNy3wj!@ss|{$4yYYHr(C%YbnLhC zVu;=ru=GvP@;2f-+rXmtLDPp|dk0wX31~P7wswJeUxEQ&flWQCT%O$g4gquotnb4C zlaE6l{sF8R0Np=>gTH`PL!k4Fl|Oep@H<#F0=oVO4*qSW-K0Nn96>H+0`IvIlBuc2i^V=RI6JyA%cCRePRUrMrQ!nJt=}7Q49}^U>_L?is0weG&ur3GA#l= zVnTVvGeP?-aA;P94^A>Cf*Ed(VCS&T18oZ<*tY%=VBaFJ#TLOnQn5IKeIzdmvSSJ4 zKs)4qMg8Bswx!5d9TUO6QQ-hfm-!;tNs5<8u#-4eM&MEXDzM%i!Na6yO$4iWC=sk) z8-WEg>%hK?!Ll^OTQ`8+nPACA(6R~aybLVzU5*{o7O?#)uwW}_xE2MsTn9P#2GIW| zgg4v**?TKES_0Pjz~no?;WDshM+EzV=Uy;jxB@%14}!@%p}LTVBgm#q(6=#!7jx(+Ldyw$N}dr;(XoX7qQ-p zCoJOgtZ5?Twn<=KAm|?qHcVcm^zPGl?u&S>m}4er3I%B%*uN0$uz?Lr!OB>$Xa$(% z2AxS@NDAne4i033ojG9RW<|YNt?Ehy6kh}86oRgsK+CP5zYiR|6YMGno9+jzcP^q> z#nN41e$66^Q}jLsx}IC4*XUBk^NVrU&2I{Ux8WQfFZq$e4M~? z6ajn$w|;X2nL)MTmQOQ$ zz@|*F+Lwc!lFeZ5m7x0?FuV{9xCtEE26k@;TkZsF%E8k6!MvTIXBTL#0Rx|kWZxKh z7WDP)iDc*Kd>L$MiexA8+aJkJlGhx`z7Wz9$-dDitbHBfId4R=kA%Dx$v)EiekA*d z`-4dKkLgruUKaFz=A-7;NPK1K9N=Sp5^?YfeMX`wg`I z4i5hbww?vc{uW!SYHA-bjI*(ij7+q#kK|uyW1kqAVpBe%`hS550i$zloUz?vW83G? zv$2x|ghOsz0D2?9kw~y6%7&BwQX5Pb3kIwJhgO5#9`pMh98A6+wCw~9yTFmh!QNUM`SecPvk0i$1D3yRW9KMr z0<&JXv2VEF25s-#*hfm*ZR{hxAK2Izsz0=`Z)AN08aoi)t*CvZ`V$-bi1!N{`$+4T zHXl1l(Kj}B5_hkSouvM#jh&?NgpF0X=_!fqx<1@DJo(TFk5)3l@w6 z?dO4`6T$ZLeT&&iDh!L+NeZVgW+&;Jy_kKXFl;doB>f8@7uk@}xnwb}E|xB4A1RB5 z9KH?5tK7sF&8u*|m(JNao~awcfY0S%kMku6~FRTAJ@XTicfp!a3a(FB@a2kGs_>>C5`fn6UhX5VP- z1nWOv%sw*w#bWjmZ}(#Mg}_6L**CgCpE@ZZBKhmZ>?DETE@mg`>|4xEVn4Q+ePr;* z#q1-kKP_e-2^m_xXo&%v^< zqS!YIzXNmnqHwaQKN`hO;(t7feW6`ZJ4snT=>7rpJF(-^lTpo=o?Pz zp7{I{O4hA-X$i0C&wXtPohI$+OQ>m_@{2E3xQb8i0ULUk&?RH_+MJ)3@cSB_r<@ecHbpsW4UV#+yfSn&$*F0#aH%U(+ z+SwaZAF*@y38}X8hwW;1+xdC5rN+*y{cE1I(+X|-XYBkzd}Fp zdHKBxHtnGbftUqbz6-_xmgMq(* z?We%vAv?d#VmM>xr4z-&c6vau@egod#7+y9W~%7hx9I`bt*%5cJrP~mj2(t%SW~>r6v{8QL>ay>3&wWln&|D;}0&Stz-1; z>{5DaoL2Hu8t_vEe6*C_n5b0rhYDBm0p~>1b`|Y6HkyJ|y5t$rd{^%bi6(y)pA+7E z>w@T@;LsL(G_BxrqA?}th^Fs#6XK%j1HCvqp?UA}=mp~!bS6gg9HPSm)+y>`5M^tl zc{N7wMbW$pFLzz@m^IN+m-xajj^^3R7RBooOV&s8A}LQgs^;1d&8sx}GopEt(Vi8} zZrPX}&Bn^T1Pt61%`0ylmqlY)*=CeGsF!*uuXa2@wIWA)@v*$d3JB z*M6x;GdLowXaPfBN4l2RAt%29_6dvL1pQmVnpUK@zoq3w-6Ii^^ENp2HWHM-6OAeC zHiWkbli!sC2#elR+;#mg(X)AxL*56-Mjs-&N*MkT*eXozK)S&W9IosD!i^t`!i1hr zL}8ymF6tD0eG1lnig?GtXde`IP!#r=DC{#Ntn32AKL^`{Szmxd!tyV{kZw_|F!c~P zAT0e#Ec~@p_-mikxCiVL7JmZShQ`NZ_#r`SO$;s5r=e$K=!$V_ym)8Fu@7U^=1|)*wZ*C}PHj%L zEmvE-+E%E|rM8u7Tcx(uYICb?P4lr26ISK<{63H2S9uE*_3$_Qo1)xXr;!JzKXsc!gm{se>=DM(zN^?*g-SfaUi%$ftK&?nA)9{h+ZD^y~zS ztHAn4!JcZ+|8daqgoBs)mi*VjOC2ko0&AW@Me3ggo1RB_`wI>}H4nb%@bQjeuY>32 z{a*%0g+q;C|0@n&gBr3A%xQA)C27@bIB-w1gJ1EtzX7?p6>|66kd5y`E_xpoDg6Ky zZ~VxIoxTHLV5dW$zsUNjgPpKnQGcw!*d-eI0&+<=*!UIL--CjOz6D2nLI3YT!%;Bg zIB5L=bohS6j{78-`ZJjG3z&ZzDl7gKEI$KQ|Bm>&Kf%Vo5Z?Ab$en+KJ^vzn;GAX5 zk+I7-+;1FYpTQqHmI3f~}Yj}rxi^0IVLHEPUC}pgE@DDb<1P;Cd zS~|d-L(Ax5#p+|r=n)-1w2U6r`Tt$U%Z3AjW0~D^!J1ewFGW-JKkMbO{B2n4t+5oR z#&zR^u{3eKe$XGwPqV!ZVBSlyJn|LpjpYHS^5t0em4-&hov+05IN@rFEWcVZ`bI1*)U$N;@5J)6-NCk4ev;MxE(-2@4+T?uEWelF{Q#{0 z5b^CF#Zs!aqR!Is|sc^1W})r?LD6j?sg$e8pVb70V-{_sdxRz(wEJvEZ*N(TI|pg5#)NS9l88JuQxgRe0T;I3LZ{_oWNs_?>inR2+@!Tf^8m z9x_YZaa66?n-WJ(#m>w)`c%c!WpNa!=(+;wZP&!{s~v*{as0|hYhfG@we}n1_?e>P zmN;%m_^oj?`5e9eCyq*#sSB!nacrxiN8ma<~<)rA1hYuiK7n1hL_^_&MxrfIR09$yD^S(b<1CgGR;^>58TW=gK z(PRG)ar|m^!KpZUT(M^)j^{P1|B7QDYB?Ln|0S^e9mn0+@oyZjQujH}aq`tk(|9MP zC=LcVc@8Qk$ccaA27{vpC%4Ep#YrFNmQ8cACdy|xdD;KSOeeQ2Fa+t`bDVtOyig}) zstUC&bn-LCDyx%UBM4c<^ie~klb+Yk6z!xVx<$*Ke4)`F@1(Oz?o4pfe|7viCmm9( z@jCgv*trp`y~N2E9^M=$_af^iCqD=FzZ7!crAXIwnUkG8Cs(IeIuG281Ovjh z%bk1;U2p|5xbi^57Q_#3f!ubbwCE}@KOb~n4F+xn`-LsnfE5K!UOiKMt&?K4&2#_H z$uF#Vu0sn(g^h(^-t|r%NK7|?-NK3+oxC=rsR$#N=SQ@Ym4I12r z@@j8|W=j6!B%j{NDnSCj+mNA0*svWfF7rXoDg~{#gLDVjEv&y2EGYw1?*c7%qs4(c zz|kFOaDTbe$2F?H2Q^E+7o_{p!WKpS4WP0LCx4aOd%u%Mys8JB+|5QFgzR_-8Yth1 z3g)Op z1{|>UCA2tyFUkpd87&mHf;w@Cj{Wdr%Y_Wtlu;X*E_6xB1OE9$? z3_paH8omPQYqWUaYq4#QnD!en?YCgZw`g$HcdEg<|L66hg>{F~V*l?&1AS<5%~2e% z=onfYavTNq97ju=`oYQ{&|=pK(a?|5AYsRVH0Y!>=qJ_xxkW!qiv~gZ1?&+vo&w8H zqoqYdVD7JA@^7e+-x;t~STyY9D<9kMFfIK7cKv|{29BuyuUlO7my@qxTF#=y0i!rz z|0r5q`8Nvm{DYQS{sl?h9q1M}DslzS0dvQIjJVCTf;Y~!YY-nJZK^}988`MIu@WpL&ExnV6JsJ`+z9|niv$eE@BP%XfzTk z$z8mheV{H18W~xF19sWL`lV7}G-!-L_)rWqQsY3lcNsKciv~Nzh2c+U4l~B^N;@ z$;ohvignP)Pzp3+PlZOx*NYFNfsS-3P+0Fpc0IK>t<2$<mL!Xe^k7F7udTCLu+F-NV$&@&iXt##1IXdN`-d=5TR`#j{ndT7MH zN1XLVan=`6PECWRUZwYvv}`X_(z6!{Dqn^s3K~JrE6~WuD@fnG}3wu8liq4RO05PYr=FMIHIUEQa=IdODBR^0UYlm`y>PeoDcR3TQ86U2Z99`g6<&D6bue4>Y=sY z5YL+Enhds1L4}H@f>tBguc$RrJ1t&m!lzee#j{FWGvZk#rKWfuS_fuABi7l_NNI@F zd=6*}ML~n1D7elX&rd`QmUy0i%MFXCw-mkM@%)jD(gpGSos*%3@vL!gL_BTM{l8;T zJb$vmX^W?7J;M1PpvevPDDGEmOpND`Yr2x-dG4qr1#C$Lhttr& z_Vjp~rP4XG5MI17o_x9{y_dw(PDRV5U_ov?Kg$W&9M98cqgN=6j8P|(YvcLjo5O|i z{2-#fD4xGBShZahq*z%V&l8KL`@#B$;%Uw~`kWC@=P9P{R^{ud+IncP@P&9EKP2+* zfeHg&gwqTN+Z*EfoY3%6Jf>Lp#?usaAWJjisRit9L4i%LgB5Rpd2gazQ!CgltauA_ zzwN`$=-Xh^J77T@Xn7ax6;{0`z2JT61?^y~u;>GEwhzVGgf$<5-VSN#0kGXCJ0%~3 z_D{e;VO=Mf^C@g@JP39x>iNB@&p>ZiJTEO7`XZj6k`;HO7vvoRQ@?@_gnSJSDZb#R z`d`&g@w8dbdeaJ;q5=v7SI|vLcF$cwL5dZzE9jl`RR7+*0t3+HE7)Z2D^@^rihM4} z1Dm$2V3XBcxdM;vu3Et+GZZ3zNZ5Hjm*=Cp8&Gh`ji9#(1qa*&whK#c2JN?igTlIE zFlQTRxE1Uami-5GmVm>;hTAk%|I6Es0Fw{w7FLvk?%SoM!lpaGf;&M=8Q3eVx(iIc zdj*Ex9bmg6FFh*<-S@1Z=XL+@yKe>CEdTx$Y%A{rpzFaEY^%UZuuoCjtn8T;Y%>4X zVY1u(n5^UsOjbPIg_Fz-7e0(-azS&7+5{alU6}u?o8`h>&1@IjtRcjOhxc=k z&=Lxg83pzT8!cdY7z%dH1xJL9^T7OYFl0X1BdlED!u7vrAp*z>wg?L&!0<(2pRhU- zOtpdji@`QwaTI7<0uBgk?O@hYFfiJOosMX*G{%J+5eGP;sBP7<3@nayVFlN67n`gm z-o>UWUjY`mTx=@$O3<*%#U^X<$}8>_UpNegA3?dkKG~`M zUR2sADm^MH6&4>8l^z$B3TyjCr9X&DPl!f^r9Xm>0dPoIf0F5=+@BC&{8?HmEFT12 zzknmc##3PaX)t66rs@?|{|ZxO{RSG(z+_Fo!(`4sVXE*EP1XMlf5BG$!ltvZS=OYL zY_s0bmE6tjOIC6>^G{mICQIG4lDk=Q*-BQa<*t=%GXJ|*LUW4R1T{Or;_{VjvfO)C z@&k^tdsVsmwAs5830fWotE#}lN5JGq!SG!uxKCJJ4W>Q@`tOzl3yU8IZ8hM4u=WWs z>&cbmW1IbVC9AGeSY8XdpF+Y>VbjwHFMI}ac%4+J4&gP=f?3ZYJn(rbS6E&z<-P#Y zo|Qh{Y2CAuZB_Cj=xkWYHtX5Dl5LjTxRS5&QeRogwsXF^67vN6z+OddveFM#dTpX! zm@Ib?CbN%Og^_W}DvXTFSK&>rcprA!;#bk^ajM|VRrID}_zkP5dV;EP4dkNcRkTsD zw`&#Mr|ADPXg_x~-K&^0do>+X?2lbdlg2Bj%UsRz?(0|6uR8txknPW}rvE91yuX^x zC=U9LAj0^UWC(WCd8&Z?NHhQ?izH{RQ)jf z+%?SdnPC4?(3Jw#T)BpfioVh9*vZ+ohCl1rr8q;YxOxrUs8r~`XAS+NYkoJJM}_>umpN|jMh*B zKkcfrCGex!!l(qYsEW`<3G|p^-j)QiDO$ECuxV=_O`thiemQ}^Qh93GTfwrjhWuGU|vr0DhB+xEZ(V`Ox zJOp>1N}!{vA*o{$X@`C!8<0q=)q#t{5^23k-?|`?AJOW%-q@U-n)sz*LD9xUoHs5> zq-iRy{)$9yTz6g~Jw^J>>_j@O*tvB_#+Jn9j4hts6MSXYCGwZYyw`)48x#44CBG<< zU&$@JIguBq)D8)N?@Q#j33^^jq-*pGR%LG{^3sd8jzr2-G<}uGZ_svsorn(|ev`F-f#Sxc8iR!3cR}!7k_ID@o|3T_KN&J0D z)4C*H&tXVS;&mV8Y2c_giLaijHze^2Lt6&ZM;#f6$jd~;Xr?60O5)osM|Kh~iLTt3 z#INC|UY100%1fNZN&Mw)&+SRP(6IBNB-)}!w`Y>5OR2r~)g(GFR<9dLqHo9O#Y;(i z!%7R|*Z_8JK)U=4&@U6|Y83TP zE=o2f^FJwuFHfd?W!I{rWU3pZm%Aj>&8mNnHYC$ZZQuRLaE#*SWSo#&lKDFuz27AB zw_lTwB+~(9x5D3($v0N7ELul%75xI&kySf@VI3bhdGb0w`}9v;N5880`g!YkVNiAC zIv%=mqSn!=vHE&^9iIfMH?E@-fyyLLuA}qKs)nt5*HLbO(nMc##*CEs^}e#O6uh4> zH--O$-8wIY7tVCePvOOvrPdUBOf{iDI)zvNJC>*L--5bUr_dexERvK$-6~!9x)cgk z2WZ@sLd#Y9x+_!o9}3+CDYQfn%Gamx>86kb=Ox{v-I=#JoPQ`B~`+ESZ?uU$Xw zjL&vU3Vo+?)ND_orwvM(pQrFSp}ISTZqmc`kre7WM=!lj;iW@OKc(Oi!C(q65gHgy z;fts4-&1Jk8WkRpiZAIXYTf5fN@Zh?D(VF?b>}18a{*Ji=>^D85r~B07eek3<_94| zKrrM6VX^_?L&B=b$ZwkhxqAu@STYsqO-9J=Mx@J~mWr=-&~yaU2puz!p=So#2 zW@LeYR#8X)vWq~ddL!x2bOwFm_|BEeo^ zsSWWVi@`QwZWKsMz*?cpjusCHE0^Mc)@a0cMx%jwF{$|6lfOe$=zu1i%R~dhf>^`{ z#G$~ZxKtTS!C@!TRV)WB@d$5^M+5R#K=yZ`B6UL7N*@yRuS7uUD#(`AQh+ee4f?GS zRj-kjCP@AS$)6~i@`$E9sBnIgIPqG9Hwcq`7l{{NB+ily*}e|!S%(5jQ>0=SgB=$m zyf7694p=XmS&#UvG?X`z2Dv63ba|!1LSOj?Bn;0$LG2l$vP@A~mY7E9$ws>VY@{pS z2-$LpXiS)wgK*j;y-Vo06ej8deUyJ0BK&d@Q6sc(20Mj$mxH6isw+Ti9@s9-*#Zs= zE3OouxC(3)dh_*hRsS2xM?m@2V8~WfsCBC(yaw`+u%bW)s%sJ7Cd~Rjgb)9p9QZnD z!di&%jzWazUJs6F>i%DO0|LTtlmdlWMc|OI{3fa3&0vc#^%fjp@D|8r#h_`M^mn26 zR+wx=So0s%|Jf!bNYGt^h~nEo({`|JJK}SEXwj$-a&;+aza8wl9r1;Ch*RE)iqzdH z-K`AqeZtbaQt`RRkh?|YcOxQa2jmf9RXM`#_ki8PqI+?GfcucH{yrH$DiGf*EV&;v zJs=u+Ks5KD4?6=7f~A$9@gcDBA!JD2i2??9LN0$;yuJ!-t3rJ4BOpBr)(Ty_q~*fW zYB`SYF%-}wOx-ON+6}qvaWJGtG$hP=LY(ahakeMLDgO($3v+A1QDOB{VzQ?}Uzh9@ zJOldIfpvALsry;TeZrFGM3v8rDuv#9a7bA3f>daaR7jZnqEraJ?m{wT&j`V+Hn>d@$^DfvYEPf9Rd>^bA zy4t}WVc`d&u@6OKLdQp7moUErqywq=+;jB-1lT?XJA}EPfFr`nPB8pauuYhC5F8Sg ze+Gthfi1$+&qV{m(l1i+CZzF8(SXp?EgBFO9}*3GB^nUAz7`D#3wuNZ--rf;j&DT+ z!u;<<1HID!t9wNQheZR2VY~bzV)O4Y5;lAfIk^uu9_WKyeiRHp26h}neBN=CH+md$ zbw6nT0pXoK*~vSB2>KDM5jqB>=ED4wQuCjr;zHZcQgLDKAUGnd`~?g@CEZcz%RMa@ zkwd6?ozVR&*e@*m4e7$qfSqR$UN8&>{Eh1#Fvw@SLgZ zasD5fiVW38&@m0{5f)DejWfU&VU`I6jtXmMuID?VP!%0mPh-zlP8pKM zFGCqa)9C0V)qS(m$f2h!E=}WaI@m8y<9}Bgu1urb6#etl_!Y$o&G%oIwqp6J{%vXe zR%hXDX?%CxvptP^w8rj8<2lOY9clF1ST&+Pnnrypy!Np){uD>x6KOoXZP?p<{!3}E zCU4AXPUG34n%C3Fs4|RxkVfw+nGU4!FK`DwN#hR)HGZDP|6(owE=~0mRq-Qf{K}E* zC=O&8N+XYoxBrz!5i0$_-#ezCO;cOC+Puxv&u)l5$5-f=&TrlJC~B=0oSV*1Xe{H> zd4{#lKb^`{Ax%N)JYP~gIh|h}GfqwCncK2ykS#OPsY@|$Ryt2HR)(b0PkQzvJe^(5C^B*7kv(xEw z#qiDP{7H?`E7I|I)2r11^>oQ~>HOZ4YqNf<2Pv@Yo=sA>5u_~kONIFlx4joIU&-7&K zsdRFW(T@$&>9DTwI4_-4^iJ`TbDSD|BfXs7&+es(s(hQ*SH_*jn^jzEqx=hblS#vk=uZ^p> zY@qK|k1#y6fxB3X;sc694{zYVehxmmfnM^{ld~IWvMONsl?~K1M)#x*)TQXxv4OUo zt6F$?1D$)GGSN91%`g7F;gS2V9vPp(KR51}l)+yOX$i_;SFW9$K_^v-?)e$?%UJzX zJ%g^$s#ujl&nVRd-j>0y0ao0Vf${oouv=KXBLf!|T&&k_rGw3VbiC)a$m&ywFHK)9qaWG>^ZEFU9AJzYz z44zPIc|U_5(~mN~$e<_vm3D_S_@U0=Xa+4%tU5Qd`Qr03e}6E$IyjTNhToJ-x=!V6 zn~}-(@Sl~*B^HKc(syI^)J!J*t>U|4GWow)rE!_`nv%V%GO0CKDdnL|wzF$@CeL|a zz>RC}cr4SjJGSqcOgf^C|9mFDW!LdSCY{hz|8Hf|kIDw4-I+8-+vIR2jaLl$A(PHE zsKH?Aj#>7s=2`aa=yS7+;oyI#3AJF>ZVS$6A^$%Cu2;m)3H zx>$Kd$Fihc>D0(&qDrF574t<2>8EH6Zsy=Xv#0 za%tfbqVslLACMc|T<}e5T%J#^`Z1R_s|p%_&!rq?(eiPd zckTNpccrgo(pU;q3EEo5lBySZrcA)^?Aj*k|ASNCe*^f@VdtIz(vLW-Z%*Q&x9#L4 zPTzh_AYGuCbL>J+XS_Rz<|tN9oy>0q_S+_tIv!cPlR3Wi9wSXAy%>K68TC+|mp_xA z1lz2kT=RywP|_Oi*b3&n5z4dFj=5(3dTc?I85Oz0OtTeB?=^Ep-7kdkxuo@jFq)(* za4?JyT-`g5cIYAgaw|8i_3;QQ*X0jHkyj7Z-h1s7q5}N#mSUx+JsJfhMw9Xl>P?B} znmhJH>l&*I*=RmhcU>972X5$!A!SJlUz$kI=^^>LL{2}v&BKqs+>T^?_S&4ntiCyg zHD=qIMuYl=?AC4i$+iAYP8um!ruMPv6rkumH-kU0;8vrJu26^?JhUc4)KH-5QN2}H zU|@L`S0GFE2`$$suh$y#D(BVdyvhf4e5rCNtr7pTo7i*(%7H?(ioM5kS=AN(o4Mv4 MiXO$4TMIV-KT2$A;s5{u diff --git a/newlib/compiler/optimize/defs.ajla b/newlib/compiler/optimize/defs.ajla index d1e7d11..569b606 100644 --- a/newlib/compiler/optimize/defs.ajla +++ b/newlib/compiler/optimize/defs.ajla @@ -54,6 +54,8 @@ record basic_block [ uninitialized : var_set; live_top : var_set; live_bottom : var_set; + + verifier_name : bytes; ] fn new_basic_block : basic_block @@ -73,6 +75,8 @@ fn new_basic_block : basic_block uninitialized : -1, live_top : -1, live_bottom : -1, + + verifier_name : "", ]; ] @@ -99,6 +103,7 @@ record variable [ always_flat_option : bool; verifier_name : bytes; + verifier_valid : bytes; ] fn new_variable : variable @@ -120,6 +125,7 @@ fn new_variable : variable is_option_type : false, always_flat_option : false, verifier_name : "", + verifier_valid : "", ]; ] diff --git a/stdlib/compiler/optimize/verify.ajla b/newlib/compiler/optimize/verify.ajla similarity index 61% copy from stdlib/compiler/optimize/verify.ajla copy to newlib/compiler/optimize/verify.ajla index 0f1d103..556d34c 100644 --- a/stdlib/compiler/optimize/verify.ajla +++ b/newlib/compiler/optimize/verify.ajla @@ -25,17 +25,28 @@ fn verify_function(ctx : context) : unit_type; implementation uses exception; +uses charset; uses z3; uses compiler.common.blob; -fn allocate_variable(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx : context, v : int) : (z3_world, context, bytes); +fn allocate_variable(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx : context, v : int) : (z3_world, context, bytes, bytes); -fn get_z3_name(ctx : context, v : int) : bytes +fn get_z3_name(ctx : context, v : int) : (bytes, bytes) [ - var n := "var_" + ntos_base(v, 16); - if len_greater_than(ctx.variables[v].name, 0) then + var n := "var_" + map(ntos_base(v, 16), ascii_locase); + var m := "valid_" + map(ntos_base(v, 16), ascii_locase); + if len_greater_than(ctx.variables[v].name, 0) then [ n += "_" + ctx.variables[v].name; - return n; + m += "_" + ctx.variables[v].name; + ] + return n, m; +] + +fn get_z3_bb_name(ctx : context, bgi : int) : (context, bytes) +[ + var str := "bb_" + map(ntos_base(bgi, 16), ascii_locase); + ctx.blocks[bgi].verifier_name := str; + return ctx, str; ] fn get_z3_type(ctx : context, v : int) : bytes @@ -49,6 +60,15 @@ fn get_z3_type(ctx : context, v : int) : bytes return ""; ] +fn gen_assert(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx : context, v : int, deps : list(bytes), ops : bytes) : z3_world +[ + var str := "(assert (= " + ctx.variables[v].verifier_valid + " (and"; + for i := 0 to len(deps) do + str += " " + deps[i]; + str += " (= " + ctx.variables[v].verifier_name + " " + ops + "))))"; + z3_eval_smtlib2_string_noret(str); +] + fn assert_instruction(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx : context, v : int) : (z3_world, context) [ var ins := ctx.instrs[ctx.variables[v].defining_instr]; @@ -76,19 +96,22 @@ fn assert_instruction(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx else if op = Bin_GreaterEqual, is_int or is_real then op_z3 := ">="; else if op = Bin_LessEqual, is_bool then op_z3 := "=>"; else return ctx; - var var1 var2 : bytes; + var var1 var1v var2 var2v : bytes; //eval debug("P_BinaryOp: " + ntos(ins.params[0]) + ", " + ntos(ins.params[1]) + ", " + ntos(ins.params[2]) + ", " + ntos(ins.params[3]) + ", " + ntos(ins.params[4]) + ", " + ntos(ins.params[5])); - ctx, var1 := allocate_variable(ctx, ins.params[3]); + ctx, var1, var1v := allocate_variable(ctx, ins.params[3]); + if len(var1) = 0 then + return ctx; if ins.opcode = P_BinaryOp then [ - ctx, var2 := allocate_variable(ctx, ins.params[5]); + ctx, var2, var2v := allocate_variable(ctx, ins.params[5]); + if len(var2) = 0 then + return ctx; + gen_assert(ctx, v, [var1v, var2v], "(" + op_z3 + " " + var1 + " " + var2 + ")"); ] else [ if is_bool then var2 := select(ins.params[4] <> 0, "false", "true"); else var2 := ntos(ins.params[4]); - ] - if len_greater_than(var1, 0), len_greater_than(var2, 0) then [ - z3_eval_smtlib2_string_noret("(assert (= " + ctx.variables[v].verifier_name + " (" + op_z3 + " " + var1 + " " + var2 + ")))"); + gen_assert(ctx, v, [var1v], "(" + op_z3 + " " + var1 + " " + var2 + ")"); ] return ctx; ] @@ -102,18 +125,19 @@ fn assert_instruction(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx if op = Un_Not, is_bool then op_z3 := "not"; else if op = Un_Neg, is_int or is_real then op_z3 := "-"; else return ctx; - var var1 : bytes; - ctx, var1 := allocate_variable(ctx, ins.params[3]); - if len_greater_than(var1, 0) then [ - z3_eval_smtlib2_string_noret("(assert (= " + ctx.variables[v].verifier_name + " (" + op_z3 + " " + var1 + ")))"); - ] + var var1 var1v : bytes; + ctx, var1, var1v := allocate_variable(ctx, ins.params[3]); + if len(var1) = 0 then + return ctx; + gen_assert(ctx, v, [var1v], "(" + op_z3 + " " + var1 + ")"); return ctx; ] if ins.opcode = P_Copy then [ - var new_var : bytes; - ctx, new_var := allocate_variable(ctx, ins.params[2]); - if len_greater_than(new_var, 0) then - z3_eval_smtlib2_string_noret("(assert (= " + ctx.variables[v].verifier_name + " " + new_var + "))"); + var var1 var1v : bytes; + ctx, var1, var1v := allocate_variable(ctx, ins.params[2]); + if len(var1) = 0 then + return ctx; + gen_assert(ctx, v, [var1v], var1); return ctx; ] if ins.opcode = P_Load_Const then [ @@ -126,7 +150,7 @@ fn assert_instruction(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx cnst := ntos(l); else return ctx; - z3_eval_smtlib2_string_noret("(assert (= " + ctx.variables[v].verifier_name + " " + cnst + "))"); + gen_assert(ctx, v, empty(bytes), cnst); return ctx; ] if ins.opcode = P_Return_Vars then [ @@ -139,90 +163,35 @@ fn assert_instruction(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx ] abort internal("P_Return_Vars parameter not found"); found_new_v: - var new_var : bytes; - ctx, new_var := allocate_variable(ctx, new_v); - if len_greater_than(new_var, 0) then - z3_eval_smtlib2_string_noret("(assert (= " + ctx.variables[v].verifier_name + " " + new_var + "))"); + var var1 var1v : bytes; + ctx, var1, var1v := allocate_variable(ctx, new_v); + if len(var1) = 0 then + return ctx; + gen_assert(ctx, v, [var1v], var1); return ctx; ] //eval debug("opcode: " + ntos(ins.opcode) + " (" + ctx.variables[v].verifier_name + ")"); return ctx; ] -fn allocate_variable(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx : context, v : int) : (z3_world, context, bytes) +fn allocate_variable(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx : context, v : int) : (z3_world, context, bytes, bytes) [ if not len_greater_than(ctx.variables[v].verifier_name, 0) then [ var t := get_z3_type(ctx, v); if not len_greater_than(t, 0) then - return ctx, ""; - var n := get_z3_name(ctx, v); + return ctx, "", ""; + var n, m := get_z3_name(ctx, v); ctx.variables[v].verifier_name := n; + ctx.variables[v].verifier_valid := m; z3_eval_smtlib2_string_noret("(declare-const " + n + " " + t + ")"); + z3_eval_smtlib2_string_noret("(declare-const " + m + " Bool)"); ctx := assert_instruction(ctx, v); ] - return ctx, ctx.variables[v].verifier_name; -] - -fn get_cond_guards(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx : context, bgi : int) : (z3_world, context, bytes) -[ - var dom_set := ctx.blocks[bgi].dom; - var all_preds := ""; - while dom_set <> 0 do [ - var dom : int := bsr dom_set; - dom_set btr= dom; - var bb := ctx.blocks[dom]; - if not bb.active then - abort internal("dominator is not active"); - if len(bb.pred_list) = 0 then - goto next_dom; - var pred_string := ""; - for i := 0 to len(bb.pred_list) do [ - if bb.pred_position[i] = 2 then - goto next_dom; - var bb_pred := ctx.blocks[bb.pred_list[i]]; - if len(bb_pred.instrs) = 0 then - goto next_dom; - var lins := ctx.instrs[bb_pred.instrs[len(bb_pred.instrs) - 1]]; - if lins.opcode <> P_Jmp_False then - goto next_dom; - var vgic := lins.params[0]; - var vgic_name : bytes; - ctx, vgic_name := allocate_variable(ctx, vgic); - if not len_greater_than(vgic_name, 0) then - goto next_dom; - if len_greater_than(pred_string, 0) then [ - pred_string +<= ' '; - ] else [ - pred_string := "(or "; - ] - if bb.pred_position[i] = 0 then [ - pred_string += vgic_name; - ] else [ - pred_string += "(not " + vgic_name + ")"; - ] - ] - if not len_greater_than(pred_string, 0) then - goto next_dom; - pred_string +<= ')'; - //eval debug("pred_string: " + pred_string); - if len_greater_than(all_preds, 0) then [ - all_preds +<= ' '; - ] else [ - all_preds := "(and "; - ] - all_preds += pred_string; -next_dom: - ] - if not len_greater_than(all_preds, 0) then - return ctx, " "; - all_preds +<= ')'; - //eval debug("all_preds: " + all_preds); - return ctx, all_preds; + return ctx, ctx.variables[v].verifier_name, ctx.variables[v].verifier_valid; ] fn verify_function(ctx : context) : unit_type [ - var claims := ""; var b : bytes; implicit var z3w := z3_mk_world; implicit var z3ctx := z3_mk_context(); @@ -236,42 +205,46 @@ fn verify_function(ctx : context) : unit_type var ins := ctx.instrs[igi]; if ins.opcode = P_Return then [ ctx.return_ins := ins; - goto found_ret; ] ] + var str : bytes; + ctx, str := get_z3_bb_name(ctx, bgi); + z3_eval_smtlib2_string_noret("(declare-const " + str + " Bool)"); ] -found_ret: for bgi := 0 to len(ctx.blocks) do [ if not ctx.blocks[bgi].active then continue; - var cond_guards := ""; + var assumes := ""; + var claims := ""; for ili := 0 to len(ctx.blocks[bgi].instrs) do [ var igi := ctx.blocks[bgi].instrs[ili]; var ins := ctx.instrs[igi]; if ins.opcode = P_Assume then [ - //eval debug("assume"); - var str : bytes; - ctx, str := allocate_variable(ctx, ins.params[0]); - if len_greater_than(str, 0) then - z3_eval_smtlib2_string_noret("(assert " + str + ")"); + var var1 var1v : bytes; + ctx, var1, var1v := allocate_variable(ctx, ins.params[0]); + if len_greater_than(var1, 0) then + assumes += " (=> " + var1v + " " + var1 + ")"; ] else if ins.opcode = P_Claim then [ - //eval debug("claim"); - if not len_greater_than(cond_guards, 0) then - ctx, cond_guards := get_cond_guards(ctx, bgi); - var str : bytes; - ctx, str := allocate_variable(ctx, ins.params[0]); - if len_greater_than(str, 0) then [ - if cond_guards[0] <> ' ' then - claims += " (=> " + cond_guards + " " + str + ")"; - else - claims += " " + str; + var var1 var1v : bytes; + ctx, var1, var1v := allocate_variable(ctx, ins.params[0]); + if len_greater_than(var1, 0) then [ + claims += " (=> " + var1v + " " + var1 + ")"; ] ] ] + for i := 0 to len(ctx.blocks[bgi].post_list) do [ + var p := ctx.blocks[bgi].post_list[i]; + claims += " " + ctx.blocks[p].verifier_name; + ] + if len(assumes) = 0 then + assumes := " true"; + if len(claims) = 0 then + claims := " true"; + z3_eval_smtlib2_string_noret("(assert (= " + ctx.blocks[bgi].verifier_name + " (=> (and" + assumes + ") (and" + claims + "))))"); ] - z3_eval_smtlib2_string_noret("(assert (not (and true" + claims + ")))"); + z3_eval_smtlib2_string_noret("(assert (not " + ctx.blocks[0].verifier_name + "))"); b := z3_eval_smtlib2_string("(check-sat)"); if list_begins_with(b, "unsat") then return unit_value; diff --git a/newlib/z3.ajla b/newlib/z3.ajla index 58e31ca..c33d579 100644 --- a/newlib/z3.ajla +++ b/newlib/z3.ajla @@ -69,7 +69,7 @@ fn z3_mk_context(implicit w : z3_world) : (z3_world, z3_context) fn z3_eval_smtlib2_string(implicit w : z3_world, ctx : z3_context, str : bytes) : (z3_world, bytes) [ - //eval debug("Z3: " + str); + //if not is_exception w then eval debug("Z3: " + str); var r e ec es : int; r, e := ffi_call_function(ctx.z3_set_error, [ ctx.ptr_z3_context, 0 ]); var mem_str := ffi_poke_zstring(ctx.destr, str); diff --git a/stdlib/compiler/optimize/defs.ajla b/stdlib/compiler/optimize/defs.ajla index d1e7d11..569b606 100644 --- a/stdlib/compiler/optimize/defs.ajla +++ b/stdlib/compiler/optimize/defs.ajla @@ -54,6 +54,8 @@ record basic_block [ uninitialized : var_set; live_top : var_set; live_bottom : var_set; + + verifier_name : bytes; ] fn new_basic_block : basic_block @@ -73,6 +75,8 @@ fn new_basic_block : basic_block uninitialized : -1, live_top : -1, live_bottom : -1, + + verifier_name : "", ]; ] @@ -99,6 +103,7 @@ record variable [ always_flat_option : bool; verifier_name : bytes; + verifier_valid : bytes; ] fn new_variable : variable @@ -120,6 +125,7 @@ fn new_variable : variable is_option_type : false, always_flat_option : false, verifier_name : "", + verifier_valid : "", ]; ] diff --git a/stdlib/compiler/optimize/verify.ajla b/stdlib/compiler/optimize/verify.ajla index 0f1d103..556d34c 100644 --- a/stdlib/compiler/optimize/verify.ajla +++ b/stdlib/compiler/optimize/verify.ajla @@ -25,17 +25,28 @@ fn verify_function(ctx : context) : unit_type; implementation uses exception; +uses charset; uses z3; uses compiler.common.blob; -fn allocate_variable(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx : context, v : int) : (z3_world, context, bytes); +fn allocate_variable(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx : context, v : int) : (z3_world, context, bytes, bytes); -fn get_z3_name(ctx : context, v : int) : bytes +fn get_z3_name(ctx : context, v : int) : (bytes, bytes) [ - var n := "var_" + ntos_base(v, 16); - if len_greater_than(ctx.variables[v].name, 0) then + var n := "var_" + map(ntos_base(v, 16), ascii_locase); + var m := "valid_" + map(ntos_base(v, 16), ascii_locase); + if len_greater_than(ctx.variables[v].name, 0) then [ n += "_" + ctx.variables[v].name; - return n; + m += "_" + ctx.variables[v].name; + ] + return n, m; +] + +fn get_z3_bb_name(ctx : context, bgi : int) : (context, bytes) +[ + var str := "bb_" + map(ntos_base(bgi, 16), ascii_locase); + ctx.blocks[bgi].verifier_name := str; + return ctx, str; ] fn get_z3_type(ctx : context, v : int) : bytes @@ -49,6 +60,15 @@ fn get_z3_type(ctx : context, v : int) : bytes return ""; ] +fn gen_assert(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx : context, v : int, deps : list(bytes), ops : bytes) : z3_world +[ + var str := "(assert (= " + ctx.variables[v].verifier_valid + " (and"; + for i := 0 to len(deps) do + str += " " + deps[i]; + str += " (= " + ctx.variables[v].verifier_name + " " + ops + "))))"; + z3_eval_smtlib2_string_noret(str); +] + fn assert_instruction(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx : context, v : int) : (z3_world, context) [ var ins := ctx.instrs[ctx.variables[v].defining_instr]; @@ -76,19 +96,22 @@ fn assert_instruction(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx else if op = Bin_GreaterEqual, is_int or is_real then op_z3 := ">="; else if op = Bin_LessEqual, is_bool then op_z3 := "=>"; else return ctx; - var var1 var2 : bytes; + var var1 var1v var2 var2v : bytes; //eval debug("P_BinaryOp: " + ntos(ins.params[0]) + ", " + ntos(ins.params[1]) + ", " + ntos(ins.params[2]) + ", " + ntos(ins.params[3]) + ", " + ntos(ins.params[4]) + ", " + ntos(ins.params[5])); - ctx, var1 := allocate_variable(ctx, ins.params[3]); + ctx, var1, var1v := allocate_variable(ctx, ins.params[3]); + if len(var1) = 0 then + return ctx; if ins.opcode = P_BinaryOp then [ - ctx, var2 := allocate_variable(ctx, ins.params[5]); + ctx, var2, var2v := allocate_variable(ctx, ins.params[5]); + if len(var2) = 0 then + return ctx; + gen_assert(ctx, v, [var1v, var2v], "(" + op_z3 + " " + var1 + " " + var2 + ")"); ] else [ if is_bool then var2 := select(ins.params[4] <> 0, "false", "true"); else var2 := ntos(ins.params[4]); - ] - if len_greater_than(var1, 0), len_greater_than(var2, 0) then [ - z3_eval_smtlib2_string_noret("(assert (= " + ctx.variables[v].verifier_name + " (" + op_z3 + " " + var1 + " " + var2 + ")))"); + gen_assert(ctx, v, [var1v], "(" + op_z3 + " " + var1 + " " + var2 + ")"); ] return ctx; ] @@ -102,18 +125,19 @@ fn assert_instruction(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx if op = Un_Not, is_bool then op_z3 := "not"; else if op = Un_Neg, is_int or is_real then op_z3 := "-"; else return ctx; - var var1 : bytes; - ctx, var1 := allocate_variable(ctx, ins.params[3]); - if len_greater_than(var1, 0) then [ - z3_eval_smtlib2_string_noret("(assert (= " + ctx.variables[v].verifier_name + " (" + op_z3 + " " + var1 + ")))"); - ] + var var1 var1v : bytes; + ctx, var1, var1v := allocate_variable(ctx, ins.params[3]); + if len(var1) = 0 then + return ctx; + gen_assert(ctx, v, [var1v], "(" + op_z3 + " " + var1 + ")"); return ctx; ] if ins.opcode = P_Copy then [ - var new_var : bytes; - ctx, new_var := allocate_variable(ctx, ins.params[2]); - if len_greater_than(new_var, 0) then - z3_eval_smtlib2_string_noret("(assert (= " + ctx.variables[v].verifier_name + " " + new_var + "))"); + var var1 var1v : bytes; + ctx, var1, var1v := allocate_variable(ctx, ins.params[2]); + if len(var1) = 0 then + return ctx; + gen_assert(ctx, v, [var1v], var1); return ctx; ] if ins.opcode = P_Load_Const then [ @@ -126,7 +150,7 @@ fn assert_instruction(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx cnst := ntos(l); else return ctx; - z3_eval_smtlib2_string_noret("(assert (= " + ctx.variables[v].verifier_name + " " + cnst + "))"); + gen_assert(ctx, v, empty(bytes), cnst); return ctx; ] if ins.opcode = P_Return_Vars then [ @@ -139,90 +163,35 @@ fn assert_instruction(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx ] abort internal("P_Return_Vars parameter not found"); found_new_v: - var new_var : bytes; - ctx, new_var := allocate_variable(ctx, new_v); - if len_greater_than(new_var, 0) then - z3_eval_smtlib2_string_noret("(assert (= " + ctx.variables[v].verifier_name + " " + new_var + "))"); + var var1 var1v : bytes; + ctx, var1, var1v := allocate_variable(ctx, new_v); + if len(var1) = 0 then + return ctx; + gen_assert(ctx, v, [var1v], var1); return ctx; ] //eval debug("opcode: " + ntos(ins.opcode) + " (" + ctx.variables[v].verifier_name + ")"); return ctx; ] -fn allocate_variable(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx : context, v : int) : (z3_world, context, bytes) +fn allocate_variable(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx : context, v : int) : (z3_world, context, bytes, bytes) [ if not len_greater_than(ctx.variables[v].verifier_name, 0) then [ var t := get_z3_type(ctx, v); if not len_greater_than(t, 0) then - return ctx, ""; - var n := get_z3_name(ctx, v); + return ctx, "", ""; + var n, m := get_z3_name(ctx, v); ctx.variables[v].verifier_name := n; + ctx.variables[v].verifier_valid := m; z3_eval_smtlib2_string_noret("(declare-const " + n + " " + t + ")"); + z3_eval_smtlib2_string_noret("(declare-const " + m + " Bool)"); ctx := assert_instruction(ctx, v); ] - return ctx, ctx.variables[v].verifier_name; -] - -fn get_cond_guards(implicit z3w : z3_world, implicit z3ctx : z3_context, ctx : context, bgi : int) : (z3_world, context, bytes) -[ - var dom_set := ctx.blocks[bgi].dom; - var all_preds := ""; - while dom_set <> 0 do [ - var dom : int := bsr dom_set; - dom_set btr= dom; - var bb := ctx.blocks[dom]; - if not bb.active then - abort internal("dominator is not active"); - if len(bb.pred_list) = 0 then - goto next_dom; - var pred_string := ""; - for i := 0 to len(bb.pred_list) do [ - if bb.pred_position[i] = 2 then - goto next_dom; - var bb_pred := ctx.blocks[bb.pred_list[i]]; - if len(bb_pred.instrs) = 0 then - goto next_dom; - var lins := ctx.instrs[bb_pred.instrs[len(bb_pred.instrs) - 1]]; - if lins.opcode <> P_Jmp_False then - goto next_dom; - var vgic := lins.params[0]; - var vgic_name : bytes; - ctx, vgic_name := allocate_variable(ctx, vgic); - if not len_greater_than(vgic_name, 0) then - goto next_dom; - if len_greater_than(pred_string, 0) then [ - pred_string +<= ' '; - ] else [ - pred_string := "(or "; - ] - if bb.pred_position[i] = 0 then [ - pred_string += vgic_name; - ] else [ - pred_string += "(not " + vgic_name + ")"; - ] - ] - if not len_greater_than(pred_string, 0) then - goto next_dom; - pred_string +<= ')'; - //eval debug("pred_string: " + pred_string); - if len_greater_than(all_preds, 0) then [ - all_preds +<= ' '; - ] else [ - all_preds := "(and "; - ] - all_preds += pred_string; -next_dom: - ] - if not len_greater_than(all_preds, 0) then - return ctx, " "; - all_preds +<= ')'; - //eval debug("all_preds: " + all_preds); - return ctx, all_preds; + return ctx, ctx.variables[v].verifier_name, ctx.variables[v].verifier_valid; ] fn verify_function(ctx : context) : unit_type [ - var claims := ""; var b : bytes; implicit var z3w := z3_mk_world; implicit var z3ctx := z3_mk_context(); @@ -236,42 +205,46 @@ fn verify_function(ctx : context) : unit_type var ins := ctx.instrs[igi]; if ins.opcode = P_Return then [ ctx.return_ins := ins; - goto found_ret; ] ] + var str : bytes; + ctx, str := get_z3_bb_name(ctx, bgi); + z3_eval_smtlib2_string_noret("(declare-const " + str + " Bool)"); ] -found_ret: for bgi := 0 to len(ctx.blocks) do [ if not ctx.blocks[bgi].active then continue; - var cond_guards := ""; + var assumes := ""; + var claims := ""; for ili := 0 to len(ctx.blocks[bgi].instrs) do [ var igi := ctx.blocks[bgi].instrs[ili]; var ins := ctx.instrs[igi]; if ins.opcode = P_Assume then [ - //eval debug("assume"); - var str : bytes; - ctx, str := allocate_variable(ctx, ins.params[0]); - if len_greater_than(str, 0) then - z3_eval_smtlib2_string_noret("(assert " + str + ")"); + var var1 var1v : bytes; + ctx, var1, var1v := allocate_variable(ctx, ins.params[0]); + if len_greater_than(var1, 0) then + assumes += " (=> " + var1v + " " + var1 + ")"; ] else if ins.opcode = P_Claim then [ - //eval debug("claim"); - if not len_greater_than(cond_guards, 0) then - ctx, cond_guards := get_cond_guards(ctx, bgi); - var str : bytes; - ctx, str := allocate_variable(ctx, ins.params[0]); - if len_greater_than(str, 0) then [ - if cond_guards[0] <> ' ' then - claims += " (=> " + cond_guards + " " + str + ")"; - else - claims += " " + str; + var var1 var1v : bytes; + ctx, var1, var1v := allocate_variable(ctx, ins.params[0]); + if len_greater_than(var1, 0) then [ + claims += " (=> " + var1v + " " + var1 + ")"; ] ] ] + for i := 0 to len(ctx.blocks[bgi].post_list) do [ + var p := ctx.blocks[bgi].post_list[i]; + claims += " " + ctx.blocks[p].verifier_name; + ] + if len(assumes) = 0 then + assumes := " true"; + if len(claims) = 0 then + claims := " true"; + z3_eval_smtlib2_string_noret("(assert (= " + ctx.blocks[bgi].verifier_name + " (=> (and" + assumes + ") (and" + claims + "))))"); ] - z3_eval_smtlib2_string_noret("(assert (not (and true" + claims + ")))"); + z3_eval_smtlib2_string_noret("(assert (not " + ctx.blocks[0].verifier_name + "))"); b := z3_eval_smtlib2_string("(check-sat)"); if list_begins_with(b, "unsat") then return unit_value; diff --git a/stdlib/z3.ajla b/stdlib/z3.ajla index 58e31ca..c33d579 100644 --- a/stdlib/z3.ajla +++ b/stdlib/z3.ajla @@ -69,7 +69,7 @@ fn z3_mk_context(implicit w : z3_world) : (z3_world, z3_context) fn z3_eval_smtlib2_string(implicit w : z3_world, ctx : z3_context, str : bytes) : (z3_world, bytes) [ - //eval debug("Z3: " + str); + //if not is_exception w then eval debug("Z3: " + str); var r e ec es : int; r, e := ffi_call_function(ctx.z3_set_error, [ ctx.ptr_z3_context, 0 ]); var mem_str := ffi_poke_zstring(ctx.destr, str); -- 2.11.4.GIT