mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

Some assertions are now too strict

Browse source 
If possible, we should set the new constraint to l_true;
and revert most of this change later.
Or we adjust the conflict invariant:
- l_true constraints is the default case as before,
- l_undef constraints are new and justified by some side lemma, but
  should be treated by the conflict resolution methods like l_true
  constraints,
- l_false constraints are disallowed in the conflict (as before).
This commit is contained in:
Jakob Rath 2022-10-07 16:24:14 +02:00
parent 74b53c3323
commit 23a747235d
2 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -230,8 +230,9 @@ namespace polysat {
VERIFY(false); // fail here to force check when we encounter this case VERIFY(false); // fail here to force check when we encounter this case
} }
else { else {
// conflict due to assignment // Constraint c conflicts with the variable assignment
SASSERT(c.bvalue(s) == l_true); // SASSERT(c.bvalue(s) == l_true); // "morally" the bvalue should always be true. But (at least for now) some literals may be undef when they are only justified by a side lemma.
// TODO: maybe we can set them to true (without putting them on the search stack). But need to make sure to set them to false when finalizing the conflict; and before backjumping/learning. (tag:true_by_side_lemma)
SASSERT(c.is_currently_false(s)); SASSERT(c.is_currently_false(s));
insert(c); insert(c);
insert_vars(c); insert_vars(c);
@ -291,7 +292,7 @@ namespace polysat {
if (c.is_always_true()) if (c.is_always_true())
return; return;
LOG("Inserting " << lit_pp(s, c)); LOG("Inserting " << lit_pp(s, c));
SASSERT_EQ(c.bvalue(s), l_true); // SASSERT_EQ(c.bvalue(s), l_true); // TODO: see comment in 'set_impl' (tag:true_by_side_lemma)
SASSERT(!c.is_always_false()); // if we added c, the core would be a tautology SASSERT(!c.is_always_false()); // if we added c, the core would be a tautology
SASSERT(!c->vars().empty()); SASSERT(!c->vars().empty());
m_literals.insert(c.blit().index()); m_literals.insert(c.blit().index());
@ -328,6 +329,7 @@ namespace polysat {
clause_ref lemma = cb.build(); clause_ref lemma = cb.build();
SASSERT(lemma); SASSERT(lemma);
lemma->set_redundant(true); lemma->set_redundant(true);
LOG("Side lemma: " << *lemma);
m_lemmas.push_back(std::move(lemma)); m_lemmas.push_back(std::move(lemma));
} }
@ -596,6 +598,7 @@ namespace polysat {
out << " bail vars"; out << " bail vars";
for (auto v : m_bail_vars) for (auto v : m_bail_vars)
out << " v" << v; out << " v" << v;
// TODO: side lemmas?
return out; return out;
} }
} }

5
src/math/polysat/explain.cpp
View file

@ -69,7 +69,8 @@ namespace polysat {
SASSERT(c1.is_currently_true(s)); SASSERT(c1.is_currently_true(s));
SASSERT(c2.is_currently_false(s)); SASSERT(c2.is_currently_false(s));
SASSERT_EQ(c1.bvalue(s), l_true); SASSERT_EQ(c1.bvalue(s), l_true);
SASSERT_EQ(c2.bvalue(s), l_true); // SASSERT_EQ(c2.bvalue(s), l_true); // TODO: should always be l_true but currently it's not guaranteed if c2 was derived via side lemma (tag:true_by_side_lemma)
SASSERT(c2.bvalue(s) != l_false);
signed_constraint c = resolve1(v, c1, c2); signed_constraint c = resolve1(v, c1, c2);
if (!c) if (!c)
@ -93,7 +94,7 @@ namespace polysat {
// c should be unit-propagated to l_true by c1 /\ c2 ==> c // c should be unit-propagated to l_true by c1 /\ c2 ==> c
core.add_lemma({c, ~c1, ~c2}); core.add_lemma({c, ~c1, ~c2});
core.log_inference(inference_sup("l_undef lemma", v, c2, c1)); core.log_inference(inference_sup("l_undef lemma", v, c2, c1));
SASSERT_EQ(l_true, c.bvalue(s)); // SASSERT_EQ(l_true, c.bvalue(s)); // not true anymore (TODO: but it should be) (tag:true_by_side_lemma)
break; break;
case l_true: case l_true:
// c is just another constraint on the search stack; could be equivalent or better // c is just another constraint on the search stack; could be equivalent or better