From 90a85d91194fd1c8b6b5dba5b6c567999525a1f6 Mon Sep 17 00:00:00 2001 From: YuhangQ Date: Thu, 17 Aug 2023 13:03:08 +0000 Subject: [PATCH] =?UTF-8?q?v1.6:=20=E7=BB=93=E5=90=88SAT-ATPG=EF=BC=8C?= =?UTF-8?q?=E8=A6=86=E7=9B=96=E7=8E=87=E6=8B=89=E6=BB=A1?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .vscode/settings.json | 6 +- Atalanta | 1 + CMakeLists.txt | 22 +- atpg | Bin 187480 -> 0 bytes b01.test | 26 + b01.txt | 1128 +++++++++++++++++++++++++++++++++++++++++ crun | 8 +- src/CMakeLists.txt | 18 + src/checker.cpp | 2 + src/circuit.cpp | 4 +- src/circuit.h | 8 +- src/fault.h | 6 +- src/gate.cpp | 2 + src/gate.h | 6 +- src/ls.cpp | 77 ++- src/lut.cpp | 2 + src/lut.h | 8 +- src/main.cpp | 7 +- src/parse.cpp | 2 + src/sat_atpg.cpp | 106 ++++ src/sat_atpg.h | 6 + src/score.cpp | 2 + src/simulator.cpp | 4 + src/simulator.h | 6 +- tg-pro | 1 + 25 files changed, 1423 insertions(+), 35 deletions(-) create mode 160000 Atalanta delete mode 100755 atpg create mode 100644 b01.test create mode 100644 b01.txt create mode 100644 src/CMakeLists.txt create mode 100644 src/sat_atpg.cpp create mode 100644 src/sat_atpg.h create mode 160000 tg-pro diff --git a/.vscode/settings.json b/.vscode/settings.json index 9874127..6b25936 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -86,6 +86,10 @@ "map": "cpp", "shared_mutex": "cpp", "thread": "cpp", - "typeindex": "cpp" + "typeindex": "cpp", + "csignal": "cpp", + "strstream": "cpp", + "codecvt": "cpp", + "cfenv": "cpp" } } \ No newline at end of file diff --git a/Atalanta b/Atalanta new file mode 160000 index 0000000..12d4053 --- /dev/null +++ b/Atalanta @@ -0,0 +1 @@ +Subproject commit 12d405311c3dc9f371a9009bb5cdc8844fe34f90 diff --git a/CMakeLists.txt b/CMakeLists.txt index 0d0cc75..bc2c70b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,19 +1,9 @@ -cmake_minimum_required(VERSION 3.0) +cmake_minimum_required(VERSION 3.20) -project(atpg) -set(CMAKE_CXX_STANDARD 17) +project(atpg-ls) -# 设置编译器优化选项 -set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Ofast -march=native -flto") +# 子模块 +add_subdirectory(tg-pro) +add_subdirectory(src) -# 设置源文件和头文件的路径 -aux_source_directory(${PROJECT_SOURCE_DIR}/src SOURCES) -set(INCLUDES ${PROJECT_SOURCE_DIR}/src) - -message(${SOURCES}) - -# 生成可执行文件 -add_executable(${PROJECT_NAME} ${SOURCES}) - -# 添加头文件 -include_directories(${INCLUDES}) \ No newline at end of file +target_link_libraries(atpg atpg_backend sat_solver) \ No newline at end of file diff --git a/atpg b/atpg deleted file mode 100755 index 14619b53d6b5b9c48a1cca63dbdbb216800ca2d8..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 187480 zcmeFa3wTt;89%&%M1q1F6>3z}sIewq6Cj$1)I<_ED;rG-NUCBILV!p}VzLWC1%gS0 z?Qu1&H|mvETeaS>T8bAWTtYxmBi?Ae5EbRDs}fNGLCyF3&CEG__9WZdKHvZUe9!l| zx;bawGxN@Sn|I!MXU?*?z&n0GT%61N40Qd<#Zp;|gygCRCEEt5JC`fhmF*geziF=1 zT!#P}k8iGe>b!1O&CF|}sy7f@u$=g}ky|tWVN7`NX`sl4P0f5_nrA z%g$@Zjj{*xYHug{>sAyvu7fm*&%D~(Q8wDSQUKcc=xg_2*{<1cSN6eA@h83+|4V;Gs-3Gx z$4%boUTc#zgT)$t@L1C6;-Zts;j1-JNlgJ8D~{j)%Y9F zYRo?OtaC@7-B5e>NI?SWVjm=T!X;B&P)j>uN{m7m!&I5iw_cq8)|xfv{O#g5)<0cw z*{#I`hW>rLiGzKz4nJ(KR4mG;;_qC1sV|b6G&+#tO1uM2<4-xv72h;sa7)6_q>Pja z@riLK4}UQ3;Vv{!8b9DlG#C=^YI5bbr<7%!ob7VOEzNVq#}QXOzJ7f9nTPKJap!Vf ztFG7Mx)9&R_%6Zs27Fua<)>9%T+49%ExtOwH{lz^_hx+C@Vyn^+wr{5}J~njc8L;a4{#t~+Y_gFi03qpmUD2;O~!~)iLBV0E4E#`WM0O`-2~dQ9o@^|9tJiAnXs%hN1n# zZw8+J>eJr)gYS${zcxnw*)ia8G3Z$rL+?{!$mg;c@_8l(+!KSIV}ZXvJGmi-U0oPM z&Tcr?{_s2!qu<+O*iT6e_yxeBe|1HM2ZixZ^K8Ag+j3LkKV)T1a47>eX488w0 zhTj_zV_wi>(76@#q~PoPJQIVS`7z`Zdq`fbyUi@;74C-y36m-5#Ug3uC}%#qiIE#gJQd47ueW&T(<1tNRlSGmZVr07%$|HJ9>!3PSSa-W2M3cUQV-O1uE`cKhO#GmZy(qNGIB&)}-VR0ky zcSt;&zz;uh7^H+d@qY+q5#IBfte-0{t|1EE{j>xe>Xvv;RCt=U$nuYnBR^pi|5jQ5 zB?ZqDbdGS96-hcvWOdgqSY%N?DWA&vS19;#s84!w-2QUR?J9e@Z|2 zcPaU|EtVBI&+&6m_1mN1&%wU=DOU8aRQxKnyKWWq9O-IO@@W#aU9M84m$o*E{|$^! zeiDaEI-6dR^q^KzYG%DG;`vCtHsCjh5ja(79%N5S)Pr5u`WkbtM; zW7k;?=AKHaa&`epFf{8T7=aH)RH@p81P@480T&s6aNL({+>%^{Wn#EKPmdneBC*!{vP;$(%J5iLmlwbo}GL>0Q|Ju z)egJ;UeUjDnd(>3pRDBErtqJr`rR((og`PCvU3wYU*So5P~v%7+1t5_uMDNfhZUad zgq)LIhN1`6#OE$$Z$<60oT2pfgpxy(vcuEN;fg#?gKtK~8D}tebFK@;Srrwf4J>7{ zR3YJ|r4^0kr8BE)%B!oct#p-^@=Dw#Mp04fD)me*ES*tVUpcF)!B<&7xo}){ZB6Cm^6Ay+ zgwOhaa``0_i+$&jipI>$%#qW}8>+||$e87+DE4J$R?IH1FZI=zSNR$|6$QoR_)~CR zMeW?W^7_hxqKOr*(#tO?_MKZ@TTxzJnV(rO4}fCd$c)lb-|YI@`K91^mTz`xWqo~Z zy{tZYG8$N2=EyEgp{73B@EO312~60EAB z4SK2z3MLiTPNonidtit7O96m=tBtaQ8P!Geq?ml?!j@}mYDbk`HZpT$!vdJ-+|mjd z&74s+wetlP=%l)#K!|ekPiLptHyZk=?pI)wfM!(0yl7aHODAWP78IZRKU%kF zVl<~EMKM=ZQ&C?zx3b0;gJ)$Rrsa+H)KvMDm4Ni0B85op|90GFW`NE5%DU?E3TSSw z8oL<(vnqW^;8*r1bSWR31;MKd*Q6}yywXW_kw^O>c$ng>(#e^n1qIUCL_3FwfZ=6h z2w3({G56~(Nevpu9_o?yHRWOm!p*~P(Ei}yX>D-i=T$Y7*214D(=xsIIN`;`#3X#U zFbq4lrlb1lL_h%00%w`>=~eSGGpWLAc;r&wf;tYKnYGHI@IcNRbU)?Q@DQ9(9L+hq zG*tD60aQjjnRIW0kLj2eYv9g&6|;d3PNM=767J}s)Er#rudghfS5@!xmsg7}ZT?KO z$voFi8(kwwLywj}9Vh&$=unUj?_6s4tEl@^EPb@l3Cxt$g{!|5N}3Dz!AZZdv9zwT zzM+=Eh;KpZybML`Pr+>QQ7bLSbm{#~H#XZ>wIklMXkziGQc7t?IpxO*ViW?E0z?CX z`x%vU%WGya@}PWv3T5Xae!@_IBO+P`C0P};4Ol5;P*^&@YDQ%Z$gT33#`<4-fzc5! zP+IP9geRD*qL)4c!}K*EBfAt)l@C!IjIOA@YHlSw$?Wom*`;;0)m0S>GKsaOvXX9} zU}BX5$(mX1M_Jj(Pnw?1Zi}mg%c^Wd+*RT82sd9fNzAx4^MSr}#sZ9LjAJ!F(`}n$ zGDh$qHSr%RjTZ8y2amWYYYu=nlSnLc7fxI{i=V3INbUbteVq0%#b8JkOrnT|oz+*G z4hm*wVN_hwYJY-{R6+;Sk*PW|o6&7X;MNo_C1Ld#?f&~2P0}5chq-01Dm_7uPE+q5DDrtOEsG7^aZ}khN6k{gn7~d*7{{= z*GFzYac+@v6C@x4v-wt=yk=DX$EW}l=9qr9x^@<}oZ_mv{_1jHZT-3PD(kCeE+{C<%`858I_IFUu1!@@`lU|L11Zl{VW8=MMdyd zo=dSfn}Mm!-%u$+??~U7qZC_GfP(%}q&2gkNJt}!bP{1_<-F>Kh z01Bj7rE<>0iZP-cE))x3> zmgFfSayW$Ik?3v`^x6j{mBGA%G}xb{49pQum1b4UuB@0NNs(O{c;?#oxE(lghlqDsWN)mZ&crcgz_ zjzoTB7UyZ9RSf06vdJ6;5i^ZaJ2#>?Yfzpy-CtEbqqG_$w?d9|DMhQoC^2fw=glge z0dHv&aSlyJxDXpKGdp5PmiTGveMaES>Z-Z|VIQ32;VWc%2abaYpXmBI;J{ypO0kX0 z*@SjgS0!ztbULDMk-}mvT0u1JGRIZX;1_Petdp5R5+fXz&Z@4(YPVGQD^%)7sWH8) zt!^yeB}i(hs70!YanyhB8fNsh2aFVH4`Pg;Cp1}ITRX>JSL$Q7EJjb6PUDPHUY1DQ zv1vqZ$QSlMJ@hx>$no2k!T#$0FT+r>tmc)Gf?8x5IZmXZTBgk^4V9%c>oGF8OcXi3 z3FF3>wZEO2~zHC2@ti26fZ zGgUdTI34v5bv3B+HKP6?*Ai9si~5JS+ElqpJWp`ltIBUYIR`sQ@vg^I*_Zx%?3fL7 z{R3rw;_&PQTuCoK!>X#VgE7>#LDj$QcXwdt^Dx&ds_Z|u3j8Lzwww5lVR?XSr^08R z^Htk&uH06Mw@97;HQ{YbB)r4{&ux+LG6&o|cvz04tSY@XFK3U3ZCnLcPY7P4tPpXu<0ss!0VJe%N+0(N}jVF@SZ

