mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

more resilient equality adapter

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-10-12 10:35:01 -07:00
parent ae7d76767b
commit e3d1849be2
2 changed files with 14 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/arith_eq_adapter.cpp
View file

@ -81,6 +81,7 @@ namespace smt {
}; };
void arith_eq_adapter::mk_axioms(enode * n1, enode * n2) { void arith_eq_adapter::mk_axioms(enode * n1, enode * n2) {
context & ctx = get_context();
if (n1 == n2) if (n1 == n2)
return; return;
ast_manager & m = get_manager(); ast_manager & m = get_manager();
@ -90,6 +91,13 @@ namespace smt {
std::swap(n1, n2); std::swap(n1, n2);
app * t1 = n1->get_owner(); app * t1 = n1->get_owner();
app * t2 = n2->get_owner(); app * t2 = n2->get_owner();
if (m.are_distinct(t1, t2)) {
expr_ref eq(m.mk_eq(t1, t2), m);
ctx.internalize(eq, true);
literal lit(ctx.get_bool_var(eq));
ctx.assign(~lit, nullptr, false);
return;
}
if (m.is_value(t1) && m.is_value(t2)) { if (m.is_value(t1) && m.is_value(t2)) {
// Nothing to be done // Nothing to be done
// We don't need to create axioms for 2 = 3 // We don't need to create axioms for 2 = 3
@ -99,7 +107,6 @@ namespace smt {
return; return;
} }
context & ctx = get_context();
CTRACE("arith_eq_adapter_relevancy", !(ctx.is_relevant(n1) && ctx.is_relevant(n2)), CTRACE("arith_eq_adapter_relevancy", !(ctx.is_relevant(n1) && ctx.is_relevant(n2)),
tout << "is_relevant(n1): #" << n1->get_owner_id() << " " << ctx.is_relevant(n1) << "\n"; tout << "is_relevant(n1): #" << n1->get_owner_id() << " " << ctx.is_relevant(n1) << "\n";
tout << "is_relevant(n2): #" << n2->get_owner_id() << " " << ctx.is_relevant(n2) << "\n"; tout << "is_relevant(n2): #" << n2->get_owner_id() << " " << ctx.is_relevant(n2) << "\n";
@ -123,8 +130,7 @@ namespace smt {
tout << "mk_detail " << mk_bounded_pp(n1->get_owner(), m, 5) << " " << tout << "mk_detail " << mk_bounded_pp(n1->get_owner(), m, 5) << " " <<
mk_bounded_pp(n2->get_owner(), m, 5) << "\n";); mk_bounded_pp(n2->get_owner(), m, 5) << "\n";);
app_ref t1_eq_t2(m); app_ref t1_eq_t2(m);
t1_eq_t2 = ctx.mk_eq_atom(t1, t2); t1_eq_t2 = ctx.mk_eq_atom(t1, t2);
SASSERT(!m.is_false(t1_eq_t2)); SASSERT(!m.is_false(t1_eq_t2));

5
src/smt/smt_theory.h
View file

@ -524,8 +524,13 @@ namespace smt {
behavior conflicts with a convention used by the theory/family. behavior conflicts with a convention used by the theory/family.
*/ */
virtual app * mk_eq_atom(expr * lhs, expr * rhs) { virtual app * mk_eq_atom(expr * lhs, expr * rhs) {
ast_manager& m = get_manager();
if (lhs->get_id() > rhs->get_id()) if (lhs->get_id() > rhs->get_id())
std::swap(lhs, rhs); std::swap(lhs, rhs);
if (m.are_distinct(lhs, rhs))
return m.mk_false();
if (m.are_equal(lhs, rhs))
return m.mk_true();
return get_manager().mk_eq(lhs, rhs); return get_manager().mk_eq(lhs, rhs);
} }