mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fixup handling of disequality propagation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-12 10:25:19 -07:00
parent d7b82366c6
commit 766b9df4e2
3 changed files with 29 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/euf/euf_egraph.cpp
View file

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

3
src/ast/euf/euf_egraph.h
View file

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

19
src/ast/sls/sls_euf_plugin.cpp
View file

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