mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-22 08:44:37 -07:00
parent 0013ae5089
commit e5df395380
1 changed files with 22 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -19,6 +19,9 @@ Notes:
TODO: If we have e.g. 4x+y=2 and y=0, then we have a conflict no matter the value of x, so we should drop x=? from the core. TODO: If we have e.g. 4x+y=2 and y=0, then we have a conflict no matter the value of x, so we should drop x=? from the core.
(works currently if x is unassigned; for other cases we would need extra info from constraint::is_currently_false) (works currently if x is unassigned; for other cases we would need extra info from constraint::is_currently_false)
TODO: build_lemma:
note that we may have added too many variables: e.g., y disappears in x*y if x=0
TODO: keep is buggy. The assert TODO: keep is buggy. The assert
SASSERT(premise.is_currently_true(s()) || premise.bvalue(s()) == l_true); SASSERT(premise.is_currently_true(s()) || premise.bvalue(s()) == l_true);
does not necessarily hold. A saturation premise could be inserted that is a resolvent that evaluates to false does not necessarily hold. A saturation premise could be inserted that is a resolvent that evaluates to false
@ -110,6 +113,9 @@ namespace polysat {
SASSERT(!empty()); SASSERT(!empty());
} }
/**
* The clause is conflicting in the current search state.
*/
void conflict::set(clause const& cl) { void conflict::set(clause const& cl) {
LOG("Conflict: " << cl); LOG("Conflict: " << cl);
SASSERT(empty()); SASSERT(empty());
@ -121,14 +127,18 @@ namespace polysat {
SASSERT(!empty()); SASSERT(!empty());
} }
/**
* Insert constraint into conflict state
* Skip trivial constraints
* - e.g., constant ones such as "4 > 1"... only true ones
* should appear, otherwise the lemma would be a tautology
*/
void conflict::insert(signed_constraint c) { void conflict::insert(signed_constraint c) {
LOG("inserting: " << c);
// Skip trivial constraints
// (e.g., constant ones such as "4 > 1"... only true ones should appear, otherwise the lemma would be a tautology)
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);
set_mark(c); set_mark(c);
if (c->has_bvar()) if (c->has_bvar())
insert_literal(c.blit()); insert_literal(c.blit());
@ -184,7 +194,10 @@ namespace polysat {
insert(m.lookup(~lit2)); insert(m.lookup(~lit2));
} }
/** If the constraint c is a temporary constraint derived by core saturation, insert it (and recursively, its premises) into \Gamma */ /**
* If the constraint c is a temporary constraint derived by core saturation,
* insert it (and recursively, its premises) into \Gamma
*/
void conflict::keep(signed_constraint c) { void conflict::keep(signed_constraint c) {
if (!c->has_bvar()) { if (!c->has_bvar()) {
remove(c); remove(c);
@ -214,15 +227,15 @@ namespace polysat {
} }
clause_builder conflict::build_lemma() { clause_builder conflict::build_lemma() {
SASSERT(std::all_of(m_vars.begin(), m_vars.end(), [&](pvar v) { return s.is_assigned(v); }));
SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](auto c) { return !c->has_bvar(); }));
LOG_H3("Build lemma from core"); LOG_H3("Build lemma from core");
LOG("core: " << *this); LOG("core: " << *this);
clause_builder lemma(s); clause_builder lemma(s);
while (!m_constraints.empty()) { while (!m_constraints.empty())
signed_constraint c = m_constraints.back(); keep(m_constraints.back());
SASSERT(!c->has_bvar());
keep(c);
}
for (auto c : *this) for (auto c : *this)
lemma.push(~c); lemma.push(~c);
@ -230,9 +243,6 @@ namespace polysat {
for (unsigned v : m_vars) { for (unsigned v : m_vars) {
if (!is_pmarked(v)) if (!is_pmarked(v))
continue; continue;
SASSERT(s.is_assigned(v)); // note that we may have added too many variables: e.g., y disappears in x*y if x=0
if (!s.is_assigned(v))
continue;
auto diseq = ~s.eq(s.var(v), s.get_value(v)); auto diseq = ~s.eq(s.var(v), s.get_value(v));
cm().ensure_bvar(diseq.get()); cm().ensure_bvar(diseq.get());
lemma.push(diseq); lemma.push(diseq);