mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 19:35:42 +00:00
Code Activity

propagation from containing slice depends on concrete values

Browse source
This commit is contained in:
Jakob Rath 2024-03-15 12:31:31 +01:00
parent 2102db2df8
commit dfb200a3c9
1 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/sat/smt/polysat/viable.cpp
View file

@ -598,7 +598,6 @@ namespace polysat {
VERIFY_EQ(e->src.size(), 1); VERIFY_EQ(e->src.size(), 1);
VERIFY_EQ(c.get_constraint(index), e->src[0]); VERIFY_EQ(c.get_constraint(index), e->src[0]);
result.push_back(c.get_dependency(index)); result.push_back(c.get_dependency(index));
// result.append(c.explain_weak_eval(c.get_constraint(index)));
} }
}; };
@ -637,18 +636,19 @@ namespace polysat {
// there is just one entry // there is just one entry
SASSERT(m_explain.size() == 1); SASSERT(m_explain.size() == 1);
explain_entry(last.e); explain_entry(last.e);
// assignment conflict and propagation from containing slice depends on concrete values,
// so we also need the evaluations of linear terms
auto index = last.e->constraint_index;
if (!index.is_null())
result.append(c.explain_weak_eval(c.get_constraint(index)));
auto exp = propagate_from_containing_slice(last.e, last.value, result); auto exp = propagate_from_containing_slice(last.e, last.value, result);
// verbose_stream() << "exp is " << exp << "\n";
if (!exp.is_null()) { if (!exp.is_null()) {
result.clear(); result.clear();
result.push_back(exp); result.push_back(exp);
} }
else {
// could not propagate to subslice
// conflict depends on evaluation
auto index = last.e->constraint_index;
if (!index.is_null())
result.append(c.explain_weak_eval(c.get_constraint(index)));
}
} }
unmark(); unmark();
if (c.inconsistent()) if (c.inconsistent())