From 016539cd61dfd777884517dc154798905145385f Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 19 Sep 2025 21:27:53 +0000
Subject: [PATCH] Implement max PB constraints optimization feature

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/opt/opt_context.cpp  | 141 ++++++++++++++++++++++++++++++++++++++-
 src/opt/opt_context.h    |   3 +
 test_pb_max.smt2         |  10 +++
 test_pb_optimization     | Bin 0 -> 66896 bytes
 test_pb_optimization.cpp | 104 +++++++++++++++++++++++++++++
 5 files changed, 257 insertions(+), 1 deletion(-)
 create mode 100644 test_pb_max.smt2
 create mode 100755 test_pb_optimization
 create mode 100644 test_pb_optimization.cpp

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 217fdaa26..6c6145ed4 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -345,6 +345,21 @@ namespace opt {
         m_optsmt.setup(*m_opt_solver.get());
         update_lower();
         
+        // Try to detect and optimize max PB constraints pattern before deciding optimization strategy
+        if (m_objectives.size() > 1) {
+            expr_ref_vector maxsat_terms(m);
+            vector<rational> maxsat_weights;
+            rational maxsat_offset;
+            bool maxsat_neg;
+            symbol maxsat_id;
+            
+            if (detect_max_pb_constraints(maxsat_terms, maxsat_weights, maxsat_offset, maxsat_neg, maxsat_id)) {
+                TRACE(opt, tout << "Max PB pattern detected, switching to single maxsat objective\n";);
+                // The pattern was detected and objectives were modified by detect_max_pb_constraints
+                // Now we have a single objective, so we can process it as such
+            }
+        }
+        
         switch (m_objectives.size()) {
         case 0:
             break;
@@ -1077,12 +1092,135 @@ namespace opt {
             neg = is_max;
             std::ostringstream out;
             out << mk_bounded_pp(orig_term, m, 2) << ':' << index;
-            id = symbol(out.str());
             return true;
         }
         return false;
     }
 
+    bool context::detect_max_pb_constraints(expr_ref_vector& terms, 
+                                           vector<rational>& weights, rational& offset, 
+                                           bool& neg, symbol& id) {
+        // This function detects when we have multiple maximize objectives that are PB constraints
+        // and transforms them to use auxiliary variables.
+        // 
+        // Pattern: maximize { PB1, ..., PBn } where each PB_i is a weighted sum of Boolean variables
+        // Transform to: PB_i >= k => p_i_k for k = 1, ..., max_potential_sum(PB_i)
+        //               maximize sum(p_i_k for all i,k)
+        
+        TRACE(opt, tout << "detect_max_pb_constraints called with " << m_objectives.size() << " objectives\n";);
+        
+        unsigned num_maximize_objs = 0;
+        vector<unsigned> max_indices;
+        vector<expr_ref_vector> pb_terms;
+        vector<vector<rational>> pb_weights;
+        vector<rational> pb_offsets;
+        
+        // First pass: collect all maximize objectives that are PB constraints
+        for (unsigned idx = 0; idx < m_objectives.size(); ++idx) {
+            objective const& obj = m_objectives[idx];
+            TRACE(opt, tout << "Objective " << idx << " type: " << obj.m_type << "\n";);
+            if (obj.m_type == O_MAXIMIZE && obj.m_term) {
+                expr_ref_vector pb_terms_i(m);
+                vector<rational> pb_weights_i;
+                rational pb_offset_i;
+                
+                if (get_pb_sum(obj.m_term, pb_terms_i, pb_weights_i, pb_offset_i)) {
+                    max_indices.push_back(idx);
+                    pb_terms.push_back(pb_terms_i);
+                    pb_weights.push_back(pb_weights_i);
+                    pb_offsets.push_back(pb_offset_i);
+                    num_maximize_objs++;
+                    TRACE(opt, tout << "Objective " << idx << " is a PB constraint with " << pb_terms_i.size() << " terms\n";);
+                }
+            }
+        }
+        
+        TRACE(opt, tout << "Found " << num_maximize_objs << " PB maximize objectives\n";);
+        
+        // Only apply transformation if we have multiple PB maximize objectives
+        if (num_maximize_objs < 2) {
+            return false;
+        }
+        
+        TRACE(opt, tout << "Detected " << num_maximize_objs << " PB maximize objectives, applying transformation\n";);
+        
+        // Clear output vectors
+        terms.reset();
+        weights.reset();
+        offset = rational::zero();
+        neg = true; // We negate because we convert maximize to maxsat (minimizing penalty)
+        
+        arith_util arith(m);
+        
+        // For each PB constraint, create auxiliary variables and constraints
+        for (unsigned i = 0; i < num_maximize_objs; ++i) {
+            expr_ref_vector const& pb_terms_i = pb_terms[i];
+            vector<rational> const& pb_weights_i = pb_weights[i];
+            rational const& pb_offset_i = pb_offsets[i];
+            
+            // Calculate maximum potential sum for this PB constraint
+            rational max_sum = pb_offset_i;
+            for (unsigned j = 0; j < pb_weights_i.size(); ++j) {
+                if (pb_weights_i[j].is_pos()) {
+                    max_sum += pb_weights_i[j];
+                }
+            }
+            
+            TRACE(opt, tout << "PB constraint " << i << " has max sum " << max_sum << "\n";);
+            
+            // Create auxiliary variables p_i_k for k = 1 to max_sum
+            for (rational k = rational::one(); k <= max_sum; k += rational::one()) {
+                std::ostringstream aux_name;
+                aux_name << "pb_aux_" << i << "_" << k.to_string();
+                expr_ref aux_var(m.mk_const(symbol(aux_name.str()), m.mk_bool_sort()), m);
+                
+                // Create PB constraint: sum(pb_weights_i[j] * pb_terms_i[j]) for j
+                expr_ref pb_sum(arith.mk_numeral(pb_offset_i, true), m);
+                for (unsigned j = 0; j < pb_terms_i.size(); ++j) {
+                    expr_ref weighted_term(arith.mk_mul(arith.mk_numeral(pb_weights_i[j], true), 
+                                                      m.mk_ite(pb_terms_i[j], arith.mk_numeral(rational::one(), true), arith.mk_numeral(rational::zero(), true))), m);
+                    pb_sum = arith.mk_add(pb_sum, weighted_term);
+                }
+                
+                // Add constraint: pb_sum >= k => aux_var
+                expr_ref constraint(m.mk_implies(arith.mk_ge(pb_sum, arith.mk_numeral(k, true)), aux_var), m);
+                add_hard_constraint(constraint);
+                
+                // Add auxiliary variable to maximize
+                terms.push_back(aux_var);
+                weights.push_back(rational::one());
+                offset += rational::one();
+            }
+        }
+        
+        // Now modify m_objectives to replace the multiple maximize objectives with a single maxsat objective
+        // Find the first maximize objective to replace
+        unsigned target_index = max_indices[0];
+        objective& obj = m_objectives[target_index];
+        obj.m_id = symbol("max_pb_unified");
+        obj.m_type = O_MAXSMT;
+        obj.m_term = nullptr;
+        obj.m_terms.reset();
+        obj.m_terms.append(terms);
+        obj.m_weights.reset();
+        obj.m_weights.append(weights);
+        obj.m_adjust_value.set_offset(offset);
+        obj.m_adjust_value.set_negate(neg);
+        
+        // Remove other maximize objectives that were converted (in reverse order to maintain indices)
+        for (int i = max_indices.size() - 1; i >= 1; --i) {
+            unsigned idx_to_remove = max_indices[i];
+            m_objectives.erase(m_objectives.begin() + idx_to_remove);
+        }
+        
+        // Create a unique ID for this transformation
+        id = symbol("max_pb_unified");
+        
+        TRACE(opt, tout << "Transformed to " << terms.size() << " auxiliary variables, " << m_objectives.size() << " objectives remaining\n";);
+        
+        return true;
+    }
+
     expr* context::mk_objective_fn(unsigned index, objective_t ty, unsigned sz, expr*const* args) {
         ptr_vector<sort> domain;
         for (unsigned i = 0; i < sz; ++i) {
@@ -1119,6 +1257,7 @@ namespace opt {
     void context::from_fmls(expr_ref_vector const& fmls) {
         TRACE(opt, tout << fmls << "\n";);
         m_hard_constraints.reset();
+        
         for (expr * fml : fmls) {
             app_ref tr(m);
             expr_ref orig_term(m);
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 991fe16e6..6313aeb00 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -313,6 +313,9 @@ namespace opt {
         bool is_maxsat(expr* fml, expr_ref_vector& terms, 
                        vector<rational>& weights, rational& offset, bool& neg, 
                        symbol& id, expr_ref& orig_term, unsigned& index);
+        bool detect_max_pb_constraints(expr_ref_vector& terms, 
+                                     vector<rational>& weights, rational& offset, 
+                                     bool& neg, symbol& id);
         void  purify(app_ref& term);
         app* purify(generic_model_converter_ref& fm, expr* e);
         bool is_mul_const(expr* e);
diff --git a/test_pb_max.smt2 b/test_pb_max.smt2
new file mode 100644
index 000000000..a4eeca282
--- /dev/null
+++ b/test_pb_max.smt2
@@ -0,0 +1,10 @@
+(declare-fun x1 () Bool)
+(declare-fun x2 () Bool)
+(declare-fun y1 () Bool)
+(declare-fun y2 () Bool)
+
+; Create two PB maximize objectives - must be integer expressions
+(maximize (+ (ite x1 2 0) (ite x2 1 0)))  ; PB1: max = 3
+(maximize (+ (ite y1 1 0) (ite y2 2 0)))  ; PB2: max = 3
+
+(check-sat)
\ No newline at end of file
diff --git a/test_pb_optimization b/test_pb_optimization
new file mode 100755
index 0000000000000000000000000000000000000000..2945f325d9873200d56eb7e514d0d188919a1c07
GIT binary patch
literal 66896
zcmeHwd3;pW`S(r86-1VZ1R^2~h=>X?35%cw!!j5YFeO0|mtm3&B$Ca^1cO$K0!j?g
zxS-Tpi_|Jr+orft*SHbfBP!C?YP2phf*RMRR+;zvob#M}&z#Jq)!+O6{&~54$aA0X
zdCqg5^PK0b_vYs3{<*VLQ&KE-^{}Q{#O0kNkvvXF|DJC^@~p{LU;G?l`K*J$rwL4^
z=ShN8dF@V3q`esL0ZREY=_UysDq%}eWg$_@=XLcOEmIV=(j`y%Y`V>syh)qRlenUK
zK2csX=QHS^kC3>cdOq?^bel{!X?9PE*C>auo#Zacm-&cHH>r>Psi?|MHq!se>`#-L
z)i(2$aXypIl4e+nQW<m=eh?}BG36C-zRnw@9+R$TI}}yr{S^7gFaPbu?z9$gd8Ypr
zpULf@sEV@_D$0u|O*o;VbX-MwRbBnK`pJ{VO`4EZTb-3FOdz{__)jr)>imTknx&O6
zHs4BJC3&Tf(gt!m$^Yh-mromYbdRdJi@FBAaNp}44L!HLN-|_O<slimNFO)3!=HmY
zk`ew$xeoWEEW+qI7yn-ky<9or`l)Mf`mSVI#>PG~MS{nV^Py-!lC*n(CBvgICK>*z
zhy0PKKr;FM9_8-x(EqZB{tX`bS9s{Z6i!QK&(wpH<GCJs9`dlWKLR3|{#=i8{T}-J
zc+_jNhx`Z+e36HqpL*E868#~W{U><%XP-y8_j%}f1^ziSNxT($=(!dHRWf_N^}uI&
z*qQGk|Ex#3H+tZgdBov*4}YejQzx@O&!b%$Ja8KClj%9s1OJ6bx!XPDPxC0Z#-qO9
zd&Kki9_6m_@aI;K{&KHJdoA^_=TQ%Pe&bQEVIFZ3^RV-44?N`I&u=~A|11ytf9Ij+
zXCC(V@UZ7v5B+%_`rq-8|JtLU+8*t7i-(>n5BpE|Xs-)B>@4$;r{z_$e(|)2o!@xq
zpY5RsZnk{*Z(jX9;^#q+cA4lA4`m+mV?FGA%|m{ehktJJ(6bKxG}$<OBr57ND+_+C
z2cGNEzB4_>fivN^kxBHQhV~kX)z8rNGVyTKldjL9e}t83`5u=17)h*Y7#|MB?jWyK
z0_iMo1?CjZ3zUY!p=IT@kx;m3-pq>Xs!&m|xFTc)0?R6^s{*x=U^o&8NYSK%i^m5l
zmj_C!t0JNLNFZEdNuazc5~!^XN0_awtDw8`+CVtu;LAc%Ca}D`s+5vTLnTOGD)Lm9
zhAI*OQAkNpXbjdy0xLo#k?OE6Li$4CFu=;%Wl~>-vW(d3nn-zN`Ng3?Ww2h{h=P^}
zidWPw3(>u+pajKpYHjF3QqsNTTBs5-!qm`;psZq*TZiQVxPjFytqBIgk*Wl)hB^4e
zEdkz?vKLdTW3%p?<qoW=TNb*IIL$TX38oaU2$l*jqX1dmN?~}U8m$~IuM!?Z8jPu{
zDz6rnsuoJHL{}>`=)iJT7N}iWSzIkV0-ePxH~^gLkml;*3($t;D?+tgjq-?as3R1t
ztqnOLR9;zAQ7%OhM${@=d=*z$S2(<rzoaZwvRrc!JD?V2lbdQ#>qvmSpd6Rr3lfvz
zR2Hl%tq6rRP2s8_bFNcGt5qe|fT}6ntmS1_z%6L>rRB=+U}{CMP~dY)VDbFI$cceK
zNqv1zPEKxdu(rH}9XzL`Fp`r~QWgvcBH>_pq;^h;zc7d&{+#iFLMW(N8KBf!e?dvX
z=_Q3Hq7yGJI<qh`B~)J$LQg;o|0wk*1~6y@BSGl>aSC#BprIsK6D%o@tn^osS#u1t
z3L_P$k5>g3AYr`pMKwY<6s(+66e!9L_)*CPr+a&>a6+JPVxTA|;P<1@(u#r=RQUYD
z>WW(b1-L7WObDT&lNIduE^`t&*1J&8TIA%C8>rF4btREGXd}OWMNyz|a-cAho4vF;
zd{Ho58bFr_2Wgy(1eZC+7R+8ySX~%EEf5*OK%^{OeGw9i&YYi<ErKOjT)rYFhXSVp
zeJBuFSrfugw6vP)ZAj%JM{RjBLDb2Om07v|6<l1fqM{n3VJM&n5^T;XudWTCSwaCE
z2!w;-l_;`2Lb;aJ*9U4s;o9n|U<KMdup*nPa{3Ps?TI4#$&w$H-3eV%AY!b0h$U<3
zk|M;`!~mLz3jX0{Pob7ZoJK<a1(h=9esHgzl_RVD!%N3_Fc0HpBv28mS{5l2J?=+T
z0-=SDUtU{NT^kanpu3b**F}DuON3DrN0{VkFp({iGbJFSIZ#o(3`3n5et)#v(Zi-w
ztOm-;vC5g5gAr@N>4oFbUq!cB8V)7I@WQH#unq|<2-VhA(gFx;pAwAGWtfkH<rM(r
zbR;?STDTJ+Vx5ALmPwVtazdy}E-j}}$NB)t7mug2unAc?6N#&hl$IQSJRy^aT~>nJ
z#N`lIBJopa&J2vt%C=6OJ7>nsKyKCq=We`vo0~OJ!iyF`ctY0rTx;f{Mbl@@3FKsr
z&zhn!x|n{Sm77B=!jvTcQgNC_cp6Ua^mK`*3Y5|g!ik$o?|zqN^%OcNB^CdAv8*d8
z^V%qf?heL(Do>T!8}~|<B%~B!WL+BmDf_R$TA9uRefVE6dgURO)!VuS7+oolZsznn
z@B_=s`&zJNGh_E(cN2C52U+(rUpJ&2cRj3!@RKgGr<T)*pV4(Qb_xeuPcydi)jy)V
zp4Lw0U;E>7tk7-i9p)p)UXK-cn)NaB7mEC;);HkkQs=7>5|{5}Njv#GT;U!3oWc6D
zOjme5ulIWy_|{cYF5STUTrP2+fiF?}1_Q6ZM9OCy_)f<247{H8<Qw?TtEHX-10UNc
z@g)Y{%zDZUe9dwxUt{1~8DC}KTUgIJ17E*X>S;FchZ)~w;H|7@i-A8}BK5Qw_|Q^`
zw;K3v*0aOF*Az?nb_3tac!z;^vYx1c?+!{mod*65;}+*r@nbzA<$D?UTLFou8~BhV
z63;a7JNUU!fq{?V=NF3%T-je{;FDRt#=w>QDg$4_^6Ly-$!|39bu7Qhz*YOU82Cn(
z-)7)Seusf?Vfl6gSN3!m_%@c08n}}0GVmQN-%GWdY!0hK;jI!-?c0m_eAbhK<Qe#{
zp8G8E!0SEmW)FOe2d?~Nmb=?SUd5v+ulzyy5t{w!><7Zn#D8_QKOyfhxI52$2-&US
z{iTTb*`eXXH9V@}^EA9u!|AM2U0oW!NP(c~t&$--^X0Ah>0>`&(y+J-2|TY=5X>Z&
zb-uh6KMNj{435b#H@Vj$4aWrKTuU?@M?}t5rr~lXl}R-kPGzgBUc<?!>RP4YWRtqq
zX}F3-N^90|o&rUdjT+utDFNN2;h1QhYm0{WaZt-@(Qr)k&b3X$`#Gp(wQ9KP6O_C|
z!}asOb`96hQ+I3lVVeF94X5Xt>WXT3h5|u5HGGhUcWL-w4YwYb4Ea7&!+UA?;ToQ<
z;X^b$Q^VD}1eEO4@FO+(F&aKh!?QKqr{R+|e1wMQY4}JD&)4vyG`v8=M``#X4L@4L
zmuUEC4KLI1V>G-*!^dcNy@nsF;j1+KI1OK?;m2!uvxd`IvAQ;D_&5cEZqo294d0^S
zCun$!hG%Q|HVqdGe@<)F@LWxPhlY>W@OBNKpy9hUe4>VTX!s-zk81dd8s4ellQq0c
z!>4Gt#p5l-|4AC&OT$mr@N^CTiH2ut_*4z|Y4|h^AEV)?Xn3}U=V|z44WF*zc^W=b
z!}B$KmWCH-xL?B;Y51uczC^?4Xn2{1pQhn88h*Nl*K7D(4PT|<^EG^(hM%F~%^F^y
z;Ttvlry9OV!xw1y77Z`d@D>d(((r8>F5eiDiLDxbwkE$r!xwA#f!hNfIN*T;9ys8E
z10Fcwfdd{m;DP@?Jn&`zVc+Jj-rFm`(S8^2j^(dyjikog^H)F9>uKSD_{1SimK8sG
zD1P=Io@bGK8KuPDi^t<jn*~n?HnE*9PX{%zr(B*6XkuGko(^VWn_Zp`WMbF5JRQWu
zu5fwU1jWKGPX{ltVwa}_m)HWAr-PQ*440<^mRPRK)4@t?q|4KRN^F43(?Los)#d3x
zE%wDer@nNc5_`|(=^!Px)8**^CH9od)4@q>tIN}YNo=#r(?Ln>dY7jIlGqh4PX{Bh
zu*=hdNUYf9=^!Mwz~$)xBsRn4>0mLI>+*CE5*z9AbN~_?;PS(WPj&g>#DDR<Q-2@v
z@3}l3e8hITJRNw%o^p9Q=!k7~c{<>TZFYG&*oa;4@^qjPyTaw^AR`ubc{;#|6}vng
zT*MZ*JRMlXX1F{ZRK#*!o(?EtBVC>jCSn6zo(?2psV+|k5wS16bLvkA5V7}Mo(>*j
zJ6)a*9AZzoJRLN|wz@nWFvK>yJRK~=u6KDlP>5aO@^p|83%fiWAjFDYo(>LT3tXNK
z3}Q1}o(>9Pxh_u!1hJ7WPX`0B0WMDm0<lz=KZW=&{_WI1kNEdoo;Lomoi0Cv_@`W+
z4gg|XU7j}nvCS?|8~)h!E<c<2D_ov7{;{yj=M!J-@^k<YTj27v@sG`LdD`&Da$TM_
z`mvENKacnUE>9c&SgOm@MnCq&x2pc}qi?#}vX=HAj(X7e7eD%-b&34Gs}lKd4E|Gt
z|IpyyHuzlz|FXevH~7a5{y~HPgTdcv@V6QKO$L9B!Cz_cml^yDgRe69r3Qb#!JldH
z^9_Es!A~>zNd})~@S_cWn86P+_<ja|kiqY}(rAB!|J2|=H2Aj-ewV?&Z1CF+{&9nU
z(BS`I@OK*gZ3cgn!CzzWR~r0f2EW4Ks|<dr!JlvNXBzx`gP(2i(+qx+!Dku#XoDYS
z@PiD#pTQqw@cY&p?Qig(8vKU_|F*&JGWeGbe!IaxZtxEp{2vVdPJ_SA;BPYcYZCaJ
zPv$hddVYSxd-<#1?<^?t=d|WLm)|t?dn^m$8J9rxtEE}}hp)jPiUnrV)Z2mNH`%uk
znbH->z|!-4y2sM<;CM&>;j2jQX{M0BP{>cbfXK1?@*6typZxTc{3pA5<fm-Ue|2AE
zAQX&a1-;@Oa$HvVX?$KaHH7xD>W*KSzk2Fl$&UPn4<dc?8>b$GY|&#eut!U=+S_hV
zg<Q&c$m^6(`C}I$k!}_uUt#{`d$(bMTbkdPb~G(S@*DiooK{rmxig8`j=PUgMt(zE
z^yipD^PAS@VI@IqJ=Q^B3y5uM5@=J#10vVUlzu+uEu_~Zq;GW7r^)o@g!D_?^kFi+
zB_aKMH+>)GN$77+NT2Sezb(@{6VgYy>5t3wbSw;A`+K_Sx5@PEg!GSbDxKdT>UWt)
z_qTB7hv7Vx<i`}9-{fyrNwlNjT*t|z_WY)K$hi<A4+syC!?4gnh0@VHDx;?JbLoyw
z*PMqnwXez4Y?)W8*dS#es38wP|2{0NsKJEH1`>Uowlb9T71nG>YSxr%MX!*`YqV6Y
z=tbO4GF7VBAY~sY;G$Q{qT7Ych8B>=X;(!>uargCNUNlAO+rw*IgaHkSuL_Igx{Kk
zs7!oMCQ76&dO4Q9kd?XHqG8EWaa2-?WNVl$l58`xe#r_0AUsL3*<=>jV<g+j!kLmy
z=hTA*>u)E?@39;gZIAoU<$Vj`A1GY*6+K)A$w(8m;8e}OU05GNA);j-qGf}WdZ3*>
zdn{JZNQGY(wm3dL8cTBcK^Wh?xVwbHggDcRYmli0qCJ|ViVf+4d!U62y&p?>=og-B
z5^W;HWt+^GzL7{<^b>4XAS*P$4R1>}n?3i6V5R4tmiNM24@t2a7TY3|n#qy3DzWZ0
zd+Ai+47f>*M|ua@DwE(Rr{86BV}3Ykf8JUtGJ1LI9GNOA+hlkvo%LTS^|uq--R8rk
zh88VVYmI-;7PfWDRH;JrAB-EF+!~{$e&MU84Qz_YAsgf|>C0xJ!|Xwu5*>ZYac+6=
zb+%+%C@a_zk`-ov9UxgzBG?|1P3JcI>R8vUNc}*tvZenb??rRIB=1G5KPm1v$hic=
zXTvTkbvib1vIFq2(o`Vq5u<R2D3s!VgRCH$S5|wwNTK>Vn(o2YPjnV&U8t2iN8H=#
zc+@GUyss{$ySC{1uc_isOBHR=e<MGp#D;gGqp``%Z_Fqaa>B~%NK_Qn7JUtJtGiPA
z-`KjQwf~wYXrvPz7{k4+(!e}|?7OfPlLfBk0*?>{J|)Ddq&K4ju)Re|-~Nn5MM=kq
zlI*aPc{XQ$`zvKFD(#fz6J<%qPe$jK75IXbG-mw9RohOvX(U0tuavz7u563?<Ol=P
z+oJQS+B{EyJ#>s<YdAboB`aH}E&Am#A~l;+-<NDUvu{XN1@U&ts$uOR$*KWoi)5QQ
z;(sC88fLGSYyq>ENLH;=F2i|IexpBHnt!}p;`Cp0W*T<DbMb?gL85)vir#}NO+)5A
zJzcz=%^hvvEsXaw@EXRy8J(!7nen#`Ty>u92A<8m=nn?o$$D-waMkNBOT=Y!mK&gG
z%OV35jeQEh*euM=t_PHbqY~wv5xtLrE6cw+I>7_dl6MSH6#9H3=(NSwM4Y;DTl7}|
zV^?E{bS<o5UtN(XzgGF`0t0VhA1*NPcE(RKaOHuK2A<C4_BL?kfiFfS@xb2=P*iG%
z0SdR=2Qan{gNIX7>BC<p6TXtb97FO6993z-j5P!tSb)WW4hjS6ut3v5xe|o%35jLN
zDIfS?1216L#jz>S^<*>tk%6Z({)&Njavy%kz}p%BwSl)VewBeYGhS`rHH@ES;027I
zV&G~JnSw*>{D$56jSFcU87Q_&5j(o~Ga7N*qN6^?rt2MI8qe!`?rCZUwY%DwmTY(R
z^c>PhyQ_wa=niu$<!)NL1m|?b4jBX(ODtlWngrUEahAv><~@r?;)L{*-1H8bHk#J9
zB&7S?^j4YPo{-+dP2VKa#qNd**O#ly<b2%BcIm6ExiSgUkF&~ZrV>!0RdQJ<`i88K
zuJbUFQLVB>iP|dYYgt**56xAU@DTL-r2ZP}lX4a0EQbdjD}2!@>S`{4emzn;n)~v!
z5rP#(LF);UP3KgfWV4w)RIsvF+VWoXrhoZJiR^Bl$a}|I=+9_x(T2lhwWP_Sjdfqj
z7Vft0XLshv?F3Eq?z(@RoPdRS-F^H=+2o=woSNbqbDc~r5dJe(vMpTbqjIsBE)D|B
zb^n>tH$nkC_w{h$NKqQt4<(z;o_kZU(sM7!doegYA;oG~tVJdXr`{p%H^{EAHk)ja
z>!A^Hw^JajQeEZN*^Zmvkekn%g!IeZ^ao^mb3*!3H+_RlZ%If$-A$*l6J4!6AwAno
zUntW%6Vfx>^ob%}bTtZ5JqC(I<ibseXp!An-F`WY3Z*vCT`^g>Lb^2~BxDelsr#lT
zQH0!liy-`5#EdASCb5X-q(!`e$3JSBc&Ji~2Da5b7tzBFt!vyOniGo{m$ZnmR>U8U
z6vc_)*sSiGn$n?1chvE25iN;DJTEetj_R)!ak^5ATAZTpxd_csJH)b5II2Cdh-FEO
zxEIgOl%t|U-CDe*?zsrfQ6aa8&cq_pk`^&XD`Krui(0Id_sPbbyTxi=F0r}~0_){k
zza{akLD&Mdj|uY<25D_HE0CHyX=d-PIaj8N{*Q`_QAQn533o#Oc~XC~ra{x+sUJFY
z8!dOr)E1dns!*p;E#yn+|9&*J!rJuY`kSSOPFe|cw?8aXvt?eXVuO@@pqcgmO6qUc
zG-&o`v;A7CHvA4?`(>(Bv7ttA57e;!sZxKora{x+E{_4ywNy?2R+(BLQ>BUxQucuY
z*8g{`V`(50G8<Z?XaNy9UqxsqrH<k@uq%YLOfQn@?ZQWVN}=!7Cvbk*_#6sCTIL@p
z(y50nL<BY!h)F;UQr`}tlFd&17M^6Q9(Lv7(l(wrE|RQN-WDz6RI&_#a5krks<lN=
z<5Xr(mTWq+V<nr-?2(dfVYZ)SYnY8^3NxCS?Ubx=70P{AvYni|Q?lu7)zgw~VfKE>
z)-d~9$u={4lVpVxq4_Gwc5-UHWJNbaYPn$LRB)b5s$oaXmq}uVogwb+gHJ&n#M<<e
z3c72Hu6>{UhGP((YjCoOgI9TwFq9S|jTwuDs5qavilkl9?GSYjL#{<kiltH0hHMdb
zB1@WRN&Dt$s^nTO`4CaEejbuaYmml_kC&6E$UIn-XYX(_PvXok|AWmIgSK4$)yZE0
zrCPnJMq62tk$4XVim!7OKTi4iL}c_}q&C?XIEB0_<lx(cLei;DO<ExpiG@7YUlcOd
zE#z#ikSE2W-`+Tt>PDM`3N9oqp%Be+GsOWo>WBKAgDx(sl0hD6%-DVb=@CBq@;$dI
zzY{0!G8$&eA*GW?fIMM<T*^RWj$~Unb);mQnLSLhHO!_-wt(5MGst01zzjTIu<4xo
zrc4!Wf`WEPww>3Rf0k?uvv*6jnb}`TwuagDk`?PhsJixG6qI<}^OJ+Hk<P^rXM5}%
zF`R+S`hHc8Ic?Ds4P5o4;Rc?~-Kb|GE*s>FfeFgx`NiK2P^@fr0F0&Dx`oP;-zUmD
z$1WQTTv>8yA}%c{GeA*jVIt`G<m5zLnmrm|EFXJW$A?mLKSNk({?}m;J_idML-<|b
znzv;LzDUAZ-G%Q@Cj4s>PU$XuRWji)3BRr%W=WeDClmIQ@Lk=7$0ZZaB;kv@3tNf8
z@>v^#GKzQTw2C`VsM-y@fXDA`2Hwsy#wG(VV0@i{r!!t-;Mt5XGVm70^9;O(@i7M8
z%y_ziXS4lXc!yB0Zzs!l7<f9%?=bKd##;=$hVhLC-pu$a16Q4*%)mQYzQDlKxjRoz
z#ATo!l?Xch<&Z>N_Lpxko9sEqjDG^nL%J6U9BN3~*$EDm2HfOJ0M~Z%V0txa(9f(H
z4;y$3<BJWvneiD0Uc>lt242AU00Ylve2j4(n$GxpnEZ4*J9z|u-oV=#-)i73jNfA5
z&5U1R;5Ce2VBl)1D8)FE<WO($TbL`+Y0vmO4)uBylW?dPZG9W~;d|rpZM6D6&pGWg
z*!+e|yYibdesP|dkGk?3(wkjbyri5?0?{WBacf#5{V-)gq%FD_%c(tm6*u%R@p$ud
zPmA}G<$>bry_1n|M}9+HtNG4GqaScv^k)>qO&R|>SCk7V9olx}H|6)jTIL<R-_g;G
zjp4#~fVR>qqv4h4B`8!TV(*9*1qAdNG%|b7DQ<j1MO(Cxq=a5DR|<!9I~;xGuhNe_
zksN)Bm;^s67eGr_{_56Vq;}};c-%ccRT9y!MdpQYP^#_?l`b?iqAA;=kGv@yM%I$Q
zL>rL)My;J1F8yxxrQfC0_1s4Lqdfz_#KBNw?y>1*7|1#vcgkp}>qI%7RLE^SN(}oO
zRq!cMyj*5sezcNWD09P(h0sud_tX7d+pQELZFy;8n<lKx>-9L9L52Kj7debf2S`Q{
zcq<&C>o0_PV^GQ6-D6?5)W18wEw7i*+2rpa6~CsTuW4ZibnoWHp&0czc@vV2)}OK`
z*KK{F;}X)*{WSb-v>p{P2v$a4B}O!OcVBX~=pCtaRY%G=PlkK<*30YFz3U*xGZu>&
zM_foX97R_u*FojSMh|k@lWaixoz#}Ne;fx$!o|Ns1Zh2PdJ*~9M?MxFLu*jBquz+e
z8~l4$U%J<d43@4$KY$AKWsWObL=^ZrPmu2DDrBKe6!{%m8W--BG1K)r;o_-s#&@`F
zvgzG@imN7jELBjZT?c<Q`uFY`Lf)Cv@C-eL{vImlHi#zKOzvL&jPIQ3=jzc*V-RZB
z|G|WqCX^zwDdWCHi5}$m#7O0~8tWjVleB_rOE_f*!lHZc6(tEN5%=gtaN(4vB4bd$
zBHF$*Jo)h3VpnKiELht3tQL1|(HGzx1bjk7G-Z5$mSc5-r97xojj55gtG2~Fg<{&G
zFTr10+j7H7Uo<R?ihRNYV$bxF=qVXBZec7CMHfytt&)C7PvW7bjB$nvm~tF!(|fWR
zmk%o2Guie-yV))#5ZAjjvIx5~q}}3GJK+i0Iok5b4KzF{Z>rG)^{GP;Eu;vC6EHSN
zMK98-ttsP-GljPyMT$sZH#tDwFOn2B64Id4D2N;0CVx+TEgs)9jEa+i4;6T)ga;4Y
zenMR$af~3FGSS<jD0tUGqu{)B8ZwSbD49Ft4l&n@Qa_>&MTVk;r%{FG{meTMxx)1H
zU9eh@5;y*})^+V9-!)=vZ4|D6@7khI3Kz6R$Gb*tewDmJa|P@Y&6JH|WKHx(h8{5q
zug^pKio>v}+`dI_Cve-;o$>OLTFZWUi7G7yBWRXG+LhlDBs};58JpNHW_)gj0(q*V
zm2LFD%Y;lSUW4(LSuA9F>{sSi$gF9tqev6|x<&Ab<E(cHU2xaxuC)D@@VbyWWWO>k
zLZ;7tW!4LsgOkfNWqh!}X);xpGzw5X+6*6d8wU<X+a!}uSYe0&dzGTEDWkwGRO|cy
zMV!4M^QR}xuf`4x1$FJH4E~Gw2bJM;VwV$6AHG7jG;+xO_qKmgcu^LtN%2G-_fR8Z
z`)lesVuqwn;mko)+GK?G4s)GDr*n-9cW{>qATZQ{-Ap*P;c2XNWtmlI8FR&wu&`;T
zj++muBnun6onVY-@O`w4YLl>%{V%P1l9aPKhbCIrPArCB{q2J8*4+)MB-Skx?#0Ru
zRz?^9SnH0`tosvMLGvB`uGxRKu1|97o_ksPE`_Xnl$ammyS1d8eRpD_bvF|GAAMIv
zfn|!>(c{^=61Xio?8jR75h-Wu9z(CueD@8p|Is?R<2A(WXcLBMio0iFSacOJKgM@+
zH0x$2TDR!GvW|Y&EQ#+vdr?|<3|aRcF$vZ=Ge%R!OY^#odwnoG{Gf5~P!!+}@^V?8
zEtcgp05xC?;L(Lv0$6pYgU7hg7TqTJI$Cb}@zxS8H_yjeFxW!`OUuo3#9dqT+~=tl
zN|zW#$9+wZR2BPYJWfk*F6pme<s>Qwj~D0#N*X1;q*eKQJeM9TyyOmkkB}5A_=U*v
zq%j7bO%pMVfvca%7R!0HUYov9R=Xb6UWajaRer;UdJK8`ptu{qywNC7sDOZ|Lphbx
z=HE!`KMCVWw{+8x{KmDUgA5-lA#?w7mdf(+HzbEs12@Z?5+diLu(oI$>P~dZ7et>#
zr)b5hhxf0qL?3-lXxJD#1v^@mr?9&vdC4uAtCf5nN|tRQ3Z5?vq1}~WPhmU$^ts*^
z^Qd_n{2ODfwBKOSaQET^$%`M3EbAQa&O<?B&f1124zXJ`jgNQNcu#VTj%%-_C`)wh
z&m`oywnDfRZ_sxpb?tRKxNh%jjl8qFB~K)^r2m?=BAXKn`w%j78lF{7`b@AC`NF*&
zaI4s%`ZsZijT#J(HWAwveM*G2(-!v$;kM|}Fnn%9%<UR~cvhP1<b!E@sGok~gEI8f
zH)TI95iIpn@sbrvxF1_PWy=Mmp6$vPMNx;^2nc;dG*B<<r|3}58^Do-xmDOa8)eHe
zj>Mc7{0<RbZHvxC;70eg2|er3G3(JWr=RC;_I`BNe3@F)=$d!HUW{OR*St<bo?Y_{
z5$_3I^CuE=;%BUg8=PK!N;U1)H9sepQr{@iB6(YPOMaW&61{6ag-F%9=6xb?op8A0
zGb#wDM6kn+g`KK+J$w(tLeX%9B_YER-NN@2VS*FB*@+g3cP$&}sj>>+5FTTxFzk_N
z?^nWKZPBHl7~%U0o9yI+X(D`=4wK>gsSMvc=-nM0;xyT_MFQT9dm1j_kiCc0^L+z1
zO=9@Yq3-k_!uKk%+NK3WLio-VJ*+Ld2Bt<&A%=QI_wc0^Y#C;iEe&;dU@qOL&nWck
zfQ|l*)MPQZfF?Y8wUKO;vrCKujaEN+>9cVm@{2v>(Rd<?d|QNI(>%<OqA$LH#fY;g
ze-*JLltK4P@Om>cxbNvl=I=RGogMJvY7;VOPY~o|ksCyNbz3|YJVVB|Mc1L)(V4^u
zYxK=_(p5yl?0*8)xXmBM;7GL*^Sq7rKvdGPpIBggjrxN(LNYQ(rQe5u*H#TO{;4|%
zZ5#GVGkfmQyTg4HA=om-2Fu<kM2|BH9wK?qf=@~;_;}IroPvjP!Pk7O7krB<_%^M^
zjhKq`8ebxLv*6jP#!n)SwHj{~VeJ(B8`P8<CL^KXpFSyTEPBwn^d=A{0J|q>lU+=&
z|A-!xCKB4B_q9TrJy=fq`2JL(+gwrglv70a6_peBSWRteSa@sqxW@p2w_RYV8~1?3
zs_JtZP@TBHmE(RK9*M%5EjVMx)^r|(Mcg-F1LMT~U#Lg(`@wIZRsLh#Z$XA`asNxv
zp55Ypk#J;NwD~E-{prMXk9%H7iY+y&-ikiIEx!RTmo|cm=R%@}IaKdPyo}{S!vsXD
zI{d;a9Ds8fnz8>uuR)=~vhl0|?4NLIDH|+RG+kRX^$B4}3+3C4$dhXe6xtTOL9n#8
z5L(xWxTI(iY+Vc)A@$Km#_(G}8XM>^T?!VHAm8VSOcVx`j9x0*z#@kcyZV{Q=KL*=
z`D-u)VpOYZhCkMIi-m<)`_aQ);hI5If*c1G^e%-tw`!$R38c0~TcSt;9f?YCoCF`E
zeWH?o1>?+`zeS2<3HV)W5yu!I#44sOS}l31jZhe1g|B`{3TZNL*VoxaP!8X0iP6Ai
zn0b<B=60c$d@Zyd%vvuITE#Ga@#DIgW2BisRT*}Rj^UcQL-LN9+eCeF+MV3Yc~DMf
z?wO_Pc@-4MkwX|%FZ4O~m9x6PeV`9nXFVddD5GYw)D$X|Yj%RbC?GH)(PSn9;xlTc
zgehnFo>F(pX`v>YC|VLV($8k>=oiAns2QTr$k8Ktj#kdmg-S>7BZdrF{Y*{59?#h|
zC!FVr)AlYhXQ}XHTXZ+Q;?+Rs$(`Z>(VI~Vdi5POjcsEP&`|_*2LhTJC5md`UPSPx
za3YQeKc|<?D1}b<Sx5?$V_Vqm^gb-g-%X~RK&>aX{0ZlDnWD_54DlA5QcNYgj|y(5
zqM_k1Q3(-eVd)T<(H8B8GMWv|j$il;_-Ysjv%4Nw&qqE-6lf=gYC)b4Yqr4yXv>9L
z8g{Jn-=X(wv0D})fpp=OX=GZPznv!hS^Xaj-GM^3kWrr?g5;ou;ZRgXgvTyX1)Lnx
z8+sV>=QOm>YIt{U!^hmsZ~1dPzRv#&v<UIXAm0B$|0`=->xL`r23Bz@Xp(ir8S?Sr
zbSM&Yko^d)Rpmp$_umm-&~`R<bP;ujCi^9N<FA1pB7VfL6XJp4+($|NJQ`MnIhmqp
zbPGRx^jGc`e~|;JrgY+-EQ)dJm{4*RETN~4##*!EVJfgKnu#)^uMtC9S3i?)4z=3k
zBU+|ggV5?SPyWe(>5o!F&{LoJ7{>6B)W4&-`4Oy%C}vycHkPHUs?4JXK=Dt!OV)i#
zx3_I02!rFo?XrfV(_eE4p7S3EZEeuj-rPL>QK7DBVVe+Y>bnvzaj`3kA?siBex$Dy
z$2*pN@dOP6H36^&?+z2tjGUUg3ir&F?s_&M?{E^G*RWU5eh6VnoOy$2Z9M;kAEQ?i
zBb{l^Thz&&5Z4_kKH`Cik!Eih*+1I{ElmpnQDci>uM`fVNvM_TGXEj+mod~OY?X!B
zG0DX2XopaS_9v5HBPQu_U_;$kt1tb^s>_5O^nMJzLdNC{L#90wkecG8(u-uAYEkMS
z&h@^FN68%Mat{a5<-1S}fsG5l67St48KLBJJAFiatAjk0@x){iT^NcexH`x)7f?R~
zohw=bPb?Z{P?{Rlgv@LqBL=gD5bHK_PDWsoccJEM$2&>vYRZ_FV1OzFg|<bPk%^#x
zd7G#xY|#U_72|AM^mQa77!#hI{Kt{=p$8L3PO%h9cV-TD!G#!<d9k+w50YuI_e~$r
zCi|Iw#M1tDtw_MiUYaD_@&LvmIin|3<TmzbIx6Cx0?dVDnlWaiC(McZI~X|ZHN%{j
z{&Ssz5W!-A7QUXy1>N;`y`Y)*VOc{50PoA5@Z|UOcE$VXE(yQi*$1wHImTNRYG$Pw
zHKDBMM60w#PexgPrh)5W`oZmFQIY<=A`e>dKFH#I4&0UgjT$ha&D;{qr)!We;Zojs
z%ZY&qbYnDwhvla7OcLSy2}0c5679lHTAHtKi1%CW9@L6r?>x8Mx2U1Da^EHqF85I(
zZkD@^&P0UU^l}lS*-pU8rAmi*kVq>M*+RE(6-9L+vxuv6$cje16V^BnqO^Vyqq|Sm
zJgSWb^7S1Es0a0Vy{H<iq|Y3M@=d>P3QMTRLBF=PfVDoyTJh*#YRtMn(Zp?{VY_KO
zw7W*~`(&s@W%*%7!#o<OTglK7qR-PJcn7gpD!<aQn+jI*cD3}769iLa@!)a#LN1pc
z`j*C_ZY@9-<ii3K;cf@bo<_S2u|tG$QrXG-gt8qdqebp`DL3Aaic?4CQ=5;`R2Y@?
zqn(6VrJZs-E20YBDX|A$Eh>dGWwciGQewyr-Fr)d?aA$iVPe+%$M>v-PNhV3q|KkB
zE{@I9<Vd=In-3Q))6M2xe?kGMQa`f!Ibyoo40qEI+XZ)bBDu3MFO6POxaxBZ7!9rY
zO#|sXo<`Rx7-SpMQu8-rW*SEWZc6*KI7K|N$*?;{1TwY)cteEdRM|3z!M50gq(c+E
zwS_D*MWYxZV~vLB<$p*f`WQs_l;|qY77b*o+(2?C>vEU>F`2$fk~<8oz^01^@&Tlp
zxP6$Sa}nIN4en}bSa@&p25#X7F8U7nIriQcVMY6-7V=l)ynCg42K=7PK`61@d^v7F
zMO)O`P36-$Af1TNYDo+&Px8>>@fblwaZi#lmr!=}8BzJR=y&jc^dVwMZDJIoirJ`Q
z6jkhKSoju>W7;7lv<`PFfrh6_yd^D~cdw{~GlZS`rZ60Q!kE~L4R`&?Wns<ge)g>k
z=e%wHP71p{cK&LAXUcZ}XNVrLC+y5mq1o~?-fL#z@!jgq6s!k!!A7**!Y=)($s35B
zWaFh6rV*hcO3^={rCEC?rTZw@c;0RZ@1{l>AsURfDj1@k5>4_>bSwqw>Py?Ly8h@Y
zyXf!<qPxf~?7GIC!X@qKHgck(*G&?}!}qcL*B5J|wCQnVlZ&-{(Omj$MRtx+O_gM4
zed8`<ZpwIw-eD9~PG>KoZAE}LqT+gyz_D(o#*;;o|BUFMGBZV)O&RCwik(HMP;x32
z4P}3Rov2tJ<_l#sLE^a?lA8_9P@E3MPOEg=S>FtIYOU#7LUq%2^)I|3%bx0%U2(Un
z2yKX*H?sL`qyK|&jK32vr%rwfuS^;5oF=^4>5i1JliqYp_A)(`Ayw=a`>T6Y`YPD3
zMH%Y51ocI)mWKjn9}rt(n&|vn5HY*qF6xBzf*%DURT=+}$6NGZFht=0>aPAPPQlX;
z;^bc-<Pl?>h*=tZP?~7@dxS&8BL)T4Luk*zQpVqj;&22j1|^Z<+kNCg%8&Ebd&t4G
zqS^weMfAm2qKgRS6AL5>Be=BR{|-q!z`Y_BQ9qTRLBi)t#v!ZLvQ8wZvnQ1K&1+O9
zeuI|!Q3F*4&d1L8&FCuG%eXzn3$gO|z3BVv&KK8dI5}_~@WB6$2k7q()3u_yywrE`
z_>)d5DGSjbh_0@Rgz6(>#Gi8aRTp0nDv699>q}sdwQ9p9Cj@KCPr%=PKH=i=_yf>o
zRxqnFP!g&4O`Ym1mbbDVq&iez6BcEZSJqUNhiX|n!H#ah91At&__OQP)fHoo^^G14
zRSqlFSqb{8@psti@5vv(AB{_c6}2HNdA{TJlW%|JO`G~3GbY%HzkBbQK{=NlP@>hC
z{!(|S)EBAtg;oSB>hKrWeIymCtu3#vva0GTDy+Jy+F-<@|8-T%tEw-mVzb?Lt*(ib
zSK^O%pL9~Nw3Mw-#*IGK3Tfq0-l9-#q`YdGuV99+GFb1c2}UBJaFwq#6hS1Q*xpus
zj#Zy))sMGU=2$Cpt&4N4i}7>3B?9OqpEa+#G*kh4h6tYW6`@)%R&S;FqOxGb7by$*
z%4=)uLcYrKWn~fHMZv0wZ=5e!S6^OH9t^Matq6w8gT)o0+TK=8P9TSV<kFAvR!uIk
zxy0rYTb$#Y>I2CoVp+w(TKuVX{6TY6;v^Zj;W}ZtZ)v!?(nnrH(Y~tc2nwkvFSSxq
z=v4DBU&iBUU&Z4m;Qv|p|8x8YY|YQTc>HALL%-xFR#Fwg?B}9<ITM1lk-!Q#t~wlu
z)KtuwUl^D`E$H_<nMqD!QkmdutHTkNAbvd5s0_qUs$E%GTrCX{yzHk+L?|MBN~pdh
zgyyfV@>?lK^f-Avev7XLsoA&2<E^;QyB%w6&;n5U^Wz0~#^YPSPq`}|Z^r@E&G*OS
zU7!^^;&C625!ZrdLheS;$)JA%T?85hrH^;r{~Yv!?gH%q{RWi&;A`gd@%SjvaiFt6
z7lW39ZUkKe+68(C=$$Xb<1d2l0__Cd3!08okmFvA$Fo5fgBE~hz7&twgJywl1U(m&
zPD{d|yFqUR?E;O0X5zW{K`+Bz&`F?+KraKW2fYz=Bj{70+d#hn-3>bF732qf9@K}G
z^4NCF=%D9<mVt&r*MU9{dM{}2S7A4(4|FeRF=!vW>UJgQSkSvc=YqZrS^?SzD}?o+
z*`W7=7J<G9S`WGx^j6S5y`dj;Ea<nOb3t>l!l(cZgRTed0Br%i>~+`;Iuy%F3+M0;
zgN^}Rgf(md=r^GCpf_UOyb1Iv&{ojTK|4S{#4auk8|KTgdCCUO!>;mN&=avSUIRKA
z=Y?B9Pr!qNcF^f~7SaX!JPta2IF=uX2R?bA>p;su-vez19T0_mp!de&@wY(#^>IAj
z3rC>zT0=HyzrC;z^f=HO(5FB*f)4!z_JPg??ErlnG!4I*TJ<UF1=<ce7c~Df<O6L5
zy%BV1XFPsCXcg$|goAzsI^%Q10pfTcDE(^B)-PZuXb1ZII?!j(*IPidzeYOZ{5H@f
zpxZ%LfmVHk`h&g)+79}Yf1>`N6`+|ol)oEvGH5#}{l0hyXg%mY(2byDyW;UjL1+I9
zegLHlPo~6`a`6Hyr9M67h(0}gHDe$md?@~J+8mFMCW%=+VVPx(!v6{QU$zl_0)4~k
zmp;2+=4t&8xv1AF>y#l=jvGH}Bv6t6T+o7FL5={vNN)uH^MO;JR2P-C9{)qn;Bgy)
z{(k9Krq1kp&}<k4meTLV|01O0?JPIF$W4C{@K2FGNl&kI(+N(wxL~fRY0qD7I0k?6
zTGf~8MgQ}WpY)`ig$7qP_*eHxecaVE0sh$wIZ;t1bGDmag!E65j?bUDI?j~oK0s7Y
zN~ip3-y<NC=-9|*;GHZteXd&u{U+?Y&@om|FLBd%vkiEX=;n{O>0L<g^K3jG(9=_;
zk>rPLq|>`-zsG&rd76#ni(k8SSp>PAkjo~y*_zxkx2#eu@!p0EJ~!gpGS5w4gY?&t
z?q%y8NdE%qC+PW?%KT*OTd*N@dp!Oa?$fsSamzS$eUH^?slO*lil4pEvk`J$KJ9}!
z=NhDs)5|G!?Hr5rTaoTnkGV*{9_b_X{90U8ApJ(97wPG#r;7qa{3Cq_(!JvQUZihF
zdNMyy{uhzH3+ef~{-3+{??w7Pq<h)lCk=lp0qLIgM|x_Tclq>v-T_FTrI&w+EPoWR
zH7I`)(r>_hS~doJ755ZVYh5|2=Vr(ilU#-&r}g(oQQlkovF9zM??rmD`ud>zJEXsd
z^hLN&u;nz@XFiNkgRrj1(`7Dl)ANu%3F*nopf*{8^sz{vuIER6YoUVDS0Q~q(#b!L
z4d=M}Hz9q&e$rc!e&&ACJCME@>C<%mb*_F3>y!HZ<o6-{XZuOdL;9-yq%T4Gn*F4&
zLi#$Sd&S%)q~C;eub6K|`khF}16bF8)o%Sdkp4K*^YnCXKObROU%id=N<E$8F(7qN
zyU^E&#$XLeFIc8EU^dd@w%L^{h1_jQF6=G09&!V*))e~A@s_(Ea#t(4S>AGQLC(S&
zRp=Y%EtiJ6u26D=lFLy{4nz{IdA-_X0@A-lda^e0A%79l55^k#Yur1&l4J1)<gGD)
zn_<geA@fW0^|W7tQ9hm1)MI_xYP&~658+sneH6)au*Q7?<9FKXB(lFx6|&S;Q6#^G
zb?QHHpSE0+r8bSpw(=pZ3pU<^b!!TAI%NwRdwiY(G15i#T!%HR&^0N!E|Qytwene5
z+YZ1y<mgiMut=L+TdV<{{wAI&Q$4;%qp3Q}a#vC<$p1G&-{!yIAw2FKnbbT-53TWE
zM0zcf(_Yi`P#r@;Osr+Tf?Vcb<MFde?jb`?PCH^=Ov9S}G{_}u&oRjR6WFsD>9?SM
zX|<XjRmXL*jwD+K*&TR{Igez|Ng{i)>kq1D3~T+n$-b$YEY;&ySr78Z9k6dXo}n(s
zz3Y!+AwcQRApJq4<4t2XeSzzT?@-QGq~DC>v=1>LD!)@X4X)fM=oyJ8FT!6h7;>7w
zCSXb`f?P6x`A|j?(o2zkJ?@>dWc*)2rI8HngLXpZ+U_!9#wM9tAu|nopr9^8HWx~p
zNrv`MKZ8uYDRY4<^FCzS_aj3-?1g31DD1P&)%9>els*ROOOXE4g!Ft-2&LyE{d$jd
zAJWT^{tVKu(DPGWcuh+E=nmL9^4)m+5!|Ppk>>i2<isjY_M;ae_aNl%BRM(%(A)F3
zvfgCVTPSk|_KaDGMMtK`(INn;yn#qBz+Unnq$kDD^M<QuR9~!>-^ZR8a*m!<x!5K>
zv_}oz6px<|xwPjopecLuSNG^Kudh%<a<qrN`8V<S8+ctU?K!PHl6&Sb$Co!k&#Z^y
zalE1J>MC&UxgY6K*j=for^<yY)%$g%PlCPFA01n?`K%Apry+d{lG6qm{q7c74%s^a
za*sn!j5FUE{XrXN&V^j>54hjZf<x7x+D+>>71&b!1aisx4cWb(_S#5KSgSxs4NRi+
zdy#$t(vQZyQ^vWjUtUCd4buDT>DvBrFVdGFeVCrUQ0Dgm8-?`qk)DP7w4qu(xUOVF
zHk6k^=J14=N*6Ij=><qH{xJF2jbsZmPVe*WD^jdSQ&0dn`rr2?+|RRXtY2whzhMB&
z(=q5ar=T?;c5s<pZLQNp`es4oBs*wb!{GlDAid~y#Oj;2{l-DouMWCEn37)9g-Pt+
zJ?wv_Sx=@(>@abrW<Qu>U1;B)V*P_{@_>h&4%=7SH>6p+Qbt(Trd0dcH0%4+Z{b%|
zwO77<hE)a$_E7q@DL6U!B*osHYW*s;T;RPgJoS?l>wfwOBl$2F)NfZ>w{W=!`^VN=
z>veBUgT$Hk#nxTQTay6Hx5L)26)+LN+4klXs}B2ODBYYo9>o^hw+*qbNU^URVr@>b
zKRw)fD#hM)xb<F&{rKV56{+@}hg+Ld?Q4Li+TUbae^0gF&a}Ex?S_HY4L$6y4zvE$
z!+z&5>y;jM+hNw1J?uXoW?hqJ-+Y*LZ<-w+U_GB^e>A}QG|hfxfYo5z4-K$>XWPFX
zU~RYUs|Hx>d)nJGt-E{L_heW*dfGQ+Sby(n?;B|SyQdu+X#Jv>{pvvLv0nC{2U>sa
zW#2x~dgEaG51Cfy!S;s1R%35_)nMy)z3n}NthV0vYlEykz3oQ^Sq+ESzZqoRb%@<K
z$a>)r`^yY#&ms2TGOTrd?58uVd-~e=R_%_y_T`z@dwuPv23ueEwSPa@y0hPTKyL28
zXzyU_oBku-9BjQj1pb1X+IvVh;Y0;)`hGOI>4VYark6%re^0R=7;SZ>*qeu1H>BE4
zL#;oh+FeIjucX=?M_6B`+B=T0uIXX79AVwl!`^s=b!VFWtI^goY4$TmTJNRV_a15e
z6V5u)+F;vP9BJKW+aC|5VB9&>`pUK+9%_AZkiB-a)zs7e<Y?>nJ?%G+wqELKKX$bB
zNl*K?M_Wz3>?Yv7?5{^zJ9^ppTORNAvOhl(>p%OgBdvQ5Cgj<J?c0V~e>>Q27-n75
zn~*KN?H7hwkN3789A<qkkj6vou3^^ghuHrZX1#t0$$WZ<{oCOf)9vQr)<b;=d9{zd
zbGY?UAN#T4)-8Pr+1A(o>L_bhU;C}2tgrgoZAV$x_p|?al=Wag`{tvp*ZbKxEBK<H
z{n1G4rvCOTBdz=U+YgPjcJ{Y_JrXXquNrCHm~MYI!rGc{zd6F%m2N*V!ul%RzH5Ya
z{h{`?BdiAxwg2g}b{%TJ<Fmdw)Nb=xHx01==(8RiVBhSs+6UM;gZglQ{qb<?m5imZ
z=ea>a{Na-O2M=x-W$hU}3irRr9DLg-t37iV?!V3)fxlq#>@l)Yd!I3WO^P!jnH`eG
zvIExv4;=8o0S_GTzyS{&@W25N9Pq#a4;=8o0S_GTKz9%LPL^25Nr`Fs;up?vKD|of
zeJ)Q-U&872mq>gkQzcc;={v8M$k;}eB55<HuURhntxT2F7EWKkR3Z;ERq3sq{&0yz
zhL)-nNp~y##ggC3R7rJm`tG1azG14;EjsMQ^_F-M!Lo)d5v+B`d6NFnpJQ&2IaIkS
z|6~t*i3h%paaDh%XQKzc#Y4|F4}1sXN^gh3;}}d_Aw0XFOYyY^e}%y}GmoQYdC`j*
zxNt-(u2oHvinC?hMz=}+2uZA7OouS-<a9dQq)VlLy)Rx(d<%}d>B5<Txahqsx^Sv2
zE_$zzE<9Qhm(4dg!WUO2Q}Ip)-xJ|%*5t<|h|@-Kt-@nCx^OHfE@mx!%uHPC#Nn=Z
ztSk6MT!6Bh-ru8(-DIiqIh#|zf5&D0;CGRAAM+czpg8l&PQ2nJ{IN^C2!MCYm_I=l
z_kaCoCifdtaW=Pi9@7G*OPJO$UB$GS=_aNvOk0_@Gwop7$<)e`C8sm>G0kS0$FzXy
z5~ejwS21m7x`}BE(^jVKOgor%GPQEKe5O98*-Z187BF4Hw1(*_rp-(@F>PVm%Cwzn
z2h&cb)_5+TsgG$k(>$gHOqVdNVY-TGGt*5>TbQ;oZD-oSw3DfL2@fWuPmp%_m}WE0
zV@iKJn64#EYnZNL+RStl(-x+!Oxu}uFzsY&O_X}mnfjPY^oRfK)tZ>+)R{9+@{L(o
zTvrvT^W}`s8lROtZc?3Kb1%!Ckd-~*ScVhxnH-IqY1Zd)6Q};4f|T{#fqg7+7-%wi
z8Xr=vbgSkh7G&aMe3OAwGm*SG-_HS_f~W2UPvS=0OS(|p54O~JD^Wb##SQ6E>j#Ce
z6Y_(c@mt|{;U<~=twMf))%yl1spgX}89&6pM?)aR8esJ?@WUXVO#j(JexSAYPN`r2
znM{6}FyJt&ll3e4i-n%UEpvQZE$|`Ee4yli0emF<qt-9uIN^7|2Ph$p-pBF}Uo1gt
z54v7uyk(8#uaLw_#l(|LPk-Q4u3EQDW%*Ga^0^-PsUG;btbgP(sW^}IU(UE%FVedT
zbZuaKSWxoH5BD+tUa`byNn*Xscq^|L@z_#a^o}IeYc$K}Gd>voB$*$M^}tUCPI}Jg
zb!jc@xeWLSXj1DmRqk~x|C7t5;Pov3Cn29{W&T+LKE|J9`PM5WP|x_=z|*ZGtjtyh
zn0&zUYq(y@KmTOBnEf`A<umZelkC5+MgsKi5nbaL-}iILt929op*52KE+p|$l33>f
zPv*BO5Bz7W=R;oqDtq3+y2FQhS*@&?$u*EaluBrp09bMTiuLp<m;7yvZv~#ro>t)0
zE^1xcm*rn&J!<`aB;)^JeE3BY5br+GEf#|0hoS2wE}oO)mY(Gjem@OdxGE&E)&oyw
z&tF;I?AIR)`E={plcfTB=Yp;tSl20ENksk}20WSm91nb!(35Vd{gR54BF2ZTl6r6E
zLL!Wt<3I!BkB6k-G?u>|crtrhfRCWnD6i|(y7U<#pKhIdu2i7b?az7WNymbi^r(HA
z(lY{hvU2^vsa=kVNc|}s=jVCI(<^n!^!$wVM9-Ice$Vy2)<ga`EWd#LGm7OOX8ims
zB*5L$+R6C0r4r|5HlFfI`-d!%xLR+gV%1LdTEl)*aZ9f~CbRz-;D@FjVVUa?dIym7
zq_dsVWii$~#>cFXz&{x;@zB5018-tIpYk|N@1D@r0}B)?SM9e|y#@eJX8$=X-_Cl5
zNj28%jBn@hWH{p=dg!5z8kIY`L<*|uS-cwud>40IdT*1ipFn;D{FdG-SZDvVi1nD`
z*ag6o*?*}A{u=N@rRs#AY1lv})6?GrpX`AzB0Tj_OYMtQA?E`pKitwNk)t``O2*ZB
zjGBLMCOs;%M(+ns{ZXB>sQ&mg<LdlI;ZfFawqp?cYO*JGnN)r^mvJ%U**w9jIBaHI
zod>D-c@Q|+v(cDOpJDlrmrBKxS$_xcWc8YaahL4b&gV9&KQ02EOnxcLoAYnIhy0Zu
z_|2@R{VHkTKiE$C{jOx?KJ0<_?kDZ9<MBbQLyiTWOwV`^{1nzRd9^g8p6xlG@m@S0
zW-xvk<K{Z;RuBDKJn)BDPue9?v07if;~~EQ6--vIVh@~tpN-mg$SSE{&3Da=tMfTE
z=l+gybDi)A<JUAuJ!2%XdZbJJ=J-6A@rQYw&tv(ijGODOMU0=@C<Ujn{1uEBFOxte
z<F^1$=7%jT|MKNh@LHCCiE(p1{Exw;C*8{9ecx!7r{7aervE1x#K@nYu9brKvHUrV
zo9m6`z?12r-vgv|nmV@}!Fqnndfr_wfv*{V+C$H49(bn*J`cuFeXq)wis>Czx~hRw
zz0CH-TWkXNal0%3cL+T)um1C6mY-|P?>$fslDb`m9(W6I8sF5pxf)knJ>>sJcq#_D
z?8GA81y1#v#p9t`pL_$H)(M%diSnrfliNvuZJG3#^Jy;Q>b(2}RyPYc*{{x>mHi7C
zUu2BiLB`d2H^NU`Vc^O9b_vV-9+q;dKW+q0cB*s!V%BpP<K{T?3gf$Z{Ctt+KV<wC
zV_o+><EJf=f{(HMPz;R8>>T5PUjm%`Q*Zd;Y7hBe0H=B#$>Z=?F82`+`R7=^s!R&r
z#`5oa$bZW6=02VN)Oxad4fnv0^T1CAPWGS1_D^Md&Sl(O*Hr;O6z5BMtx_;OMbb4M
z`fm{OtW+aytp7pozgsx1FUCExr_AUVM=@^3PcGx;zQ8ZWPpv?{JqI|o?_{HW@gA!v
z*Iaj9$MV|@`OPf9j{U~V6ze6%)pIb_@BR*)&JC>AM4LVq_)u%nlZp6ez-b&-&x5dR
z6W2c0U&S2=ZWPxrbY$|IdQNvX<Fgpgsh0r#ZV+8T#?AHErHuCqN;!m|xHdCxp69dz
zPZo!-viwc#7&ZL8&$!QM-)|YeyIhv1`bGNT<Tp3o*c@vpaH{VLV;sn3eCsMHsr)dT
zarJytwaZzIui^R@aRHYBPgbw>9{4uk)L!dukP1|LwXy!WtY5X)Ta15rfs|ME{X*!;
zwA6D|xJ6tkLz3Gw6gc@oJy%ur8Vj84QO^glOcmEufn)#vXUY2{vF5Y9dQPaudHO>O
zq<{03Qc(P^3vThQdQ$(~$@1zstg>et<GH*(;bREv9ma3HRO+YS>k=2bN;3Zs0#5dv
zzebAvl*O|dH^-9|jJNRmnWqzLgNOcmJ@BVk&kaA91@bb;dYAFkpGlm4hmEe3q0-Ji
zhMhx!C#%;umM`Y@$s(!7ng!g)_c~d^@@9X((nJ5RSl*mZ@Ar^@+5;bSq>QV{9Oqcs
zh-)<PWc8W=T*N2WE05(Dd&pO@{G=u+IEUr$0#4($dY?h{i-$e*w6mV~c$}QYdiF4G
zo*QQkOK$&s;8bqcHmShJdV(JE5#Ur`^`3=_e|m0A`0eLP1(R6M?|@@T-0j*9+}91Y
ztT#OH&wwZM|M$SD+<ar488Dpd#p8flr;P?q^5%Kbt&E%F`5%ENE4K%XCq3=FKe~<U
zG6Xn{OItX8aQq^#!jf<#C#%{D1cJrofk<$f1)w%kw{&S%iB%d3hnAJs;uB4Q2)@5n
zQC$_Pg=A@UU|B_Vaj+s#icb&K2Jl@atE3tq-@;d%O0%+)O9YmdSCt2X;c#$eAXF6z
zue6qigO#B`X<cRIN@UTv03;&`q7i&HDo|4#;4dWw>7zqgB{elxVDbFI$Yhulir{Nj
z<Ff<E8wo8VgR282WkFbnPkiAsR^`j8LZx#qz?YGJV3x`so@FIv3CvzFeV#wypFb-Q
z0C(#Ag#mv)gZZ--Sb<q*&!0YT&P*$C>fAGCOrIM#WA^Mqe^H=l`i!}L<XB9fSeihe
zYMPbnUtujCAE;bTmE#ook*EpeDSyF~0438`qd4_M{?OWF@nto9{mQ@KbbK93ec4Gc
zLbsn4L#_m0`I4o&A9k9R;}pHLCK$jczDQnuuPT5~c!`gH5m+0F1VZ63K1Ed)tSYSt
zg;f>ki&Qgn{R>dOGRt3ZB3X>@PO*^l2`o`pX~iV@*(ozC=b(>P&CE&EN=b#0oQZ)z
zRp_EXu%e<Gb*c`}De;SXuv+<bD>H9FPBxh&6RAGSocff&u?f`{pCV&B_VW=g)AE9x
z30!ObXctrz6;d-h)fdsJ1LNUx*>?ODFJw8BvZ#-Qp;D*o8K#ik@&jTktU#zV7zwha
z-1y4Fl#5-QlOw;*Cz=lpE*(`_p%+}3t76hIc9Lvpc=7_uLJCDpO{9<Nt&oA^da<&0
z895O#N?!q7TE0w~B{^x<oHOukwbJscKwWL9)KN+iq$@>7plA$7sQ*h3a!r)~nAMtn
zJU)_V)Q7877&$QzD5<Z{$;rvpKkqiD1hE9q1TmI`gXNK0#8F`oKm0klfq7I3d<G8R
zew$NpI<OT*fx^jw!booR((3R<!Ek8+1&Xf+ia}MnRK@>^RdtmCd>+nUuJ=Up;SV=v
zqWB!0e?{J@bLY&MxoA;feAa}l+#L3<96+cS2Nvf{QNt+uZGb<$hXhnUNTV}8S9ftp
zstM#~<z`K^P{E2&RRSctt@`R*Epn)msFhT3=@Dsm1D4kY85-a80Gf;d!Uy^yWip1q
z)rKw%&`=1mqB-Wb=PHBcRY)j|ObB7%N!D!s1!&6gvT>_XsZg+T4o2GSfWL53KzE#@
zUyYRP9Ue<U0q2u<d2sdg8FK<TS>wreRCt*gUli`5CkE*Iip0_P`Y<oa&j)fg6%%li
z80DS8wKP-`2#1!EnA5dRq^^a}S4xNJUY;nru;Iv(6$O*Us74?BQ~g?Ve6|D&BQB=Q
zKp!Kgt9c<%T3gKndxAkzs8s^X%d1Kq{fT}kPZ&9!!AbZAMTie6s!=zvn8xq__r1|S
ze^TJoI`mO3TxmX;<@n==+CT%19!IhR{x8=C193s&1T{=glH;mqPb}_gYeQ%#`s8Oq
zcb1_mCe!~gMb~tj4rZN|h4{=01eVofI0=Pot7!;{tPHHc5>Rvrw!v9N&<Z871N?~Q
z9*@D778@9umSKpf?Cy8WkeJPBOvjpbMNSU2W(7PDh^(v$VGXsk+OKzCbj<Q9)z>gk
zObG-cW#Q_J0u|NE@Uc%ZD`Je-%Ta@7IOH`X&}x^w0A<Un>g4>AIG5yxF2saXQaE0<
zn4HpOOa>~-i)mmFqS0u4a~f^@1Zb6GATQt)yPuT^O^g5A!I-NDV?`~7;A%11X$u#O
zUsz=D94J0q%5k%ws&F5biy(?yHRX%-QL?$_M}`<J9<jl}`YBo07DKWcx-rb=<j^>a
zE*HV)jWHC`&@Wdh%R(1&t<(Z6aZMeLTujn5GCE@^XHfc2#Ij#57g#Tr79{e+Yjz^~
zj;K;WLO9Fe3X7NV*gw_Er42R>V&0<f0+*@^@df}@6U!emB4PEJlPwqR^jTgxA&6zB
z9E!+IVv#LbXTnemeRDOhd4=m84q+=tA19W>iwvc1EBS=oP+_D33pcNoocFrm!~jLB
z*JOlYws2ygC@0|e>%#*1QMNoy(sIS(Mnbqst(BZ5v}wC?s5>7|pbr|Gu2S=sr+uCk
z#?o~<?TZ3s<=EV-^>M-iKrR+(MI#0nvrD-v3T_3bGHO4N>+T2k(~&38+R=>>(S0YY
zUH}|^LnxxfdEG|_IYmuYJ5PN{&-QRP>t=Vt29K7D2#oG=k!-10QiO%##6Y(>K+JKf
zljdZLHW&TE4^g&8)QkOGT2Zi~Qk!|Qra(yUU-siDHNc(7pEuX5Oj{TkU~m+Q<~@92
zH3r;**%)#Q0|^02M*UBNhL#y63r@$pWrluWaqeV&i*XT_@N%HQ{;4WbD^{TY)8bX^
zdrz#Bcx6D1Ae~cLCk{qvETSm`1Ccs^-~jyLMmZyCl6BvYaq;*-AzW3nQXX2t!?3>a
z#3U}3bH6i-(i(w2tY3!NMqk`vnLuYl)ZotUf%ed0(dPn1^JenVl=M*X3L4twuqsxA
z#$fC?jAhhZCRfbTCN&$&xmg50#jZ?rHt4dvWi%8Pov9BzdNgU4s4)s{$K$=ZP)!)`
z6E}wxtFkLPPM|FmHh{c^BG~D{#xaQU3`froj}eSGm~P8!YpQGEb-jLa!evL%0H@C3
zXr|W&yqt;R7?b{V0=~;%R}t|~hE)|b(r{?=pg;~2RitH<v457cwR_?sTE?7t+y++F
zu0<Q+UTs4O7VCF+txUdF&XXsRbjZhxel={VeTbY^ut_heu8ZitkcEg-p$HaFA}$iv
z@3~mZ*Ou>h3IC&pwV63{Fo^jnLd0<9_>dZ462b(BOwP<p!L5cKt=e#-9Mx#Vy&$1l
z6yM~b|6*vDfz6RFb8!b#UQ}+*$)T+eMtX9UKXKW~okldTTqcXPp4>&?EU=0?xSVdB
zt%C>}F3VY;@%R7Lfx&(%pmk1aXG}ll>?DVjq#>vL?bPkWP!;`A2KSJK*N~W{lbz|R
zV{s9cDoka0N~N;T>HXBKIM?7|AFU%S)6hUM_K6r%#aWX(bdm)6rV|d%N<@_aRosev
zh(IkrUY@I}<`VlKH4wT}H=Sk5F$OE}obqZM@dRr_v;z#|Z&iq4JaO<CpX)ZHvu&a(
zvhMNtODRcesKS|dk1{8^wR7S`t1ox`uEL3WgW7e8(`qd=Iabvlh*06>E?>LF?}_5%
zwz{qgr@YI=h(eYoIYQ9ZNo)z%PMy-AzN(qs#~h+BV-QLVaM?0boTIlH6UBKiN=Eh3
zvDI;A@*tY524(5fA3hJv%<VqVXx8Us;~0$3z~po#PGrRygzg2{N}ZqVt-;?Pk;nY(
z8@a(o#dC6H%<*(V$rKsV0~6>VQtzR~oLxC`inDK#zL8T0jWvO=TG48Id7km-6k(ck
z9u;C~K@SRxs4KJj{f!{v@ONR=ML0qXEWjLBi6iKlGjWQo4w2ko!jhh5bDD{kJ5ftT
z{O~53LMQlG2GB!+%4A1KBGRST)Z8p0H=;J5a&u%ZlbqvLveM~TiBsl&yur`&l07IA
z$KKAcBW%(lH?ah<f-{y$|G6o;EeVpC0av^2LGxkKDKF7X#|`ojk_~ZWRDbTi7t<H=
z7+SDfbIVRFH?XX-x{8m>aGXW~sh(UXgrf`{(U4W*xtOzNa@WQ@ZM#L$81`dg?1w)l
zau256O}OfsYVq;IV;yHx2=-u2ump#*$<9mNm1Dy51-Vp^ecZ~zq9771291OzEmL<G
zibCNUD+_<~D3pc6&a9d+{pGC4N)0NmE3YUWhd+lTrSRlr9KCBG#LI%UWmZ<{$|@8g
zX(TLDR^U*Xj(da{GXbQ9Llr^Fz;`tj5i3jVcCv7rwX7N}-PDFktSlP5tSoUHn-#7W
z&qK39W&FB9St+zB4#kw<xL5p9BRsUD;Y(<hZz4z?>YntF8Bi%q4px?<EU6tU2rCQk
zLsa552lbl8|CHi&C;Z+n{m!twGWqv(6vb;p2^YT(<zPqQ4!=_6<e$v>6;<yEstmo<
z4O4n=M$ccy`4t^y$fp@Ry-%d)SHGXFsLzl$^Ph!u{CS*eRe$w;3PmSy{)3pB_6LE}
zyMZcyl<jvYXCNENcPhVn--%w2q%11G`W}X&>iZWE5tr%z3xU$NB~*U(Jqbl0=X}b3
zC8y|RNT+XAC|-T9LeW;vPxh0Y%6^6|daa9ms`9JvXDF(^pP|ZE`BnXI=KM2Qq52+&
zqU!q{lpn7aI_0bUw*w=eDE-cR`5br@-}+^?|E);W^ZPiTqT+8BX$sVPl#1SE<j<Zc
zg%wqDN`>MTZ87raaehUe52dgIl}}N6-AlJ${eFp}rxdD^B~|$p`h<~R{a%}*>OE5>
zZ~E_9&ac{E{a&%6o!lQ(exJHw`VuJFukx$k?^jgyW0lP;|8GYARTNOT6s6xw(k~T%
z3i|*z3FY4@Q#zT_XV>+MWcBNxVDKwc&i7~3_i+?8%Tv6fJ)n?GRBlq=b5K;tsWKI>
zXn*7<n^b=FUZbKu<ycmr@+o~ok(v6A%CEkops31E{huzCU&YZq!1VIf_jeTC;ZeTQ
zbF^W<)k>w{Y85~6re@-$@+tIq<R?topVul=G8HA`v@1`$r(62FRV0#a;41&|2CmfU
z)TpA!k>4saF5v+PuT@&~?!B^K)$3qj%66GU{@g-=jcbfg5a)*~R{`{{X|nw7|CSO{
Jj0^^A{U4~D<R}0D

literal 0
HcmV?d00001

diff --git a/test_pb_optimization.cpp b/test_pb_optimization.cpp
new file mode 100644
index 000000000..a62235e65
--- /dev/null
+++ b/test_pb_optimization.cpp
@@ -0,0 +1,104 @@
+#include "z3++.h"
+#include <iostream>
+
+using namespace z3;
+
+void test_pb_max_pattern() {
+    std::cout << "Testing PB max pattern detection\n";
+    
+    context c;
+    
+    // Create boolean variables
+    expr x1 = c.bool_const("x1");
+    expr x2 = c.bool_const("x2");
+    expr x3 = c.bool_const("x3");
+    expr y1 = c.bool_const("y1");
+    expr y2 = c.bool_const("y2");
+    expr z1 = c.bool_const("z1");
+    expr z2 = c.bool_const("z2");
+    expr z3 = c.bool_const("z3");
+    
+    // Create PB constraints like weighted sums
+    expr pb1 = 2*ite(x1, c.int_val(1), c.int_val(0)) + 3*ite(x2, c.int_val(1), c.int_val(0)) + ite(x3, c.int_val(1), c.int_val(0));  // potential max = 6
+    expr pb2 = ite(y1, c.int_val(1), c.int_val(0)) + 2*ite(y2, c.int_val(1), c.int_val(0));                     // potential max = 3  
+    expr pb3 = ite(z1, c.int_val(1), c.int_val(0)) + ite(z2, c.int_val(1), c.int_val(0)) + ite(z3, c.int_val(1), c.int_val(0));       // potential max = 3
+    
+    optimize opt(c);
+    
+    // The pattern the issue might be referring to:
+    // Instead of maximizing pb1 + pb2 + pb3 directly,
+    // we should detect the pattern and introduce auxiliary variables
+    
+    // Current approach: maximize pb1 + pb2 + pb3
+    opt.maximize(pb1 + pb2 + pb3);
+    
+    std::cout << "check: " << opt.check() << std::endl;
+    
+    if (opt.check() == sat) {
+        model m = opt.get_model();
+        std::cout << "Model: " << m << std::endl;
+        
+        // Get objective values
+        std::cout << "Objectives: " << opt.objectives().size() << std::endl;
+    }
+}
+
+void test_pb_max_with_constraints() {
+    std::cout << "\nTesting what the issue might want - auxiliary variables\n";
+    
+    context c;
+    
+    // Create boolean variables
+    expr x1 = c.bool_const("x1");
+    expr x2 = c.bool_const("x2");
+    expr y1 = c.bool_const("y1");
+    expr y2 = c.bool_const("y2");
+    
+    // PB expressions
+    expr pb1 = 2*ite(x1, c.int_val(1), c.int_val(0)) + ite(x2, c.int_val(1), c.int_val(0));  // max = 3
+    expr pb2 = ite(y1, c.int_val(1), c.int_val(0)) + 2*ite(y2, c.int_val(1), c.int_val(0));  // max = 3
+    
+    optimize opt(c);
+    
+    // What the issue might want: auxiliary variables p_k for each threshold k
+    // For pb1: p1_1, p1_2, p1_3 where pb1 >= k => p1_k
+    // For pb2: p2_1, p2_2, p2_3 where pb2 >= k => p2_k
+    // Then maximize: p1_1 + p1_2 + p1_3 + p2_1 + p2_2 + p2_3
+    
+    expr p1_1 = c.bool_const("p1_1");
+    expr p1_2 = c.bool_const("p1_2");
+    expr p1_3 = c.bool_const("p1_3");
+    expr p2_1 = c.bool_const("p2_1");
+    expr p2_2 = c.bool_const("p2_2");
+    expr p2_3 = c.bool_const("p2_3");
+    
+    // Add constraints: pb_i >= k => p_k
+    opt.add(implies(pb1 >= 1, p1_1));
+    opt.add(implies(pb1 >= 2, p1_2));
+    opt.add(implies(pb1 >= 3, p1_3));
+    opt.add(implies(pb2 >= 1, p2_1));
+    opt.add(implies(pb2 >= 2, p2_2));
+    opt.add(implies(pb2 >= 3, p2_3));
+    
+    // Maximize auxiliary variables
+    opt.maximize(ite(p1_1, c.int_val(1), c.int_val(0)) + ite(p1_2, c.int_val(1), c.int_val(0)) + ite(p1_3, c.int_val(1), c.int_val(0)) + ite(p2_1, c.int_val(1), c.int_val(0)) + ite(p2_2, c.int_val(1), c.int_val(0)) + ite(p2_3, c.int_val(1), c.int_val(0)));
+    
+    std::cout << "check: " << opt.check() << std::endl;
+    
+    if (opt.check() == sat) {
+        model m = opt.get_model();
+        std::cout << "Model: " << m << std::endl;
+        
+        // Evaluate original PB expressions
+        std::cout << "pb1 = " << m.eval(pb1) << std::endl;
+        std::cout << "pb2 = " << m.eval(pb2) << std::endl;
+        
+        std::cout << "Objectives: " << opt.objectives().size() << std::endl;
+    }
+}
+
+int main() {
+    test_pb_max_pattern();
+    test_pb_max_with_constraints();
+    return 0;
+}
\ No newline at end of file