mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

fix disequality conflict shortcut

Browse source
This commit is contained in:
Jakob Rath 2023-07-20 15:10:58 +02:00
parent ec4be975ee
commit 4142201d88
3 changed files with 50 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/polysat/slicing.cpp
View file

@ -185,7 +185,6 @@ namespace polysat {
auto args = {x, y};
eqn = m_egraph.mk(eq, 0, args.size(), args.begin());
auto j = euf::justification::external(encode_dep(lit));
LOG("calling set_value");
m_egraph.set_value(eqn, l_false, j);
SASSERT(eqn->is_equality());
SASSERT_EQ(eqn->value(), l_false);
@ -233,6 +232,13 @@ namespace polysat {
m_egraph.merge(sv, concat, encode_dep(dep_t()));
}
void slicing::add_congruence_if_needed(pvar v) {
if (!m_needs_congruence.contains(v))
return;
m_needs_congruence.remove(v);
add_congruence(v);
}
void slicing::update_var_congruences() {
for (pvar v : m_needs_congruence)
add_congruence(v);
@ -764,9 +770,10 @@ namespace polysat {
else {
SASSERT(c.is_negative());
enode* n = find_or_alloc_disequality(sy, sx, c.blit());
if (is_equal(sx, sy)) {
SASSERT_EQ(m_disequality_conflict, n); // already discovered by egraph in simple examples... TODO: probably not when we need the slice congruences
// m_disequality_conflict = n;
if (!m_disequality_conflict && is_equal(sx, sy)) {
add_congruence_if_needed(x);
add_congruence_if_needed(y);
m_disequality_conflict = n;
}
}
// without this check, when p = x - y we would handle both x = y and y = x separately

1
src/math/polysat/slicing.h
View file

@ -101,6 +101,7 @@ namespace polysat {
// for each variable v with base slices s1, ..., sn
void update_var_congruences();
void add_congruence(pvar v);
void add_congruence_if_needed(pvar v);
func_decl* mk_concat_decl(ptr_vector<expr> const& args);

40
src/test/slicing.cpp
View file

@ -274,9 +274,44 @@ namespace polysat {
s.pop();
}
}
};
}
// a = x[3:0]
// b = y[3:0]
// c = x[7:4]
// d = y[7:4]
// a = b
// c = d
// x != y
static void test8() {
std::cout << __func__ << "\n";
scoped_solver_slicing s;
slicing& sl = s.sl();
pvar x = s.add_var(8);
pvar y = s.add_var(8);
pvar a = sl.mk_extract(x, 3, 0);
pvar b = sl.mk_extract(y, 3, 0);
pvar c = sl.mk_extract(x, 7, 4);
pvar d = sl.mk_extract(y, 7, 4);
slicing::enode* sx = sl.var2slice(x);
slicing::enode* sy = sl.var2slice(y);
sl.add_constraint(s.eq(s.var(a), s.var(b)));
VERIFY(!sl.is_equal(sx, sy));
sl.add_constraint(s.eq(s.var(c), s.var(d)));
VERIFY(sl.is_equal(sx, sy));
sl.add_constraint(s.diseq(s.var(x), s.var(y)));
// sl.propagate();
VERIFY(sl.is_conflict());
sat::literal_vector reason_lits;
unsigned_vector reason_vars;
sl.explain(reason_lits, reason_vars);
std::cout << "Conflict: " << reason_lits << " vars " << reason_vars << "\n";
sl.display_tree(std::cout);
VERIFY(sl.invariant());
}
}; // test_slicing
} // namespace polysat
void tst_slicing() {
@ -288,5 +323,6 @@ void tst_slicing() {
test_slicing::test5();
test_slicing::test6();
test_slicing::test7();
test_slicing::test8();
std::cout << "ok\n";
}