mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

The justifications of value propagations may contain undiscovered bool/eval conflicts

Browse source
This commit is contained in:
Jakob Rath 2023-03-18 07:52:52 +01:00
parent b75fcb5714
commit 142e33d2f4
2 changed files with 37 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -263,6 +263,7 @@ namespace polysat {
if (c.is_always_true()) // TODO: caller should avoid this?
return;
LOG("Inserting " << lit_pp(s, c));
SASSERT_EQ(c.bvalue(s), l_true);
VERIFY_EQ(c.bvalue(s), l_true);
SASSERT(!c.is_always_true()); // such constraints would be removed earlier
SASSERT(!c.is_always_false()); // if we added c, the core would be a tautology
@ -277,6 +278,27 @@ namespace polysat {
}
}
bool conflict::insert_or_replace(signed_constraint c) {
switch (c.bvalue(s)) {
case l_true:
// regular case
insert(c);
return false;
case l_undef:
VERIFY_EQ(c.eval(s), l_true);
s.assign_eval(c.blit());
insert(c);
return false;
case l_false:
VERIFY_EQ(c.eval(s), l_true);
break;
}
// TODO: could keep lemmas? but whatever, this case seems very rare
reset();
init(~c);
return true;
}
void conflict::insert_vars(signed_constraint c) {
for (pvar v : c->vars())
if (s.is_assigned(v))
@ -389,16 +411,13 @@ namespace polysat {
m_vars.remove(v);
for (signed_constraint const c : s.m_viable.get_constraints(v))
insert(c);
if (insert_or_replace(c))
return;
for (auto const& i : s.m_viable.units(v)) {
signed_constraint eq1 = s.eq(i.lo(), i.lo_val());
signed_constraint eq2 = s.eq(i.hi(), i.hi_val());
if (eq1.bvalue(s) == l_undef)
s.assign_eval(eq1.blit());
if (eq2.bvalue(s) == l_undef)
s.assign_eval(eq2.blit());
insert(eq1);
insert(eq2);
if (insert_or_replace(s.eq(i.lo(), i.lo_val())))
return;
if (insert_or_replace(s.eq(i.hi(), i.hi_val())))
return;
}
logger().log(inf_resolve_value(s, v));
@ -571,7 +590,8 @@ namespace polysat {
}
std::ostream& conflict::display(std::ostream& out) const {
char const* sep = "";
out << "lvl " << m_level;
char const* sep = " ";
for (auto c : *this)
out << sep << c->bvar2string() << " " << c, sep = " ; ";
if (!m_vars.empty())

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

@ -148,6 +148,13 @@ namespace polysat {
*/
void insert(signed_constraint c);
/**
* Like 'insert', but check for missed lower bool/eval conflicts.
* If such a constraint is inserted, replace the current conflict by this one.
* Return true if the conflict has been replaced.
*/
bool insert_or_replace(signed_constraint c);
/** Insert assigned variables of c */
void insert_vars(signed_constraint c);