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

When adding clauses, prioritize bool-propagation over evaluation

Browse source 
See test_band1 and clause:  v2 == v0 & v1  -->  v2 <= 0
This commit is contained in:
Jakob Rath 2022-12-12 14:46:38 +01:00
parent 587e77648a
commit 917e1b6a4c
2 changed files with 29 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -185,6 +185,7 @@ namespace polysat {
}
void conflict::init(signed_constraint c) {
LOG("Conflict: constraint " << lit_pp(s, c));
SASSERT(empty());
m_level = s.m_level;
m_narrow_queue.push_back(c.blit()); // if the conflict is only due to a missed propagation of c
@ -217,6 +218,7 @@ namespace polysat {
}
void conflict::init(clause const& cl) {
LOG("Conflict: clause " << cl);
SASSERT(empty());
m_level = s.m_level;
for (auto lit : cl) {
@ -229,6 +231,7 @@ namespace polysat {
}
void conflict::init(pvar v, bool by_viable_fallback) {
LOG("Conflict: viable v" << v);
SASSERT(empty());
m_level = s.m_level;
if (by_viable_fallback) {

28
src/math/polysat/constraint_manager.cpp
View file

@ -142,8 +142,32 @@ namespace polysat {
return;
if (value_propagate) {
#if 1 // this should be already done with insert_eval when constructing the clause (maybe not for non-redundant clauses?)
// (this loop also masks the mistake of calling clause_builder::insert instead of clause_builder::insert_eval)
#if 1
// First, try to bool-propagate.
// Otherwise, we might get a clause-conflict and a missed propagation after resolving the conflict.
// With this, we will get a constraint-conflict instead.
// TODO: maybe it makes sense to choose bool vs. eval depending on which has the lower level?
sat::literal undef_lit = sat::null_literal;
for (sat::literal lit : cl) {
if (s.m_bvars.is_false(lit))
continue;
if (s.m_bvars.is_true(lit)) {
undef_lit = sat::null_literal;
break;
}
SASSERT(!s.m_bvars.is_assigned(lit));
if (undef_lit == sat::null_literal)
undef_lit = lit;
else {
undef_lit = sat::null_literal;
break;
}
}
if (undef_lit != sat::null_literal)
s.assign_propagate(undef_lit, cl);
// this should be already done with insert_eval when constructing the clause (maybe not for non-redundant clauses?)
// (this loop also masks the mistake of calling clause_builder::insert instead of clause_builder::insert_eval)
for (sat::literal lit : cl) {
if (s.m_bvars.is_false(lit))
continue;