mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

fix underflow bug when subtracting unsigned numbers

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-01-21 21:01:02 -08:00
parent 987efced76
commit 64ba44d2ac
2 changed files with 12 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/seq_eq_solver.cpp
View file

@ -663,7 +663,7 @@ bool theory_seq::branch_binary_variable(eq const& e) {
if (lenX + rational(xs.size()) != lenY + rational(ys.size())) {
// |x| - |y| = |ys| - |xs|
expr_ref a(mk_sub(mk_len(x), mk_len(y)), m);
expr_ref b(m_autil.mk_int(ys.size()-xs.size()), m);
expr_ref b(m_autil.mk_int(rational(ys.size())-rational(xs.size())), m);
propagate_lit(e.dep(), 0, nullptr, mk_eq(a, b, false));
return true;
}
@ -792,7 +792,7 @@ bool theory_seq::can_align_from_lhs(expr_ref_vector const& ls, expr_ref_vector c
// ls = x ++ rs ++ y, diff = |x|
else {
unsigned diff = (i + 1) - rs.size();
for (unsigned j = 0; same && j < rs.size()-1; ++j) {
for (unsigned j = 0; same && j + 1 < rs.size(); ++j) {
same = !m.are_distinct(ls[diff + j], rs[j]);
}
if (same) {

48
src/smt/theory_seq.cpp
View file

@ -1267,18 +1267,11 @@ bool theory_seq::solve_nc(unsigned idx) {
nc const& n = m_ncs[idx];
literal len_gt = n.len_gt();
expr_ref c(m);
#if 1
expr* a = nullptr, *b = nullptr;
VERIFY(m_util.str.is_contains(n.contains(), a, b));
literal pre, cnt, ctail, emp;
lbool is_gt = ctx.get_assignment(len_gt);
TRACE("seq", ctx.display_literal_smt2(tout << len_gt << " := " << is_gt << "\n", len_gt) << "\n";);
#if 0
if (canonizes(false, n.contains())) {
return true;
}
#endif
switch (is_gt) {
case l_true:
@ -1292,30 +1285,8 @@ bool theory_seq::solve_nc(unsigned idx) {
case l_false:
break;
}
#if 0
expr_ref a1(m), b1(m);
dependency* deps = n.deps();
if (!canonize(a, deps, a1)) {
return false;
}
if (!canonize(b, deps, b1)) {
return false;
}
if (a != a1 || b != b1) {
literal_vector lits;
expr_ref c(m_util.str.mk_contains(a1, b1), m);
propagate_eq(deps, lits, c, n.contains(), false);
m_ncs.push_back(nc(c, len_gt, deps));
m_new_propagation = true;
return true;
}
IF_VERBOSE(0, verbose_stream() << n.contains() << "\n");
#endif
m_ax.unroll_not_contains(n.contains());
return true;
#endif
return false;
return true;
}
theory_seq::cell* theory_seq::mk_cell(cell* p, expr* e, dependency* d) {
@ -1561,10 +1532,6 @@ void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) {
return;
if (m_sk.is_indexof_right(s))
return;
#if 0
if (m_sk.is_skolem(s))
return;
#endif
expr_ref lim_e = m_ax.add_length_limit(s, k);
unsigned k0 = 0;
if (m_length_limit_map.find(s, k0)) {
@ -3182,16 +3149,16 @@ void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) {
m_max_unfolding_lit = mk_literal(dlimit);
assumptions.push_back(dlimit);
for (auto const& kv : m_length_limit_map) {
assumptions.push_back(m_sk.mk_length_limit(kv.m_key, kv.m_value));
if (kv.m_value > 0)
assumptions.push_back(m_sk.mk_length_limit(kv.m_key, kv.m_value));
}
}
}
bool theory_seq::should_research(expr_ref_vector & unsat_core) {
TRACE("seq", tout << unsat_core << " " << m_util.has_re() << "\n";);
if (!m_has_seq) {
if (!m_has_seq)
return false;
}
unsigned k_min = UINT_MAX, k = 0, n = 0;
expr* s_min = nullptr, *s = nullptr;
bool has_max_unfolding = false;
@ -3210,7 +3177,8 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) {
}
}
}
if (k_min < UINT_MAX) {
if (k_min < UINT_MAX/4) {
m_max_unfolding_depth++;
k_min *= 2;
if (m_util.is_seq(s_min))
@ -3224,6 +3192,10 @@ bool theory_seq::should_research(expr_ref_vector & unsat_core) {
IF_VERBOSE(1, verbose_stream() << "(smt.seq :increase-depth " << m_max_unfolding_depth << ")\n");
return true;
}
else if (k_min >= UINT_MAX/4) {
throw default_exception("reached max unfolding");
}
return false;
}