mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

add assertion back for failing unit test, add comment about what is the bug

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-23 11:30:26 +01:00
parent 5e1ad37533
commit 5e7ff769b4
2 changed files with 9 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -127,7 +127,7 @@ namespace polysat {
*/ */
void conflict::insert(signed_constraint c) { void conflict::insert(signed_constraint c) {
if (c.is_always_true()) if (c.is_always_true())
return; return;
if (c->is_marked()) if (c->is_marked())
return; return;
LOG("inserting: " << c); LOG("inserting: " << c);
@ -150,6 +150,7 @@ namespace polysat {
*/ */
void conflict::insert(signed_constraint c, vector<signed_constraint> const& premises) { void conflict::insert(signed_constraint c, vector<signed_constraint> const& premises) {
keep(c); keep(c);
clause_builder c_lemma(s); clause_builder c_lemma(s);
for (auto premise : premises) { for (auto premise : premises) {
LOG_H3("premise: " << premise); LOG_H3("premise: " << premise);
@ -162,7 +163,7 @@ namespace polysat {
clause_ref lemma = c_lemma.build(); clause_ref lemma = c_lemma.build();
SASSERT(lemma); SASSERT(lemma);
cm().store(lemma.get(), s); cm().store(lemma.get(), s);
if (s.m_bvars.value(c.blit()) == l_undef) if (c.bvalue(s) == l_undef)
s.assign_propagate(c.blit(), *lemma); s.assign_propagate(c.blit(), *lemma);
} }

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

@ -76,8 +76,12 @@ namespace polysat {
// Ensure that c is assigned and justified // Ensure that c is assigned and justified
premises.push_back(c1); premises.push_back(c1);
premises.push_back(c2); premises.push_back(c2);
// var dependency on c is lost
// c evaluates to false, when the clause ~c1 or ~c2 or c
// gets created, c is assigned to false by evaluation propagation
// It should have been assigned true by unit propagation.
core.replace(c2, c, premises); core.replace(c2, c, premises);
// SASSERT_EQ(l_true, c.bvalue(s)); // TODO: currently violated, check this! SASSERT_EQ(l_true, c.bvalue(s)); // TODO: currently violated, check this!
SASSERT(c.is_currently_false(s)); SASSERT(c.is_currently_false(s));
break; break;
default: default:
@ -88,6 +92,7 @@ namespace polysat {
// c alone (+ variables) is now enough to represent the conflict. // c alone (+ variables) is now enough to represent the conflict.
core.reset(); core.reset();
core.set(c); core.set(c);
std::cout << "set c\n";
return c->contains_var(v) ? l_undef : l_true; return c->contains_var(v) ? l_undef : l_true;
} }
return l_false; return l_false;