~dN177r@#Iwu+&sBW2Ip8S@zT5#%Qt%ZHxJ$twcEEc~dv?IP6@0Y= z-o%4;__RCVJ&OJ=2Yi{5=XM9YNXfI?0bilyX*l4fJbN5)Q=a=B@Saa3oi5eCY0oPa zUx^NQn}R1f;7tmi?10xPc!~pFrr>D~c#(ou-0!&2s|X4!Bvr#{oC@{av1Dzh}xP*#Yk|_3nV1c9`aXn|?CG0bi-cW3~g{rr@~_ zc$0!_4tSk{7dhZ%3SQ!X7b$p|18(}sMhD!|y8~{@VYvft%3*~AZu+-}9q?R5&q@b8 zMZs4);7JPJ?tr@#e6s`Iqx99~fOjkSb_d+_Z#@pUY0ru3{Eq2QOgSVu;HDgs9dOex zr8wX#6+LMVc$mu5TQ=6Rkb2i!c@w9El7 zni(e?S(^jiq~OaP@a`*Q{X}*C$dt2L&Q;@=wZ`FV#=9jk;B_(J%VNOIaqq-$jsqv$ zv<35JtWSy!KE;B%T${bpt_A@{ zn=?OMHn^-IpKQ0m%`=32(rtq$m`HFnY;fAH`RTF2*|+)GZ-Zl@8~GGQ=u}7f#Ir;j z91DNzlVpSANV)Y%w!yLRwmvB~IF1flpEMg>9ZeO_GHh_uxA8%?4UQv%)+g5n$5BS> zquJnUNiUui+2FshYGYj6;78lwWj45ZW|fa;+u+C8>et!e=9y1EZnVL13fcNJ+2H0o z(tNng20z}ajrTHbaOOMA&vF|)#RTHI!UjLd27lNFKg9-LX@jTQ;Hz!$Q*H2e8~m3x z_+}eC%?9tX!P9N6KwG1 zHn_(IUtxn^Y=b{+gHN=_>ZjP? zSJ~icHh8HGo?(NR+2GkWc)1OpYlF|R!GFH}Spq*x;AaW^EPv&u|F?g?dDWhNl^gif-`Og!!h9buK3 zaNHA$v&u{~?g@SMqscE5jNsoYGocUutuhmh;NL1U@eBT~G82yA-zqcF2>z`y6O7>B zDl@SN{;e_-ihDxkR+))J@NbowKm`9*nTbR2Z^2wsS&MGre2>z`y6NKR3Dl;(%{;e_-g5cjOpC-!JSY;*#!M{~z zLJ<60WhMf_zg1=e5d2$ZCjP*`Rc68u{99#ipn!j?%)}q~|K8-E2|wuHDl^ds{;e`M zTA+Wc%ncUsZnb7KblTV*Evz`s>yq7VFAWhVH* zzg1>p5BytYCiK9+Rc0a&{99!v@WB5;lmA>%{?IDtiSp}KnF&1bZ5osi9GOc zm6^Z;|5llaJMeFnnXm)@R#_9}a;wb59r(A(OxS^ctIR|l__xYlQ9j8kGhqk*tuhmJ z;NL1UK?nX1DE{FMPsQ)axlaTi^nWNX+!tN;JIZq%;xx-Oj<0${#QGVP} z{jD35iNvmE8K9OY9T<>MXY z;g0f9M>)Y!{^47P{vG8n9OX|O<@X)sw;bhH9OVv2d5xp|cSregNBPf=^1Y7o?T&KL zQEqjV7dpy*M|rNJTs9n!eDb1q+h2oK9bYF$S}!*4&X2{#et;Xsx}z!B8!){SCgL;R?8ijm4eT>=iS6!aY(o^bd|X*~E9#Q^VXRvlUAG%W zK1)`0SFmpL1*tCI;hKIys?kj%C|?gsTF&*UNxmNAWdOq=8~t}FEZcC+o1EG134E_L zZvos~Eq{k$PsaO{~&<6Op#f}>93gYVE; zaB^yrCon8k(-XB|5!C#;|L~3jwYfIn?NQw_DesY$qjbtGw>xeVJ~ zge7juO>%hy-B3SC_vHNOOQJB`pq&h#22xQDf2~1J8CuS6-xYk^BdGX9uNoht815v#_535G0$uEoeRi-i`g|V}<>N@79^(279(#j6D(8Y!Z_Yk+ ze5+`&!+4ZB5MltXlUR8HD+e%qRo^cgvj7QmfQFyrpO5$`(zi!o+HEjC<6}qPrxRUt z-$#oUJB)Ms^!>wrXWwB!?0vVb4UEGjv7!hEn?37^5|B z$k2jAI!I$?``3R3ora>fTU_<)x;V5FFTY}1=xQ`BxnkM|semyTq{r^+TF4XH>`3T+rfLSL|F^ur1sX67`Y(F*bq} z4zw$Q5tu{AV0ytdykspcz&I6x(e&Zxindut^AhL;vbR3Roxn55h(lA_6=DI*rX=q* zg>;Z0^M%yqqyU0Q^VRZkmq42E2jGA-B%1uxB4a$@g@JFvPmz_|gon!z~(j0|96`8?=K6 z_yS`vXoqj)fZUJFl7sd+lGjv8`%uu%ic^46^@TnN`I>lPi&vOWgds+eN5H_O=AQDZ4nNv0uBm5OhJd+ZG8S(JmfGDoNSJJ;{A!>z2CMyc6|< z!=G|VyZ8=d{yV$)r{aDIdo%6A2O^F8(Gqr1*7VctVkN3ucF_z3p#2x1UD?G~NQ)`E z=tf4;VHd@c*CCSjZ+pq-Zey%TdtigIi+70^b}`O;(w|)%0%XcA5RN=Ip|Z{T2X)2yFE=MGUY-aJWuZ${=9OnnvJ2#m4{?!OWVK0_kqR zmIKzbrVeEU3h!ybdl`89eH@ebLL->C+2_gg$kM$6zc8A6*+L84lR%KbneZci4HLeK zScI{*w&Rhp`b%*06lm*VgE4Dn_UBG6f50?N?oiZ7;s4jM5|z{OEA{y zZkYjBYV6#NN#%0f*;qb>C|||{E!fJni56%j*P(s5$D`0o@*3_&A-qgD{V1unu_@-4 zc6dK2)qa%{eG`l+fT%u!OL_oTL=w!eWg z^$2?vGJVxYncgFj3!z?#C0XE}c=jem`Y0U@rk4~;s4c1d&0S;q7ZBK!q;~~SGl*Rz z_=g{-c6!n1HeWPagyK~bF`*sYdHsfZg%-Ob*huN z8~JAmX=^8DgaOGieBFX71a~WNA_Vkz!a(6GkPX}Ih^}xdQU6Z0v(UL)4g!U-0PxUP zxMRZ)q8p0UR0%4CJE9+C5#xnUjG*KU1zQ1xV)Xd$3*DxWFJTX_Mk5k~dM`y{atbYo z2oP4=S_)eYm#|rPKh4&nSr}oJT^2%$f8m2C*z6Jhc`&+49$-c@s(6Dl5P<5>q&9&- zn$+3YIieVEq`gF;J(6uMMVruMkVK?hmWC#%vD6I& z(TXL>XPA2qpC1SBvC&wL{R=HV7$Y2!K}9T#i&{Eog{W0BpoqkwrN*X zBts7munkyw-mGQf#268TibeNA)MBrv;u?M-f-U?RS;V5-PRKN}HW4*Lo57Mtjn8af zA>pF{f3XAvaG=aY!Aa1O3bsNK$#MN-ND}!A5D6rqIw`X7s_2f>*}*o{4PC&=BZ?@I zrC7yh&*K@9B&+MAxJtR-X|R@p3U9M+6!ART!Qle#tc}86~m{#t2udOumW5m+mW0U)qrJp%O!MvL(nMi1>A`W_+be| zf-R{@yu#}y7@zOz?Ja28={r`iOgiwmhgb3V6+DLFHOg#Yg0Ti=ELZ?4A&7?mS6Kzi zeJC8|yJQ)2$w8EELJ1S^iz`3@E%gPI*;OvPz_@5co!JVOqF@?elZgdk530HpxCr2} zs%keGLh};9(iN;-!O8#|u3!%XX3WI?JoTLdi;=1p!6T_q0#g#+@u?)vE=M5S3@~U3 zKOqGf`kNSyi@@oaJT3< zi9m~)iRYm`*7%wF3F){^m^(1wPqF znc`{%dI$M~fn10@n%O<uSbYQ?1w7NM_KfFlxq+A3cZaS z@xSA36`mWLSo1NNe-1sUT9_0>@pb~nH*w#F7VP~3T*Hq}?!Ddcn) zmLT*|A5nTv?;)bA&8Q!G0tsX=7W#{sNR}(`zS!?VZMkMOE@Z=3V4cDgL<6w~2z`XX zYBvw2r_?km6FF1RGW;j>7rwU-O&OH$Xrh)|9nlWY-7*QeVOBYURrVnTOtN?5Dn)!? zN0f*UpKFP@35hC**exJJ#3NukO2lK~s{4?F^?!H2BEFsAVAdsX2oayRTZ(wG(nnuY ztVI3LM9>(q6m}Lp%+A1bV+?Daq_{dpwXg`Y$?;6eU}*p3?S%}Kj_$^7_*T>nzhl$V z%eMQsE$pU>1nR$`VQ9HZAxCi}Ld0A7cmW<$`q!vy6|PbXz7L|b&@jgu=Le9|QsaC} zLccQ425JcREBq55P}je{kmLMhsM~H+wqYsvo#N1pL-G-H9lB3hpc;NM>?5hw$eIcg zy}<{?OloX-pQKJsosB-Pj?g(NLgz_#IuSqBalDE6DM&VhS>q+C=O|L=Ln{#hhg>Q# zZONI*S__N2C7}FeE|8G{0|bR$W}e?UT!mteA%DI7Jr;^Nz}DS(Om4TUYnQrmb0tDq z_;f8QC(iN2f9L2kN zgF0Us``d5s0! zrJoZo9@bPRUY=(iVoESZ0*tmIfu=vYtpBz{?QK~{w%z+r+URxgXydT7<2rDsglK?Z zWk<+13CWNxHj2_5?0J6SJ4e&~U=92050dVMDO#`~!>d;&$%cPm)xd5qHnMKUZFs9Z zmm_7P1ry4*#<`|wfgiNs;>1asei_6uVLwm+WkI4>Kg1ii-W%9tjLgHEz&z2zhIHmK zZLSO5?lOvTZ8H{~ca<{w$d9l^z?G~2Z#u-GR=VRkfU!6>=70URtsB$F_dpzHcX2v$mMwb2pBgtxr)VJdp=SRyuq?N1NQMZfnztP$!>r> zf%lE~F|V<^w?x!&eQK`p)c1t!HvSAlpeWCJn`OEDHM&5ZQZAq6p$=OQMjiI88JD69 zzUUVEM`hzTcw$WEpGy@gtcB1KE50w8 zFcMIaq=w21*$Y1If|xb^?@5$4nBTvX zq^?;3^E6f*luZ6@2dZEQ-2@c0Q0#OIg0`|Q+V}(<85Js0B%m&$Sn!1Q0n)=?Vc++bu#S}NGLO0_4G@Q$xz>iwslf28k!K{~1H*X5Oa$sL^=DWtD ze{#9<^j{fAq0L(6eT-vp_v}%)6HW$O-P^y`9`zsq<1iIfJg|LCTda|vT9$|N3QZ`u zTum1m@4aa@)-THjMPbx~d5JA^iKkVd5v@B56qbUr%=Wy_Rtw7^+Zb!i%ccg-$7yqU zzuPz)_k^uVp>}o~Pl)R-W9At`O1A=?@mG+~I@2=*> z9*?vhpN+@R<}A=;3=nkgGoCAqb6o-Uugsg4ch$5FGtYLP*dnB9oqu;fab@cFOT4My z=R!d4Cnl$UzhS0XiGwur3s2zntF*vJTJz4HB22dl=T0K;L)ZRVh+sb^_TJ$mUygHq z(}v!EhZ{^gzvU%ozi&8>g&e|ryqYw)w_DlG26aXKa#26)a$eG5Mm^fPFE7;A?H{Pc zZPH%<(KieTK6yzZNbKzfY56Xf*`D+@jm<(^m;Vfmx3L$aCT#l?-w;h7`zZ>>;4b)q z86a^}!cf$Un})Vg?L+hN&}PqCa6-n0HrWsHyH`y}vzPHa(O$;$bbGmJak^_YweO3^ zqoNHnBQh8MK>%&|Gut<`+2t+TQU%~sILZIZ^!(rE|9|MO$S!ZE{5DM}ic>Na^7iTz zvbE+;%>!$6djp-JS+EGx4%=+nQSZmWc<;qOFUxahT3`@Pp5buWxLg@*or$K1pL3M>)+Yx+kt&4&0z1RBS+XB#k!Z$PuU!xXm7QvPc=>M;Wc!op{E(-C7#5}>jKo>9X(AFG zVYrDEZgUW?t?&Ad)&lQ`w+cHZxaU;?_J>4(D(xG3jEs(myzX5SLtc*&N3{I^08mVM zmAvbW-Fs1=i&q3zqJ=>s)AzRMdN{TBTq{S=NHCKd)lI9;8u z=Ou8Kbixi7>BzT^izZ<7G7Q1m0|Eceku$)#d|n z?v`KC$E}7A_;KT?w|nV@0GTXs)&2A9%s|&T%RNr?0p%i@ z46K=WG%hK8)XX-Iexw#SLeoK0B6W|mU|(f!)AV!6uxH;lo?!etUOlO>b({Z9uU?$w zMdiRmTtHcl%U6e^<1m4D!Y1EdeN188j~@LHigmicTY%~I5G|0V^^QxH0xPf!OxgvO zdET7Y5cWP#x&ub$HgBMU1b72uOg6)Rp4o=J#E!K&{%{@)p&iyujEKQ0oHvkSsu%AG*oFgo>Z32Vfp(KT7z4zEC4X*))LCI* z2FQofz-0Jw_y=!rj!kc$h2EpyPTLaE+p|zWTV%X){*;=-TN9m0jL4I``qhauFyv27 z6H3ZYP2^h@i0$>$wSeJ`Gkh51U$|Rtz+-RV%v4YF5AONn@i)$&;a*kX%3FrR+=YSa z)WnN6#h(M|0>cb#l*H%10yd5D&@EiRhC;00-wglK@=tJ{THw>nZN^bhxDXc4N5-cz z(nYJ!5S1Itz>Zf(zgTaC??i-jBEl_W5}?NMFbliKlF&=zc%uG0soTBjv;9{|MffD}3A6I!AlPwymdj^! zESu?|FnQv=v#tL3J^Iu{ZA@_z{1lV{TY}3*hrdOKa9%H>v8T5K?fvbXHDIqcw_@?n z{<>}BKX0ny0|~IT*`N>(tIc{?yr$j5vc0!}q$6XsJ73>8&zw9weMfvR38WYpndgi!!Q@m<2rLQYGSoFInq ziKZVHqN%e)gJzzbE`O;vC*=Q#i^?P+n|Hi$mg4m{X|W6>NS;x#k?i2ktH-B8UQh6? ztOVnFNRI)Vk7{e)h@9W{%xyNo!R2@ZAHp7(0(5^TD?JCsUA9WlAJPcp;3M{J6z_;7 zhxoRh`@~#V-c-w2Jb@qJfJBrC`O;pPx{Y!~aJ0t1*5gQv?w1DS*|*nY3FjR;|9LbZ z3g!eEH%gN!v&m(zC+8jirQVzm5pU^Jq{(cjG!V8x8tBuw3<`h@)qVbu}KRwLeSeaIXS%RZuu?IU~o823MNhCnL8(>b2Ajmvm+A7$L07UGH&^DX9w*KG3xCI?S&5rkvxfyO+6 z@#s}e5aXdd%nu(Jv%#Gv=7&Xz;olpBNpx`Rfr%L5XW@|=)S*labc|%Z%ok!>16h2(Yy-=T*j0!%lN53k~8#v(2IjFhE%aMs)niS4c zJ?n&&kMX7>>mFV>TtuXc!4}RxZ&3ahM^m)V$w4ec;==uR5Peufbk@pwae{RcOe>IUE3uM?~hLh0(LsE@r*OI#-bW+KM z>AO8kh-2~MB-{}H^&|2F`+;q^R4*b>+epP;(MBfD0x#Ks^h4g@eAqA);?1c`_T_K| z^dSgmKVH2NPGEM5SFeH?P6B0QI|m*w40d;feuM5K`Vls@C$rs#-?lAtp;Mb zs(h1EB&U>;DC^ST>dqkrfesH99Q0>s0Y8Yy_UdIA)Ce2Af&B=%^4zy?Dn!V0TYFy0 zCU@&!<7McTD?_hT?8eH_3o#%=uR+TS5O0Ig!r($+s7w>l7q%6(&VpQ!gdMFN?v}IA zOw$X~ygD6V1G+6t@#d^63~cba$N!VPV?@G>{T=nZ)Xr-f-s{cq1~7ej@rD(G7H?{@ zarldz$Z+SykWIn3L&v~}n(o$rp)X9~-t=~DtWe-F+E{>^+&68)1>wN57jZ=|z6(Ui zCc1gG-)JRwhM8Rq2i@#qDCy6EgZDueuNgOkUYMD2Bk2xwYoHpD z@Td_gB=jHw4g7^ehs$D*p8}FHCd!iVOA16xxk&(HLb~&da9T z$EK=3g^`C~DaqLLyb=J$@zGlP%i0obwO|~(aRZu~u1^yaz{#+DSkrD}5*}-TO&Bl` zkh|pp23M_nh4teVpuq(#n2ml!Ly-yh2EOB~7no%3hMV#97Njv=KQp2qyXCoWz5$Gc z_=0>}fA;0cnU>;ixriM?aR(IL8OpGWFi2qB@Cm}Yy*aOY1KTV;YI+^07o!8a1xU&p z2S8AtF+p`=SYid@hquF^=#m!ezJ;;7wA$+vVX=WPSZ=;9+2zZ^)F_w@9S*^n>ktUP zkfY2)+u*SEwxEsO2PY`nt?sZ3)7< z-o@@)9%9!^aJrs@^mY^io7Wj9BG+*> zdZ;kSWq{(<4=)US8BVg~bcI-F%s>(f!|Om{&H*^{Z5(?iW8DLty-Ib#D`3W%@GMov znE(*T1#?+f^jwAty^Hb1T()`91DJj8_XO~&$Q9Usf7gFcVa~U{Dh5K)K?@QV^JpB# zE~Mf(n|acA^qI{vIsg|^=H8sW!roa%DqIa$(M=zS9I5aI?luL<#ds%s+p2 ziu>kMIjEW&lU?qXLvc%=3nRb19nrZjk$JG2097Me4Ck$@(7qRw66RS9X&d))9kl2& zZ%ze9D~t-*z&ksg0Qp8b4KBwsPcu%#qt}tV4{Q`&gzui&hPT}iceq>60X#4JE%z-r zl?tA|=d4giG<{-5wf<_p4*u^@F6PMD;tP>~#T41=KQZ(nFj(<{N1qUhpMH$JOl-kj@_-7R;6624_i!9#Aw-TzRsm)&%R{t|@`{X^cq8^l|87~dwJ$Asth z<cV@m9fu1F-a4g&WdptQk zzVz(zDT`Bu=~+Wp3yx3opF}(2J|YkaKDj$eS5pl?iCHfEvQZC9pDFTl*iR~aSe?N! z_mc|Le$sn?r+D!uAkX87?VFbfQSSmy3w@80J^mD~HJH%)Pz-!G^}%& zSMjp8i@|-edzH*GvtXr~)8M5Mfj%NC4MWPjC!C@M;IlMzdNC4a_@SQW_7tsoJ-`Mg9S=&r}m*XM8GnbcIHN$H;iZd=H@r z=9)JmgB$jZ7lGM!a~^i$_boI@ijdL+(hNzG;eSO-f8P`LIg<;Ro%b34`Ww#I99T3W z6{*lg+qHp^?8Xfrp1d*66PO@=k_gF6#6uW=@hXgehq{QKIxYVU=J1n7Hc5cdNjTSs-7;)hXP3+GUhO)6}a9tKoC0ZA4-S zzdkeGcnVK-uGyhiVFRHHfyS$+rixz@MWj@6J|ZO@^~CxO)`uvwOI!C*g2qTC^cW&1 z;{r$nRj(Y2s$DB1q0|c)Kpa2jdf(cR75=UiS+LS1zNE&T5^QJw0$vJ9%=NwrTHq+0 z`2!T03ueo>FVGbkMWere&pP4$p z7-C%Cr|&@)S&pjB?v{nLD4Mz#H=ecDxCxGSX*oUa8;=KA%re7Ljln`9!h|j`0emfLKI)F7%v%TArMa`ROu|#ZfcoamuL}-f|R+ zSE6`@xjUA36%O8y{Vj*ZPQc}|p(FJ0(~@aRcFIZDB4_cURn0e5%%%s2|krY^Pyjm=r z#>GM!mbc98rWu!gL07d2iP~JOp|SVZTa?n$?yJ{yDJGjU<>aF+*+^;HM!jVp++wQ3 z3AO{-JQ0T&XScBheo6~IzXC0|K)?DR73}y8w>yl1P-ys;HvUpr9UBI-wh9#cyg_mB z+TfZ!Vmew5&b_)@+@MD6KA?V84!hiEq(933u1qbH-r!37)≫*WE45eNZs~a0>LI z3Oql5oQ`{BMTC^lebAGrpRc12G~W3uF;*iBBK%7=m+lhdLWL0ki7_{V5gXmeV-RV! z?f3AEs}D&2Gx&>e3C3a28^uwC(?RZ*k1^Ja{a_&UPuyYr!t_F#xRvW`@xyx^`_pmG zF?1npMNQ7>-qhT1i*YuQ1;@@l4nE-xEM_RW)_hpDF5jH$qnu>*(wm6je-`H#hCs@%u*hXgjawsYv<0IWClXbv5WZ!vU| zjpIJ!(7}2cZxC?YBxBrMO-Ii}V!Vn#Zl;+;ClalAh|@n#!Ddoa*KIn}#3z}9 zvDSYCtMd>zHBg%b{WEu+sC7;d{(aK~3?A$eXn}JOHV!a8=TM1u@Z1fVH}W|+R1C8$ zw;*(v(fknEVvx~*ux^*pz;g3O+^gdsboKX-h9Q54C(@8RLbrm_sQnB`6}gP~C_XhzWE%N&--v~q%jESGkWY_v=U*7>O`*MkzkSA1lp{i- zE7RO96*gCPpK5p&DtbX<1|5%=c^%X73`1?Y767EB#Ze}xv|ywH3#Tv zG{Q~9#@y{sEX=`qwNA}lfY${)!668kzMFTXmh%B1j8k*gxo^Cajo=wmjJN&_4q*3K zsMvo9)ZKCqs`UHwpTc7M{069SdC5Zccojf;z`>%3<22&eh7M9TAab@feEc(D7nl>2 zT_6Zxyu;0}Et%Ug_Zq)>81AwZW1r(8;vX|YpTTbm|H$wPQ*Wq@4k9?#gCvmg064<^ zSl-`>dt(nemS(mwbTRy>x~GryM~b1TxVJe-D;^RXYPnH{Cyvo1Y`YgnkzsYv)NEuF znijfnY6wP%4IC{F2hn#Mn;!%z3=}a1a|6-6^iv9+=G6KE?!-nS@;qXX4U0W`q4>u&gB3Tfm9g zg^j11jSI0A9vTi)FnS3Jj_o-UHgJj%&W`YH)H|Kx-5B9AA7j_C@P2*#izo1j@-D)k z>^44Ou!5t7!nfGH2fd8+AnPeg%TwAs$SRu$`4D+YdWxv_TI)}ABc2>=4?5k5H)pTSjV!17g&Vo~k1^cH zpHbzfyAf%NuM3%2Ze+bEnm=#*j3`C9k-2@{NG@a~oCr)&gl3{6IllO zld005e0LV?rx>ikmcHQq1l${c0tM2RHiT;6qSU<*E}hCf3dZ>CI^4_kh27SgKkv_< zoP5`R@+XZeK+69+{$wmTiRn+0`tvb$&qH`h(CFfpy1dQX|RDe?q|m~f6@u}^ncQy)KioZmvDv^k=Xso@6M2JA>lr9 z9`PsN-W%1puRj?AA4z|*l@1U>d%-tW5y{$vs;F#XA0a8*u!!YG0;`jdxnuksaU-py@h0!5&L0~)iC z>^=u`wm01nFHhm5Z_8lJ2{^UQL!&s`6X@}#eQbmglcu<*lTeT2N& zMFp9AkrAs0?QKXcU<-zezDcMfvbPHX4{uTHvAh?#tO@-RFpT5`j^qV*A=t+JXZc%y(z-IiRRCXqT)Xd*`>#}6A|*Lc;}*J{R1eF`cIA92-h2P`F>~~-k2PX zl`>XG1-N8xG3J3bA$T`iG`E*9b;Jeb5V4^29}4*t$phoY`KTM(1z%VBq3-4}K4|5c%ZVeEo!c{gQYOUXZE4IVN44%hU8nlF+}Nt>+DkYahJ76*3yp zbg`cQi7VHATW79&6#>ijf%=?y29Pr$ZybDVvQg)5sRb~vc}rY~PtEl$b5de`px?Ql z{0GO!>xZ^(K{T?dQ@-e0F`zU4MhXSha$WtsPlOR74#kT_F3n+WF8&z5yNfC-PF(AP zXqhz+o_YKC=vr(3WIrN#;~G4tDR0(-ZL&&%tK+Ncb$B5H>#;c+(&q@_#~~S1oQrD) z>>Szm=8cK?adA1AJ41I;kGAE7Jg@&>zEiRpgm5oCSwwj1oswb}%;`bC0yG&QZ!q#s z$;v-qwHb)KQ?gpRveMV6+>K9ECZmqCoXT9sN>P+XX6!v3@vAm zzbNz!I-$R4+2TK6Z$$EFSt4qC^(OM6k9amOCmFwD6h6I)Sb?o%DY02-H#Mh)wZyxOcrVgNEX~U~#=ki-|CwFj)&9-Eo+P^I zIC$kcM^|y7Nw8A9kESopMbDn#otn7(gC*>wVFDeZewh+g@&V+O3JA>v5Y`4H9^Xb3 zxh;nghSK#|yBK$Thqw!B^5~_=nv2ysj%f1^;@aSDSp*O1#r9S%`~zWnqMnUA{1_CA#+;+Hg#@WPoSpl+YYby zJ1rQ$DNnzjjFRvYJi@86EAayr2a_I{4X8NCqvXdl3Kz_JroJHlIY_pbqm!nFpVX1% z-qk4K#BITw1^T1Rc;u(|6v*F>$#Xy1f$y7nP1ohPpuu)(57+e_UzfCZyj#-kp93*v z(<(do=k8@_?tZdo;5CW)?kBtQ2Noyhr@!rfazEP*TrdPpH{rqNd`!O-aBhD3YaIu# z3IpDW>$}9UvE$?4v~T?At7khp4wf|4fwqo=M~JJZx7|Aik*vGrNp!>ZB?yo%(MPoN zzU*Rsh`6Ef;_~&Q3YaO+)9<9=pkC`X9>L7lC&p_75tC4^t?$6;=|?~^sQODKF}wgN ze%3T|8z*r7!%mso#P7;U|1QpyBla0;3D`G`Z=d1-(i+r7CF!qlc<^z1S+EOER!~D) zGmI;VAebHUn(o%%4|G;AygYrvFpqvGt*uaBN^3*V>QQb7>Q2^i9vIgY#vAV2)_Kyq z7^M$|eX#dF34VSq3_m$zcGGQF4GH)g`RJ^KB^^eTF_ioNbtTciz+UIpXg zuzX067iEvZcwv4ND>G)oKsBv`85x?N?z^XvU1X!XTX>VJ-%Z=Z(d!J9QbWx6a=wM3 zR}9Hd-x1qLO>4x2 z=0A=?Y^8@00%$Y^z#C8VCcL-swQo`(-pb^HX15Xl4T534mDo60_^ujrT;maPI?L(ujh1$;55Qc^$+D?2$)ykW&l9ur%0x0Y5N*qhObND8>bLA*@`;aNlaCzds&;ks}D0XD} z)4(iFc75S)c?<;NEE;Ui@|W&a(_BplQ`{|c@T}?JVEjV|;%2D3kWS-E992B$l4PM6*;xCr}6(6cA-D{2`o3(Fd)#~b&Z zI-?ekcOp3DCwrQEv4b(1t(tqWgK;hJu}z{lqc$F=(-tvSy%3K9gdqXlb7FhSP_`NH5L$o3ug(rjS7XxRva6?o1*@lH!V?8r_v2TnBA!qIN`#_cD; zaFi2NjG_p}+i;5DOx(#g^ZL+gQYd;h$&_~3+u?yqTCc~Lrx;rsfJJWG@}G=KFiyEi zx(=@59AKO*OXdaRQ&HbyTdnWv7exe zZwj>pKvbw5R)hJ2dHB55K!iL4w_NrbTY{3Zln@X6t9V--Cg01g+0AdGxeF+{?WV_O7UEFT!J{Z`J_$sYYz z;-3c~eO9}Z`nKcgIplo~7`NM7{uL~n{zm>wkN63+Bp-fNYXX7;an1#20&y-+i`!#d zw+GZH%Y!IF{F!UPS0A}Nr8Jfz9JwhM{BV^N!7gLvTi~DnSR*n;kKwqru_GYvSMdG~ z+#C0SOu4l02)%GC<8iTG5^E)%!~aokt$%|}>z&+J3LadAs(B5t{6;*Zd$z}`{! zUDVa^3t9V7E#)%(Vs{wz&c@A+l zx8qO*x?vMNVT1(bT0I9_Qt9ex1#ldIZ!pRzE}oa#ZJY{3&n1E!@!sDK;}gNyZ3^49 z_^APz54#?9u;sgn{Q~3i2*zaN^&4f{qhkmuKn#dkb_Hv17iwuq?FRl$@`4rO?sn-> zL35XogQ6YmZbz9P{_`c`tW6z-&_obEUj4y%{y@JtG=B}H8oWoKkn=Zw?9hdOviUb_*RHqm@5>;yrJdo}AXUU)=*jQ#9 zqn=+Pp5G?g^Tpmq@0bTu*^T`D8)TyR2Hn+~{OOL1a@8DGPyx2P@B;zN zmm9}Ie;)i?XkpGL{tvCn$ZihdK=>Za2suI!awz2*c7toZ8_v#H1su}9(?8E9Mm;|D zMUW5rcl8!!xL@oFHKQipZ|F>ckPGROdYYw9mebDq>Lio^S0*X@+}%13(hN<*AK8yI zh356SVt|S&||UFO}RO7o-y;%{LgR> zDM2uiY%JP>7C_6co|61Qj$NqDU)|)tu5kg#CV7ptz&dZv$G+1=J+gq)!QA(RA^eCI z#u2FMY2FBA@ASR+RTbJez}yc3k;^^Ap~YN*4#xdpF}uO#J-P zkPoso=Y7T!0fZ43VYVEp#r0@-d6(`$nlt~sAg#G2bv1CLIL8)v9Y7DuS4es{dvm(o zH*SP*3j?2ki|cSk-LvkK1ibBGT-qcD=n2@gq1$aEMKCa8^~Qb1pWtuDty{T5(K~(s zQH{ovUcsnqHtB_&MDt+QWb_~$Y0qLQ$La%8j_Uaz>Cov&yVP?ppTkz`*0MLr;BC}y zVEwbnfbg9d>=E83go@wd)PfhK$g}bnVSY3Ft;-cSWb*=W#z&O#bKqS>IWF9Iu?p^C zIk0PHpa>>dl-!w{AtQmuc8HR+NNItMKehiYet~)`C>on#ql9Dfg?e(>ejwtIe=Huj} zl$1^W!zjRr{B_hbQRKWZSW`ALph4WyWVN7egs@c- ztkmxbZAD$vpZ?Dkp%C>8;x^Xr#!J1 zt(FK0Vr7UX0d9}iQj68L`bzt3YbUjJs9J|G1{@J*aX=h6$Ee^4PVoQ!);{MB32OV^ z`@ejYyU!liUVH7e*Is+=wH>;en^e~%?l~tCW11UyBS)BoLpHhelQ(nIBH^a@+1fwO z6KdR}CXf6BNW^)6X-o_HbqNm6mr%YWJSYfI)ho5pL>rS@FM~WA72hD)dy>ok&Jwko z4@ze%OA%SCvstMJLB;PTt2tm&f9DI{%)tY9FsiTipPk{xX1(=;wxK_QSqc?N=BPAB zlTd6TU4dLN zmk59HOf4sQa)k}FymOs}@V{tnyA5h@Mbsv zGH%Axw~-F7lNXb|m^0Aa`k$2_PGu|tHy|OB7`moh*@IN}%Qj#pA-KBPFS@FSD*2Be z6u^3V1nbug*4F(ZIH9JZASF1xT^QOG10w&p$NUH&^dfCuk9Un~d5J`wv;q|B1rM@aVZ(ca3V*Y7^Yd%H;nPLd%0A6P5Um zD=|4LAzl*9qJ+B!u@CtS3gqosYS}~87lGGXIFG5)5X|G0`3%c!7#>?1^}#;`1m=OV zT?ER*6aghTMsfteI#d+s?ex6NFKid~^f$dSv(Og>%L_B#9%XK^%q_SS%+A0769k7| zuYt89Zz|E#1=9ikH}6K<=kDM-q!hQ6)-wUY^4w>zAPi&qqNGMd=rCunb1tl;>+?!I zkP9p6FS*Y|cC}H$k8%n6e2C9p=eY=1S4|21kG5;GjhHYy!QHw>cSCnL15BQ`vCm9o zF2S{|^7KD7XkZk$pv1Xp*6J@(1gvH16>R*UCPJPZ|Kd0TT9Rr_=>tI%RZpX8Njhx% zKV{p$kj#>B=4%4;7m0gfCZo_1gd1mXz&QfRYeb}}1|(DIRdAZ_+xY|HQc1NGjtQ%S z=#<2sZm{6Dx-Jc*yz~^}@ygj~ISDi=pbLA1Cs|~>)C1c1djnQA(<%wgmOx;7n4?;9 zr+_5W63f(4*`_r9Tpw5h{Bwrazw9Cn9m`!-A@C?t#RpFN&@a}pgfH;$Uy~Wy zkIPIv4_~^@LuDtabT%Jx+Y50}NFV42M|4+TR$N zH+w-nBD1^(S2uBsxAka$AY5|Uhu<7GDR$W(s8Ye^*xYLgX5CXVF5{ZCBO4APL$j~l zP!^9g3nzp!hd&fPTUYh0^sDHkb!-Eb^x{vEo6l_n=3o4A7MLeV^i z{wV_@)&HD--NJ0k<6k=Gas2BDLjPm_bzV!Bf6XSCX`&v$7FZOjb2Ul5cbF=A zbNngBUObOK9a#8zeC{*&cvh5id2l-MpTVEn|8@Q}&i@+xY0S9OVwdktg=5Aw#ePyw zK)fkEuJI123bHETOkc{fhDiTleCZ+oS~_QZX)+byZ^iM;&tsJSAK^#VcvIB)DFk{o zn8%CaG=c4_`l{&&*m*pK$lKZO!_(XT-9s1;Nd1tdixIG!Efs_WOa}qKB*oOsarz%fmu4}Ty z>l*k;c_Zb=4@<_-Ycf_CKSE+orGGb%%ue$7I`X!gxdRActTu37r>o;>@-_-xrd#aT&zJ=sY3#RX}PU@OqIl!uwn=hc1%$FtwDvdyW{3U@5pst47G&<20#-SiLCUenf}F+a{`oxyL)Z){cCphv zRlSBTkU`x^;RkPkf4_@p5UTA4<()2Kq$0-HD3R-W7kM*)rA#gMGa}mVY394AWh51@ zA_P6J)sMOHnc_-pbn!)2z1|)BuEp1_$jSw=&Xsfns|d|3d{mxV^W7{5O=iy8YXM40nK^?Zah0W$mIC4?gnG@-F1@aAe~N?)%K-sAz7D@ zHM{hCm#}5Ac}6z%DOJ3lZJ2f{4;Z)uI>^qfw%H;N&L%Tkjns7tiL%^&GLgQmN&RJk zk$>&3VlXmaJ=d;hM5l1<4h}mT$fl?!Me*Al{uUbFVv$pH`W zdnBt6dA}rsL)c3oEJ72Mr|v*6`?;Zg7dsTlOn6i7u=9S3iQ!go$0m_cz3Z9{5!Vh7 zzQN-)D(cE~5#u+Wi>=cgQr8GveA!=sBRcJdk5y%v>x_mq#nRWUQcdCXeo4|$I^&{j zdRxZa^nTi!-S+fWT67d^b0wPImwd_)-9AZFZEJ?(D{jFE8*XzA-)yj0!(A?D)7q^i z#XxpPVf(>#AKKlPSmzw8;Awj-H(Fmaw`tvgF$+m-l-?DZ(?+7k&pRzSZ3JpIVjuWT z;4S6Zdczu}a>4It!kxQhLbh&eS8(7*VLbPzC*dz<#9tTETCkC5rw=B+N%6+*gG2J; zo9%w&MP*Fw%hT3qxPQsqBfLcE8Kr;M8h7b9ISpyjzffuCk=dOy z-==w@Q4hXP{PAHta7`Cn_h@W`y~vV<*ToCNP{y73y-}-q)7kd zgd{X6c_LCr<#d=tBqohBF$rfc*r+u#`_4yckFY&SjE1NRWCmwyA!1!)l9AQU&WuwbYHp=Q`#%3j>uSAlOJMh8By0kGUFpK)gM%cfom3Fyh_>Kuj z*IRp$badFeVjJuI&1Y*~Tpq&WN`>;#f=XYEQv%Yhm1_w)3F&TwKPw__uvOn3I!Q*7 zSr#%#hdaNLi1gJ^M9Qcsj=WZ>R+B)kuk2DdWEBsY2y%HCCth*6%bVp=mshS(e#uE; zwn9Ov!=-Z|Gbxml(2_I(jXS4~#H5{_m?Xup;QL+J1Ht0^69pva@D4(G%?QEU)4)q9 zLa=e1Dv`w;=*~USBQA?F-Yg10hSh__g6rCQ{ zu`o=zIh!)hQrsNL6OEpeXvDtKG zLelRI_+e*Sk%Jrgk*3*Zk2fT)*vygDobQ!OO2R9(Yc9ddReFjAF^SsBWaUvUY|{eY zrEuX6n^O{*>_d~@0u@nUBmw`L@2Q&yA7`zDeQ8CSNKkkADWkh`PiI#@Ihmn#gNy^{ z29kx9Mt=2&b(abj`AEiNzuam5x4k9mu*6u$>#7EguBwS9f1MW8wll?N z%wL%EZqpRCtV;}HFGM&#(;V>`EiI56*8h3TCYX;z;nsN><#l#g@u!1zCTOT#06^_7 zD1;@%rKOr$;MI^O_8#h$%SaBzrBUE5tF=+S;L7~^LhjDeHayrnU;Z(( zeI0PRj-1LMNyZK8%#)Z9hfw@yj=}_Ox!Ni9ulptIU7TkdmQv+?5|;eKKvX@}Vf9$H zmEw3Nkr{9-Y$GAZoA&6oB&Kv7s-w;J)R-kEeBzjE*5?#axYo3oe^UugbfRT^6`R-MT@6>x2*ivTyb3_U|6_v2_7|9fw?oF=z;;3*Y#>a&*$0)XVeUmy`BP0yxp6c=|g6 zpHN>PeBUbc!MCqNfT2QO9C-8rPZi*Tje_0J*8`j0)X|ACQ?d0D&rW*P5?q*A<2NVL zq|nZ!JoyZ7bgY(3r|0>yH2xr;~YPBg4Z2(P+*lC>|@NJ4n zUX<*Jo8M54816)|k0n_Hvr<)<5ke>)X9~B%CiJPPtYj>S(_*`#z$ya%Ean}M9;#;L z_~b?Pi-a=%SHF-|MdW}So`}zXz^$4R6#M$XUpvu2^j|oM7D`L^g0j2{JRmr=?5gm?JUhRjC`%=}E2cX;m6=q+Gjdb+ zF}@rEp&cJvgxMATI03SC2|1?lZUpE-4MP78CqN$?@*3Jr4Q-nwbj>FuiAz8w7kZ|R z6FuyDyc@fR8ADah%wQ~7SsYrUVR$rl*#bDMV1}`A$12oaB+})kGl6O}%}p<#rhe@- zyA;7ra|OTJY0jZ$|TT2$IMQ^~z6I?4%!~R{z zsi@=Bc?)fqWj93hx(v`pO3_^?$V4!&z3Awp1L%To+oM>zET-BF+XKUEE}QI{%f{e* zVVD=cgd(Ymb#^fx@PnsG&|oF4SY1(AZUg0l=`4<_^1wb-27^el%B0T_TK#$SDEKk8 z`42Phew;FXmHzoA|G33&SSUlxU?vQ3+N6^<>ib&TqD*kuc0ost)$y zs_-;~yy7e9xV(34l&TJzTB{@!Wu*w_XM=-!?+*)!N_sbmMv}5dPNiRV@&Zn1OcSNs zEjIv-e~`$aeMv=vt1|2A(|=GADwyXgm>*VfAQjmB%`e}k^6xejmRAXc^eWy0yW&iM zPi7`hf?mG)s=(ji4?Wh*mplFf&k}o>p7bV{!&RqK47$>NA&}6fFaD(K5hVIm#Y(eN zMup>eByHUzIQ~m^UzWNzQ@1u|NVC|ppEZa)_WIe&2u9U z^lI7jRFX*ZLf8jAJGp*lUApsrOpU!CV-Dq8k-$G_8FbkAidaUFq%s#&sMIdedCzCQ zJEL*~C^vJDL62Hz_;CJNspInIQ(7t}H!DWv@2L2? z(f=KUTh5*QLs`Gdsjh}xG^t9M2l8B578o4EYDJ4{|=X-ee;mmocX(wmF}qeNOI}np+x_CDKMa|t<%e0?&e~sm%Cvn z2f$i2WD2s&9sf6B*5*EL=PwVBF0!kRVDaBztJr&P&#QNFf%4G(&I_v$9W@=63kN>dS&_+P4o7%ScSH7!Wg$Fo5z19-PK30o4#@E8$SzO5BE~C~_Tm7R+GWqBM}HJ`}kn-#9PG1 z&|Ab%FqdKxZcesuLE-l55Li$97Km>b798^y;S_G8>(i}e$;`}Z^lT&P)V0YTh$>v*q}d*UI|vdVTz@NO4uh@>anZ z`-rx>6|xsfs!-?SZ$l$?8`_`0CDJ|A$crU!w%%Be%{}AKqFtRpx7jFNdP9oP=tLa2 zS|;+?3VI=wS@%axe#73LO?L~*2DcB_X!y4uCC;PmI6Sf1J)zQITC?n1ud$zKjmX!U z{gLlfrUidtX&l*c^_Q9Swy@FcpTk@dB2%U?1CLj+4D`k0*(lq9mu!#m%%MF4kV-G> z8EpK)y(bCYrh>P1Jh>Nj0=!*Pp&45Q)P;Ck`&oEPrk{^qkGwI72923T!_{{Dkdi>s zazxTQ9c;aTAN6cQ?){2x|LXD9PM+dJN2e0K*>r1TT2*MsUSd0{Bx(-5GzATsAi`aSZLt#n+#A&! zq-A_L7PDaxhgwU${z$6~8H)1L0kECQ9a6v=-Nli^Q9l)!IcB zv*Q`5@9MU19~kS9k8%Y%KV~tA-FrrH$C{Q~&|vhNcUt8++R)1jv^ef0jIm*FyO$HN*;eyxUqbV+`F8~OD+ z$gd-5A{vwkv{F*3|X;Yo(kL2X`fyN`AK<%KXFIXAf`<^Bra2d|%yCI*x^#B*`pOkIiHH|!X zzCc*-|As|HtTa={f&dq?BfoP0PqRRvljbHPE8qi;+7Z$EF)H=;boK=!wfeI@!sqML z5BFYQCJxt|Me#Ra`+5qy#nu-cHY~K>Xv955-hEH1Y+cS@U+Q`4RLU^7uGDE= zVUrH0j1GXxqIZ#wa1HFq3yj)6weh~w%)@OjGaF7tua?aknD$v+zAoh2yCmNiyOrpx zadB){o6z^$!ewS=wTqPy%Tr14D^s^f*hWyGii6+g(s{V63oCfhp98J1ghQ16{yz~t z<_W8@&ReJ=&_9vfPVsrbn=Srz4S_5EhLjwI#XDGm0{!Fk*rF0~s8Or)X9x=8*uA?$ zSkW{JRd;Yy$J9c87I7wj;*n|yEaZ4t^`lVX|1J-!w^lxbhpm9z{=2htX$GVm`mvDG z1}a&fA@mJ~QUB=~LZ^n=f9Mi|j<~P1)-3j@4)q<5#vqqz@!7&Ox0Q{hjNGhj*AH+r zG9li=l4bQAlzxk>xZ@^hSpZvCq>jJW9g<+o=>%3z#VC$dkdgW?% zr1ib~`;wN?lcSAQms41FuFz3E>LXJd*(_<@GuVOk)8v#5zCYH8IqbKj621NvDS}3J zbhSPc0mZ9NIht{zg<#eMtIzynAwgROA?_{Qf#N@1+$($Kd`T$Jq;v>}A&lqDa zczn?qV~w@#b!x5G7qc_yTY+5S-i7whCO+7zB`NYhaJ8VvUE~e?NOW%FS6=QHEWttS zvf$+nhDUMP&P_JhNJzmmA1D@nZ`<^6p81EWhoRIJo}3~eIGv>#{PUW9N{z|!2sBjTTkTXwELZ`KRUK#BXvakntwmE!}bo@$*g{w30K=O z@(cbEG$Pi>Nf;-dX-ac`>W+3_^RIN}pwMhN^c@^Ozu<3|E6369M{k?5tOFp;&L_10 z*(jjD^HvBSa5o5UC%*(;Z|367e&~7=D}&6YT)f#~JO2|w{F5*~nK`LCnVCJ(-{n6U zpcCGU^mHs}!ATzqXPQ~**I}&R?`FZt{9z$*XqJ5oYPW6CdjBa_&fZgO>KITd$&;zq zr6QS-<4ME&T?BpqIC2CHCh}LqAGVxMz*c|7Y;`Bcemdzm1h=5F zjb9yXp98e4q^&#l@Dx|}J@28}_q=;HqU?0zm({L*Ce-pTBdFV#YuR@kayhFEI`!ef zC!1pg$I+i!#_yWw;Q-m#DY!ArAPNFM9>>Kj6u!%uF(J@_TscLH%Q;WaT$ z&2LM1{RSlZ8LYGAxc~0b_{TZ)>OAI_t}Zi+-Y3TE&i`Z=XyED7$vW9 ztFOk*?Wl8xW@og`7^!vO*8pJ=E9bR`y12E<8}3Et5oeA#{9{xiGj{kArru?=5pwB+S85%4sfB)H zHmMx<+(*Pl<;aZvo5HVzxkm@Sw)O{8WiYkJ)leE7N}LYII7JB#Lkky%bx?L>?lU+g z7go}lxzC_A7gkbj;peY%pTXIA;osziAIybS!*#jO;Qm}#NtYFVPR)G=OY*`!dErvj zrFotDT{8O_%+Jf#5r%`tT>jt>dEtNLg-cV}N(9w$d36pdOj?jvYDz9Ccp?{84f{l` zUsxEQq~>V8Stn5EpXpxHv_~quR#WW1q@hP8h*csx)zeL}U*R8pFtNzxQmBim(==d1AMN@ifG&A4` zl2e%>`|#6{$_&u2&O3+fK>+6qU$LKqzfVa=$R~Y^#mnn2k10cTu*4zTxvVApSe``s z0KEJhd@5!9uUYnSC6>R)<$r3CRs9}6`T6%({trgkmArAKjmdQIT>x5bnTM>(X3h+I z+@cQNm;84WGu!+{VIi)11{C?TD{@^_#4^#BYh1aWdnj@RMTCJ`Z(RAPu9N7@rLNRr zQ7H=S;tE`;0;f}e%)47h8eQHU?PpkhwutNaS;~K)%U@ynt6csUx~$^|^veG&<^Ob~ z)n94(XR)p_1~e^9UUdZS-=Cp7EFC%Qx>Z@z5oYh}|mub*%gic)B|u|*#? zbvbeACksyUor7NqTTfGhqYV|*pY{pJtZ1^VCg;Fck!S}{JBE=?8HS0B4wmL;i-tD- z+yc2q8TnnPU-H}#TQ~+8X8*_1+qqyPpU4Lq0WEjr5BnILx zCDKiI)65&*MRfPuy>d?N|rPtysfq0DX*)?jnQ7gzmd%H-(faynPK;Yh0FjZ zGi9^nF^me?OGs@>qsr%BtQHU#x>O|#tu320#R6+hnZXSu(6J)jci7zzzt+HV;M&T| zr8Wn&zw&(Q!)~JUd&g<}fcIvrsKeRYd)J%xS|ChUk!lj<9I$w8%OEomyRA|Y&eNN7 z1Mu`-NJTvIgP+GeWOQ_UoxBe@vgrm#1Vb{@Igindpb)a*vUQ+Jt;eoftacW3RV<#zp=7M{Cw&^M&o;P! zwn3{>ZK9O>T^rR~lUVb~OT>x03%!gA1kYU15A!PWQ^YV6A=*zUL22Z@83YO9wR{Uy zpWi$6GPMe}@uA;^WK!n&`sG{wvUC-;?r5g+p?9j!L3F%T8Hu}rUl~yWjdcAHa&Ov4 zBiZLsh4r`4bV1SXLgn_V7bD#^Vj|I5d*@3cZwM?czc!4NH$MEMlpl@9-w2g5A}nAT9zGR%`he*dW%& zIXjfo3GPu^G}O=7M)xTV+G{9G4o40K?LC4*Y@Z_j{Qbn*F0X8+Tx8d=P(=WO$v{bkeQq_?y?`yFZq7v@42eLnu7)7EaCqGlF!U{N6?Z%6L+r^*t$M{~VE)U(G?z_CS z&!S>o>8f)VUOrHvG{{jQ49%=C6IHe9&u+ei$>zAD2oO?qXug3xAikSp-FD&U6%7aw zlu|eaXhr%>|E02xiW2{1;Ad;}#a-qTqtpN9`t%dY^n*HB*(JCCj_$`a@*WNPiu`ly z3U@yS9Rf3#O8n~K;WXxh6TV@vpYZ&DtYR!SN~8WT=-SF=3)G9Hzw(zKK)?Npn9yJDBc2oe+Yg*s*iul zxsBbcp`WwpCpI%-Ki7V(pr7E^zn99}bQ37PF%Q3-z)~-FYCdSap+5amGX0R24+8`) zssV2~BH?`p^MDt@EA2fMo)hWf(IftJ+5wN{$q_FmQLzb+;|ZuKnFnm<0H-%1IWqrT zM1J-ALL{a%w^mA06szvyH`ejom*I(d<^v*p%b|%HqB{Y)huRp2k{d(NKwME6w-(4W zERDpyVK@rqX5yNNd)ngMTARxJ#j%IXu%m9JSZ0bJ9^s2=_!&FyaYi^ul{=6H_D8Ny zBm_4p%XyZ?k;|P}){%kxIo`_I5}tv1sdHATbFJ<_e!0Aw zBr|7J*DN1j4H`c{hCF#V58w?Lbh`~=GJS?IX+fXt9zU8Nq{{IPJnb}nr}2&cJGV&r zhO1&4Xj1>h(De%|T1Z~Z1!a9HuCCbl$FYuIW34Nmz7AVPc=~vF`ZFO;`V~*-SAP*tS9ES2{CXwof)9reIrBE6X;3@{Y^=iZIuGLr-eV>ucu22f&vLrP zOc6rFzfV#*{Y|(#NP|-xg39g z&7ZW7@dM6{BYysw=fL0H%UK@eath7F>a43tFBXfF(NKr z+6_nnJxSLfn`PfM-Cw)6))zv$eAe9ArK%^%s%vv%#M9AT$fI`#S7SkKco%Yvz9WVo zGAZ4NEMWLr8SkKsKNEdrgz;1wm-NE&JjT5bma{A8`IsSQ**j~f*3wCse!`i&)TDQFA^EdX5OOpx1LO=+QzJ^oWW`tQ1oJWfpY(UdDok zJ$JKfFl0gXu`CNZ*|DHM@3M`_u`L!Pz7w(_Q95(_fu8N>NAl(8@gIMW{{jCI>zS?z z)%-u^KTW{#h5TpD5D=Efe;&~Hzs!F=6+MO=Kg)j_8NvTE{&UIhg5dvx|LjCd|9kvr z$!VX#e-11Am-)|4*7rXA=NgO7@|D=1BEFIn(@ruAmaN?PH%{%G+{jr+C^vq~vV>w9 zJdq4JxzX=0{&kN~AI?d z3!sJgkn@k|15oBG4#ZvnO|$4MhTgoPFNO{(1Zdzk04mD|sO;;77&3rvyt_AsKKb%C z0eaPjnPycV44u~ppgYR9iJ{*R zEd_~?Ez7*otR%I%Pc(1217n^gWaW~{fCKq3!Pr&1J(NFI;K=A zB~w_@_SuR)%~mv_S4GuucnguZc~(AXTl{%kqs?J* z0Y_}2_ySCRPgx>No<3NZ92@Yqh@nsqg4WW!Vez}1+2Jh}Py5s%w8@cvX&&x=xvQ$m zj`BAJAXyD=V-_Kl#~YMxBqMnI=Z~jwBwuzsYDN#eK)p*@B2XU(RKfU>MtY%I)=2Nd zNcVw}my@#+@(05T#`jzQ6^$?FS#CY?Z<(oPT-zGosTUWF@3?X|EPpAisUcg_=4?&p z_Nr+_ubOsuHJw#h)39ySv{$d1UYuSCQ-!Ok+-gG8@2Ge6Z=>FUrCXg+=7|}Fy}PPc zO_ffa{P55MJpC-crVvkFubPhTRnu?>Q-{@*g{dLGrVyr@UNsf>s_6g+(_w`$?VMjz z2-7B}Q2yBclzR(lXGjY)hH`egpY+RVCE5 zwyqIx)j_N(sn9Ra5q={opZ^}=4`KEGr7GTT&+_R#LRTdFB;iC-RbN?HU+L%7_b?;t zkLq2Yie&5C#p=7;om`{X(*@J5J3G9r=qGN6&jI3k!nm6iM}G(S&k!T?O74otC;_| zx!Z{+aMT*iUl-c%g^1z4ANtea8~o$&sG1V4rqis(=sP^Udjh4t~^mG(gBov|TE8|zo0Yxl| zBApb;xlC4KX2_xc$sp~nVaP-(LHSHB)B{EbLWd8aZqme2qx&!;UD(c~hAaGeXHv?5 z17%f1msCx3CKZPR`zd zpY;MJxWq=1iyjwN2eG#_s%?;q`=0$y?pyu?e<~;$|MK99m%{Nkx@b2fJRNLUTbO@p zn7=GoU6B8K7Vl0|g5LuG@0ZefX{LmPYQ{}A$y@wGL_rLfV$8nSomVKTL4%uKC*{UM za3sRF@{pQx2XDP7SQvj-FGu5zuFiEki5t{4=GDh1`ZwzOz&|msF7)+{!S&Xs{Cdo# z)fWGkt{z4iyJrU%^)Sb*p23Cnlm?F#!sB2$+0`+k#?D(pI&n|x(oE}xMEkc!l~Ad)*va(Cp&u}}h6Hm08~42OJJ~b|%eQ<{`IT?F^5AtLKt(Pk zHJ%|Yv;l{sQ!0+q-vFnm#&IOlyv;LD0lp+4HuP4PaHEBzpPr*1ai!pUAFEaPJ@KLa{z%0y`zVZ$PHclIuN!>X z?|mG;w61C04^Dk0Om_zX!DiQ==wKk2VgOkE=upuvUDJQGJVf+&{>v2*U zg~trfg^$S#zmpgK#fV&2H{X2*Pk! z_B^2AGnK1EnFkksCMt5(t_bT1ao;bjMd!??}D{5$Y z(2*^;JeZRgo|g?T4JL*8!%jU^Soz6$U@r(k3Udz3c5u1CxGCE%UjO^j+Z9xlXI~xp zti_>J`x~4o4NQ44`H&hdy?wqTDNHM|f%V3hCcKMEQzN=kBXG_Tx|G9bZ48w~^ zLs)g|7jLB^DqXo5O82(sqZl`0rRfP(iTLtX{39L3@hfiXyo(wV-kAy6RHl?t|g>7QLoFt%WE>~<0sSVDJghy9`mZ%F@aA?a!Fa{i^@iTv=} zDxX^+vM@px3V|%KJeTHqGfxxFKE8 zl^$2+|BR&0H*36Os_0@(nvQnSzuG~YYvL=?CsftO>NfNCZYggBxBjXwcKg=Y?KG>i z%d*<^Kh>Ph5-T{LX)UVrey@l+o;Dj?=l!PusAD5EUJx7*K`^@3n^;8*xqzT1wxBz9 zy8*I2IYzA}8X#)C@dnPI4S-M+CtKYHLE$b<{;WE7`8R{!_=8hCZyWPNgF5foPV#m3@FY>Ku;Dp154nh z+eI3}9VV=A)TZBL+<>$5O}S~#2XpH_8j}#pYHmHs?o^#l|DeiWM`De4QI&uzYx!z? zW9#0dx;j6IK-?yL$@Zn-j&@sr0(>V17qiT|eW3`DdBmo_8`!{MT-)O&MOW*1XJqIe zrG>W^-2KY3TJK6X%&S{=NlfIK;~85v*LpmSwX(H;&DJ9Cu7%XYj(X?B#GTQHKDpUD zzJyD0O4B4}Ubfz;`Wy4Mvoq9m`_f5y-h)E;y4%&5{zi3m8v+#${=tH5^VDW<=aGC` zS6nZ8ex3Ibd{c8MGvwk7d&A=?%_G#k$Xm$ zYb5XL1votCEmSR7fOD1i#LAS|O}=|>r!42O;ipWzxCCB>gJ7}`Phf&TW*pUQY8k_O z2Dt`#@v!YjWks#KdlQBxyuXX@!Tw~G=k5OE_@1#&+2A_#b+@io?<(wefHxg#n+|JW z*phM7!RUW=pE&6q(KdT0q=cR3Rx76S!~v=iXQkfc2HxmkTR{_}*3^w!S*L$r3HPlD zZ`ahslVL%ZIS_taM(J9w$UAaqaaZl2u2iO~ZGut5<8s<~VL*2U^xNVYF-IMO@u%F@_Pi~HA<*2HdF)&ID` zHStB-W|5~hmRf-Wjs*&){~+*d)4#^O7C%2p@DqPF_LH+|hpUlg>0jfG5}$$Z$2w~m z=45*}gbprZogbn5NMu;Vs3w&OU4u80nUOEu2B z@>2yjFMDRgD~Uxx|HPt~1}2I>%+b@bEt5x*Z^%;e@!JFGRP#IbR(-#^Wsl4GUApf5 zpAJ1(<4o@6wM*A6`{`i!`QhY)_gBUbCy(9NGS>gJWSBa=bY0y~hYqpO%QHtWE?&BB z=26R*J>P@j=Au?_>B}?YYm1ZVjmtjlc_rDtcJs0ir#@F&n_jf+nVz)@m$<;JwJChn zcf3bE$9N^(wVC6J>nGk{@3je*Izv|mGdYT|2-jIr^NXX4`JsrYNLISh~X0{H5H{_t9y z@(x%eGW6hjIF~@@SDqNtP~P%2IAAOd2OOieG6(+|EeRa3A4`&d#HU+erfnpc-hgM? zo3Z|xS?2%zlPx-WUs?!Baw`!hR3!F4pi#~$<1kftUCUd9cO~cW#&V5;GfG>ff zv`K2wT|>Uk;g|On|9iAdZ0knNl18mV4T;RqWrAeX2mVDg@8Y5vnVYMj8n;pvuuT_+ z^462L)fJw{vCD7y53fe@C2T3yF_kS|9QE6OXw%;xQf95}$r7coN1w zsw+51EXMnZjb7$zF{(snt{9a!s`CR3_7{sCbr%`WnONLia+&%SvZqt2A~=oec06C(K+^TT@fY@Eiql;}6 zpu~||o&29nKcPFFOKaL+Elw_aq<4R+KE8C;9`)(PJ&Vtoe~f)U zIBUE5^!+`5$G@YTnXTZWQ_DT)qSuc|72ltD^rK{anT_lZ!DehU?N@GS02ffY@*fH zm*H~mp7sRJAoChe;i{tZT;{;BncAY_37MhYDQ|mPPNY`_#}ggmFGcf()#rG($u<9< z@OwmE{M)m4jnT{--&`@g{N$u%c^ zF7?XzAL{Md@tpY)#>RrN&!^>D@1VN)L9-r?FggG_?ZI<@M6a#eq}OlPdb{&l0<7=OV$7Fm}tnqRj8rVn^KzejxXiE_>-|rH;u(Vie0{5zguFN$yV`KlIg_e zgx6m_?7e2{sbQMG>P^>V&%x`R#8AGO@+Oql#4jwJQIlx*OXFK+mPd5wQ3p{8Acivipw3e0j+z{bIPn}@Z$^qdzG3vB$rp69C zcLT2OZh#;^c$Z}4bDG{=I_DMH=WO~XX(;%%p}yL>iEaj-wM#NRh~6nR>|wB5ZhVsI z_igdbG-E%%Eb-`;o>DjdAle)Jt~|8hljRs~M7ZSlzgQ%PQ0UY3c08BPIxCnVx->JijmEiLsp=%yMDAByaO%{HuUI-uhhn(8Bpe z^by}Sd3?*LV`mY^-$UY99TLZP`x3{t0&+8hq}W7&y+&V2Ez-t+$E z{PE6zZGd?Iw`n;D14Z)&;NBgaoVXpvW1|NCz{>HlR^KdfKkFZupExXNL&&dDDM$7NllAUt*4rfeG z557h%;eI5(Db}I&Udz}ATEmj*Pr{cH;xBNghopN-`KM=u@mIF?D7d&3mpS|Z%%oBy z*7@hYL)C2j>(d8R;!w8*#mxSkIhSHVkn~C_#k|KPN@sAn?S##V%s9CDl+rQBl+LVj z{E`PsbQ0bWE<=_!!%wBZsXD2z_2%qw2)}xr>YF_;NAthWeEWj_%>Ls3{6Z+s>(8-K ze{$U^odLvoz1eZ*q0zib_wCP)GlIPC{4K9L)lq-eW&6{cp6-Nh^cO2Qbzt}K{nC{8 zO>KYiQfV*t@IH-{U`gHl#L>dXh$X2JubY9~YxFvKFZ8Xy*@;XQ`p%89Ilm^_v^O>j zhF1Dp-lFT?&`NvFN(T$Y%ah)AsZ45EY5j<$$7T-S8}-pJZI)*rf(6Iy3$-OUMswt$ zRC;RJ(j{;2)2$~s`$O2}Q9oIlqURcd7K?O8)@plbTXYOlx%Zo-#HX4;+#) zzz?hUktmBty%}hO4Zp!m0wodXJhyuE+854^bF(V3DXs$)BsG}9 zfItn`w9%=LUq@jujekP^_kTLS{oxlSMf2-2@_fP4*3juS;XBe=hg0#1{8kgYvOBm$6W{5HxPX`%b5VIqOntjK$NwC-!ExlAFaGv_kDo6yT%U!X z8<}$dDt`KD*#H0I=cG}qAsdN8?QfK&yst?dVk8oqcma=r^-5Nu%77$V#v;0=*aP?M zVe5uBh`XsR!xbZ&xh@JM<4?4H3FTVrI);-6Tx-f~=o$9vqWj84hn!KB`X7o&FngsL z-Z|Ki(C%AlIBFl*T~nqH6wQfrO{srly+p>PWv6q@P$n{3QuBWgZ}M~CP4oiz(^PMO zd&wKpeYVX;J-@4W3I}p?O*LOK9~`;;4N+42dPP!+)D{)F{5&_(&C&#xx(Dhf*7*ki zro5vPDeshqdQ>hQ{aFKRPISj^C!Nr9W;jpKm~duR`5O+cTXw2TKUmZLKygj`gT)*J z$LbzTw0AdnsXI9^ThxCX|31|J=)tw=J!{j)l*IeR>iebpjhRp~tABbzNsm5^)^h)a|HnEIeYFcXVk2=ruMte0J=MCE2$#Sqe=XtfS7FBZ+&k?gCuJQVN zKhSAj=Q&JIRIF`z(8W3?6Is)~vN%v`gb(op@r{IcwNr8xdUV{GQslI6dvZ0WjlH$64#xS_HH39{p% z@_i)3(HMt}%yWZ=u!ZqM{N-53pTGh>2$ShoBYD-^rR}bf#1cKUvXw{2hNPe8!)q<| zYIgUM75y)(B9+Gvk6o0uU}8)wuXbH&742%TS|G9{(ygU!ca2s(m~Uo=)KQ05bAXo| z+5fV`bLAD}l-Hf^+;xpw^(G)VP2fOflZjM|w)Rg4H5*6e9SZA*6+|H!n9^Q`ySePT0wl9c1r2nm5+K6FOJ{Zw> z=#o_NB5zc!cX0`&+ttVmQ6sZ|<*M!ZvxCc;aB!*V@o8(6A}v2oSf#CG(@5DjOym8neH~#uO?!h&+@M~9o};X<=C^bABb6-)P;{(S_6%%iGnNVm-9ih{H{% zvwEw$J!)GO4W=TmUDaZoRNA`2YnLX4@Zi?Fy>_)qxUBVNuU%(jgon0Xue#Ngjh|$c z+>ni6$SNY4!T1DySZ=)m4m8p4F+u?rZM^^c5;Cdn=i6tGERD_Geh_%T-YYZgaCR|? zi6xhz{rUFRwV~YV9Yr6oP^hk|O?Tz=)3x4F77>j%=3?Z-Org38#?qAF+!Bdi$Lu`7 zG7W3D@mqK^jzvu8>~q;WCDI=)dvn_AWiL%zlSp&O`8tQ3+Tz^r+U3MNQOf!F%lvPL z>r2<2{?n2nRSX(QP5#n#C;fErSM?e0N#0z;9%ylEx6a5{ahu?yWgo6tooHXDGxBG7 zB4z>`m^G{PQQ`u#R@Lm?#i>~Wjd#a&+u5<)1aIid+I^3#$}|)wCaz}75o;d^&Ymbka_jBNT<(%6dQn02fGGM;VRU=fz{E9bK)dC3_w;DVqS}3{tAe>? z(fosHgWrK(Lx|puQf7#W>3y3yc$|VtkJ^&T92KH?C>=^+7?4Hr#+(_$+suEEI7#?@ zm;XPO@xsz|*dQDj;%0&E;X-(+ST@1*z7`%gpG2qo=4$sDbQj6Iy8v`~ird%Y z^x6ZxuFA)!(QHp|n(c{bRsm>skfYhBVjV$Aj%Ihr(d?74Img>kH^gbtj%JA-QxNTF zmgvfYXh*X|4=IRtG)wdcc5FWMQAe{hfSeGUv({pv*&U$S$L!s4Rb2 zskKrJmo@F60{-wVL9aEaMM`O=f`4_;0ah#AwR%a zy7+r+>|_~!dd(SouUb+dKj-U=Bj3~&MrN3Cb<&(q-QT8C)1tUSIJPW-n&h8OG}b|M7DI= zjB&^&Ii?twcFS8XO8oO2_csum*{xlsI9s~z;!TU`10Fr+o<(y>?<&-!y( zsal80oIirb3)&s{MQtLX7I&xO>o5AbZoJ)WBYt;fn|?7woyRZDFz%;e#LCsUHa>VL zmL&B;e+mm}`Xji|0r)B!sVs@CENo`Bg4pQ zcI%RqS6#tb6^iXH@Z<(`IS9Duei`~TB+^f%I6d_|HJ`LmB zAK;gUFaqb6<@^O|%4=*~<}YuP4&*IPYx;Q!hO@dUJ)unFGf6C<<4o$GpTbZf^!_2W z>t^|jpKi)pH>^~T!uBycmE4O0dZkf5%W>Vvgc)Cog0N?A#On`hR*Sf{^E8K zDOPVkY5UhRYV>|Cs^RL)s#t1qdX7Fc)Z$~ZwMfR7#yVaivObL)2|H_W<05sCUiY08 z>-?>4O2fg$;JEW`6G1~)uBeefd`G1wmj=~W3zDP zrY>^%&k$piRIH)KtJ5B^CS6~}$z<$`%S~hx#cnlo{?jytYxw_SSg#!oPO|kZG~Qpj zF1e`-Vz}ZSweS7HF|WVP=PQ_x7zbIki0d#N{Y%$LXVa&jchRjtULj1sEGVBAlm{7< z(K9}MPDI!0STs5jedhe7p|rMTwnLc2l-I2*;^S%_3lbOyQ(Oc*+<)&SOEsIL<4@4p)p#A;>38-B)WDef%Z2gQqfggVwjrx~To5UZEtAeNB z&xY0YC;4>xn_l|jOW(LbwRxv7CX+|o)gA$MF{w7pj`E6Z^+*`Brzj=ZiBq0mB=)VqTX8c44j>eLX2Eon;tNajQ(~H>IiCs ze-i?i#sJ%v=Ue{{`B`l?Aj$Z$SjPsIj}%rVFb)3aENA9up4A>%&q;O13?LJq@V+r> zjpPYT`Zy)LzqP#QG}FtVyV|-WTBGAnPaBVA=<}2*O2iL%wsmc?zmtAA+VeV1cpK9> zoMDJ{Jj1_9ud329)8@^Iw59j_)#y=+U4490>)b?piEbPVECQ{l4UyHP^rkVPIxv~bR6Ni3?;bj z*{mhI8i=>k6K+l1<6&|(mdj3OFIyk6cjU0jUI%XUFJR7vD&|&hs_4?t;gzk6>%DU- z@Pt}!Rj4S&jqD=W>6OMfB6HF zuL;S9g>fYnnokxlk^xjIbM{Uw%OyL>Z03M^WRj$q6<(||qBs$+3}==Wi-cKR4Z>gy zY|t!gaY&p}JJ5>1MH9zS4RJJ)(%bG96d17(3?SgM=NIzM+xc^34p!AsD+4>gy0ern z1f%Jd8*J|)82JXj_8B#YoIbnEUva-q{Dz=;jQgF>oDaNvNhO@hrdj#PzT%gH}(zGmy4nO|>M?tGAxX`G(GY@w|6 z>pcx_zPkC9NdL_tZ-YN&B}2wc)f8*lp9u{7DQ&py!jj82=5O=BR_kIn(fpg9V~%0Q zE^>${0Z{z)PXcsE2|rkoM+qb0pc+pofh$uLp@gGFC%YWRI#={IPrl}L2Jwe_2ma!b;Hm!p=vWazU z67|JcWe0G3QN~&t2U@Hoz?N> z!Pz!Q)#br70+wbRE!MdgIfCEQr2n|8xPxT8!(O}Y7yN>JAsm^ptGK)C z*V44sZaNcu88fSBq5m4;yc6Z<{%-hoRxrwH#j;@w3b4XO(@jc)sIIk99;s(2#@SK+!auF)x%T>sFww4PVz&6GL@>x;75 zd9{^a;!sm_x;zxxcQv8Cu1edh=U&;mm1HJlnV_jjFZRZ9WquL2#ko+=Mvr3jlS*ph zT(dV; z)AwsTnq1V=Ke_1Tfyv?rLcA_rG;8wlQb=y(f52T_t(db+<2!hmcEolSHPraFj>i7) z)eXyMI`h`4LxAx7Hjqj&1zb*qoV)&+PswKcpZ2Va-8DRgtG3c}So3 zAIEqzb}J1d`-hP!MV5t;C1E6YMrZ6+9!3rbBll5cMNRwSf%OwtD=ig&YTA$qUTU}D z2i0I6Tr27fvHlqAp~*9!hwmG;Xcpl6JDj(D5x%Dg-`vxk>__x{U*HOv+*69^N`Z};ygCz)-a(L-eYrq6(;n;eQeHUVL~tb$L5?%LNo@! zX?(bI&dV&S_ynS(p&gdu-0QFrhq52x&exXTLBZi+5^- z?qhRyBEj&!Lk*huknEo`U3+yAZ!CTepLvo|D#U*~f^3NYSEqdjpE<9P&v2$R*x?(F zGlh}h%6oXy?C`&4oA_VT8~lctd4!*>e!yy*Y2K79V)qW=s#ntZ+!(SNJr^YPz{{!g-U+o1o$ z!-PKczi*h(hyJ$@6SDY^=>Khwc_R7`Ug6`5@qRD43h{mvEAAK3z44tKzZc%!%K902 z59wZO>oaa`{kLd-H-OB?IW#YiCGEwE&&PR=<}Ljtv?IM~-V#=X3HdZ{3DT#iL_W=1 z!q3BmEY4{viG5A`OcElR51RRKM}EP(1f8jJjU6ZiV-R`@A|3|%f`|i|0|gNaU|j_f z{h8zi5mVrJXthQklRMX|JPtWNGj-J-Bvfg!a~jo!z31|_*>O7=DU)c!o@Q{Yvx|^fUwRi+C(_dF z;H;yKNbk(5Br0UdBctBzTvP8IS{+-ktcF)Sq(Al(&w{r#b(}X!(R|esZ6#y3uc_g* zr^?@-#5_gvesW(_+OjXN^GtjQ9`Buad0Ec8(j0kLG8J*{0j4{C8Oats#qX#AQ9iVVC_{Ej@SmCxTebFWXbx$>8em zU%F!?S#Vo-jAXaBjXOr#5P%lbUuc)?|B@rmg!eDqG5VJ77+s({MictnG3t8vWAKcn?eqyCxBKjuaSRR{_rtlH64 z(-dyH+V7yW{s^w%2hOSBDn;=}@M#w+>TX|aA)TPM`(Y$Ofv-QBx08(Sb}82^rn_BA z)i5YEmj%ODnmx z#zC7*Z#(2yJCQ*p0bN*q(s`8kaAm$4QeN*jGVoG9>d?y^eV_-eFvhX}QPn~&({gj{ zqQ~22k1lHEI{HPxer%K6^mJ5mN+$(gGk&CuUhzAHMzG}@cJ}^E&tP|jEXC+i1A!p*)^<+c%b2kpogs;_!B-w}I(hnB<8mA+hF5eE4Nd>L`e{s^XboW%>S1oo z(?UI!-4CGxMHzbjvKMU*&Pm5&Aok!RceCp})IqG-;&3yM`!Qc-8paXnWGopXE`lcW zcpssz%9jwaHi=`g8r zB~HXY1UUn&X`Y^p7wYJ&@K}=TEca4;XYEVpKy&(h#EbFLj$wJ}EY}w}=#Tn;C!OL} zLopk)51sg$IMQ>~U-38+HALki{(VL@jsz>N7UwS1XIAyB}YTO7Z=sYusp%Y(NfS5A|9k>bE4&v`QLOnXq zMUVuCRwJqb$V|3^l=Yht}EkJmtpmL&DI5X)@ zE%XQ(SIscFIf-fVW->Y0zm0Z44&R8}FQwektu#Ic)z9!4B7YnZNIdA-umcsAfyALC zR31`>_LBzsLWb3uYPe8+vun{#&I`)}sP{q7gtOq{)g(1I$`fofp3b*&6j6J;ToZOvE%h5Dq zVTBeuX1=OE`M{s){G%uyC$Gc%u-G_33C)OrBfcJ;6XW+t%G&ubl&uM|3 zwxDCBkH!WV2U&ZMcPG?|qVBQ?;8eXu#$Ay(8Hs&jqwO1Sq8_ULBS{85cN2nF#c(D-8hbA}SQ>XFuE5Sm|pZgzteT{b`Atz7Nb1(^QerxHrV|^0?KZ@ir0`NKqbg>rSL-hfLeASI?AP8V)l z`Hk3iwTItR(S9K+%8D*xZZfC;T5agWn8nb(XbxB!=R7QA(8B`wEs&fkqxuv2M1zok zX!k6aBa%y@aW;0>JRe{GBwwM{s`|mJud2wq)&G>*Mhi9tu#mKRl>VV}vf9Elh!g~l zAMSh;6c}wsr6BEf?53??B7|I=Xd?ZkGc6nQumpv~4zj_eBsl7SO}utk2;|3@nHpz9 zjcJ4wb&^d0wSe;BtTVs)29FvfCHd77lwFU8ce+S;#F{Qz?@FStlkjG&uS3>Nv_A+{ zLw^wZ=~K@BLCQ(i8GUb=#WZA(*+BE+;&NbMXsiTS;I z#xl`AEmW4nbd8&Pca4AW;Zm+=^{4o=*a>nU9?;;^MKUWT5f!LAKyZHFW1H}lp4Ll?_zwir}B^=P&vrZ7FGnv;%gU%;mXAa|yLjdmgEXuY1a!Cf{?~ z^HF<@s)gDjg7 zI!Rxdf%&TEeS_+30y3wufcp7zqgrq58$;LkXG5H!=x!_e1YMXg;BW`NXs&imywNs-=lwQK z`*xe*gbv2rO_U2aR}OGS1O4DEe4X<7>1(Fbj2XgcG{!&jOY+j{cR`&f1jRz zjT!uCpCG!BuqZhi?1|OE^^R|NhRO#4ImlkYgkmodZHmN{32)YCkXiW=0yDc}P#T0? zaM(oW9Y_+;KC~AD1x!*U?CEz2a+# zSHS!S#43dE+6uYCCrisY8~d~{1?JajUK01lLT-mEyii=Crf|UX>8)>WvAmE zy{MD$#z|}BH6NajE7LV#HSNvb&((+Cb)f;LfQyx!61u@`0sDpV|61-q(44^zzmVJ?~vBJKz; z%ExK>1)1)cwV9fjTg3zM9d57wRysK<7yh5Szqu$I(Tk`|x4xcSnS66&%xZ7zWX+Xl z3ZK3i*$JN>;n{_hmrJ~dj*s2(0&*Af{pv?#N%5tH3wSpq3xlyJgT|tbyv&>AX9{Vb z?1A`|Yei3{aRkQzkYf;~*r&>J97-d;J4qy9dT z1XF`%!~PsJa|T?0=Q2LSrc?0KFw0cOU)o0jUtesOETSWV3=q(D*>3$x9Hjm}HvO84 zbik~HGqvVd6dGc=?zSI)s=Yj&x$0<;sE&l4ToZ$$tDb2_^#f#G(r5zl1r;Bg^FO9? zQ!{wp=6Awf2pCVfp$#>jlByzM1}V&oTS#Gqm^;^^(r7R2@1{pL-%A;+6$160Saf9j z2^HzwhcT0eq(M9*PbtqusA(sCIS2eZuSITHE4X9=)(V~?4QL#{DxJW&%YpJZ?|~V- z8f8%ZiN@FrBHb=X7YWh=A~l0lo!URK7a^eM>Awf*zx(lD@Az#_V;)8p7{N?$<)Ofr ze=_G$9QT=8%Hx_ZGSCD8)B5Z^Xuy9UugA$1;30wC4QWtBkU?d4V8XwaHB0qLx(VI9@mCFf`j4vs`j;9?B8w_tM;hJ^-`WU{-#!tZFt#rLCf z&bv7$c}wZ#ZH;>CYG?)@YQs5^B;yAB@7>M+C(@k8M;Q<(!#+`zLE@K@0KM72yTO24 z&egpDGns}Y^{1-=mXhp$_1sQURc_yAwP5R3v#G8VPB|uRFGo`CF=^WonbWxK5YJ+M zGY{eYnA3P)GI$|Q=y`1`7|~Qc{SM;kgv*c4V!?Q6%0SUXx;IStz)D?r{EFLZYY=+9 zxwa;qIk9{BW#_7Zv!uR^o&@*8k; zKof+|IW*!BIGXy~@Up%zdD*qk)Pi)D>pz~ByQoWuR&qbe>B$9q*7MnCl=-7n5%kd< z*P|ZXdA4I2CdZX*ayQV=9Cu3#L}qfYBU44^;GNV-ktGiZ@T;@#cB7u@3R($()vA&Y8yLh#Ndg z(x6SEs9V-!RE7CyODHSC4_pf0VapeC1c}ySXvrklAgHbmIWz8IhCIuRKNew;(FL6`c0OLk8NhR z)ncA(&Bs1=b%#M8Go5bb+My4!ZaJ3v+b5K0^1qw*OTA+AP=fd}K}C zXV=cop>3L7+iMc0n>ybDLhY9BZO!-v|HW^9Jl8*n@WaX2J;UW3Zaf%pJ56O(gN|2R z5L^fx6Lza(0@?5q-fFdeeG48J4m{=??;C~VQnwo`irfNvenJQAoTJ7=8u2k6`Ywcc z_8vX^5Ayb<7rKgfJn#+pDuZ~}(znP9q!=j3vOSw&(8Sjd1!Jk;NF;6SO*|6IR}f7u zAVs2QGZHkN-|)=PZ{Fv2%thl5>>$<%J6GU8ll#h5p0n1GV>N%BKYq8aN1O)HnO{^;d6#M`djkkEvDu_2=1^PdppQ%08qdh3JE2I--3-=L)Jii)-n)(mblOPN=_0{-> zd$G3(IO@k@=7)De@Ug2=CU+d(^+mtQOf#K57YhoR$#`#H&tKN2FJ|!X-H@>s>tT10 zrzW%SvGRHEeWHMLe00*SsJ>YF+~%M$6>5stakIC=GhL?!R!>#+UBp$t`wR3*#8r73 z&qqL@T{3w3Uh(HPdMe_=e zbZVy!tu1d|q*1~(Mggh2dp7e)(Aim)N zQu2fNkL-M7>{}x+e=VenH;%sp_n7LooQ3(T3lne8T8N*=yBlLS6P;VoRSUWo0X&7E zLz)|nLt;^J6Jt8-FOb(2qi^8#EhdV&?DY+ zrXrZ~&Y3;m$D;QUMYsgyB&!8fBL3SADN&fIs zYQLdsAz&kD-6VcXBZZB#+>NwTCd=JGUBFFMInYG?DjRYC@qPV?crDxcqXsefFB)Vz zyP*lJOzx#dGAEfD97OS+bGX{?Y27SXPHTt*xrb6tKO~|a7ePI_CwjAYy|B;%C*G?QylGewB&pCNa`mA%o_ znBBT7bNGd?wC%ePM{)32O53Hw-`tgXY0?h*@9nlLD`GD>1HqaXmjBT9^71ctH(UX6 zK*oXV3E3MF>%>tf)Qp+6R~qo4%`FYonC^b@4NKvh;Cz)x{LFM$4@e)dIezW-v_0_+ z3-O@7wYvYV?F&XUq~fuc^KLsMe_v+pHd=vTI6(nKoPf+@+u8Z;W_R@K$mis={G} zhltmTY~641FX1Uv6VN=n>+b)kAHut|;`?16#`->fr}X^z-46Qr-6{0(yFJw#b`@Qj zz8{Cq?cTM0*#R7s{29G-v@g>26F!Ewoo@B~=BKM#;e^K5e}l}hM$j!ke%Iq0ao)a% zX5oct{^>iMLeAfX!>8|F4F1lX@6&gjx)~g?dUal8Z!-DmyIJXbmS0IE;Xi#xBo`A2 zAM&E?!o)R=AuL9qSn4I z&vM^K-FBAyj&%fve`LnW$t=xIGjw(3_dwx*5*)~5fC^we%tcEO@OszoFnRHU+bgpg zueb$edx+Lh4_sN&lv(!-nGT$~N{X|CrqcJ|XWKg?UTpg|zqM_0ek=DgGixtRXVvH8 zo0Bi-X2cNfHLC>ObHKIfrbHsiKEl7!_U)hcw0-oaeLy_h_U%QjyFToEd}rIve9Uz& z#PZuAbNVmKEeKfR_|s?c`t&S!%r2AWZMW7vL!a%w@m_GvbZ_1WKC-Yz0wf&6z9c|w(+=CGb{eDd%s`g95 ztW|B7C(Lig-IeQbm)(T_7H#x2-O%lI-$Gp$=Iip)X-^e5V4hpu-QKp#4U0Akd)PR> z9DKHt*wFv?d1}Pt>?ZZ`ih#$ho{Q-5FNQ1EsgG-YkAF(q?U^J}&u>;AyL^u?9p3I4 zB2v#T{0^G&oreIO9GFX5@*5Vw7O;d5=5CcO-i`~?3uIT{7?FVpkKPP410kgL2#($p)F8!GE08?(2~oDeov z?2{0}Tt~Z;(#Ty*?z!!GH)~$0L1f~+_YgXBBcHaBMg!N5 z?Vq2fX|Lmr>m7m!?8NJ{+9Hox9%L?P} z=>x!sz=n z7r&rc=6lFDuwKp~IaHxqWQ67v^U(pYFyw_|pAV@vX0VFK!iC?%cf2&ncWk2FGYFh{ zJs+*3gPKWMIt$SK)%y9K@5J-Y*?1z#OSO^bE~8TN+~uLrgdVkvZ%72HvlRb%#-cQ; zm%4bfYCm~@#;20H=>;PMpXTS{dBrO0qoJ?4F%QO6ONKeAf02Sj{{nz@8VJ1#-~y)xq{eLY z)UCuTHY+_}0H{(tr$yYWqBGG~vg*D-$pT)_qLb>e)m<;Y=a-3Z?xN0+4`$0d5fyZ1 z^K+*TddA-4_0lop&Ua1jSp|p-mGV<4zVcjj6*MC!QJ>}dkfxvG-6zS3jOT_rlu4Z9 zLn4Xv&rzZw5_z=xPEQ)jtm>1n-)5ZufP)xL#^}c1EaN6Ta1S?Tu$a5WqpySRY-H%s z;hyx=O{)cs=Oz>GAQ+o*){>c)4seKdeZCGO-aBI78um3~PqX_PZjsLxv0eE5nw|Jo zE6yu&&vBTFb|RLPhBy+%kZ@oPwo={!4nZeBe)~@ z2*?|A5&r!+r*Y)#k?1{APoAOs8I30!J(qzT+o%wzEx-|_M%q*$Kkh)UEWC-jY#D^Q zoPoM{$~i6O@ojH$hamP7h=?PC z8g~27{Y=B3cfGZ1|A7(D!xxXeatMrdUSf=AS1rC!{bhW^BQ$D#h95j1e;zsRVLx34 z4m>NcOB_h-emWoPU7V}y^(PF-&NTc5j~%@NAIPDVu=mlPPs9?walDRFpiQu4a5_=& zudQTwaAKR%1qv9J`1%u2{mfcKKbUh_X8hC6MAYq|$3(?JGDg~gewO6xXYmalVqUi^ zO|?BZ$wm4vcteV}Bfccn?YZSL-iH%iZ>w%|+X>_xdUtxBzZx4gzUQ&H&pg|Z1-JA^!drvm!^00>Zavp*VI}u%gVW>q`5K!z2P(HDN-;aL}T>^<8rNo`6zNZ)k^Bko1 zZ;YKygf2n&h#`PALxxZA9apB*Q-VVS*Hvdylntf(}uD7BZ_jFq;+Vk9$`;KwB6l0v7=IIPN8U1cjaF1D3a zRN9Qiwi0`Jq0?SbKAId|T;bCrslAHlS15Ai9FLsNQ9-%-lG!pbGpOKs&; zo283wmByvjc)HkTEUPGAf}hUP!g3>pDvOMxdS6CMVP#>Jv5YwOemaWkQ)C=AYHV^< zUx1Vlph{LdBwevT)nVyM4o4@NuCJd&mP2w3S+5Xv2}Du7mRHz|jk)%v)n$dwipoio zs>H1=smfVAY0`3A5wPdv%+DKf-kBqf_Hw8Af5eF4lo;0-NA=<{yQDn83SJ^6^K^>{k;jon#v+8o*1JEHV9MlUY zL5-NWB^^hhpttsN+}eu+pOxEe#Z`iWqn)KT^d_$3#*(taB?5V=!)9D+uUcB@EGp$_ z<5?m5*D&ZpY{(~N_Hy)GdOniP&YYda^5@KB`Lprg>^XUC%KT~5=s#wjZJD3P=FHC{ zP+5qcW3`bTV8#XKGGh{hmN@MWSOi{MyQnFvt}0vt?redmaMdE?=+UE%vien%n9(?j zjWhz##m=JY6)s(DUs7FBUB!HN#;VeaN~d3bjAY~gIVwQL!IW9Hl0uY>&8}F%@*pfW zyKt$EO|4i;27#qaBxPb%V8@mg)}R@nfznJ=87oSRP%4&23c`{{C#SIDifZTw-H&IB zD=)EDIoQ}_mXgetR~0&;1x2{WC4Pb-D_Oy@b!E)g`S`vS>;dJML3u}v1n;AHSYvRVI>rFY_ezt z>k7NGw1P8+`eg?u>2V*NK4oG+deME%vvZvjt=6KNnv|53v4I1LxhU6}l2TM!SZQ@u z7TTRvcr_}w5dYC7vI*utHoX^rUQ{a$GPcTN%4>G6H6;})NlKvd$(?BBg$T|+RQ-z8 z!uF8Nv6a7=3Nu#p9a$x?_h-O~)-ee8bry=oAg{z&q-_bxx!`!n$I zOBp8>PnZZ*!!952&*}Rwt3Us*x6$>$`LrBFW1|7vu_zWPuUhrS0f)rN2LaDR4L{DJ-k9iLn>fXVN5lx!q|ktEjjH)`AaD7_t@&D;_hfcu^E1hl`B2 z(OKavEW=%~v8dchFiNnHL!x9;xO|Bfqp=e#cmgYk7r=7Zix(NsgAasTl|=jo`>`m+ z=%R}1a%Ymgd^ksAM4n_!GBV`LEOW&Dg5{Ht`SL3Izoa->fE0j5MzWv0klc6)a-KbR z(L`a3N^M1#kRw?n#&8-Zq`4&{?5hT+qvBgjiWemNhi3juU{iWvQx*}{QPzW)|CIPZ za^OK;6yy2=UaHN>x4qbp16_(Q!p$Ik&?mu@9i*3u`*p$KZRvl~%bXMWn9oa9WdJC73 z*dLi5We*_7s0rB%K`scmR~^eyM$zPy%hBE(9#x${t`t|6sC1Qpn=)_Q4Y;$6M0HPH(`;yWgWRjntb5vG13aKSRPzLg= zb`*oCXO^P)Jv#*T5~@F4Qv64uKUKVGr&eGpAu2R%n9)(_blNK6uA{q`+g4cB8gT>- zMN~chL-aP1gP3rM+*Q>u<~m^qs+{&B>eh4_Wx>R+@c$FtuPeRYg{!>YO)jrD#_jd) zZS;D}R(ri8Z}56w!?Q2&w+=hJoA38}jT`ZY{n;C_x}0{m*E&#&tCCSl7|3wEXL0^9|-*T`5m;IC&eHh2x5Co)zJ zxOW)J37B>!$`4ooKj&`j^Vhk6`S2z?09$ z;YfgysCO;)A1C8?1~xvo0u}(0Lt?>(ZUI>0WE;501E)u13Ca(0BZqv0X6~d18f2O z0w-hgaFx3>e((v0#$UyXQIwFR*DZpa&YYs72!n+V>A_Mqkd z`=K{jMRwq7O)jBr*!}t{|Q@u z7V>?>>#YH7e;Tjk0e0YcKSL7uy#jhb%j;fm@^H|<3p&8A55ONVdB4}|fSu?7+yt2M zsn=ToyU+r-5s)sZ4Zk#(&10GxgJwufpU5VSz@w>HK5Ww%qR8q44Ta6aUn<>P44a?; z#u=u?4Vn=jy&|%foj-Weh;fOKoJhYA(DNtI5kg*+pA&x_z%xoOFQQqEzkSFLU6o&i zYsTMeLAXbNYY)Qh0d8*)?p@&a07rS!Mf|$(7tD_~yAVH^B7PCwAmE4}nF+cGHxfAF z7g)Xw;C2P!Xj5Bj5Uv!sr-E=-0Jjym!19sogZbSXg5TB<{Ps$If#vG}?vbE;zXPr% zDBnnJ@A91t9F;GSADvMf%r6T#;ulDl58S38Tp4g1feVy#EpYb&M`o0+RQ#<4uC)+5 zwFxmL&ahgW88>L9E;G(pr*}lf4a$r&Oo@xkjs{lTf{fZ{FVdBQ*XfiF7wK;YaP`1V zAw*7`p-x*86&E=hX(Rb_rW5rE_uPo*A0z!@UwZ8?*x6g{D_U_GD{BcjeTyv?E=PzsC}{&>^BmKEr#2m&A zp&jqV05>2EUrX2Va+0n|SxT7d3f!{2}# zySdbs`_idygJ| z(M{dnS8>m##Tgp4sOf5*DbBc34_?}$s5m2}BXeoG)w)J58`6{atwJyLULz%A zB%3be?}3ljhI{>wMk$*aJ=-$VCmU+ZrjVkU5zUIhBLnp)g^#uneDx2i{2+%w-QfJp zLN_ehAHi>02vN@uiO-7W<=%*V$hW(b^2t^6fwIedvPlPdK3SAcR-8q97x)1a)TH1S zLeK8Y^~=!`O3xm_*g-PYAH?8~%Y?r@5omw-f8P^=>sU~|(F0_kpz^#JQjXAzG$bDY z17(Eo$aM+4q%J{UrA}m_B?^O7VrDd}L0Sva?n2sP$R=bt{Ow8QcsZn;r$lFk#Aioq zb3(Nj<%_=z^ntDLbyF~|>OX_S6eNck!M34EqkDilTkn>EBrx9LkFEe6?>o=mHcgtq z#sMAm&s6+nERyYWIm&>G+NU&$i~VJzw_LLR4!cRVJg;}z{B4;n#thhu38BkI zA)in-z^& zx`?c}W{vJuh$R^~I0`;Jg2f2wOFfQ$t@gQQO@Jb)di32z-QM{~t3N@MhinahH(o9~a4{7P=hsP`CHb zB%8kgkG2WyTmG_4C)qp^LN>7GLN|@5PYv=|gx`9H$b;(pG4dFM7z(d%0r1CAUy|o{ z_^VdyFv?$tEIs^5#AJ9KPWgRxAYDyX>+mC4E+MCac+77e>GocX=QLK_K=!AXKPK(A zMSD+3I|<(+70JItdAA~Fex{WAb3e~lO=-?B| zd7JimbuN^}=R%ZMR}AX2rQ2JFd;Kp6KxNZdiqhBVrenliBBpwnXrVtFK|@zSf4q?sNYG35r`+%@_}WpzYdAKfRBQHbS`0kVK38Gh*|#1Fe^4Ehm4 zKwkgD=pyXAP8(7i`PfMP>I?Xp{ZMWr?)Co!Ph2E}J($dAAU4?s-PhjlC;b^Zg3$n^Cz^BcX42_AipbGf0D0SgA$1OjItlSnq17SZJD1<bpWWV5_O`(G?&U7yK}F z+_2Q?SL#;7{!&|z3|ArFrvUY5`SVSJekAVe_AVg&7&TwyBKsxsy*e;kYTOX{_B~v_ zdy(&r#Q#kMopF(@n~`q}^1X><{SxpYWxa#TdMfgyI?#MP0pl>2-8R9CWH$)9Uhq!0 zw-NXHhk*|vyWGG^z!M>U6q{QOeq1Iu`1zd!pRyVJxQ)0~<<~2N^Q3ndT7DCbUpDJ=dY(J2J^K;Sl>Gt_%qac^7xcLp5~vk&x~u=>gGm-tS9$p zLe%qxDgJu4Ys2{FRJIWq-}T>$vJoFzn^`x&>$T&aVVLa^Tb!vH3K3h(012((>;wJ7 zXj5TxF;3U%X2%)LaY=J9_%!lKj&^Ze5{4q(bWL2+j5y@&ISylm5ABg_G1+rgWi&y#38*oCrvycD{Edp_<1 z(q+KkuOK*tgQ3t}_?3tM4R8a$18y$*LvWdSTq}p-NPJ$aeGVRWP(%w+1qeC_NqkGe z_t#lR$9GR}zNS!oNye?-`~(gR=C@l!w8}RxnMVA2%v8WD3x5Vo zE4~B21k#~A^68;Na=wiE%lVG(Irv6Bl4nKd$3?=kd*MaFCm($F&c&hNhv&1oH=lwY ze44>$ZLZh5pX%o?&or8ULCk7-ZVKizHQLXId_oWSbY0TzorHS^eGgnySh5p+=~>MC z_r^sM?Ep-J4fDO;bfU#rvy$TL+$SyMoeq5kPOOMeWPmmiw4;cY$AT7ee}i;yA)ck- z8PAhHv-4*pXWCD&5YM(#I`r)|6cd+n_RpQPYkG;<;u8;VuU7E+_{e-3gZN}e2kxHmmO=5w zUhfdf+dpPOUm7W1Amh@$wUKLKanM5$feBn2$%l>C%!PMRwN- z-VT%vLkz!2XI25X8n~mGI}(qrpkKcT>-K^Lk4fwWZVzy0k_^x@dIVl;Xf7-Jr{C^OkF)3&f(=>xo?#!}|G^`&(Ca;)1{mE*eaVt6 zijClF3^jN*^3PuGg9`p=-$os`YrOxXk?SJtG*TO3wK39B%L?E6R}8uqq@^#g>2+|9 z)%jK67<~bs{`ux=dt(^;E7~&=JoKNE1jW42gdu(x_D{S@!=UQPdeD2Ymx5wXbdjxS zF=BiIj@IHsmKD9(x6V_beLrLqW5Pkaeg&_64PNg&;$=CKzJ!U*z&oLOHeqT-`|Um@ zfB7*?_IR7j=;@nOaNooyrvl8AFJ6MZJ4ml@MjBkiD-wF#gnfJuLr(geRbKGH0{xtl zJ|rq%3@r;}UxC-_NU#5!pH~vxB>k;kua?U7pvntAQ=qPV!KVa1UWZVw8noY~#A~JC zMe=fj*Ph$G-YB3r-t3#_%n(x)nu!EWb27y=Cnr{&=1h-H1+P}{T7x{MP#z1x@F?au z7SJ9-x;&g!o`*iJABl8aU$JHz7*q4FCuhagYIFk+6UQLEq$^;Keab|?zg`<|UNQh> zr#`O#7leh2#`K&sU^lRL=h+DS_zkl8RqvM#)$v_0ZvL0o`#k0>`isGz*Ad%n0_zy4 z=cwb^q32#xU~>8V#{*ac{h+?2H~7nJBL8s<_9>wc=$XhXv@bFZ5sJ;dW6B6HC4nbh z0Wy4RykCZvP%-5glm%*z`2w7JTxs}Q4db*GW!Xpw)HyJ=37c34Up7O#N_aAut&6b_ zy@_;l57Lf&4Evk(BJB-WDeWOI{~V6i$Ib~Yu4&OmB&VzAeyE=7Vg@{?I+v7md(o}< zMS7Go3^oe&+D!I@_kR;&a%*&R8uhD{x(MA(8uVB}&h_OA(C>S~>$MTiug82Hllv;X zjZJbNM|r5hinr}9@L^ASePtnbRK|CKr+$ns>aH>oq9rmGUWn z7NaESl9lmnx&k2tK084ZH3qmPJG2kz{Hc6tvJ^905S%7K(`U8rKF!lS8}`&VoOE=1 ztVVybpxZ>hy&C%KdlFEa$VlPx-hP56`UOoXV{d6E-OMwS_ykR)K{x=gnTt3#cCeJPMlhsCF@9 zcj=VBMzFVZz+J0X?vG%v>6J$#*jl2Y0dEBef+@^U!qwG7CxwXoc z)7W3Msn|U6tyWoc8at#@?l_HIqs;yGRMr+b6!&}kX5juW(Iav1iBUG6s(B;crP+2W zdo1Bb4W4|^Pq`My&h=NohR=;feKvHy(cMnylSul%-;sn{g;D@`OYDP*>*Bz z_xZ_m-*5^&{oAQ@@7L#8jdB_74wN$UYEIpvQQUple&}K!_JvNlzYqIKr+gd1?u;;D z+csJta=0>@O|7C1;k`XUql~w#)<^;4rBmQe(exjz+@sMAQ*w2)m9-kpW7IoH%m#W6 z)fkH3fH8xWTsBNu%4TB#!Eeg@Km_Iea|GqRlIQ&@a#c+4hR)kmujc*8n8WA2mY#>t zd)ZaW+5~osR@t7we$gtQ8Q2|qo8o?bGp;_U-snK(pCE_-zK_^P++Hzim+NN#KPc?M0!M z{aLvwfz@f1XA;;~TICZ1yIHTaB(QGu&IHyFseET(Z}e3@ObJNmI-qLqK6 zurbP-e(c9s<(mYyKAzG(6;Em3jz1MN4;cvmq=ESCH4y)O2IVf1d5y^Y^tpgvX_R$Q zY^~yk2ectlxi^Y!?F)2$6y2hPai=LeG;9P~ljW83GEYTgeG$vx1O5`rZq}8(7t3za zpY(DpJE;Fij~_dtl&k_d8R4cqi_* zh>kS&&4~)qzdBI)emtumO!uD;R@P6TzR)y*{ctj2nod!En!q|wQJ$T^o;bBb2UPP= z<&BB#wW0L*gQ3dv6WN|K=>DIH%99h>b;Fd0CbD~m5oXu0tW^`)jb|$NOk`bW66TjP zm0KsW*0avT{Y^>A4QcE^l2Vt(z8kJwGlA_Nq5L?J-FCL}_cXS3q=F)Lj#R+myOGKU zq#gB=2FczZL#W4+iQSIm{s$(q2T}<0NQ&~x1orS)!oM(9d4B@Cdz|v+1a?g-YJ5lP zkWa_6f2S&Mk7us&B&xrT2l~PBl;LCJDMQFKbu?{W{Ya;Lsb^g}rA^QNs#osRvsV4z z(Hq~1P`>ZOJQ2$Ceb`NXlr4SO<~~l|7WeDhwaTh_>_1xN=R6u*uD7tybjq#sSc9TG zJBO`}Ql6N@4n-;7=CTK4l$+FEzAD6P3{!$9J&eV~GkcOMN@9?4}7 z4I<1dgOnHNvF`>c?Rjk9Nrd_3B<0;acF$nt?m6tu!ODYk*lk0UU+1z7r#+(u>YbrP z)IC)BS020n4CNXNd;1LKy?JbXqH-IuNqR;L)Ej3L(NAY9pUz>ok5s;&!#;zg=dtTY zDIe#uO{0|Oa@nC#gt>jR@_H`YHd=Xm4s${D^Vp^_$^#bm;uvMCh5a>|Fx!%qT^9C1 zvhu2hJ&4Ab$6icPKCrN^6y+-mdul9UJ{YU~Y+=`oQ(SY|&T+}Wyq~JvGMB9zPfs_F zS2oOL`}zIXB^>B_5f*^YD~dL>=?U@ludiSE}=QVz^zZ}9t1Cn-

