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 backjump state from conflict

Browse source
This commit is contained in:
Jakob Rath 2022-11-14 14:33:19 +01:00
parent 406696f0a3
commit 01af25ca02
6 changed files with 3 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -187,10 +187,6 @@ namespace polysat {
m_kind = conflict_kind_t::backtrack;
}
void conflict::set_backjump() {
SASSERT(m_kind == conflict_kind_t::ok);
m_kind = conflict_kind_t::backjump;
}
bool conflict::is_relevant_pvar(pvar v) const {
switch (m_kind) {
@ -200,9 +196,6 @@ namespace polysat {
return true;
case conflict_kind_t::backtrack:
return pvar_occurs_in_constraints(v) || m_relevant_vars.contains(v);
case conflict_kind_t::backjump:
UNREACHABLE(); // we don't follow the regular loop when backjumping
return false;
}
UNREACHABLE();
return false;
@ -412,9 +405,6 @@ namespace polysat {
SASSERT(contains(lit));
SASSERT(!contains(~lit));
if (is_backjumping())
return;
unsigned const lvl = s.m_bvars.level(lit);
signed_constraint c = s.lit2cnstr(lit);

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

@ -90,9 +90,6 @@ namespace polysat {
// we should find a way to use resolve_value with these lemmas,
// to properly eliminate value propagations. (see todo notes above)
backtrack,
// conflict contains the final lemma;
// force backjumping without further conflict resolution because a good lemma has been found
backjump,
};
class conflict {
@ -154,10 +151,8 @@ namespace polysat {
conflict_kind_t kind() const { return m_kind; }
bool is_bailout() const { return m_kind == conflict_kind_t::bailout; }
bool is_backtracking() const { return m_kind == conflict_kind_t::backtrack; }
bool is_backjumping() const { return m_kind == conflict_kind_t::backjump; }
void set_bailout();
void set_backtrack();
void set_backjump();
bool is_relevant_pvar(pvar v) const;
bool is_relevant(sat::literal lit) const;

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

@ -86,9 +86,6 @@ namespace polysat {
case conflict_kind_t::backtrack:
out_indent() << "(backtrack)\n";
break;
case conflict_kind_t::backjump:
out_indent() << "(backjump)\n";
break;
}
for (clause* lemma : core.side_lemmas()) {
out_indent() << "Side lemma: " << *lemma << "\n";

2
src/math/polysat/saturation.cpp
View file

@ -97,13 +97,13 @@ namespace polysat {
if (!inserting)
return false;
// TODO: add as a side lemma instead of changing the conflict
core.remove_all();
for (auto d : m_new_constraints)
core.insert_eval(d);
if (c.bvalue(s) != l_false) // conflict is due to the evaluation of c, so it depends on the variable values
core.insert_vars(c);
core.insert_eval(~c);
core.set_backjump();
core.logger().log(inf_name);
LOG("Core " << core);
return true;

6
src/math/polysat/solver.cpp
View file

@ -707,10 +707,6 @@ namespace polysat {
revert_decision(v);
return;
}
if (m_conflict.is_backjumping()) {
backjump_lemma();
return;
}
m_search.pop_assignment();
}
else {
@ -747,6 +743,7 @@ namespace polysat {
report_unsat();
}
#if 0
/**
* Simple backjumping for lemmas:
* jump to the level where the lemma can be (bool-)propagated,
@ -775,6 +772,7 @@ namespace polysat {
jump_level = std::max(jump_level, base_level());
backjump_and_learn(jump_level, *lemma);
}
#endif
/**
* Revert a decision that caused a conflict.

1
src/math/polysat/solver.h
View file

@ -210,7 +210,6 @@ namespace polysat {
unsigned base_level() const;
void resolve_conflict();
void backjump_lemma();
void revert_decision(pvar v);
void revert_bool_decision(sat::literal lit);
void backjump_and_learn(unsigned jump_level, clause& lemma);