From fa5a50c4f982aaefa7c6ca358b2f9fc8e91a80ef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 12 Mar 2025 11:43:31 -0700 Subject: [PATCH] fix #7295 Signed-off-by: Nikolaj Bjorner --- genaisrc/genaiscript.d.ts | Bin 127689 -> 135966 bytes scripts/mk_nuget_task.py | 1 - src/ast/simplifiers/extract_eqs.cpp | 62 ++++++++++++++++++++++++++++ 3 files changed, 62 insertions(+), 1 deletion(-) diff --git a/genaisrc/genaiscript.d.ts b/genaisrc/genaiscript.d.ts index d2709fb4808cf71529e28e981c82463e9aaaa2f9..10b31f850e82027b00457ed0f406f4aa4e9f5462 100644 GIT binary patch delta 8465 zcmcIqdu&wKnb!egoPpQ|8?cQ7hj9qtdLA|y7Gn$s%p(Qt*w8egl)0Wc~ zq5Om{OqZXVD+qo}WOY+_b<5<(bwd#C;b~zzw9pgp>Dd$S#abfrN~W%5e9m!2e$=+| z1^1NcxSE+3UQZ8eE?=wLSiiS+gCFEqA{_tenSNe#GNYCYnyux9E97&d?Q-iEJ7wX( zp7s1HwG&HLGI$yzrITf1X<2-|O1Gf~CkDvw$PVQPARxRnXeLWM}KRyx#ikn(zp?$p^P}$cNevY|jW$aD3)$+G(bt@r^e79}W>VE%b`Ci+`p?4Z;l>Qj6^{EC9qk)-#}+M;KGDFpSG^P8Zp&NIdii!oOH=jsfLwmJV^90y#r?7Ap8h0B zCSQ)W)42ziAqn6YP;Fj@N(Deb)6^HsY5G(#1_Ac;Bzt@1t&ZI-eW9ho)!1~ee7YmK zu4W^-w>L@TGyW|p89E%$>iEPAAa(w#Fp^mmgJV^B|u3eORj@n9!|E6 zb*qFCowTe;L-f01){Ti!s8}+&CmImsij$L&Gpiv?O)IabW161uKPdW`Iy&7G?<;Hk zpV*pHd2Lc4y9!&AZ*1Gykd~np|5yHzR%Y88M@lwW%Hwk1|hn+n-h-Unk{%(t zAKV~+F|cpZ+N0hde~ZntzJ7L%{LaB7h#H&x8aU)Q!ls%!SZ*5pRb%4`-90sFTDCxm zb%kAi?@ZsyxKb!|AfG{%;gp-48duVaB9!0zP4m{O4WPdI>^s>RDbQt3dEKKIw{8Tq zg_&`voZ~KBO?BPz-Z;(L<u`ZxOe;ZZQ~(l;xvB*Y_4BM|03}y>(Zsd7 zDKhe~y>;DPV#_i6Q}XqZCi(c~OnI|&mdURcHp+EZTI3hpXI2+97uuP!p_r(CK2j`% zpUaivryqQvdMnw&yK{|g_PW2x>OTwRahO0!W^nifLMg-1@c_U)HLp}k?bimEuWpqy z^dXDYsKX@R5UNuptcoCCluhL$^79Y07WHvt8+e$U2SzX;WV&#%eCvk6T8cWM9m`R> zX!;(GdSCfEdq^JoYNUMbufK6$os-UqyoMNW_HI~gZF%Iy&TaP}v(mGpn(YXWeAaMG zIJ!;R72QJ7_1@UUTD%J?wCT@ru&6L|e{3FReN>Zdxv~6jBjat&UZ6c-lZAipX_8>1aaEOOrh( zEXxp@8KG01V@1pRoRZZp#sO6oN?ee!R^-0)4O<;5;aIPxp2860=cpx|9Bd361>4unO!dDPT^Ma_r~dIKr8 zx$^8q_Ex?3_)l3!C6{Gmb=yd?0KY=%y3@BhmVM~T!e=@n^H%WUQPz>X0=Ob%@5+TV zOQCA`1s{U>`HEkweA8g>v&uS)jWx)3RyHMqqA6x|*T7UggkKt5>+j z&Z`eMzr*@XZN!;r7=O%q|I|e%ix#Fk#T-1OS(|VWjOAe z(UH|$ZAvA?VEW`1=6eNLdkGfYL60^u7vPa!pmY_-+VHGvYbVd08$GG+bJpziFLria z-09tx>|yWvKd?wQC}Svnwie5|ZXp)Z)RxfTUW$v-V>yAcYf+MMAT?4cHN`5doMJjH zP%1Jie5pTC*)?TYS|%0e!_z85r8SdJ2rke+3A;a(JH}HxGFColaOi}{>`3w0;(JOI zi?|*f=pDq#!EQ53BZH#TXG@rh{hp07QfNKS zk=RiqF>s{%lF1a$J8^!@GIzK%YydkjfS=I)JVq^yIoXXIZOl;{H6tb{bNfB8avFVe z92y}o1=1(Vp!ia%F`-{WKaLSYO~UFxuCYa0=+kf{C3s5A87p1PliyHDY*+a2Pbeas z8%=N;L=UA%M7;m~J9ff*;Y%11{^V8Ga7dXXZ03&G)(o@?a?pGh_SY#u7jJpr`y$)s zCH|S!RgQj+O?5U78-heR3E9wqU!j{?yqjNRruXNsv55En)2y!EK5eC`J5UW=>8ysd zFylar8NWe=t|}ISvJ*H0PDh1>cQ9C{a|8=lLs=I7eejotri3b>@*X^eAe$B_fa5pwJFQ;ay$SrBFzclxPa31#qtP6V%2oASDmOvA#fkJ{S zdQ-ds^DMmtqjoK%_KD%Cts#^{O)nfL@*qTl;?t^F1X$kXgt8%=AH9L5=@T!prqY=J zrqzg0!e;!bAq*FII@tGh39*g!8Y?cAb^!>rNyHuS3-v;g$s#3`HWOObz>5NGL40K_ zgb@ufISrwiQa%kOSO6@{-eygBsfByQ7x||2hj7kE_=b7_r$3Rvd^hL4CRuyua(<%T z4A}*O9`f2>V%z?I-ogV~nr0=Wc_bz7Sb2fsjT#3B0I=P>U}1ikKv7Zy3i2N?j(E~A z4>)POlF(og_&dZ5R~^Zx3RJOBLih#0vAftkpF!d5G+qp1xCKvHcmaX4R1gWxR+*5R zdyPBA3IA-!8gP9626R)fP_q`P-No-hW`IV@WWQGxm2MGw*{5rNuPQFWb#y-aN2?Vg z2#3Dkp;Ewfw{Ea4mA1cOKVK1G$el%j1Af`a57=VO8fV1H1?%t}xMlWGg; zv)+LmY7SGY7iI)%AF*gJrVJVL8I)R#=V;ErQpx0JNxAOb&b7G6|6ATUZBp|8-rzks z!5VwUv>E=0Hm&(vRZdU`rF1D?-mf*bLEaeO=w&BZb7@qgCrCdpFW^H@WI>C(6cZXb zQh1Hap$d{YtDOa{sV8BiPSr9)W6PkvEF|%b;e*k&0&00^Yf@sJ21)?(Go*3n2`ntNKO`p2n&QC9^Xr^)u4>?aS{aDymAwlCdC;1OXDYquljuUbTo2wAZ6bmML+K&zfVyXmE z0inEgcOV=cAFpEfUQw`yqJTIq41z8Sf`uG@C-f78KOF3X7+Z+`bW#56%dN|yzqK_0 z4RuVZ0rIf#P#-Y89}_TW&?~oZvYRW}A@9*wSWD&eud<)1CnNL! zY=EY5DsTQXh^lk8%6Y1PoBvY)*$agZ|9n9GW#4~N@kZZeyGlzuy7&(+;j4*1a9I9d dF@XK~HyHI25TxgtE@-zf8lo(0)a6IRW#3&d{BpBo)iv~n6s4;>AL)1hQ;(f1OSrMBwZO^;+ zob&sg-|uwyd)5;_6^=X_vRGtA;)F1epT ze6f8QrLi@X_SAKNt75OVr!s_Kyvhb%JPO;ebt)&w3K5jLdG+(*iRyaod+*JBZQOqx zX|DTULhxbjKDaPoQ}IS*RfXq}6L!|^L`m)I`t``YMvPJ{Q6h^1YX(Qf5apq*u?|KW z%RJr)7mj%G0QN>{i0h4-UwN_L3+;<4w7(jO6^1|eK&#IK*L~Aqsjr5;DB{Ac;fyToR~*0v=%@oR01t5-{6G^RAmGL;lg6d1BQBE~e}s)tlzIOGQ$Ex7tUDM4jqnppdf@BDW5&#DWiWsi}7~Wi@El3_l&@)&LuGAK& z`ndphr5e?3$D5k^~H2ap&PApkHRgB<;>7iKel_*vs6tkLCA_@&*g>F(XCu32d zSnM_*iZO#9x!x>@=Qfz1nc&hU^`s4XY}s^h{lS^@i4u%Z8Hc$(DlkEXdwC*Zx+x}6 zS!StnGqLA%lUjWkmAV_|&dn6TISJ?GB#e__u#V?g|6z$lqeRNhXFOgC%_C*&vN`?- zBVhz|rJXl{HQjPLmYX(v)Xbgglnt`PFlF>fxSvxZctiHc23&^~W+cTdoDE|lV=9CU zZyBU#;}e+uN<78|3D3u|&+EgYgk>(uG45*q(~3Ra;&LIBhPp-(*(e#my}Xjek{+s| zZ9l8r6<4TSgE>JFF+(095<}2OB#w0P^o{~XHYP$dw|evjnv$B3h>@*7!p3SMFt?T= zm)ipJ8xJy#a6*vp4KXE5I!uHRCPJKPnP=O>;KFPS`@5MR(+3G#LyFi#g_qr?UXlI)ZCrsKI<+KTV2^ZwN zW^5`L5y4j7gd%?miw<)GI+W!(!yZ z33#NWEM?3hO`{TFf?@uikc>kj7DVG(3%|RvC3z^y_gnjuuX6mVvu%7*jn)L-nlZ zjG?j^n3QGphu4q?PG54t>JqztF@ZXq#!^(bY(<^$VzN}dHHr%Lzqg{|e09!tK){T%jd0n z*D-V;Pj5Vq-p^NuPN6b=%PF)YU&V3c)*H{FZ?JkzLbLS3n`oiC#!!S9Gq$i%#cu4` W5DhZ(Q^TYt*J;M}2MY84u>T85tLeM| diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index cfac605c7..b85ec4c8e 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -1,7 +1,6 @@ # # Copyright (c) 2018 Microsoft Corporation # - # 1. copy over dlls # 2. copy over libz3.dll for the different architectures # 3. copy over Microsoft.Z3.dll from suitable distribution diff --git a/src/ast/simplifiers/extract_eqs.cpp b/src/ast/simplifiers/extract_eqs.cpp index 8ab6be641..b14e01292 100644 --- a/src/ast/simplifiers/extract_eqs.cpp +++ b/src/ast/simplifiers/extract_eqs.cpp @@ -20,6 +20,7 @@ Author: #include "ast/for_each_expr.h" #include "ast/ast_pp.h" #include "ast/arith_decl_plugin.h" +#include "ast/bv_decl_plugin.h" #include "ast/simplifiers/extract_eqs.h" #include "ast/simplifiers/bound_manager.h" #include "params/tactic_params.hpp" @@ -81,6 +82,66 @@ namespace euf { } }; + class bv_extract_eq : public extract_eq { + ast_manager& m; + bv_util bv; + bool m_enabled = true; + + + void solve_add(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { + if (!bv.is_bv_add(x)) + return; + expr_ref term(m); + unsigned i = 0; + auto mk_term = [&](unsigned i) { + term = y; + unsigned j = 0; + for (expr* arg2 : *to_app(x)) { + if (i != j) + term = bv.mk_bv_sub(term, arg2); + ++j; + } + }; + for (expr* arg : *to_app(x)) { + if (is_uninterp_const(arg)) { + mk_term(i); + eqs.push_back(dependent_eq(orig, to_app(arg), term, d)); + } + ++i; + } + } + + void solve_eq(expr* orig, expr* x, expr* y, expr_dependency* d, dep_eq_vector& eqs) { + solve_add(orig, x, y, d, eqs); + } + + + public: + bv_extract_eq(ast_manager& m) : m(m), bv(m) {} + + void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override { + if (!m_enabled) + return; + auto [f, p, d] = e(); + expr* x, * y; + if (m.is_eq(f, x, y) && bv.is_bv(x)) { + solve_eq(f, x, y, d, eqs); + solve_eq(f, y, x, d, eqs); + } + + } + + void pre_process(dependent_expr_state& fmls) override { + if (!m_enabled) + return; + } + + void updt_params(params_ref const& p) override { + + } + + }; + class arith_extract_eq : public extract_eq { ast_manager& m; arith_util a; @@ -311,5 +372,6 @@ break; void register_extract_eqs(ast_manager& m, scoped_ptr_vector& ex) { ex.push_back(alloc(arith_extract_eq, m)); ex.push_back(alloc(basic_extract_eq, m)); + ex.push_back(alloc(bv_extract_eq, m)); } }