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

slicing: fix dependency tracking for values

Browse source
This commit is contained in:
Jakob Rath 2023-11-06 14:17:28 +01:00
parent f49440690d
commit f09d37f93f
3 changed files with 21 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -899,30 +899,35 @@ namespace polysat {
SASSERT_EQ(root, root->get_root());
SASSERT_EQ(root, other->get_root());
enode* v1 = info(root).value_node; // root is the root
enode* v2 = info(other).value_node; // 'other' was its own root before the merge
enode* const v1 = info(root).value_node; // root is the root
enode* const v2 = info(other).value_node; // 'other' was its own root before the merge
if (v1 && v2 && get_value(v1) != get_value(v2)) {
// we have a conflict. add interpreted enodes to make the egraph realize it.
enode* i1 = mk_interpreted_value_node(v1);
enode* i2 = mk_interpreted_value_node(v2);
enode* const i1 = mk_interpreted_value_node(v1);
enode* const i2 = mk_interpreted_value_node(v2);
m_egraph.merge(i1, v1, dep_t().encode());
m_egraph.merge(i2, v2, dep_t().encode());
SASSERT(is_conflict());
return;
}
if (v1 || v2) {
if (!v1) set_value_node(root, v2);
if (!v2) set_value_node(other, v1);
rational const val = get_value(v1 ? v1 : v2);
enode* const v = v1 ? v1 : v2;
if (v && !(v1 && v2)) {
// exactly one node has a value
rational const val = get_value(v);
for (enode* n : euf::enode_class(other)) {
pvar const v = slice2var(n);
if (v == null_var)
continue;
if (m_solver.is_assigned(v))
pvar const var = slice2var(n);
if (var != null_var && m_solver.is_assigned(var))
continue; // TODO: could try to detect possible conflicts by checking value
enode* const vn = get_value_node(n);
if (!vn)
set_value_node(n, v);
if (var == null_var)
continue;
LOG("on_merge: v" << v << " := " << val);
m_solver.assign_propagate_by_slicing(v, val);
m_solver.assign_propagate_by_slicing(var, val);
}
}
}

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

@ -154,7 +154,7 @@ namespace polysat {
enode* parent(enode* s) const { return info(s).parent; }
enode* get_value_node(enode* s) const { return info(s->get_root()).value_node; }
enode* get_value_node(enode* s) const { return info(s).value_node; }
void set_value_node(enode* s, enode* value_node);
unsigned get_cut(enode* s) const { return info(s).cut; }

2
src/math/polysat/solver.cpp
View file

@ -1007,11 +1007,13 @@ namespace polysat {
}
void solver::revert_decision(pvar v) {
LOG("revert_decision: v" << v);
unsigned max_jump_level = get_level(v) - 1;
backjump_and_learn(max_jump_level, false);
}
void solver::revert_bool_decision(sat::literal const lit) {
LOG("revert_bool_decision: " << lit_pp(*this, lit));
unsigned max_jump_level = m_bvars.level(lit) - 1;
backjump_and_learn(max_jump_level, true);
// NOTE: happens in 42448.smt2; but does not seem to be a bug.