mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 10:05:32 +00:00
Code Activity

fix #7572 and fix #7574

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-03-07 10:46:29 -08:00
parent 8df45b442b
commit 80f00f191a
26 changed files with 213 additions and 152 deletions
Download patch file Download diff file Expand all files Collapse all files

86
src/tactic/arith/bv2int_rewriter.cpp
View file

@ -147,12 +147,12 @@ br_status bv2int_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr *
br_status bv2int_rewriter::mk_le(expr * s, expr * t, expr_ref & result) {
expr_ref s1(m()), t1(m()), s2(m()), t2(m());
if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
if (is_ubv2int(s, s1) && is_ubv2int(t, t1)) {
align_sizes(s1, t1, false);
result = m_bv.mk_ule(s1, t1);
return BR_DONE;
}
if (is_bv2int_diff(s, s1, s2) && is_bv2int_diff(t, t1, t2)) {
if (is_ubv2int_diff(s, s1, s2) && is_ubv2int_diff(t, t1, t2)) {
// s1 - s2 <= t1 - t2
// <=>
// s1 + t2 <= t1 + s2
@ -187,9 +187,9 @@ br_status bv2int_rewriter::mk_gt(expr * arg1, expr * arg2, expr_ref & result) {
br_status bv2int_rewriter::mk_ite(expr* c, expr* s, expr* t, expr_ref& result) {
expr_ref s1(m()), t1(m());
if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
if (is_ubv2int(s, s1) && is_ubv2int(t, t1)) {
align_sizes(s1, t1, false);
result = m_bv.mk_bv2int(m().mk_ite(c, s1, t1));
result = m_bv.mk_ubv2int(m().mk_ite(c, s1, t1));
return BR_DONE;
}
@ -203,12 +203,12 @@ br_status bv2int_rewriter::mk_ite(expr* c, expr* s, expr* t, expr_ref& result) {
br_status bv2int_rewriter::mk_eq(expr * s, expr * t, expr_ref & result) {
expr_ref s1(m()), t1(m()), s2(m()), t2(m());
if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
if (is_ubv2int(s, s1) && is_ubv2int(t, t1)) {
align_sizes(s1, t1, false);
result = m().mk_eq(s1, t1);
return BR_DONE;
}
if (is_bv2int_diff(s, s1, s2) && is_bv2int_diff(t, t1, t2)) {
if (is_ubv2int_diff(s, s1, s2) && is_ubv2int_diff(t, t1, t2)) {
s1 = mk_bv_add(s1, t2, false);
t1 = mk_bv_add(s2, t1, false);
align_sizes(s1, t1, false);
@ -234,9 +234,9 @@ br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) {
rational r;
if (!m_arith.is_numeral(t, r) || !r.is_pos())
return BR_FAILED;
if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
if (is_ubv2int(s, s1) && is_ubv2int(t, t1)) {
align_sizes(s1, t1, false);
result = m_bv.mk_bv2int(m_bv.mk_bv_urem(s1, t1));
result = m_bv.mk_ubv2int(m_bv.mk_bv_urem(s1, t1));
TRACE("bv2int_rewriter", tout << result << "\n";);
return BR_DONE;
}
@ -244,14 +244,14 @@ br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) {
//
// (s1 - s2) mod t1 = (s1 + (t1 - (s2 mod t1))) mod t1
//
if (is_bv2int_diff(s, s1, s2) && is_bv2int(t, t1)) {
if (is_ubv2int_diff(s, s1, s2) && is_ubv2int(t, t1)) {
expr_ref u1(m());
align_sizes(s2, t1, false);
u1 = m_bv.mk_bv_urem(s2, t1);
u1 = m_bv.mk_bv_sub(t1, u1);
u1 = mk_bv_add(s1, u1, false);
align_sizes(u1, t1, false);
result = m_bv.mk_bv2int(m_bv.mk_bv_urem(u1, t1));
result = m_bv.mk_ubv2int(m_bv.mk_bv_urem(u1, t1));
TRACE("bv2int_rewriter", tout << result << "\n";);
return BR_DONE;
}
@ -275,8 +275,8 @@ br_status bv2int_rewriter::mk_rem(expr * arg1, expr * arg2, expr_ref & result) {
br_status bv2int_rewriter::mk_uminus(expr * s, expr_ref & result) {
expr_ref s1(m()), s2(m());
if (is_bv2int_diff(s, s1, s2)) {
result = m_arith.mk_sub(m_bv.mk_bv2int(s2), m_bv.mk_bv2int(s1));
if (is_ubv2int_diff(s, s1, s2)) {
result = m_arith.mk_sub(m_bv.mk_ubv2int(s2), m_bv.mk_ubv2int(s1));
return BR_DONE;
}
if (is_sbv2int(s, s1)) {
@ -341,17 +341,17 @@ expr* bv2int_rewriter::mk_bv_add(expr* s, expr* t, bool is_signed) {
br_status bv2int_rewriter::mk_add(expr* s, expr* t, expr_ref& result) {
expr_ref s1(m()), t1(m()), s2(m()), t2(m());
if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
result = m_bv.mk_bv2int(mk_bv_add(s1, t1, false));
if (is_ubv2int(s, s1) && is_ubv2int(t, t1)) {
result = m_bv.mk_ubv2int(mk_bv_add(s1, t1, false));
return BR_DONE;
}
if (is_bv2int_diff(s, s1, s2) && is_bv2int_diff(t, t1, t2)) {
if (is_ubv2int_diff(s, s1, s2) && is_ubv2int_diff(t, t1, t2)) {
// s1 - s2 + t1 - t2
// =
// s1 + t1 - (s2 + t2)
//
t1 = m_bv.mk_bv2int(mk_bv_add(s1, t1, false));
t2 = m_bv.mk_bv2int(mk_bv_add(s2, t2, false));
t1 = m_bv.mk_ubv2int(mk_bv_add(s1, t1, false));
t2 = m_bv.mk_ubv2int(mk_bv_add(s2, t2, false));
result = m_arith.mk_sub(t1, t2);
return BR_DONE;
}
@ -420,23 +420,23 @@ expr* bv2int_rewriter::mk_bv_mul(expr* s, expr* t, bool is_signed) {
br_status bv2int_rewriter::mk_mul(expr* s, expr* t, expr_ref& result) {
expr_ref s1(m()), s2(m()), t1(m()), t2(m());
if ((is_shl1(s, s1) && is_bv2int(t, t1)) ||
(is_shl1(t, s1) && is_bv2int(s, t1))) {
if ((is_shl1(s, s1) && is_ubv2int(t, t1)) ||
(is_shl1(t, s1) && is_ubv2int(s, t1))) {
unsigned n = m_bv.get_bv_size(s1);
unsigned m = m_bv.get_bv_size(t1);
s1 = mk_extend(m, s1, false);
t1 = mk_extend(n, t1, false);
result = m_bv.mk_bv2int(m_bv.mk_bv_shl(t1, s1));
result = m_bv.mk_ubv2int(m_bv.mk_bv_shl(t1, s1));
return BR_DONE;
}
if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
result = m_bv.mk_bv2int(mk_bv_mul(s1, t1, false));
if (is_ubv2int(s, s1) && is_ubv2int(t, t1)) {
result = m_bv.mk_ubv2int(mk_bv_mul(s1, t1, false));
return BR_DONE;
}
if ((is_bv2int(s, s1) && is_bv2int_diff(t, t1, t2)) ||
(is_bv2int(t, s1) && is_bv2int_diff(s, t1, t2))) {
t1 = m_bv.mk_bv2int(mk_bv_mul(s1, t1, false));
t2 = m_bv.mk_bv2int(mk_bv_mul(s1, t2, false));
if ((is_ubv2int(s, s1) && is_ubv2int_diff(t, t1, t2)) ||
(is_ubv2int(t, s1) && is_ubv2int_diff(s, t1, t2))) {
t1 = m_bv.mk_ubv2int(mk_bv_mul(s1, t1, false));
t2 = m_bv.mk_ubv2int(mk_bv_mul(s1, t2, false));
result = m_arith.mk_sub(t1, t2);
return BR_DONE;
}
@ -459,13 +459,13 @@ br_status bv2int_rewriter::mk_sub(unsigned num_args, expr * const* args, expr_re
br_status bv2int_rewriter::mk_sub(expr* s, expr* t, expr_ref& result) {
expr_ref s1(m()), t1(m()), s2(m()), t2(m());
if (is_bv2int_diff(s, s1, s2) && is_bv2int_diff(t, t1, t2)) {
if (is_ubv2int_diff(s, s1, s2) && is_ubv2int_diff(t, t1, t2)) {
// s1 - s2 - (t1 - t2)
// =
// s1 + t2 - (t1 + s2)
//
s1 = m_bv.mk_bv2int(mk_bv_add(s1, t2, false));
s2 = m_bv.mk_bv2int(mk_bv_add(s2, t1, false));
s1 = m_bv.mk_ubv2int(mk_bv_add(s1, t2, false));
s2 = m_bv.mk_ubv2int(mk_bv_add(s2, t1, false));
result = m_arith.mk_sub(s1, s2);
return BR_DONE;
}
@ -479,10 +479,10 @@ br_status bv2int_rewriter::mk_sub(expr* s, expr* t, expr_ref& result) {
return BR_FAILED;
}
bool bv2int_rewriter::is_bv2int(expr* n, expr_ref& s) {
bool bv2int_rewriter::is_ubv2int(expr* n, expr_ref& s) {
rational k;
bool is_int;
if (m_bv.is_bv2int(n)) {
if (m_bv.is_ubv2int(n)) {
s = to_app(n)->get_arg(0);
return true;
}
@ -498,7 +498,7 @@ bool bv2int_rewriter::is_shl1(expr* n, expr_ref& s) {
expr* s1, *s2;
rational r;
unsigned bv_size;
if(m_bv.is_bv2int(n, s2) &&
if(m_bv.is_ubv2int(n, s2) &&
m_bv.is_bv_shl(s2, s1, s2) &&
m_bv.is_numeral(s1, r, bv_size) &&
r.is_one()) {
@ -508,8 +508,8 @@ bool bv2int_rewriter::is_shl1(expr* n, expr_ref& s) {
return false;
}
bool bv2int_rewriter::is_bv2int_diff(expr* n, expr_ref& s, expr_ref& t) {
if (is_bv2int(n, s)) {
bool bv2int_rewriter::is_ubv2int_diff(expr* n, expr_ref& s, expr_ref& t) {
if (is_ubv2int(n, s)) {
t = m_bv.mk_numeral(0, 1);
return true;
}
@ -528,13 +528,13 @@ bool bv2int_rewriter::is_bv2int_diff(expr* n, expr_ref& s, expr_ref& t) {
//
expr *e1, *e2;
if (m_arith.is_sub(n, e1, e2) &&
is_bv2int(e1, s) &&
is_bv2int(e2, t)) {
is_ubv2int(e1, s) &&
is_ubv2int(e2, t)) {
return true;
}
if (m_arith.is_add(n, e1, e2) &&
m_arith.is_numeral(e1, k, is_int) && is_int && k.is_neg() &&
is_bv2int(e2, s)) {
is_ubv2int(e2, s)) {
k.neg();
unsigned sz = k.get_num_bits();
t = m_bv.mk_numeral(k, m_bv.mk_sort(sz));
@ -542,7 +542,7 @@ bool bv2int_rewriter::is_bv2int_diff(expr* n, expr_ref& s, expr_ref& t) {
}
if (m_arith.is_add(n, e1, e2) &&
m_arith.is_numeral(e2, k, is_int) && is_int && k.is_neg() &&
is_bv2int(e1, s)) {
is_ubv2int(e1, s)) {
k.neg();
unsigned sz = k.get_num_bits();
t = m_bv.mk_numeral(k, m_bv.mk_sort(sz));
@ -552,12 +552,12 @@ bool bv2int_rewriter::is_bv2int_diff(expr* n, expr_ref& s, expr_ref& t) {
}
bool bv2int_rewriter::is_sbv2int(expr* n, expr_ref& s) {
if (is_bv2int(n, s)) {
if (is_ubv2int(n, s)) {
s = m_bv.mk_zero_extend(1, s);
return true;
}
expr_ref u1(m()), u2(m());
if (is_bv2int_diff(n, u1, u2)) {
if (is_ubv2int_diff(n, u1, u2)) {
align_sizes(u1, u2, false);
u1 = mk_extend(1, u1, false);
u2 = mk_extend(1, u2, false);
@ -577,7 +577,7 @@ bool bv2int_rewriter::is_sbv2int(expr* n, expr_ref& s) {
lo == hi && lo == m_bv.get_bv_size(c3) - 1 &&
m_arith.is_sub(t, t1, t2) &&
e1 == t1 &&
m_bv.is_bv2int(e1, e2) &&
m_bv.is_ubv2int(e1, e2) &&
m_bv.is_extract(e2, lo1, hi1, e3) &&
lo1 == 0 && hi1 == hi-1 &&
m_arith.is_numeral(t2, k, is_int) && is_int &&
@ -590,7 +590,7 @@ bool bv2int_rewriter::is_sbv2int(expr* n, expr_ref& s) {
#if 0
// bv2int(b[0:n-2]) - ite(bv1 == b[n-1:n-1], 2^{n-1}, 0)
if (m().is_sub(n, e1, e2) &&
m_bv.is_bv2int(e1, e3) &&
m_bv.is_ubv2int(e1, e3) &&
m_bv.is_extract(e3, lo, hi, e4) &&
lo == 0 && hi == m_bv.get_bv_size(e4) - 2 &&
m().is_ite(e2, t1, t2, t3) &&
@ -612,7 +612,7 @@ expr* bv2int_rewriter::mk_sbv2int(expr* b) {
expr* bv1 = m_bv.mk_numeral(1, 1);
unsigned n = m_bv.get_bv_size(b);
expr* c = m().mk_eq(bv1, m_bv.mk_extract(n-1, n-1, b));
expr* e = m_bv.mk_bv2int(m_bv.mk_extract(n-2, 0, b));
expr* e = m_bv.mk_ubv2int(m_bv.mk_extract(n-2, 0, b));
expr* t = m_arith.mk_sub(e, m_arith.mk_numeral(power(rational(2), n-1), true));
return m().mk_ite(c, t, e);
}

4
src/tactic/arith/bv2int_rewriter.h
View file

@ -84,9 +84,9 @@ private:
br_status mk_sub(expr* s, expr* t, expr_ref& result);
br_status mk_uminus(expr* e, expr_ref & result);
bool is_bv2int(expr* e, expr_ref& s);
bool is_ubv2int(expr* e, expr_ref& s);
bool is_sbv2int(expr* e, expr_ref& s);
bool is_bv2int_diff(expr* e, expr_ref& s, expr_ref& t);
bool is_ubv2int_diff(expr* e, expr_ref& s, expr_ref& t);
bool is_zero(expr* e);
bool is_shl1(expr* e, expr_ref& s);

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

@ -146,7 +146,7 @@ void bv2real_util::mk_sbv2real(expr* e, expr_ref& result) {
rational r;
unsigned bv_size = m_bv.get_bv_size(e);
rational bsize = power(rational(2), bv_size);
expr_ref bvr(a().mk_to_real(m_bv.mk_bv2int(e)), m());
expr_ref bvr(a().mk_to_real(m_bv.mk_ubv2int(e)), m());
expr_ref c(m_bv.mk_sle(m_bv.mk_numeral(rational(0), bv_size), e), m());
result = m().mk_ite(c, bvr, a().mk_sub(bvr, a().mk_numeral(bsize, false)));
}

4
src/tactic/arith/nla2bv_tactic.cpp
View file

@ -131,7 +131,7 @@ class nla2bv_tactic : public tactic {
for (auto const& kv : p2) {
expr* v = kv.m_value;
unsigned num_bits = m_bv.get_bv_size(v);
expr* w = m_bv.mk_bv2int(m_bv.mk_bv_shl(m_bv.mk_numeral(1, num_bits), v));
expr* w = m_bv.mk_ubv2int(m_bv.mk_bv_shl(m_bv.mk_numeral(1, num_bits), v));
m_trail.push_back(w);
m_subst.insert(kv.m_key, w);
TRACE("nla2bv", tout << mk_ismt2_pp(kv.m_key, m_manager) << " " << mk_ismt2_pp(w, m_manager) << "\n";);
@ -235,7 +235,7 @@ class nla2bv_tactic : public tactic {
bv_sort = m_bv.mk_sort(num_bits);
s_bv = m_manager.mk_fresh_const(n->get_decl()->get_name(), bv_sort);
m_fmc->hide(s_bv);
s_bv = m_bv.mk_bv2int(s_bv);
s_bv = m_bv.mk_ubv2int(s_bv);
if (low) {
if (!(*low).is_zero()) {
// low <= s_bv

4
src/tactic/fd_solver/bounded_int2bv_solver.cpp
View file

@ -190,7 +190,7 @@ public:
for (auto const& kv : m_int2bv) {
rational offset;
VERIFY (m_bv2offset.find(kv.m_value, offset));
expr_ref value(m_bv.mk_bv2int(m.mk_const(kv.m_value)), m);
expr_ref value(m_bv.mk_ubv2int(m.mk_const(kv.m_value)), m);
if (!offset.is_zero()) {
value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true));
}
@ -293,7 +293,7 @@ private:
VERIFY(m_bv2offset.find(fbv, offset));
}
expr_ref t(m.mk_const(fbv), m);
t = m_bv.mk_bv2int(t);
t = m_bv.mk_ubv2int(t);
if (!offset.is_zero()) {
t = m_arith.mk_add(t, m_arith.mk_numeral(offset, true));
}