mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

new core perf - add merge_tf and enable_cgc distinction

Browse source 
perf fix for propagation behavior for equalities in the new core.
The old behavior was not to allow congruence closure on equalities.
The new behavior is to just not allow merging tf with equalities unless they appear somewhere in a foreign context (not under a Boolean operator)

The change re-surfaces merge_tf and enable_cgc distinction from the old core.
They can both be turned on or off.

merge_enabled renamed to cgc_enabled

The change is highly likely to introduce regressions in the new core.

Change propagation of literals from congruence:
- track antecedent enode. There are four ways to propagate
literals from the egraph.
- the literal is an equality and the two arguments are congruent
- the antecedent is merged with node n and the antecedent has a Boolean variable assignment.
- the antecedent is true or false, they are merged.
- the merge_tf flag is toggled to true but the node n has not been merged with true/false
This commit is contained in:
Nikolaj Bjorner 2022-11-23 11:37:07 +07:00
parent 11b712fee0
commit 22353c2d6c
10 changed files with 177 additions and 132 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/arith_internalize.cpp
View file

@ -372,7 +372,7 @@ namespace arith {
enode* n = ctx.get_enode(atom);
theory_var w = mk_var(n);
ctx.attach_th_var(n, this, w);
ctx.get_egraph().set_merge_enabled(n, false);
ctx.get_egraph().set_cgc_enabled(n, false);
if (is_int(v) && !r.is_int())
r = (k == lp_api::upper_t) ? floor(r) : ceil(r);
api_bound* b = mk_var_bound(lit, v, k, r);

47
src/sat/smt/euf_internalize.cpp
View file

@ -74,10 +74,8 @@ namespace euf {
}
if (auto* ext = expr2solver(e))
return ext->internalize(e, sign, root);
if (!visit_rec(m, e, sign, root)) {
TRACE("euf", tout << "visit-rec\n";);
if (!visit_rec(m, e, sign, root))
return sat::null_literal;
}
SASSERT(get_enode(e));
if (m.is_bool(e))
return literal(si.to_bool_var(e), sign);
@ -119,7 +117,7 @@ namespace euf {
SASSERT(!get_enode(e));
if (auto* s = expr2solver(e))
s->internalize(e);
else
else
attach_node(mk_enode(e, num, m_args.data()));
return true;
}
@ -188,6 +186,7 @@ namespace euf {
return lit;
}
set_bool_var2expr(v, e);
enode* n = m_egraph.find(e);
if (!n)
@ -195,8 +194,8 @@ namespace euf {
CTRACE("euf", n->bool_var() != sat::null_bool_var && n->bool_var() != v, display(tout << bpp(n) << " " << n->bool_var() << " vs " << v << "\n"));
SASSERT(n->bool_var() == sat::null_bool_var || n->bool_var() == v);
m_egraph.set_bool_var(n, v);
if (m.is_eq(e) || m.is_or(e) || m.is_and(e) || m.is_not(e))
m_egraph.set_merge_enabled(n, false);
if (si.is_bool_op(e))
m_egraph.set_cgc_enabled(n, false);
lbool val = s().value(lit);
if (val != l_undef)
m_egraph.set_value(n, val, justification::external(to_ptr(val == l_true ? lit : ~lit)));
@ -349,15 +348,6 @@ namespace euf {
else if (m.is_eq(e, th, el) && !m.is_iff(e)) {
sat::literal lit1 = expr2literal(e);
s().set_phase(lit1);
expr_ref e2(m.mk_eq(el, th), m);
enode* n2 = m_egraph.find(e2);
if (n2) {
sat::literal lit2 = expr2literal(e2);
add_root(~lit1, lit2);
add_root(lit1, ~lit2);
s().add_clause(~lit1, lit2, mk_distinct_status(~lit1, lit2));
s().add_clause(lit1, ~lit2, mk_distinct_status(lit1, ~lit2));
}
}
}
@ -476,26 +466,15 @@ namespace euf {
return n;
}
euf::enode* solver::mk_enode(expr* e, unsigned n, enode* const* args) {
euf::enode* r = m_egraph.mk(e, m_generation, n, args);
for (unsigned i = 0; i < n; ++i)
ensure_merged_tf(args[i]);
return r;
}
euf::enode* solver::mk_enode(expr* e, unsigned num, enode* const* args) {
void solver::ensure_merged_tf(euf::enode* n) {
switch (n->value()) {
case l_undef:
break;
case l_true:
if (n->get_root() != mk_true())
m_egraph.merge(n, mk_true(), to_ptr(sat::literal(n->bool_var())));
break;
case l_false:
if (n->get_root() != mk_false())
m_egraph.merge(n, mk_false(), to_ptr(~sat::literal(n->bool_var())));
break;
}
if (si.is_bool_op(e))
num = 0;
enode* n = m_egraph.mk(e, m_generation, num, args);
if (si.is_bool_op(e))
m_egraph.set_cgc_enabled(n, false);
return n;
}
}

93
src/sat/smt/euf_solver.cpp
View file

@ -316,13 +316,23 @@ namespace euf {
SASSERT(!l.sign());
m_egraph.explain_eq<size_t>(m_explain, cc, n->get_arg(0), n->get_arg(1));
break;
case constraint::kind_t::lit:
case constraint::kind_t::lit: {
e = m_bool_var2expr[l.var()];
n = m_egraph.find(e);
enode* ante = j.node();
SASSERT(n);
SASSERT(m.is_bool(n->get_expr()));
m_egraph.explain_eq<size_t>(m_explain, cc, n, (l.sign() ? mk_false() : mk_true()));
SASSERT(ante->get_root() == n->get_root());
m_egraph.explain_eq<size_t>(m_explain, cc, n, ante);
if (!m.is_true(ante->get_expr()) && !m.is_false(ante->get_expr())) {
bool_var v = ante->bool_var();
lbool val = ante->value();
SASSERT(val != l_undef);
literal ante(v, val == l_false);
m_explain.push_back(to_ptr(ante));
}
break;
}
default:
IF_VERBOSE(0, verbose_stream() << (unsigned)j.kind() << "\n");
UNREACHABLE();
@ -345,24 +355,30 @@ namespace euf {
euf::enode* n = m_egraph.find(e);
if (!n)
return;
bool sign = l.sign();
m_egraph.set_value(n, sign ? l_false : l_true, justification::external(to_ptr(l)));
bool sign = l.sign();
lbool old_value = n->value();
lbool new_value = sign ? l_false : l_true;
m_egraph.set_value(n, new_value, justification::external(to_ptr(l)));
if (old_value == l_undef && n->cgc_enabled()) {
for (enode* k : enode_class(n)) {
if (k->bool_var() == sat::null_bool_var)
continue;
if (k->value() == new_value)
continue;
auto& c = lit_constraint(n);
propagate(literal(k->bool_var(), sign), c.to_index());
if (k->value() == l_undef)
m_egraph.set_value(k, new_value, justification::external(to_ptr(l)));
else
return;
}
}
for (auto const& th : enode_th_vars(n))
m_id2solver[th.get_id()]->asserted(l);
size_t* c = to_ptr(l);
SASSERT(is_literal(c));
SASSERT(l == get_literal(c));
if (n->value_conflict()) {
euf::enode* nb = sign ? mk_false() : mk_true();
euf::enode* r = n->get_root();
euf::enode* rb = sign ? mk_true() : mk_false();
sat::literal rl(r->bool_var(), r->value() == l_false);
m_egraph.merge(n, nb, c);
m_egraph.merge(r, rb, to_ptr(rl));
SASSERT(m_egraph.inconsistent());
return;
}
if (n->merge_tf()) {
euf::enode* nb = sign ? mk_false() : mk_true();
m_egraph.merge(n, nb, c);
@ -374,9 +390,17 @@ namespace euf {
m_egraph.new_diseq(n);
else
m_egraph.merge(n->get_arg(0), n->get_arg(1), c);
}
}
}
constraint& solver::lit_constraint(enode* n) {
void* mem = get_region().allocate(sat::constraint_base::obj_size(sizeof(constraint)));
auto* c = new (sat::constraint_base::ptr2mem(mem)) constraint(n);
sat::constraint_base::initialize(mem, this);
return *c;
}
bool solver::unit_propagate() {
bool propagated = false;
@ -412,37 +436,44 @@ namespace euf {
void solver::propagate_literals() {
for (; m_egraph.has_literal() && !s().inconsistent() && !m_egraph.inconsistent(); m_egraph.next_literal()) {
auto [n, is_eq] = m_egraph.get_literal();
auto [n, ante] = m_egraph.get_literal();
expr* e = n->get_expr();
expr* a = nullptr, *b = nullptr;
bool_var v = n->bool_var();
SASSERT(m.is_bool(e));
size_t cnstr;
literal lit;
if (is_eq) {
literal lit;
if (!ante) {
VERIFY(m.is_eq(e, a, b));
cnstr = eq_constraint().to_index();
lit = literal(v, false);
}
else {
lbool val = n->get_root()->value();
if (val == l_undef && m.is_false(n->get_root()->get_expr()))
val = l_false;
if (val == l_undef && m.is_true(n->get_root()->get_expr()))
val = l_true;
a = e;
b = (val == l_true) ? m.mk_true() : m.mk_false();
SASSERT(val != l_undef);
cnstr = lit_constraint().to_index();
//
// There are the following three cases for propagation of literals
//
// 1. n == ante is true from equallity, ante = true/false
// 2. n == ante is true from equality, value(ante) != l_undef
// 3. value(n) != l_undef, ante = true/false, merge_tf is set on n
//
lbool val = ante->value();
if (val == l_undef) {
SASSERT(m.is_value(ante->get_expr()));
val = m.is_true(ante->get_expr()) ? l_true : l_false;
}
auto& c = lit_constraint(ante);
cnstr = c.to_index();
lit = literal(v, val == l_false);
}
unsigned lvl = s().scope_lvl();
CTRACE("euf", s().value(lit) != l_true, tout << lit << " " << s().value(lit) << "@" << lvl << " " << is_eq << " " << mk_bounded_pp(a, m) << " = " << mk_bounded_pp(b, m) << "\n";);
if (s().value(lit) == l_false && m_ackerman)
CTRACE("euf", s().value(lit) != l_true, tout << lit << " " << s().value(lit) << "@" << lvl << " " << mk_bounded_pp(a, m) << " = " << mk_bounded_pp(b, m) << "\n";);
if (s().value(lit) == l_false && m_ackerman && a && b)
m_ackerman->cg_conflict_eh(a, b);
switch (s().value(lit)) {
case l_true:
if (n->merge_tf() && !m.is_value(n->get_root()->get_expr()))
m_egraph.merge(n, ante, to_ptr(lit));
break;
case l_undef:
case l_false:
@ -889,7 +920,7 @@ namespace euf {
if (m.is_eq(e) && !m.is_iff(e))
ok = false;
euf::enode* n = get_enode(e);
if (n && n->merge_enabled())
if (n && n->cgc_enabled())
ok = false;
(void)ok;
@ -938,7 +969,7 @@ namespace euf {
case constraint::kind_t::eq:
return out << "euf equality propagation";
case constraint::kind_t::lit:
return out << "euf literal propagation";
return out << "euf literal propagation " << m_egraph.bpp(c.node()) ;
default:
UNREACHABLE();
return out;

6
src/sat/smt/euf_solver.h
View file

@ -45,9 +45,12 @@ namespace euf {
enum class kind_t { conflict, eq, lit };
private:
kind_t m_kind;
enode* m_node = nullptr;
public:
constraint(kind_t k) : m_kind(k) {}
constraint(enode* n): m_kind(kind_t::lit), m_node(n) {}
kind_t kind() const { return m_kind; }
enode* node() const { SASSERT(kind() == kind_t::lit); return m_node; }
static constraint& from_idx(size_t z) {
return *reinterpret_cast<constraint*>(sat::constraint_base::idx2mem(z));
}
@ -171,7 +174,6 @@ namespace euf {
void add_not_distinct_axiom(app* e, euf::enode* const* args);
void axiomatize_basic(enode* n);
bool internalize_root(app* e, bool sign, ptr_vector<enode> const& args);
void ensure_merged_tf(euf::enode* n);
euf::enode* mk_true();
euf::enode* mk_false();
@ -250,7 +252,7 @@ namespace euf {
constraint& mk_constraint(constraint*& c, constraint::kind_t k);
constraint& conflict_constraint() { return mk_constraint(m_conflict, constraint::kind_t::conflict); }
constraint& eq_constraint() { return mk_constraint(m_eq, constraint::kind_t::eq); }
constraint& lit_constraint() { return mk_constraint(m_lit, constraint::kind_t::lit); }
constraint& lit_constraint(enode* n);
// user propagator
void check_for_user_propagator() {