mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

superposition hotfix

Browse source
This commit is contained in:
Jakob Rath 2022-11-23 16:53:26 +01:00
parent bef1b9b429
commit 76c106476c
1 changed files with 7 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/math/polysat/superposition.cpp
View file

@ -49,8 +49,6 @@ namespace polysat {
return {}; return {};
// Only keep result if the degree in c2 was reduced. // Only keep result if the degree in c2 was reduced.
// (this condition might be too strict, but we use it for now to prevent looping) // (this condition might be too strict, but we use it for now to prevent looping)
// TODO: check total degree; only keep if total degree smaller or equal.
// can always do this if c1 is linear.
if (b.degree(v) <= r.degree(v)) if (b.degree(v) <= r.degree(v))
return {}; return {};
if (a.degree(v) <= r.degree(v)) if (a.degree(v) <= r.degree(v))
@ -74,7 +72,6 @@ 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); // 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); SASSERT(c2.bvalue(s) != l_false);
signed_constraint c = resolve1(v, c1, c2); signed_constraint c = resolve1(v, c1, c2);
@ -82,37 +79,25 @@ namespace polysat {
continue; continue;
SASSERT(c.is_currently_false(s)); SASSERT(c.is_currently_false(s));
// TODO: move this case distinction into conflict::add_lemma? // char const* inf_name = "?";
char const* inf_name = "?";
switch (c.bvalue(s)) { switch (c.bvalue(s)) {
case l_false: case l_false:
// new conflict state based on propagation and theory conflict core.add_lemma({c, ~c1, ~c2});
core.remove_all(); // core.log_inference(inference_sup("l_false", v, c2, c1));
core.insert(c1);
core.insert(c2);
core.insert(~c);
core.log_inference(inference_sup("l_false", v, c2, c1));
return l_true; return l_true;
case l_undef: case l_undef:
inf_name = "l_undef"; // inf_name = "l_undef";
// c evaluates to false,
// 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)); // 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
inf_name = "l_true";
break; break;
default: default:
UNREACHABLE(); UNREACHABLE();
break; break;
} }
// // c alone (+ variables) is now enough to represent the conflict.
// c alone (+ variables) is now enough to represent the conflict. // core.log_inference(inference_sup(inf_name, v, c2, c1));
core.set(c);
core.log_inference(inference_sup(inf_name, v, c2, c1));
return c->contains_var(v) ? l_undef : l_true; return c->contains_var(v) ? l_undef : l_true;
} }
return l_false; return l_false;