From 64ba0b631abb24ea68461789f76ea62308ea7fc3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 25 Feb 2021 10:35:14 -0800 Subject: [PATCH] fixes to seq solver --- src/smt/seq_eq_solver.cpp | 96 ++++++++++++++++++--------------------- src/smt/theory_seq.cpp | 28 +----------- src/smt/theory_seq.h | 1 - 3 files changed, 46 insertions(+), 79 deletions(-) diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index 5b931c193..a549305e4 100644 --- a/src/smt/seq_eq_solver.cpp +++ b/src/smt/seq_eq_solver.cpp @@ -467,7 +467,7 @@ bool theory_seq::branch_variable() { return true; } - unsigned turn = ctx.get_random_value() % 2 == 0; + bool turn = ctx.get_random_value() % 2 == 0; for (unsigned i = 0; i < 2; ++i, turn = !turn) { if (turn && branch_variable_mb()) { TRACE("seq", tout << "branch_variable_mb\n";); @@ -880,27 +880,26 @@ bool theory_seq::branch_ternary_variable_rhs(eq const& e) { add_length_to_eqc(y2); SASSERT(!xs.empty() && !ys.empty()); - if (!can_align_from_lhs(xs, ys)) { - expr_ref xsE = mk_concat(xs); - expr_ref ysE = mk_concat(ys); - expr_ref y1ys = mk_concat(y1, ysE); - expr_ref Z = m_sk.mk_align_r(xsE, y1, ysE, y2); - expr_ref ZxsE = mk_concat(Z, xsE); - expr_ref y1ysZ = mk_concat(y1ys, Z); - - dependency* dep = e.dep(); - bool propagated = false; - if (propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_len(y2), xs.size()))) - propagated = true; - if (propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_sub(mk_len(x), mk_len(y1)), ys.size()))) - propagated = true; - if (propagate_eq(dep, x, y1ysZ, true)) - propagated = true; - if (propagate_eq(dep, y2, ZxsE, true)) - propagated = true; - return propagated; - } - return false; + if (can_align_from_lhs(xs, ys)) + return false; + expr_ref xsE = mk_concat(xs); + expr_ref ysE = mk_concat(ys); + expr_ref y1ys = mk_concat(y1, ysE); + expr_ref Z = m_sk.mk_align_r(xsE, y1, ysE, y2); + expr_ref ZxsE = mk_concat(Z, xsE); + expr_ref y1ysZ = mk_concat(y1ys, Z); + + dependency* dep = e.dep(); + bool propagated = false; + if (propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_len(y2), xs.size()))) + propagated = true; + if (propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_sub(mk_len(x), mk_len(y1)), ys.size()))) + propagated = true; + if (propagate_eq(dep, x, y1ysZ, true)) + propagated = true; + if (propagate_eq(dep, y2, ZxsE, true)) + propagated = true; + return propagated; } // Equation is of the form xs ++ x = y1 ++ ys ++ y2 where xs, ys are units. @@ -924,27 +923,26 @@ bool theory_seq::branch_ternary_variable_lhs(eq const& e) { add_length_to_eqc(y2); SASSERT(!xs.empty() && !ys.empty()); - if (!can_align_from_rhs(xs, ys)) { - expr_ref xsE = mk_concat(xs); - expr_ref ysE = mk_concat(ys); - expr_ref ysy2 = mk_concat(ysE, y2); - expr_ref Z = m_sk.mk_align_l(xsE, y1, ysE, y2); - expr_ref xsZ = mk_concat(xsE, Z); - expr_ref Zysy2 = mk_concat(Z, ysy2); - - dependency* dep = e.dep(); - bool propagated = false; - if (propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_len(y1), xs.size()))) - propagated = true; - if (propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_sub(mk_len(x), mk_len(y2)), ys.size()))) - propagated = true; - if (propagate_eq(dep, x, Zysy2, true)) - propagated = true; - if (propagate_eq(dep, y1, xsZ, true)) - propagated = true; - return true; - } - return false; + if (can_align_from_rhs(xs, ys)) + return false; + expr_ref xsE = mk_concat(xs); + expr_ref ysE = mk_concat(ys); + expr_ref ysy2 = mk_concat(ysE, y2); + expr_ref Z = m_sk.mk_align_l(xsE, y1, ysE, y2); + expr_ref xsZ = mk_concat(xsE, Z); + expr_ref Zysy2 = mk_concat(Z, ysy2); + + dependency* dep = e.dep(); + bool propagated = false; + if (propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_len(y1), xs.size()))) + propagated = true; + if (propagate_lit(dep, 0, nullptr, m_ax.mk_ge(mk_sub(mk_len(x), mk_len(y2)), ys.size()))) + propagated = true; + if (propagate_eq(dep, x, Zysy2, true)) + propagated = true; + if (propagate_eq(dep, y1, xsZ, true)) + propagated = true; + return propagated; } bool theory_seq::branch_quat_variable() { @@ -1082,26 +1080,22 @@ bool theory_seq::branch_quat_variable(eq const& e) { if (ctx.get_assignment(lit1) == l_false && ctx.get_assignment(lit2) == l_true) { lits.push_back(~lit1); lits.push_back(lit2); - propagate_lit(nullptr, lits.size(), lits.c_ptr(), false_literal); - return true; + return propagate_lit(nullptr, lits.size(), lits.c_ptr(), false_literal); } if (ctx.get_assignment(lit1) == l_true && ctx.get_assignment(lit3) == l_true) { lits.push_back(lit1); lits.push_back(lit3); - propagate_lit(nullptr, lits.size(), lits.c_ptr(), false_literal); - return true; + return propagate_lit(nullptr, lits.size(), lits.c_ptr(), false_literal); } if (ctx.get_assignment(lit1) == l_true && ctx.get_assignment(lit2) == l_false) { lits.push_back(lit1); lits.push_back(~lit2); - propagate_lit(dep, lits.size(), lits.c_ptr(), false_literal); - return true; + return propagate_lit(dep, lits.size(), lits.c_ptr(), false_literal); } if (ctx.get_assignment(lit1) == l_false && ctx.get_assignment(lit3) == l_false) { lits.push_back(~lit1); lits.push_back(~lit3); - propagate_lit(dep, lits.size(), lits.c_ptr(), false_literal); - return true; + return propagate_lit(dep, lits.size(), lits.c_ptr(), false_literal); } UNREACHABLE(); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 65d3be15b..244057521 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2544,7 +2544,7 @@ void theory_seq::deque_axiom(expr* n) { m_ax.add_replace_axiom(n); } else if (m_util.str.is_extract(n)) { - m_ax.add_extract_axiom(purify(n)); + m_ax.add_extract_axiom(n); } else if (m_util.str.is_at(n)) { m_ax.add_at_axiom(n); @@ -2583,32 +2583,6 @@ void theory_seq::deque_axiom(expr* n) { } } -expr_ref theory_seq::purify(expr* e) { - app* a = to_app(e); - expr_ref_vector args(m); - bool has_fresh = false; - for (expr* arg : *a) { - expr_ref tmp(m); - m_rewrite(arg, tmp); - if (arg != tmp) { - has_fresh = true; - tmp = m.mk_fresh_const("purify", arg->get_sort()); - enode* n1 = ctx.get_enode(arg); - enode* n2 = ensure_enode(tmp); - justification* js = ctx.mk_justification( - ext_theory_eq_propagation_justification( - get_id(), ctx.get_region(), 0, nullptr, 0, nullptr, n1, n2)); - ctx.assign_eq(n1, n2, eq_justification(js)); - } - args.push_back(tmp); - } - - if (has_fresh) - return expr_ref(m.mk_app(a->get_decl(), args), m); - - return expr_ref(a, m); -} - expr_ref theory_seq::add_elim_string_axiom(expr* n) { zstring s; TRACE("seq", tout << mk_pp(n, m) << "\n";); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 1e54734ea..94fe410c0 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -496,7 +496,6 @@ namespace smt { bool reduce_ne(unsigned idx); bool branch_nqs(); lbool branch_nq(ne const& n); - expr_ref purify(expr* e); struct cell { cell* m_parent;