From 766b9df4e2514fc2cd72bccba134d3c35c1feb7f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 12 Oct 2024 10:25:19 -0700 Subject: [PATCH] fixup handling of disequality propagation Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_egraph.cpp | 16 +++++++++++++++- src/ast/euf/euf_egraph.h | 3 ++- src/ast/sls/sls_euf_plugin.cpp | 19 ++++++++++++------- 3 files changed, 29 insertions(+), 9 deletions(-) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index eaa290bbf..215af84d7 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -82,8 +82,11 @@ namespace euf { void egraph::reinsert_equality(enode* p) { SASSERT(p->is_equality()); - if (p->value() != l_true && p->get_arg(0)->get_root() == p->get_arg(1)->get_root()) + if (p->value() != l_true && p->get_arg(0)->get_root() == p->get_arg(1)->get_root()) { queue_literal(p, nullptr); + if (p->value() == l_false && !m_on_propagate_literal) + set_conflict(p->get_arg(0), p->get_arg(1), p->m_lit_justification); + } } void egraph::queue_literal(enode* p, enode* ante) { @@ -201,6 +204,17 @@ namespace euf { } } + void egraph::new_diseq(enode* n, void* reason) { + SASSERT(m.is_eq(n->get_expr())); + auto j = justification::external(reason); + auto a = n->get_arg(0), b = n->get_arg(1); + auto r1 = a->get_root(), r2 = b->get_root(); + if (r1 == r2) + set_conflict(a, b, j); + else + set_value(n, l_false, j); + } + void egraph::new_diseq(enode* n) { SASSERT(n->is_equality()); SASSERT(n->value() == l_false); diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index 8822b07e7..4280b4780 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -278,10 +278,11 @@ namespace euf { */ void merge(enode* n1, enode* n2, void* reason) { merge(n1, n2, justification::external(reason)); } void new_diseq(enode* n); + void new_diseq(enode* n, void* reason); /** - \brief propagate set of merges. + \brief propagate set of merges. This call may detect an inconsistency. Then inconsistent() is true. Use then explain() to extract an explanation for the conflict. diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp index 5a26c0651..fcaa72460 100644 --- a/src/ast/sls/sls_euf_plugin.cpp +++ b/src/ast/sls/sls_euf_plugin.cpp @@ -141,11 +141,16 @@ namespace sls { m_stack.push_back(lit); g.push(); - if (!lit.sign() && m.is_eq(e, x, y)) { - auto a = g.find(x); - auto b = g.find(y); - g.merge(a, b, to_ptr(lit)); - g.merge(g.find(e), g.find(m.mk_true()), to_ptr(lit)); + if (m.is_eq(e, x, y)) { + if (lit.sign()) + g.new_diseq(g.find(e), to_ptr(lit)); + else { + auto a = g.find(x); + auto b = g.find(y); + g.merge(a, b, to_ptr(lit)); + } + + // g.merge(g.find(e), g.find(!lit.sign()), to_ptr(lit)); } else if (!lit.sign() && m.is_distinct(e)) { auto n = to_app(e)->get_num_args(); @@ -158,8 +163,8 @@ namespace sls { if (!g.find(eq)) { euf::enode* args[2] = { g.find(a), g.find(b) }; c = g.mk(eq, 0, 2, args); - } - g.merge(c, g.find(m.mk_false()), to_ptr(lit)); + } + g.new_diseq(c, to_ptr(lit)); } } }