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

Disable problematic resolve_with_assignment

Browse source
This commit is contained in:
Jakob Rath 2022-10-31 15:17:32 +01:00
parent eca72ffda1
commit eba59356f3
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/polysat/conflict.cpp
View file

@ -429,6 +429,7 @@ namespace polysat {
// The reason for lit is conceptually: // The reason for lit is conceptually:
// x1 = v1 /\ ... /\ xn = vn ==> lit // x1 = v1 /\ ... /\ xn = vn ==> lit
SASSERT(s.m_bvars.is_value_propagation(lit));
SASSERT(contains(lit)); SASSERT(contains(lit));
SASSERT(!contains(~lit)); SASSERT(!contains(~lit));
@ -441,9 +442,12 @@ namespace polysat {
// If evaluation depends on a decision, // If evaluation depends on a decision,
// then we rather keep the more general constraint c instead of inserting "x = v" // then we rather keep the more general constraint c instead of inserting "x = v"
bool has_decision = false; bool has_decision = false;
#if 0
// TODO: this is problematic; may skip relevant decisions
for (pvar v : c->vars()) for (pvar v : c->vars())
if (s.is_assigned(v) && s.m_justification[v].is_decision()) if (s.is_assigned(v) && s.m_justification[v].is_decision())
m_bail_vars.insert(v), has_decision = true; m_bail_vars.insert(v), has_decision = true;
#endif
if (!has_decision) { if (!has_decision) {
remove(c); remove(c);
@ -452,6 +456,9 @@ namespace polysat {
m_vars.insert(v); m_vars.insert(v);
} }
SASSERT(!contains(lit));
SASSERT(!contains(~lit));
logger().log(inf_resolve_with_assignment(s, lit, c)); logger().log(inf_resolve_with_assignment(s, lit, c));
} }