de}z;sm230ZGnvYoJhpp^av+bj zWl_6}CM2eY3BD_gin)8}#c(DiZL z4#lAws8Hk>C7sO{_x+bXkABjndsP2m0(++K9T9g5!%1tIAU&mCgK0*$&a2rI&t8u} znzpF*+Na{#WAP%rzCYq+AUx@Qt@36xbLo^l(aan1ckNTr?CvQ3176yzG&+Lr_H4~$ zGRb#nw`hMJz~1Sj+Yu-AAoYC%6;Nu<~gda$$KNl2$5eqlyuuqyW{Uv5!#IUD@HzYmA zh%S^u%W25tJ$@aRz;Ov2m%woe9GAdx2^^QeaS0rkz;Ov2m%woe9GAdRNg$&^kTqQ+ zU`D-6Ch;nh3=`sCxY}0cUZuxq9G-7cT2bR8;Q!d3~B|0&Z;kT3J= zlKe7ce!=|M8j+wy@@bN=Rzin_1rk~$Y?t{N8++#Kkoh*N^|(ts56;)JU*Iz&Kcj>O z37Ldlvi=C3v zfE}M`_>D*AuRg8)RN$L~@EM;8{MH~m^9X!<5Z);H1oLN-PcXhU48BR?)$#?GOU1X# z`l|Z&d-X%*tHNIOmJfpS{k{63=BL77x%%)y_5Hp2q4HIsMYgN@TZIKPggvm7h<2}) zuw#MvE&gYW_7Kpe{tkw;4o(-gKZ(mCfY^0_{RVG{6xasAFVi%UFSb?ki}rZXh1eUv z3gmNaGvt@Lo{yt&DhSbxJsWf>004*d?gw3$F?ay7vWHR~7R zfsRbQ=1&H?SFJG9>xDtoBxr`k^^exY4T+mSFhOHLS+t`yy0}TvlcUq4&pIhV)2~m) zpj)S$q(SDoRHi;L_ty@5YznCLi7Yz$JTL(FD$0%T?9ym{iHl{}??8hK{xqXUj}iaq zX!|nz;w42zV{r0niG9f!`?$0TI48BzSyEW##3A3Mql@@xrf67Sty(4Bt4yQlbWt;u zK@qr#xTt@`wTk9qE!K-PICj&%q}*0)q~pq$))ZA$vLj?Sre|(dHk^Ws%yHDLvy_eD zrT=t;OKdoW)sAluETxlb&jqtl6H<+%mZ<;cj5Ur@|4P(jXptGo z%{Z#0ykZp2@+`V!6ix`GqeSt=iBTmE;)iNniu2MdD{!D{)u`(7754JtQT*iHDm)a4 zipmPBO4X!vBJQY?qLP5$XfA3tvz)1@P|I#~s`qo{v%bKs)kkI2o_?o_x==nMa&YN! zsjaEf^musWA3Es8Aa#HZAlET1OACqDG5Qi?@TEhyx*{ZA@%b--X>{l}s^8KR-^b_Q z^u$Lpb=>cX@5@wwp(h?E2}{4ECq9~~{!33hyg7B;4S1l#R}73H@o_9Uggw@=c$N_o zZ(tc02QZemI+oz`7XzQ_SUbm`a$Y~PUH_EyJE zWU5~pm_!FJPxVK8;s>!(>8JL@pTt7>NjiA9s$bcY9$s(=`>(_4D;Xj2SVRwT>3m*# z&xbmu?(7f78+#(;FC9BQ41Q=B{25{Ji6QZN_O&Rn9Jn&yevHm42JVtMMEaKU@*~3xep^O1vWoe@NnMgYXL@1fM2}SIe_q;#-2~ zlhDw-y@K$i65k$#Zyt8kd?P=`RExqaE{@pT{mT-s#?@3lr$JGPk0XfB zOyDWsVEWr6UX2SbmieBF2|DpPB;!wNd9DPW%Tv}@rPpGJB7DIr!Jts`Sts#ooKr1l z8}P(mwc8F!|8*GpQ{mMTf1^tf(s__{{UGtz%JC~lpxLWvI9?vNK+t)Nbe)bSC;W?& zzJO!#u1|vG-zX5TN<0m9M6brZ=t0`XgI_m?H!(j@S00okW=Z@f65l21Rs1*vW{8g(uf9am)BBLTJa-F(O8<$(vwH;o3)x=?UwirlAZ^PfFCwg@JZgp$(ZUkT`uu)iv->z0DD8F|EECQEb%9wA^2P% z>DBTqk$5#;PiKA6^_IjtCH;JXW|l<3$3g=-E;^fvu7@Q4IZ3a2HvNam@;@x-{w(=l zB=H_eF9Ew(;+r28^eTVdnSxLDp9EgzzeM8IxWCH(9}-_I=~e!RB);o$!H1tqgNGFf?i$M=@iM>dBAJnA8wWYp(JPd690G*zEa|!2*R(H z{3jI%#urNduSxt(60h2~L&HUR-j{f(M(m{#0zauxFfa1-jo(qW*8|FXs6_rC>Tf0KAMelN`vi^lwi=)3j{LfOsOjS_!O zk-$GC`TQ*Lha_H_QPwb8@UeU-2t`m3VbMN0tAy zWI>;26ZC3%9+G%NiNLGnnUo^vJ3bY7IwOa!O%i{%q^GlP=sIJppf_}h-*lD@UAIX5 z&r8H_Ip%g}YX z#3%k){9Z2ryGP=i5vHMw&X1vMkHoi1dOFjEu5W;+^6ZoIGPOL*#|ykAsGK{2Cw=(5 zT%@P7Rp|Oi;#;l|zxxZo;t)e3{^~j^hBz#A3|JU?dy_%4Yz%7J~qD6^AmH(3x-zxcRm-O~?1^=ccqJS!X;CTXHP%7{~`z-OTc7f+-Yk=3I zD*lq5^h3@Ue2hy4o}Y&S`r9Nvqr4}6P=?I6Lf~6uIe(CNgG1mqOZ>h}L0^8AKw$Xe z*U!L{{eMc@bE*Dp@DxFRlca~a;8(iD?~wQoiC-x3cV8_KuS{Phwq%?vXGAF5wmDCyOZ-$2R7 z7KYv->6_{$p#+r@-x`E(ka*V6lm2$#N&aelMk62po#T7Qi(Zy|GJ^QL$LV{=ox+v> zS57~Gy%r*V6-qu)SwhZ(WxMCfa{dW;79wu8Owt>NiW*7t&4y=FeTT5%b&3fRZp6pfdy!HCUgzp{SYnFTrL43AKJ}uh><2EViH>U~y-B$>_+V8%Scy&D+!#BTX zS&2TTS3EOzI@POpyzWGfAHtGkc_bS)6nLuF`vn5CP(IL^gnR}CmH#y0iN1BcC^$a@ z18G)Dd@!FPv!L&g{$Yx&?;44(eMV&1F7wsSpqmqW#V7j%Px%J7`x1!{&et?k@ClB8 zE&!hR7^VE{WWF0DK3LA%BtE!ZUISheBL4X~@cksuK%j@i845oT_=G@0c|SZ1{gg2H z6&#Ow= zZcn^Fo)$6b8SP;|;7y_B(#Q5VCTIp~vf;A@wQ- z16jWwk`X_Qz*9S_``&6L&Apu7fRECN3aNH=C#Ubti1s~%;y)rUG=2*33BB2{E5gv< z8V0{34E{ZiH?ZWFMfo?%ynYEopEf^qdHxK1sCumpgMXCcF<+h|^-6Y(&n3P?mZw1C z^%sQZKM;7*A9dfIsy|c1(Elk6z9tO*IgUqMMLG!lY#_*Jzr;6PEy@qG#;;$157k~X zx!vpCAMIi6;gw1XUVF!krfDa|loniRA8HPRv4l3zMQH*aG0GoWXw765vCX^G?a9-60rAw}m~-@xA4@ zFAIZT6$bx682mTDQ@-kcW;I_!Vd!!ug~6ZC@fb&18Nc|s|G3Kq-Y8H#{;vqb=Q`lY z4^j8otM=_RP7l43;}M-LN!QnsUfmymnn1Gwm@kL2+oc>2J~)GhE;^@=u3Cw2k@_Ir zN!ApGPfHklpCVCyb$`D)9~lRHsPg26!MBIOQ#?HspWNcm_)6eI^{*!2jlAYP|GSgZ z_hagN3owuT>JG#I6m%S;qzMEQf#>#9#zXj--yoO^e5mr2hQZ$z2LG_+U;Bc{mA>Ub z*K1+ujfmrilG}M<@XUJg?3ojbmKI|Np=||EzWtChD<%Gkw)RrVrlm9x@b zzQkOV>r6>0DlM$EIx7q9&MI?Jc5Wg5!!^!Vk)z0=__vYU1IUB5Ewq?^YhxT!m5h8!&buJEqM^)%Jv%#;NRBb* zW2;AT?|Kyf)_NepG1Mbm&c{}dV^I&PdTOz)q_DcosWxKnMCi+JYsO>A`j{kkEEyf9 zj#ALM&NS=1#c&C2Hu4Zt9fkHv^UR`S$t)WVX0kQcR)#K{Qsp$~rdfeXEwfcgUy~5o zY1Ua*8~ULw+XDJ=YUbARieej25=xmuy3=8MTWHf2QcFWK4v>wt*yb#>m!(^06*{c& zr)_4tPfB)6>hwaVjofH5G$ibR`lIe?wq@0YWmabe=1@ol_rDZ(LAv7Fx z!jDb1W~mxU#--Rw59Jd}rF|)x8$wwf6=n9KOF6HJRueG%4J*~P&sm(DE&fuV&pC_n zzr7}VUhY^cNtfFE|84aeT~tw4EGmaa@CoGD1`f3wpj88!IFp*#FS@X8O}e1Aw$O{I z;Tn8u_!j4nLN__sg>3VbfHuz_n}UvJFUOqTX{|1|FRQlkE|$G?sbzL9I0zxhZkK80 zI+DEtX8pMw5ISL0YLad@+zO5RHLyqOs2LfF|*ZpyLb zFQ)we!(4pAoyo_b8h?%Z_p z`m*U4H;t***>Fazb|?H4yx45cCG$uFDzR7$+nzEJ?|IvnRAOxB_Oh_tXBTzhf!tTD902bQN_+z-h5+u5w(Jxpr?m&%f}vLOfXqQI)CGYBV1(e*ti{w zQ4c?T$qG}5&|w@&{KrI*G3A~`VZySqiXu5QaNEk;Zu#tVs})D^@P${5k>wSYOW_>) z45x*>OtP?CrNqSgj|gr5frSdNI)6yX#!4?6L9?Pu;A(R@%>z(Hkn41mg}ttHRO96dP9l0GS@1i?2X_m*7Z_GUmZFe+@U#(zEO%kN)GVeEd^~zFynz z#$momJ!9U?JnONI1Y}Z!#r*rZN`X~XFSeSk6UL7pH{O~&IwfUXDlHD=I&%=$vRBy4 z?at9<&I+re(!PB3*sxDh!ah-#8d9uTSTVDSbv6;-qO~;|>v;oEPIm0nyUd1j5*IU$^6CWMy^e-v6WV0UE6$Q>Rj zDYTPyth3@0TY1&7b)$KH%aEIDCFO$@vVFQWajLztsM_vKq1_{hrIb`wEVY){%WM?j z@=*m0Z{q{EU@opM3GeW#`%;cAaqzYYIY45TUt=$#Fg2Ym>NI0+_uGeFihXCN5{D2A zNB_-?d;;|if#EkP%U!9**6L(DgYr1ioIA`cSzTW{7CDC~MJTu7chxkUNdJFO-QGnB zqf6Lq^}kWtKP02x)e5h)a&PqiOleWUP}|o22TJ?9Y8pN4=3f`ncm&@ zo0%TEXLffa3t55`36YQxn25lMLx>1~+#wPP0SJdqfB=L!_ujhwsqWsHowxo;jI>+b z)phH8>(>2MRl0d%NjZOE(r|4hUZtTBhu-IgUSo-M4Q=`Tex09Z`)s)>+w1O`Bi3J` z)V!Zf*<*A`+^%wRd;eOJ_N6O{Y)ljX?B;j7s2H)T5hQsNA{1~9tjl<(vd*54y z0AxAY{rymr9(GDhP^Dg-+fYtB$4K!W^y8K5a7jN_G=5HlYE~B>lobEHmfc?mpVv5w z*UwLV*)j(Ed&?NV{|a`hnbUyGd~-|)EVkyv6X+DIa-!WHKuK}GyJ|KJ^vQ|0VLI?# zfu(miW*bBY?5#>JTYQ$k8DLXdPlTEFS^EXbfD|1hYPZjrM0IbImi=(eG{YqJ*&Xmh zTItp6t~9&#zSmtnuhN^)t&Apdl+ez}K@>eEhFmLpblcVl19AqW_%K#gk>c^IdMP$s zOSf87$X6BQ(z`?*mT3zzPZX=^@=SNKV>ot)&F>Bn z`g4uB=hi`oOmf+}@H^kE30Sd?{F`aNGR>05BB9qZkV-yfBnyO-=g5bvw#6xu)fU69 zCgA;$@P!gqYQXu+0{U-ki&#S*ss0;|M}5-tb{r+|CT#5EDYiF|(b)LY3pTM!ujYW$ z+L0z#5xTO1u;&W&yww%SSka#=B{#FUoCQ%I)X;If@7P+X#|LnCtHQYo6+LRheY7<3 zgaEzY#g})8xT^Fu1Jy6k1EziAcrf{f!*|{!{H1d zxi=o%LQ-RHAKbXt23p@T1(!2twZ#}Or|Lija1WVj-?0VVxpm;uwPhqiC86Z?Gskqh zsEhOEj1W9psr!=%JMl*SLD0DM{bn2-H{tGeabdn#?v+MKOa*{Vqjjhfk~Vg3A_Zs@W_dsb0LTR4vf&Oy@7iIeEwIDqxjs9 z`>7i$n1GXFnZ<>H_s`Z$lAGSr3jv9da|Sr$v_4uc8A3Ypy@>lQV`iYx=1b&v7FLMo zsdHz^lQEZGxyF7mFp3kzb9W!?-MDKW+`ipyLydQ1?`|9GJGthJCda0C`e=9exx1Y` z>@IG$n(HV9PI)%!;X@-)hn;YD_vXWgH}*QlYqog7iCW|7q}_9qVrVzzuFsZvam`yx zX5ep_x#>M>jiU4RSplNy?NDwk(0Hv7To!g3`zP2$FNbddYj-lqNH#BH*@fRV_#=PR z3y$c}fK)K!-OKDPgz0q9HHETJ5RU;N4^*y&Xq0P20( zBfDm(+i*A-<$y!LwlEeEJTxnk=Zx>Rn<6<;4F3avSk++=3PFenAqzd%Tmvf`^!jb5R>=Y(>(%ZEZdgwL%Ypew6tGq_}w# z1f$i&pmrYMl(~L5GSeiWRRm*;-kRVN;B)k7-|(&pCsQ;Kl*1MTaxjlvDG+QgvHPnDF zlp}a*7SoEA^nN#tvHul(0do&J@?5-^IXMDL>Xsu1()bA&IGb=+=8Vc-|BPyYfZ zRf4UB|M@{TJUDcQjai9qv~fIu#<)bXiu2c7g-Qoko{Q3l@h!(jgri;@4537+=@6&x zM7L2v+U(^Yg=ZeoI=az3;av{G;XBBW$prJR5X3=rf`ymu!DZ~`xpa)vnCj@-j$kjDK09ugs%TOwwnzhYuGo@E2z5lgrj)!}o$xVrsdh{K8oL9xw3 z6((>%RlH1zJZ6c~mdiMpb>>LWN0i)jusT1$YC6Q(4DNswnztdoA$)?I&>Rok4V(*c zE*1F9eVl)dHXi1us`7szbjvQi^%_x>)*tLUs~?7>8xe;fyUaTS!ttn#;xN6B`q}u% zBI&(Xj?UCERXjkCP$uN*CePZ8bFzA`<$cIZe+Ib_R7zHrOkzS0qeEcJq(*?+ zEBaPRO_y;H*lgJ{O88|pY4SipIN9jYW-&+*nDqB>>>@1LEMYrigMBDcn{0S8I!-c9 z7Efo(F=y{0P=RigYy-$XJ&0w^dM`o>=?RnBsMp@_ zk>s7@9jw5DaZ1m|K|L$>fOvEq$0)#2cyjU`4lr|a^0ujdF1LO>2*+(+3#Il-;%h|w zbyCLgk%U?6Qf>x%%|hiR$3>Q~O>mXyA+*1U?2t!D4yFms>LOC{*RpYiw(WqCnT`Qm zzvxT#HnCCN9|R@w!iqu}4vGnB6r2+?4#qpbj5pD@ypYEM1LVI|^}1Ni0CNOxC~X{g z)I~b0)W@`@I@17nmfH3R7&sI%0n?Mw+$w1_zDtsZlRfqIowO zz^&HJjP(tSpGhx*W(gc;=kOjlO||pFl0;VCL)rn|FfWYGVgEJ2w#^*m1XsB3Ih0Xt4d_3{Y?#H2y6ciIJE z6Le`A0q3v-*{{HTXAEi87F3$z1^F#wX6CVKMGnWZXV5AL7g1hi8QY3WaT(Pb&15!& z>k-09Ea9m>!5|gH<3@87O@b!Q&S{cT5Z;`#Ton7NKO6RK6bw?&!iL%4R(S)Fa zA|#x|@&)@G68MA`UJSm)!N4Z~`!pU*8ckyR8cjSlPa^w}1ieNRdJDWVU24V=+bo*F zsdcJ3?ISmRLoqO(i`G-ztRz?Qw~;*bnew4(AWNzx`+Bi-xNoi&i~x;|0O==;a4o2hELk@)I9WFP7QzUz^~%IRQhSC=_Ho!6qKKa zZ{jsy{;q}Bura6n-@5R)50id+AN%xG%02sOxf=63Jmky&jlEA!!_R0!8@m1XM+>jx zulFjap;O?BlOJ7&M&+mQ@7Vg<@UKq$-SYqJz`y+uf!FYzuN4ba{L$FIIq-k_veZPw zZ+==+O6ZpVFGLfHTe8v6d)4o3N^R58A`5g)OHDdzC zPvJGBYrgaF>3yNQ0{^strT-O9Bc1^;#c46S_WsJJE&OYm(1t6{JJB~Pf7OXs_-CAW zN=rWtcPzZbX8*gkd^cZ()0B5=;D2o4`(E<9Z?@5WKmzgzfwbKs9^;MZ?R|DVr+ zA6a;}oo`t9?>UvzR}E(t-YKT>pFJrb*9RAV3a61jseymtrogXgLL0j9^e!oj2`?=C y+h3P>3jU2h#Xp_bpG2JEo}`rjFTWzW_Kx$h<*}l>C9B|n|CYf2+^Mkh+V~#~w3X5T diff --git a/b01.test b/b01.test new file mode 100644 index 0000000..b255349 --- /dev/null +++ b/b01.test @@ -0,0 +1,26 @@ +* Name of circuit: experiment/benchmark/b01.bench +* Primary inputs : + LINE1 LINE2 OVERFLW_REG STATO_REG_2_ STATO_REG_1_ STATO_REG_0_ OUTP_REG + +* Primary outputs: + U34 __new_OUT1_OVERFLW_REG U45 U36 U35 U44 __new_OUT1_OUTP_REG + + +* Test patterns and fault free responses: + + 1: 0000001 0000101 + 2: 0101100 0000010 + 3: 1100110 1010000 + 4: 1101100 0001100 + 5: 1100010 0010100 + 6: 0101110 0001100 + 7: 0001010 0011010 + 8: 0001000 0001010 + 9: 0010000 0100100 + 10: 0001100 0000000 + 11: 0000010 0001000 + 12: 0000100 0011000 + 13: 1000110 1000110 + 14: 0101000 0010100 + 15: 1001000 0010100 + 16: 1100000 0010000 diff --git a/b01.txt b/b01.txt new file mode 100644 index 0000000..8647a95 --- /dev/null +++ b/b01.txt @@ -0,0 +1,1128 @@ +-- Configuring done (0.0s) +-- Generating done (0.0s) +-- Build files have been written to: /pub/netdisk1/qianyh/atpg-ls/build +[ 20%] Built target cadical06w +[ 25%] Built target cadical_sat +[ 30%] Built target sat_solver +[ 50%] Built target atpg_backend +[ 55%] Built target atpgSat +[ 70%] Built target tests +[100%] Built target atpg +======================== +parsing file experiment/benchmark/b01.bench ... +>> Fault: G1 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G2 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G4 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G5 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G6 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G23 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G12 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G48 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G46 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G47 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G49 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G16 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G8 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G9 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G10 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G11 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G13 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G14 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G15 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G17 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G18 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G19 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G20 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G21 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G22 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G24 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G25 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G26 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G27 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G28 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G29 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G30 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G31 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G32 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G33 stuck-at: 0 is_stem: 1 is_po: 0 +>> Fault: G34 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G35 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G36 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G37 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G38 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G39 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G40 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G41 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G42 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G43 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G44 stuck-at: 1 is_stem: 1 is_po: 0 +>> Fault: G45 stuck-at: 1 is_stem: 1 is_po: 0 +building lut circuit ... +====== Circuit Statistics ====== +PI: 7 +PO: 7 +Gate: 49 +LUT: 24 +================================ +====== local search start ====== +initing lookup table ... +[1/24] +[2/24] +[3/24] +[4/24] +[5/24] +[6/24] +[7/24] +[8/24] +[9/24] +[10/24] +[11/24] +[12/24] +[13/24] +[14/24] +[15/24] +[16/24] +[17/24] +[18/24] +[19/24] +[20/24] +[21/24] +[22/24] +[23/24] +[24/24] +ganerating fault info ... +staring local search ... +sat delete: G3 +sat delete: G7 +start with fault: G1 SA0 verify ... successful! +step: 0 fd: 36 +step: 7 fd: 33 +step: 15 fd: 33 +step: 17 fd: 35 +Cover: 35.71% pattern: 1 new_detected: 35 undected: 63 time: 0.00s +start with fault: G1 SA1 verify ... successful! +step: 1 fd: 15 +step: 2 fd: 22 +step: 3 fd: 17 +step: 6 fd: 29 +step: 8 fd: 24 +step: 9 fd: 17 +step: 10 fd: 29 +step: 13 fd: 24 +step: 17 fd: 27 +Cover: 63.27% pattern: 2 new_detected: 27 undected: 36 time: 0.00s +start with fault: G2 SA0 verify ... successful! +step: 1 fd: 13 +step: 2 fd: 13 +step: 4 fd: 9 +step: 7 fd: 13 +step: 19 fd: 4 +step: 27 fd: 6 +step: 35 fd: 13 +step: 42 fd: 4 +step: 43 fd: 4 +step: 49 fd: 13 +step: 52 fd: 13 +step: 56 fd: 13 +step: 60 fd: 13 +step: 80 fd: 6 +step: 91 fd: 8 +step: 116 fd: 6 +step: 124 fd: 6 +step: 127 fd: 13 +step: 133 fd: 13 +step: 136 fd: 13 +step: 153 fd: 13 +step: 155 fd: 13 +step: 157 fd: 13 +step: 159 fd: 13 +step: 161 fd: 13 +step: 163 fd: 6 +step: 174 fd: 13 +step: 188 fd: 6 +step: 196 fd: 6 +step: 210 fd: 6 +step: 215 fd: 6 +step: 244 fd: 6 +step: 255 fd: 13 +step: 258 fd: 6 +step: 276 fd: 13 +step: 282 fd: 13 +step: 287 fd: 13 +step: 292 fd: 13 +step: 299 fd: 6 +step: 301 fd: 6 +step: 308 fd: 13 +step: 311 fd: 13 +step: 313 fd: 6 +step: 327 fd: 6 +step: 332 fd: 6 +step: 335 fd: 6 +step: 350 fd: 13 +step: 353 fd: 13 +step: 376 fd: 13 +step: 382 fd: 13 +step: 385 fd: 6 +step: 403 fd: 6 +step: 407 fd: 6 +step: 420 fd: 6 +step: 434 fd: 6 +step: 446 fd: 7 +step: 448 fd: 6 +step: 451 fd: 7 +step: 458 fd: 13 +step: 460 fd: 13 +step: 462 fd: 13 +step: 473 fd: 6 +step: 483 fd: 6 +step: 495 fd: 13 +step: 498 fd: 13 +step: 500 fd: 13 +step: 519 fd: 6 +step: 521 fd: 13 +step: 524 fd: 6 +step: 531 fd: 13 +step: 536 fd: 7 +step: 553 fd: 7 +step: 556 fd: 6 +step: 573 fd: 13 +step: 587 fd: 6 +step: 596 fd: 13 +step: 633 fd: 13 +step: 644 fd: 13 +step: 649 fd: 13 +step: 651 fd: 13 +step: 653 fd: 13 +step: 654 fd: 6 +step: 655 fd: 13 +step: 656 fd: 6 +step: 657 fd: 13 +step: 659 fd: 13 +step: 661 fd: 13 +step: 662 fd: 6 +step: 663 fd: 13 +step: 664 fd: 6 +step: 665 fd: 13 +step: 666 fd: 6 +step: 667 fd: 13 +step: 674 fd: 13 +step: 678 fd: 6 +step: 683 fd: 6 +step: 695 fd: 6 +step: 699 fd: 6 +step: 705 fd: 6 +step: 708 fd: 13 +step: 712 fd: 6 +step: 726 fd: 6 +step: 729 fd: 13 +step: 731 fd: 13 +step: 736 fd: 13 +step: 740 fd: 13 +step: 751 fd: 6 +step: 754 fd: 6 +step: 769 fd: 13 +step: 773 fd: 7 +step: 778 fd: 13 +step: 783 fd: 6 +step: 787 fd: 6 +step: 790 fd: 6 +step: 793 fd: 6 +step: 795 fd: 6 +step: 797 fd: 6 +step: 800 fd: 13 +step: 806 fd: 6 +step: 808 fd: 13 +step: 815 fd: 6 +step: 818 fd: 6 +step: 821 fd: 13 +step: 826 fd: 6 +step: 841 fd: 6 +step: 843 fd: 7 +step: 845 fd: 7 +step: 848 fd: 7 +step: 850 fd: 7 +step: 854 fd: 7 +step: 869 fd: 6 +step: 873 fd: 6 +step: 887 fd: 13 +step: 906 fd: 6 +step: 908 fd: 6 +step: 911 fd: 13 +step: 913 fd: 6 +step: 919 fd: 6 +step: 923 fd: 6 +step: 925 fd: 13 +step: 945 fd: 6 +step: 964 fd: 13 +step: 977 fd: 13 +step: 980 fd: 6 +step: 982 fd: 6 +step: 994 fd: 13 +step: 998 fd: 13 +step: 1002 fd: 6 +step: 1004 fd: 6 +step: 1006 fd: 6 +step: 1018 fd: 6 +step: 1020 fd: 13 +step: 1025 fd: 7 +step: 1027 fd: 6 +step: 1046 fd: 6 +step: 1060 fd: 7 +step: 1080 fd: 6 +step: 1090 fd: 6 +step: 1093 fd: 13 +step: 1096 fd: 6 +step: 1099 fd: 13 +step: 1104 fd: 13 +step: 1117 fd: 6 +step: 1124 fd: 13 +step: 1126 fd: 13 +step: 1128 fd: 13 +step: 1138 fd: 13 +step: 1147 fd: 13 +step: 1152 fd: 13 +step: 1155 fd: 13 +step: 1160 fd: 6 +step: 1170 fd: 6 +step: 1174 fd: 13 +step: 1188 fd: 13 +step: 1191 fd: 13 +step: 1195 fd: 7 +step: 1198 fd: 13 +step: 1203 fd: 6 +step: 1207 fd: 6 +step: 1210 fd: 6 +step: 1216 fd: 6 +step: 1218 fd: 6 +step: 1224 fd: 6 +Cover: 67.35% pattern: 3 new_detected: 4 undected: 32 time: 0.02s +start with fault: G2 SA1 verify ... successful! +step: 1 fd: 7 +step: 2 fd: 5 +step: 4 fd: 7 +step: 5 fd: 5 +step: 6 fd: 7 +step: 7 fd: 5 +step: 8 fd: 7 +step: 9 fd: 5 +step: 10 fd: 7 +step: 11 fd: 5 +step: 12 fd: 7 +step: 13 fd: 5 +step: 14 fd: 9 +step: 17 fd: 11 +step: 18 fd: 7 +step: 22 fd: 11 +step: 24 fd: 11 +step: 26 fd: 0 +step: 28 fd: 13 +step: 33 fd: 13 +step: 35 fd: 9 +step: 37 fd: 13 +step: 41 fd: 9 +step: 43 fd: 13 +step: 44 fd: 9 +step: 47 fd: 13 +step: 52 fd: 13 +step: 59 fd: 13 +step: 62 fd: 13 +step: 64 fd: 3 +step: 65 fd: 7 +step: 66 fd: 13 +step: 67 fd: 7 +step: 68 fd: 13 +step: 71 fd: 7 +step: 75 fd: 7 +step: 76 fd: 13 +step: 77 fd: 7 +step: 79 fd: 13 +step: 82 fd: 13 +step: 85 fd: 13 +step: 88 fd: 7 +step: 91 fd: 13 +step: 93 fd: 13 +step: 94 fd: 7 +step: 96 fd: 13 +step: 97 fd: 7 +step: 98 fd: 13 +step: 101 fd: 13 +step: 104 fd: 13 +step: 106 fd: 13 +step: 108 fd: 7 +step: 109 fd: 13 +step: 110 fd: 7 +step: 111 fd: 13 +step: 112 fd: 7 +step: 114 fd: 13 +step: 120 fd: 13 +step: 125 fd: 7 +step: 130 fd: 7 +step: 140 fd: 13 +step: 141 fd: 7 +step: 145 fd: 13 +step: 147 fd: 13 +step: 149 fd: 13 +step: 154 fd: 13 +step: 156 fd: 13 +step: 160 fd: 13 +step: 163 fd: 13 +step: 165 fd: 13 +step: 170 fd: 7 +step: 171 fd: 13 +step: 173 fd: 13 +step: 175 fd: 13 +step: 180 fd: 13 +step: 182 fd: 13 +step: 183 fd: 7 +step: 185 fd: 1 +step: 187 fd: 13 +step: 189 fd: 7 +step: 192 fd: 13 +step: 193 fd: 7 +step: 194 fd: 13 +step: 195 fd: 7 +step: 196 fd: 13 +step: 197 fd: 7 +step: 198 fd: 13 +step: 199 fd: 7 +step: 203 fd: 13 +step: 205 fd: 13 +step: 209 fd: 7 +step: 216 fd: 13 +step: 225 fd: 7 +step: 228 fd: 13 +step: 233 fd: 13 +step: 237 fd: 13 +step: 239 fd: 7 +step: 240 fd: 13 +step: 241 fd: 7 +step: 245 fd: 13 +step: 250 fd: 13 +step: 252 fd: 7 +step: 253 fd: 13 +step: 260 fd: 13 +step: 264 fd: 13 +step: 268 fd: 9 +step: 270 fd: 7 +step: 275 fd: 7 +step: 276 fd: 13 +step: 277 fd: 7 +step: 283 fd: 13 +step: 289 fd: 7 +step: 291 fd: 7 +step: 292 fd: 13 +step: 293 fd: 7 +step: 294 fd: 13 +step: 296 fd: 13 +step: 299 fd: 13 +step: 301 fd: 13 +step: 308 fd: 13 +step: 317 fd: 3 +step: 319 fd: 7 +step: 322 fd: 9 +step: 323 fd: 13 +step: 325 fd: 13 +step: 328 fd: 13 +step: 335 fd: 13 +step: 340 fd: 13 +step: 343 fd: 13 +step: 345 fd: 13 +step: 349 fd: 13 +step: 355 fd: 13 +step: 361 fd: 7 +step: 363 fd: 13 +step: 364 fd: 7 +step: 365 fd: 13 +step: 368 fd: 7 +step: 369 fd: 13 +step: 370 fd: 7 +step: 371 fd: 13 +step: 378 fd: 13 +step: 381 fd: 7 +step: 383 fd: 7 +step: 384 fd: 13 +step: 390 fd: 13 +step: 398 fd: 13 +step: 400 fd: 7 +step: 404 fd: 7 +step: 406 fd: 13 +step: 408 fd: 7 +step: 412 fd: 13 +step: 413 fd: 7 +step: 414 fd: 13 +step: 416 fd: 13 +step: 423 fd: 13 +step: 426 fd: 3 +step: 427 fd: 1 +step: 430 fd: 3 +step: 431 fd: 1 +step: 432 fd: 13 +step: 433 fd: 3 +step: 434 fd: 1 +step: 436 fd: 13 +step: 437 fd: 3 +step: 438 fd: 1 +step: 440 fd: 13 +step: 446 fd: 13 +step: 452 fd: 13 +step: 459 fd: 13 +step: 469 fd: 13 +step: 474 fd: 13 +step: 484 fd: 13 +step: 489 fd: 13 +step: 492 fd: 7 +step: 494 fd: 7 +step: 496 fd: 13 +step: 499 fd: 13 +step: 510 fd: 7 +step: 512 fd: 7 +step: 514 fd: 7 +step: 516 fd: 13 +step: 518 fd: 13 +step: 520 fd: 7 +step: 522 fd: 7 +step: 527 fd: 3 +step: 532 fd: 13 +step: 534 fd: 7 +step: 535 fd: 13 +step: 538 fd: 13 +step: 540 fd: 13 +step: 543 fd: 13 +step: 545 fd: 13 +step: 552 fd: 13 +step: 556 fd: 13 +step: 558 fd: 13 +step: 570 fd: 13 +step: 574 fd: 13 +step: 575 fd: 3 +step: 578 fd: 13 +step: 580 fd: 13 +step: 582 fd: 3 +step: 583 fd: 13 +step: 584 fd: 1 +step: 587 fd: 3 +step: 590 fd: 1 +step: 591 fd: 13 +step: 597 fd: 13 +step: 600 fd: 13 +step: 612 fd: 13 +step: 614 fd: 13 +step: 622 fd: 13 +step: 624 fd: 13 +step: 632 fd: 9 +step: 637 fd: 3 +step: 638 fd: 13 +step: 648 fd: 13 +step: 650 fd: 13 +step: 652 fd: 13 +step: 658 fd: 13 +step: 665 fd: 13 +step: 667 fd: 13 +step: 671 fd: 9 +step: 677 fd: 13 +step: 681 fd: 7 +step: 683 fd: 7 +step: 684 fd: 13 +step: 687 fd: 13 +step: 689 fd: 7 +step: 690 fd: 13 +step: 692 fd: 13 +step: 694 fd: 7 +step: 695 fd: 13 +step: 697 fd: 13 +step: 699 fd: 13 +step: 700 fd: 7 +step: 702 fd: 13 +step: 706 fd: 13 +step: 708 fd: 13 +step: 710 fd: 13 +step: 712 fd: 13 +step: 714 fd: 7 +step: 715 fd: 13 +step: 716 fd: 7 +step: 717 fd: 13 +step: 724 fd: 13 +step: 725 fd: 7 +step: 726 fd: 13 +step: 728 fd: 13 +step: 733 fd: 13 +step: 734 fd: 1 +step: 736 fd: 13 +step: 737 fd: 3 +step: 738 fd: 7 +step: 739 fd: 13 +step: 740 fd: 7 +step: 742 fd: 13 +step: 743 fd: 1 +step: 745 fd: 13 +step: 746 fd: 7 +step: 747 fd: 3 +step: 749 fd: 13 +step: 753 fd: 13 +step: 756 fd: 3 +step: 757 fd: 1 +step: 758 fd: 3 +step: 759 fd: 1 +step: 760 fd: 13 +step: 761 fd: 7 +step: 762 fd: 13 +step: 763 fd: 7 +step: 764 fd: 3 +step: 765 fd: 1 +step: 766 fd: 13 +step: 767 fd: 3 +step: 768 fd: 1 +step: 769 fd: 7 +step: 770 fd: 3 +step: 771 fd: 13 +step: 774 fd: 13 +step: 779 fd: 13 +step: 785 fd: 13 +step: 789 fd: 13 +step: 793 fd: 13 +step: 795 fd: 13 +step: 797 fd: 13 +step: 803 fd: 13 +step: 815 fd: 13 +step: 817 fd: 13 +step: 818 fd: 7 +step: 820 fd: 13 +step: 822 fd: 13 +step: 823 fd: 7 +step: 825 fd: 13 +step: 827 fd: 13 +step: 829 fd: 13 +step: 831 fd: 13 +step: 832 fd: 7 +step: 852 fd: 13 +step: 856 fd: 13 +step: 863 fd: 7 +step: 864 fd: 13 +step: 865 fd: 7 +step: 866 fd: 13 +step: 868 fd: 13 +step: 870 fd: 13 +step: 875 fd: 13 +step: 877 fd: 3 +step: 881 fd: 13 +step: 882 fd: 7 +step: 885 fd: 13 +step: 886 fd: 7 +step: 887 fd: 13 +step: 888 fd: 7 +step: 889 fd: 13 +step: 891 fd: 7 +step: 893 fd: 13 +step: 894 fd: 7 +step: 898 fd: 13 +step: 901 fd: 13 +step: 905 fd: 13 +step: 907 fd: 13 +step: 909 fd: 13 +step: 914 fd: 13 +step: 916 fd: 13 +step: 918 fd: 13 +step: 920 fd: 13 +step: 925 fd: 13 +step: 932 fd: 13 +step: 935 fd: 13 +step: 940 fd: 13 +step: 947 fd: 13 +step: 949 fd: 13 +step: 950 fd: 7 +step: 952 fd: 13 +step: 954 fd: 13 +step: 956 fd: 13 +step: 960 fd: 13 +step: 963 fd: 7 +step: 964 fd: 13 +step: 965 fd: 7 +step: 966 fd: 13 +step: 968 fd: 13 +step: 971 fd: 13 +step: 975 fd: 13 +step: 978 fd: 13 +step: 980 fd: 13 +step: 985 fd: 13 +step: 993 fd: 13 +step: 996 fd: 13 +step: 1002 fd: 13 +step: 1010 fd: 13 +step: 1012 fd: 13 +step: 1019 fd: 13 +step: 1025 fd: 13 +step: 1027 fd: 13 +step: 1030 fd: 7 +step: 1032 fd: 13 +step: 1034 fd: 7 +step: 1035 fd: 13 +step: 1037 fd: 7 +step: 1038 fd: 13 +step: 1039 fd: 7 +step: 1040 fd: 13 +step: 1041 fd: 7 +step: 1042 fd: 13 +step: 1043 fd: 7 +step: 1045 fd: 13 +step: 1059 fd: 13 +step: 1061 fd: 13 +step: 1063 fd: 13 +step: 1065 fd: 13 +step: 1071 fd: 13 +step: 1073 fd: 13 +step: 1082 fd: 13 +step: 1085 fd: 7 +step: 1089 fd: 13 +step: 1091 fd: 13 +step: 1095 fd: 9 +step: 1098 fd: 13 +step: 1102 fd: 13 +step: 1108 fd: 13 +step: 1110 fd: 13 +step: 1117 fd: 7 +step: 1119 fd: 9 +step: 1125 fd: 13 +step: 1127 fd: 13 +step: 1129 fd: 13 +step: 1131 fd: 13 +step: 1133 fd: 13 +step: 1138 fd: 13 +step: 1140 fd: 13 +step: 1148 fd: 13 +step: 1153 fd: 13 +step: 1155 fd: 7 +step: 1156 fd: 13 +step: 1158 fd: 13 +step: 1160 fd: 13 +step: 1163 fd: 13 +step: 1166 fd: 13 +step: 1168 fd: 13 +step: 1169 fd: 7 +step: 1170 fd: 13 +step: 1171 fd: 7 +step: 1173 fd: 13 +step: 1181 fd: 13 +step: 1185 fd: 13 +step: 1197 fd: 13 +step: 1201 fd: 13 +step: 1203 fd: 13 +step: 1205 fd: 13 +step: 1211 fd: 13 +step: 1214 fd: 7 +step: 1220 fd: 7 +step: 1221 fd: 9 +step: 1233 fd: 13 +step: 1236 fd: 7 +step: 1239 fd: 13 +step: 1243 fd: 9 +step: 1247 fd: 13 +step: 1252 fd: 13 +step: 1255 fd: 13 +step: 1257 fd: 13 +step: 1259 fd: 13 +step: 1261 fd: 13 +step: 1267 fd: 13 +step: 1269 fd: 13 +step: 1271 fd: 13 +step: 1282 fd: 13 +step: 1284 fd: 13 +step: 1288 fd: 13 +step: 1293 fd: 13 +step: 1302 fd: 13 +step: 1313 fd: 13 +step: 1319 fd: 13 +step: 1321 fd: 7 +step: 1324 fd: 13 +step: 1325 fd: 7 +step: 1327 fd: 13 +step: 1329 fd: 13 +step: 1331 fd: 13 +step: 1336 fd: 13 +step: 1342 fd: 13 +step: 1344 fd: 13 +step: 1346 fd: 13 +step: 1351 fd: 13 +step: 1362 fd: 13 +step: 1366 fd: 7 +step: 1368 fd: 13 +step: 1371 fd: 13 +step: 1378 fd: 13 +step: 1388 fd: 13 +step: 1398 fd: 13 +step: 1400 fd: 13 +step: 1402 fd: 13 +step: 1406 fd: 13 +step: 1418 fd: 13 +step: 1421 fd: 13 +step: 1425 fd: 13 +step: 1427 fd: 13 +step: 1433 fd: 13 +step: 1438 fd: 7 +step: 1454 fd: 13 +step: 1464 fd: 13 +step: 1466 fd: 13 +step: 1479 fd: 13 +step: 1485 fd: 13 +step: 1488 fd: 13 +step: 1489 fd: 7 +step: 1490 fd: 13 +step: 1491 fd: 7 +step: 1498 fd: 13 +step: 1504 fd: 13 +step: 1508 fd: 13 +step: 1513 fd: 7 +step: 1517 fd: 13 +step: 1522 fd: 13 +step: 1527 fd: 13 +step: 1534 fd: 13 +step: 1539 fd: 7 +step: 1541 fd: 7 +step: 1546 fd: 7 +step: 1547 fd: 13 +step: 1549 fd: 13 +step: 1554 fd: 13 +step: 1563 fd: 13 +Cover: 67.35% pattern: 3 new_detected: 0 undected: 32 time: 0.05s +start with fault: G4 SA0 verify ... successful! +step: 3 fd: 3 +step: 6 fd: 2 +step: 7 fd: 0 +step: 9 fd: 2 +step: 11 fd: 0 +step: 12 fd: 0 +step: 13 fd: 2 +step: 18 fd: 2 +step: 22 fd: 10 +step: 23 fd: 8 +step: 26 fd: 8 +step: 28 fd: 8 +step: 30 fd: 8 +step: 31 fd: 3 +step: 32 fd: 8 +step: 34 fd: 3 +step: 37 fd: 3 +step: 60 fd: 2 +step: 62 fd: 0 +step: 63 fd: 2 +step: 68 fd: 8 +step: 70 fd: 10 +step: 72 fd: 8 +step: 76 fd: 10 +step: 78 fd: 8 +step: 82 fd: 0 +step: 84 fd: 0 +step: 91 fd: 10 +step: 100 fd: 2 +step: 101 fd: 0 +step: 102 fd: 2 +step: 103 fd: 0 +step: 104 fd: 2 +step: 106 fd: 0 +step: 109 fd: 0 +step: 111 fd: 2 +step: 112 fd: 0 +step: 113 fd: 8 +step: 115 fd: 8 +step: 118 fd: 2 +step: 119 fd: 8 +step: 133 fd: 8 +step: 135 fd: 10 +step: 137 fd: 8 +step: 148 fd: 8 +step: 152 fd: 10 +step: 156 fd: 10 +step: 157 fd: 8 +step: 160 fd: 10 +step: 171 fd: 3 +step: 179 fd: 8 +step: 182 fd: 10 +step: 192 fd: 8 +step: 207 fd: 2 +step: 208 fd: 0 +step: 211 fd: 8 +step: 212 fd: 2 +step: 213 fd: 0 +step: 214 fd: 2 +step: 215 fd: 0 +step: 219 fd: 10 +step: 221 fd: 8 +step: 223 fd: 10 +step: 226 fd: 10 +step: 229 fd: 10 +step: 234 fd: 8 +step: 241 fd: 8 +step: 244 fd: 8 +step: 246 fd: 8 +step: 249 fd: 8 +step: 251 fd: 8 +step: 254 fd: 8 +step: 260 fd: 8 +step: 262 fd: 10 +step: 268 fd: 8 +step: 274 fd: 10 +step: 284 fd: 2 +step: 286 fd: 10 +step: 288 fd: 8 +step: 290 fd: 10 +step: 291 fd: 0 +step: 293 fd: 8 +step: 294 fd: 2 +step: 297 fd: 0 +step: 298 fd: 2 +step: 299 fd: 0 +step: 300 fd: 2 +step: 301 fd: 0 +step: 304 fd: 2 +step: 305 fd: 8 +step: 310 fd: 10 +step: 312 fd: 8 +step: 315 fd: 10 +step: 317 fd: 8 +step: 319 fd: 10 +step: 321 fd: 8 +step: 323 fd: 10 +step: 336 fd: 2 +step: 337 fd: 0 +step: 338 fd: 2 +step: 340 fd: 2 +step: 343 fd: 8 +step: 347 fd: 3 +step: 354 fd: 10 +step: 356 fd: 8 +step: 369 fd: 2 +step: 370 fd: 0 +step: 371 fd: 2 +step: 372 fd: 0 +step: 375 fd: 8 +step: 378 fd: 10 +step: 381 fd: 8 +step: 383 fd: 10 +step: 387 fd: 8 +step: 389 fd: 10 +step: 391 fd: 10 +step: 410 fd: 10 +step: 415 fd: 10 +step: 418 fd: 10 +step: 423 fd: 10 +step: 432 fd: 10 +step: 436 fd: 8 +step: 441 fd: 8 +step: 452 fd: 10 +step: 456 fd: 10 +step: 466 fd: 8 +step: 468 fd: 8 +step: 470 fd: 10 +step: 483 fd: 2 +step: 484 fd: 0 +step: 485 fd: 2 +step: 487 fd: 2 +step: 488 fd: 0 +step: 489 fd: 2 +step: 490 fd: 0 +step: 491 fd: 2 +step: 493 fd: 0 +step: 498 fd: 2 +step: 499 fd: 0 +step: 500 fd: 2 +step: 502 fd: 8 +step: 503 fd: 0 +step: 506 fd: 2 +step: 507 fd: 0 +step: 508 fd: 2 +step: 509 fd: 8 +step: 510 fd: 0 +step: 511 fd: 2 +step: 512 fd: 0 +step: 513 fd: 2 +step: 519 fd: 10 +step: 521 fd: 8 +step: 523 fd: 10 +step: 525 fd: 8 +step: 531 fd: 10 +step: 539 fd: 10 +step: 542 fd: 10 +step: 543 fd: 8 +step: 547 fd: 3 +step: 549 fd: 3 +step: 551 fd: 3 +step: 558 fd: 10 +step: 562 fd: 10 +step: 565 fd: 10 +step: 569 fd: 10 +step: 575 fd: 8 +step: 577 fd: 8 +step: 579 fd: 10 +step: 582 fd: 8 +step: 586 fd: 8 +step: 589 fd: 3 +step: 593 fd: 8 +step: 599 fd: 10 +step: 603 fd: 10 +step: 605 fd: 10 +step: 607 fd: 10 +step: 626 fd: 10 +step: 629 fd: 10 +step: 635 fd: 0 +step: 639 fd: 10 +step: 641 fd: 10 +step: 654 fd: 10 +step: 661 fd: 2 +step: 662 fd: 0 +step: 663 fd: 2 +step: 664 fd: 0 +step: 665 fd: 2 +step: 666 fd: 0 +step: 667 fd: 2 +step: 668 fd: 0 +step: 670 fd: 10 +step: 673 fd: 8 +step: 674 fd: 2 +step: 677 fd: 8 +step: 680 fd: 10 +step: 682 fd: 8 +step: 687 fd: 8 +step: 690 fd: 10 +step: 692 fd: 10 +step: 701 fd: 8 +step: 704 fd: 8 +step: 707 fd: 10 +step: 720 fd: 8 +step: 729 fd: 8 +step: 731 fd: 8 +step: 733 fd: 8 +step: 742 fd: 8 +step: 750 fd: 10 +step: 755 fd: 8 +step: 759 fd: 8 +step: 761 fd: 8 +step: 783 fd: 0 +step: 792 fd: 10 +step: 802 fd: 10 +step: 812 fd: 10 +step: 815 fd: 10 +step: 817 fd: 10 +step: 821 fd: 10 +step: 824 fd: 10 +step: 830 fd: 0 +step: 831 fd: 2 +step: 834 fd: 0 +step: 835 fd: 2 +step: 838 fd: 10 +step: 845 fd: 10 +step: 849 fd: 10 +step: 853 fd: 8 +step: 855 fd: 8 +step: 866 fd: 8 +step: 870 fd: 10 +step: 873 fd: 8 +step: 879 fd: 8 +step: 881 fd: 8 +step: 883 fd: 8 +step: 887 fd: 10 +step: 891 fd: 8 +step: 894 fd: 8 +step: 896 fd: 10 +step: 898 fd: 8 +step: 907 fd: 8 +step: 911 fd: 8 +step: 916 fd: 8 +step: 918 fd: 8 +step: 923 fd: 10 +step: 934 fd: 8 +step: 936 fd: 8 +step: 938 fd: 8 +step: 943 fd: 8 +step: 952 fd: 8 +step: 954 fd: 8 +step: 957 fd: 3 +step: 959 fd: 3 +step: 961 fd: 3 +step: 963 fd: 8 +step: 966 fd: 8 +step: 968 fd: 8 +step: 972 fd: 8 +step: 987 fd: 2 +step: 990 fd: 2 +step: 992 fd: 2 +step: 993 fd: 0 +step: 994 fd: 2 +step: 996 fd: 0 +step: 999 fd: 2 +step: 1006 fd: 10 +step: 1011 fd: 10 +step: 1024 fd: 8 +step: 1026 fd: 10 +step: 1032 fd: 0 +step: 1033 fd: 2 +step: 1038 fd: 10 +step: 1053 fd: 8 +step: 1059 fd: 3 +step: 1061 fd: 3 +step: 1078 fd: 8 +step: 1080 fd: 8 +step: 1091 fd: 2 +step: 1094 fd: 2 +step: 1095 fd: 0 +step: 1097 fd: 2 +step: 1110 fd: 10 +step: 1112 fd: 10 +step: 1122 fd: 8 +step: 1125 fd: 8 +step: 1126 fd: 2 +step: 1127 fd: 0 +step: 1133 fd: 2 +step: 1134 fd: 0 +step: 1135 fd: 2 +step: 1136 fd: 0 +step: 1139 fd: 2 +step: 1140 fd: 0 +step: 1155 fd: 10 +step: 1159 fd: 10 +Cover: 67.35% pattern: 3 new_detected: 0 undected: 32 time: 0.07s +start with fault: G4 SA1 verify ... successful! +step: 2 fd: 11 +step: 4 fd: 11 +step: 5 fd: 16 +step: 8 fd: 12 +step: 13 fd: 11 +step: 19 fd: 5 +Cover: 83.67% pattern: 4 new_detected: 16 undected: 16 time: 0.07s +start with fault: G5 SA0 verify ... successful! +step: 1 fd: 3 +step: 3 fd: 2 +step: 4 fd: 2 +step: 5 fd: 2 +step: 8 fd: 3 +step: 11 fd: 3 +step: 12 fd: 3 +step: 13 fd: 3 +step: 16 fd: 3 +step: 18 fd: 3 +step: 21 fd: 0 +step: 25 fd: 2 +step: 29 fd: 2 +step: 32 fd: 2 +step: 37 fd: 3 +Cover: 83.67% pattern: 4 new_detected: 0 undected: 16 time: 0.07s +start with fault: G5 SA1 verify ... successful! +step: 1 fd: 2 +step: 18 fd: 2 +step: 21 fd: 2 +Cover: 86.73% pattern: 5 new_detected: 3 undected: 13 time: 0.07s +start with fault: G6 SA0 verify ... successful! +step: 0 fd: 3 +step: 1 fd: 4 +step: 4 fd: 4 +step: 8 fd: 3 +step: 9 fd: 4 +step: 10 fd: 1 +step: 11 fd: 4 +step: 15 fd: 4 +step: 17 fd: 4 +step: 18 fd: 1 +step: 21 fd: 4 +Cover: 89.80% pattern: 6 new_detected: 3 undected: 10 time: 0.07s +start with fault: G6 SA1 verify ... successful! +step: 0 fd: 0 +step: 1 fd: 0 +Cover: 89.80% pattern: 6 new_detected \ No newline at end of file diff --git a/crun b/crun index 6a6824a..6718396 100755 --- a/crun +++ b/crun @@ -2,13 +2,17 @@ clear -cmake . && make -j +mkdir -p build +cd build + +cmake .. && make -j if [ $? -ne 0 ]; then echo "compile failed." else + cd .. clear echo "========================" - time ./atpg -i $1 --lut=12 --seed=19260817 + time ./build/src/atpg -i $1 --lut=12 --seed=19260817 fi diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt new file mode 100644 index 0000000..c3f90f3 --- /dev/null +++ b/src/CMakeLists.txt @@ -0,0 +1,18 @@ +cmake_minimum_required(VERSION 3.20) + +project(atpg) + +set(CMAKE_CXX_STANDARD 17) + +# 设置编译器优化选项 +set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Ofast -march=native -flto -static") + +# 设置源文件和头文件的路径 +aux_source_directory(${PROJECT_SOURCE_DIR} SOURCES) +set(INCLUDES ${PROJECT_SOURCE_DIR}) + +# 添加头文件 +include_directories(${INCLUDES}, ${PROJECT_SOURCE_DIR}/../tg-pro/src) + +# 生成可执行文件 +add_executable(${PROJECT_NAME} ${SOURCES}) \ No newline at end of file diff --git a/src/checker.cpp b/src/checker.cpp index 044880d..a5aa118 100644 --- a/src/checker.cpp +++ b/src/checker.cpp @@ -2,6 +2,8 @@ #include "circuit.h" +using namespace atpg_ls; + double LUTCircuit::check() { // static bool init = 0; diff --git a/src/circuit.cpp b/src/circuit.cpp index 7731696..f62b5bb 100644 --- a/src/circuit.cpp +++ b/src/circuit.cpp @@ -4,6 +4,8 @@ #include "circuit.h" #include "paras.h" +using namespace atpg_ls; + void LUTCircuit::print() { std::set st; @@ -184,7 +186,7 @@ void Circuit::init_avg_dist() { } for(Gate* g : gates) { - printf("gate: %s total: %d cnt: %d\n", g->name.c_str(), total_dist[g->id], total_cnt[g->id]); + // printf("gate: %s total: %d cnt: %d\n", g->name.c_str(), total_dist[g->id], total_cnt[g->id]); assert(total_cnt[g->id] > 0); g->avg_dist = total_dist[g->id] / total_cnt[g->id]; diff --git a/src/circuit.h b/src/circuit.h index 9ae08c7..57efb16 100644 --- a/src/circuit.h +++ b/src/circuit.h @@ -5,6 +5,8 @@ using ll = long long; +namespace atpg_ls { + class Simulator; class Circuit; @@ -26,7 +28,7 @@ void ls_flip(LUT *lut); void ls_main(); void ls_init(); void ls_random_sol(); -void ls_gen_sol(); +void ls_gen_sol(Gate* target, int stuck_at); // checker double check(); @@ -53,4 +55,6 @@ LUTCircuit* build_lut_circuit(); void init_topo_index(); void init_avg_dist(); -}; \ No newline at end of file +}; + +} \ No newline at end of file diff --git a/src/fault.h b/src/fault.h index 2c405e5..3722f04 100644 --- a/src/fault.h +++ b/src/fault.h @@ -2,9 +2,13 @@ #include "gate.h" +namespace atpg_ls { + class Fault { public: Gate* gate; enum Type { SA0, SA1 } type; Fault(Gate* gate, Type type):gate(gate),type(type) {} -}; \ No newline at end of file +}; + +} \ No newline at end of file diff --git a/src/gate.cpp b/src/gate.cpp index 82b80a3..5fdb84d 100644 --- a/src/gate.cpp +++ b/src/gate.cpp @@ -2,6 +2,8 @@ #include "assert.h" +using namespace atpg_ls; + int Gate::cal_propagate_len(bool x) { int fpl[2]; diff --git a/src/gate.h b/src/gate.h index 577d630..ea3c24f 100644 --- a/src/gate.h +++ b/src/gate.h @@ -8,6 +8,8 @@ #include #include +namespace atpg_ls { + class LUT; class Gate { @@ -57,4 +59,6 @@ public: // [ cal_FPLS(~Vx, fanouts) - cal_FPLS(Vx, fanouts) ] * - FPLS_COST(x) // [ cal_FDS(~Vx, fanouts) - cal_FDS(Vx, fanouts) ] * - FDS_COST(x) -}; \ No newline at end of file +}; + +} \ No newline at end of file diff --git a/src/ls.cpp b/src/ls.cpp index 353a849..67dda36 100644 --- a/src/ls.cpp +++ b/src/ls.cpp @@ -5,6 +5,9 @@ #include "circuit.h" #include "paras.h" #include "simulator.h" +#include "sat_atpg.h" + +using namespace atpg_ls; LUT* LUTCircuit::ls_pick() { @@ -144,19 +147,79 @@ void LUTCircuit::ls_main() { printf("staring local search ...\n"); + std::queue> faults; + for(LUT* lut : luts) { + for(Gate* g : lut->inner_gates) { + if(g->fanouts.size() == 1 && (g->fanouts[0]->type == Gate::Type::BUF || g->fanouts[0]->type == Gate::Type::NOT)) { + printf("sat delete: %s\n", g->name.c_str()); + continue; + } + faults.push(std::make_pair(g, 0)); + faults.push(std::make_pair(g, 1)); + } + } + auto start = std::chrono::high_resolution_clock::now(); - while(num_undetected_fault != 0) { + while(!faults.empty()) { + + while(!faults.empty()) { + auto [g, stuck_at] = faults.front(); + if(fault_detected[g->id-1][stuck_at]) { + faults.pop(); + } else { + break; + } + } + + if(faults.empty()) break; ls_random_sol(); - ls_gen_sol(); + auto [g, stuck_at] = faults.front(); faults.pop(); + printf("start with fault: %s SA%d\t", g->name.c_str(), stuck_at); - // exit(0); + std::vector inputs; + + printf("verify ..."); + + int res1 = sat_atpg(g->name.c_str(), stuck_at, inputs); + + if(res1 == 0) { + printf(" unsat!\n"); + continue; + } + + assert(inputs.size() == PIs.size()); + + for(int i=0; ivalue = inputs[i]; + } + + int score; + simulator->simulate(PIs, score, fault_detected); + + if(simulator->name2gate[g->name]->fault_detected[stuck_at]) { + printf(" successful!\n"); + } else { + printf(" failed!\n"); + } + + for(LUT* lut : luts) { + lut->input_var = 0; + for(int i=0; ifanins.size(); i++) { + LUT* in = lut->fanins[i]; + lut->input_var |= (in->value << i); + } + } + + ls_gen_sol(g, stuck_at); int res = simulator->verify(this, fault_detected); assert(res == 1); + assert(simulator->name2gate[g->name]->fault_detected[stuck_at]); + int num_fault = 0; for(Gate* g : simulator->gates) { @@ -192,11 +255,10 @@ void LUTCircuit::ls_main() { std::cout << "Execution time: " << duration << " milliseconds" << std::endl; } -void LUTCircuit::ls_gen_sol() { +void LUTCircuit::ls_gen_sol(Gate* target, int stuck_at) { for(int step=0; ; step++) { // printf("step: %d\n", step); - LUT* pick = ls_pick(); @@ -223,7 +285,10 @@ void LUTCircuit::ls_gen_sol() { if(pick->isPI) { int score; simulator->simulate(PIs, score, fault_detected); - printf("step: %d fd: %d\n", step, score); + if(!simulator->name2gate[target->name]->fault_detected[stuck_at]) { + ls_flip(pick); + } + // printf("step: %d fd: %d\n", step, score); } } } diff --git a/src/lut.cpp b/src/lut.cpp index 9c121f5..db89922 100644 --- a/src/lut.cpp +++ b/src/lut.cpp @@ -3,6 +3,8 @@ #include "lut.h" #include "paras.h" +using namespace atpg_ls; + void LUT::flip_value() { value ^= 1; for(auto&[out, id] : fanouts_with_id) { diff --git a/src/lut.h b/src/lut.h index 7b94d85..2af1887 100644 --- a/src/lut.h +++ b/src/lut.h @@ -1,9 +1,11 @@ #pragma once -class LUTCircuit; - #include "gate.h" +namespace atpg_ls { + +class LUTCircuit; + class LUT { public: LUT(Gate *gate, LUTCircuit *circuit); @@ -71,3 +73,5 @@ public: void cal_score(); void cal_update(); }; + +} diff --git a/src/main.cpp b/src/main.cpp index a76cad8..11021c0 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -1,6 +1,9 @@ #include "circuit.h" #include "simulator.h" #include "paras.h" +#include "sat_atpg.h" + +using namespace atpg_ls; int main(int argc, char *argv[]) { @@ -18,6 +21,8 @@ int main(int argc, char *argv[]) { circuit->init_topo_index(); simulator->init_topo_index(); circuit->init_avg_dist(); + + sat_atpg_init(OPT(instance).c_str()); // circuit-> printf("building lut circuit ...\n"); @@ -31,8 +36,6 @@ int main(int argc, char *argv[]) { printf("LUT:\t%ld\n", C->luts.size()); printf("================================ \n"); - - // C->print(); C->ls_main(); return 0; diff --git a/src/parse.cpp b/src/parse.cpp index 5e3451b..26cb84b 100644 --- a/src/parse.cpp +++ b/src/parse.cpp @@ -6,6 +6,8 @@ #include #include +using namespace atpg_ls; + void line2tokens(const std::string &line, std::vector &tokens) { std::string token; for(char c : line) { diff --git a/src/sat_atpg.cpp b/src/sat_atpg.cpp new file mode 100644 index 0000000..4492319 --- /dev/null +++ b/src/sat_atpg.cpp @@ -0,0 +1,106 @@ +#include "sat_atpg.h" + +#include "circuit_graph.h" +#include "iscas89_parser.h" +#include "circuit_to_cnf.h" +#include "fault_cnf.h" +#include "fault_manager.h" +#include "sat/sat_solver.h" +#include "solver_proxy.h" + +#include "util/log.h" +#include "util/timer.h" + +#include +#include +#include +#include + + +CircuitGraph *graph; +Iscas89Parser *parser; +FaultManager *fault_manager; +FaultCnfMaker *fault_cnf_maker; +std::unique_ptr solver; +ProxyCnf *proxy; + +std::map fault_map; + +bool sat_atpg(const char* name, int stuck_at, std::vector &input_vector) { + + if(fault_map.count(std::string(name)) == 0) { + return false; + } + + Fault f = fault_map[std::string(name)]; + f.stuck_at = stuck_at; + + fault_cnf_maker->make_fault(f, *proxy); + + SatSolver::SolveStatus status = solver->solve_prepared(); + + for (Line* l : graph->get_inputs()) { + int8_t val = solver->get_value(line_to_literal(l->id)); + input_vector.push_back(val == -1 ? 0 : 1); + } + + if(status == SatSolver::Sat) { + return true; + } else if(status == SatSolver::Unsat) { + return false; + } else { + assert(false); + printf(">> UNKNOWN\n"); + } +} + +void sat_atpg_init(const char* file) { + + graph = new CircuitGraph(); + parser = new Iscas89Parser(); + + std::ifstream ifs(file); + if (!ifs.good()) { + std::cout << "can't open file" << file; + exit(-1); + } + + if (!parser->parse(ifs, *graph)) { + std::cout << "can't parse file" << file; + exit(-1); + } + + solver = SolverFactory::make_solver(); + + if (!solver) { + std::cout << "No SAT solver, can't run"; + exit(-1); + } + + fault_manager = new FaultManager(*graph); + + fault_cnf_maker = new FaultCnfMaker(*graph); + fault_cnf_maker->set_threshold_ratio(0.6); + + + proxy = new ProxyCnf(*solver); + + while(fault_manager->has_faults_left()) { + Fault f = fault_manager->next_fault(); + + // printf("Fault: %s stuck-at: %d is_stem: %d is_po: %d\n", f.line->name.c_str(), f.stuck_at, f.is_stem, f.is_primary_output); + + if(f.is_stem) { + if(fault_map.count(f.line->name)) { + Fault& g = fault_map[f.line->name]; + f.stuck_at = g.stuck_at; + assert(f == g); + } else { + printf(">> Fault: %s stuck-at: %d is_stem: %d is_po: %d\n", f.line->name.c_str(), f.stuck_at, f.is_stem, f.is_primary_output); + fault_map[f.line->name] = f; + } + } + } + + // exit(0); +} \ No newline at end of file diff --git a/src/sat_atpg.h b/src/sat_atpg.h new file mode 100644 index 0000000..afc1926 --- /dev/null +++ b/src/sat_atpg.h @@ -0,0 +1,6 @@ +#pragma once + +#include "circuit.h" + +bool sat_atpg(const char* name, int stuck_at, std::vector &input_vector); +void sat_atpg_init(const char* file); \ No newline at end of file diff --git a/src/score.cpp b/src/score.cpp index a2d3514..1b223ab 100644 --- a/src/score.cpp +++ b/src/score.cpp @@ -1,6 +1,8 @@ #include "lut.h" #include "circuit.h" +using namespace atpg_ls; + void LUT::cal_score() { score = 0; diff --git a/src/simulator.cpp b/src/simulator.cpp index 49defbb..15fe79f 100644 --- a/src/simulator.cpp +++ b/src/simulator.cpp @@ -1,5 +1,7 @@ #include "simulator.h" +using namespace atpg_ls; + int Simulator::verify(LUTCircuit *lut_circuit, int** fault_detected) { // lut_circuit->check(); @@ -33,7 +35,9 @@ int Simulator::verify(LUTCircuit *lut_circuit, int** fault_detected) { LUT* l = lut->fanins[i]; input_var |= l->value << i; } + assert(input_var == lut->input_var); + if(!lut->isPI) assert(lut->value_table[lut->input_var] == lut->value); // printf(">> LUT: %s\n", lut->name); diff --git a/src/simulator.h b/src/simulator.h index b8c9d96..b03acea 100644 --- a/src/simulator.h +++ b/src/simulator.h @@ -2,8 +2,12 @@ #include "circuit.h" +namespace atpg_ls { + class Simulator : public Circuit { public: void simulate(std::vector &inputs, int &score, int** fault_detected); int verify(LUTCircuit *lut_circuit, int** fault_detected); -}; \ No newline at end of file +}; + +} \ No newline at end of file diff --git a/tg-pro b/tg-pro new file mode 160000 index 0000000..7f0eef8 --- /dev/null +++ b/tg-pro @@ -0,0 +1 @@ +Subproject commit 7f0eef881be4d91aef0095e3a889e485a4e42f5d