mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-05 05:49:13 +00:00
Code Activity

non-deterministic calls are marked

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-28 19:13:12 -07:00
parent 54257b6629
commit c739e581e4
68 changed files with 253 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/tactic/arith/bv2real_rewriter.cpp
View file

@ -443,9 +443,11 @@ bool bv2real_rewriter::mk_le(expr* s, expr* t, bool is_pos, bool is_neg, expr_re
expr_ref gt_proxy(m().mk_not(le_proxy), m());
expr_ref s2_is_nonpos(m_bv.mk_sle(s2, m_bv.mk_numeral(rational(0), s2_size)), m());
// TODO: non-deterministic parameter evaluation
expr_ref under(u().mk_bv_add(u().mk_bv_mul(rational(4), s1), u().mk_bv_mul(rational(5), s2)), m());
expr_ref z1(m_bv.mk_numeral(rational(0), m_bv.get_bv_size(under)), m());
expr_ref le_under(m_bv.mk_sle(under, z1), m());
// TODO: non-deterministic parameter evaluation
expr_ref over(u().mk_bv_add(u().mk_bv_mul(rational(2), s1), u().mk_bv_mul(rational(3), s2)), m());
expr_ref z2(m_bv.mk_numeral(rational(0), m_bv.get_bv_size(over)), m());
expr_ref le_over(m_bv.mk_sle(over, z2), m());
@ -462,8 +464,10 @@ bool bv2real_rewriter::mk_le(expr* s, expr* t, bool is_pos, bool is_neg, expr_re
// predicate may occur in negative polarity.
if (is_neg) {
// s1 + s2*sqrt(2) > 0 <== s2 > 0 & s1 + s2*(5/4) > 0; 4*s1 + 5*s2 > 0
// TODO: non-deterministic parameter evaluation
expr* e3 = m().mk_implies(m().mk_and(gt_proxy, m().mk_not(s2_is_nonpos)), m().mk_not(le_under));
// s1 + s2*sqrt(2) > 0 <== s2 <= 0 & s1 + s2*(3/2) > 0 <=> 2*s1 + 3*s2 > 0
// TODO: non-deterministic parameter evaluation
expr* e4 = m().mk_implies(m().mk_and(gt_proxy, s2_is_nonpos), m().mk_not(le_over));
u().add_side_condition(e3);
u().add_side_condition(e4);
@ -543,7 +547,9 @@ br_status bv2real_rewriter::mk_le(expr * s, expr * t, expr_ref & result) {
expr* ge = m_bv.mk_sle(t22, t12);
expr* le = m_bv.mk_sle(t12, t22);
expr* e1 = m().mk_or(gz1, gz2);
// TODO: non-deterministic parameter evaluation
expr* e2 = m().mk_or(m().mk_not(gz1), m().mk_not(lz2), ge);
// TODO: non-deterministic parameter evaluation
expr* e3 = m().mk_or(m().mk_not(gz2), m().mk_not(lz1), le);
result = m().mk_and(e1, e2, e3);
TRACE(bv2real_rewriter, tout << "\n";);
@ -587,6 +593,7 @@ br_status bv2real_rewriter::mk_eq(expr * s, expr * t, expr_ref & result) {
u().align_divisors(s1, s2, t1, t2, d1, d2);
u().align_sizes(s1, t1);
u().align_sizes(s2, t2);
// TODO: non-deterministic parameter evaluation
result = m().mk_and(m().mk_eq(s1, t1), m().mk_eq(s2, t2));
return BR_DONE;
}
@ -650,7 +657,9 @@ br_status bv2real_rewriter::mk_mul(expr* s, expr* t, expr_ref& result) {
if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
// s1*t1 + r1*(s2*t2) + (s1*t2 + s2*t2)*r1
expr_ref u1(m()), u2(m());
// TODO: non-deterministic parameter evaluation
u1 = u().mk_bv_add(u().mk_bv_mul(s1, t1), u().mk_bv_mul(r1, u().mk_bv_mul(t2, s2)));
// TODO: non-deterministic parameter evaluation
u2 = u().mk_bv_add(u().mk_bv_mul(s1, t2), u().mk_bv_mul(s2, t1));
rational tmp = d1*d2;
if (u().mk_bv2real(u1, u2, tmp, r1, result)) {