mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fixes to seq solver

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-25 10:35:14 -08:00
parent 080c9c6893
commit 64ba0b631a
3 changed files with 46 additions and 79 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

96
src/smt/seq_eq_solver.cpp
View file

@ -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();
}

28
src/smt/theory_seq.cpp
View file

@ -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";);

1
src/smt/theory_seq.h
View file

@ -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;