mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Remove conflict_kind

Browse source
This commit is contained in:
Jakob Rath 2022-11-17 12:24:10 +01:00
parent 00e8c53f9a
commit 38a43bd087
3 changed files with 9 additions and 56 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -25,7 +25,6 @@ TODO:
- force a restart if we get a bailout lemma or non-asserting conflict?
- Find a way to use resolve_value with forbidden interval lemmas.
Then get rid of conflict_kind_t::backtrack and m_relevant_vars.
Maybe:
x := a, y := b, z has no viable value
- assume y was propagated
@ -162,33 +161,17 @@ namespace polysat {
void conflict::reset() {
m_literals.reset();
m_vars.reset();
m_relevant_vars.reset();
m_var_occurrences.reset();
m_vars_occurring.reset();
m_lemmas.reset();
m_narrow_queue.reset();
m_kind = conflict_kind_t::ok;
m_level = UINT_MAX;
m_max_jump_level = UINT_MAX;
SASSERT(empty());
}
void conflict::set_backtrack() {
SASSERT(m_kind == conflict_kind_t::ok);
SASSERT(m_relevant_vars.empty());
m_kind = conflict_kind_t::backtrack;
}
bool conflict::is_relevant_pvar(pvar v) const {
switch (m_kind) {
case conflict_kind_t::ok:
return contains_pvar(v);
case conflict_kind_t::backtrack:
return pvar_occurs_in_constraints(v) || m_relevant_vars.contains(v);
}
UNREACHABLE();
return false;
return contains_pvar(v);
}
bool conflict::is_relevant(sat::literal lit) const {
@ -270,7 +253,11 @@ namespace polysat {
}
else {
logger().begin_conflict(header_with_var("forbidden interval lemma for v", v));
set_backtrack();
// set_backtrack(); // TODO: add the FI-lemma as a side lemma.
// The FI-lemma should not be the new core, because that will break variable dependencies.
// Alternatively, we'll need different types of variable dependencies. (one where v=n is in the core, another which only ensures that we don't skip v during backtracking).
// But since we now also propagate evaluated literals at the right (earlier) levels,
// we don't need to follow the variable assignments backwards to find the backjumping level for the FI-lemma.
VERIFY(s.m_viable.resolve(v, *this));
}
SASSERT(!empty());
@ -337,6 +324,9 @@ namespace polysat {
for (sat::literal lit : *lemma) {
LOG(" " << lit_pp(s, lit));
}
// TODO: call clause simplifier here?
// maybe it reduces the level we have to consider.
// Two kinds of side lemmas:
// 1. If all constraints are false, then the side lemma is an alternative conflict lemma.
// => we should at least jump back to the second-highest level in the lemma (could be lower, if so justified by another lemma)
@ -387,10 +377,8 @@ namespace polysat {
SASSERT(!empty());
m_literals.reset();
m_vars.reset();
m_relevant_vars.reset();
m_var_occurrences.reset();
m_vars_occurring.reset();
m_kind = conflict_kind_t::ok;
}
void conflict::resolve_bool(sat::literal lit, clause const& cl) {
@ -447,16 +435,6 @@ namespace polysat {
}
bool conflict::resolve_value(pvar v) {
if (is_backtracking()) {
for (auto const& c : s.m_viable.get_constraints(v))
for (pvar v : c->vars()) {
m_relevant_vars.insert(v);
logger().log_var(v);
}
return false;
}
SASSERT(contains_pvar(v));
auto const& j = s.m_justification[v];

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

@ -79,17 +79,6 @@ namespace polysat {
class conflict_iterator;
class conflict_resolver;
enum class conflict_kind_t {
// standard conflict resolution
ok,
// conflict contains the final lemma;
// backtrack to and revert the last relevant decision
// NOTE: this is currently used for the forbidden intervals lemmas.
// we should find a way to use resolve_value with these lemmas,
// to properly eliminate value propagations. (see todo notes above)
backtrack,
};
class conflict {
solver& s;
scoped_ptr<inference_logger> m_logger;
@ -98,7 +87,6 @@ namespace polysat {
// current conflict core consists of m_literals and m_vars
indexed_uint_set m_literals; // set of boolean literals in the conflict
uint_set m_vars; // variable assignments used as premises, shorthand for literals (x := v)
uint_set m_relevant_vars; // tracked for cone of influence but not directly involved in conflict resolution
unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it
uint_set m_vars_occurring; // set of variables that occur in at least one of the constraints in m_literals
@ -114,8 +102,6 @@ namespace polysat {
// e.g., because one of the watched variables is unassigned but irrelevant (e.g., x is irrelevant in x*y if y := 0).
sat::literal_vector m_narrow_queue;
conflict_kind_t m_kind = conflict_kind_t::ok;
// Level at which the conflict was discovered
unsigned m_level = UINT_MAX;
@ -141,10 +127,6 @@ namespace polysat {
unsigned level() const { return m_level; }
conflict_kind_t kind() const { return m_kind; }
bool is_backtracking() const { return m_kind == conflict_kind_t::backtrack; }
void set_backtrack();
bool is_relevant_pvar(pvar v) const;
bool is_relevant(sat::literal lit) const;

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

@ -73,13 +73,6 @@ namespace polysat {
out_indent() << assignment_pp(s, v, s.get_value(v)) << "\n";
m_used_vars.insert(v);
}
switch (core.kind()) {
case conflict_kind_t::ok:
break;
case conflict_kind_t::backtrack:
out_indent() << "(backtrack)\n";
break;
}
for (clause* lemma : core.side_lemmas()) {
out_indent() << "Side lemma: " << *lemma << "\n";
for (sat::literal lit : *lemma)