mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-21 16:16:38 +00:00
Code Activity

backtrack_fi

Browse source
This commit is contained in:
Jakob Rath 2022-04-25 17:37:50 +02:00
parent fc2633c964
commit 6bf897aad8
6 changed files with 113 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -41,6 +41,8 @@ namespace polysat {
scoped_ptr<std::ostream> m_out = nullptr;
unsigned m_conflicts = 0;
friend class conflict;
std::ostream& out() {
SASSERT(m_out);
return *m_out;
@ -52,13 +54,15 @@ namespace polysat {
public:
void begin_conflict() {
++m_conflicts;
LOG("Begin CONFLICT #" << m_conflicts);
m_used_constraints.reset();
m_used_vars.reset();
if (!m_out)
m_out = alloc(std::ofstream, "conflicts.txt");
else
out() << "\n\n\n\n\n\n\n\n\n\n\n\n";
out() << "CONFLICT #" << ++m_conflicts << "\n";
out() << "CONFLICT #" << m_conflicts << "\n";
}
void log_inference(conflict const& core, inference const* inf) {
@ -72,6 +76,8 @@ namespace polysat {
for (auto const& c : core) {
out_indent() << c.blit() << ": " << c << '\n';
m_used_constraints.insert(c.blit().index());
for (pvar v : c->vars())
m_used_vars.insert(v);
}
for (auto v : core.vars()) {
out_indent() << "v" << v << " := " << core.s.get_value(v) << "\n";
@ -86,12 +92,17 @@ namespace polysat {
out().flush();
}
void log_lemma(clause_builder const& cb) {
void log_lemma(solver const& s, clause_builder const& cb) {
out() << hline() << "\nLemma:";
for (auto const& lit : cb)
out() << " " << lit;
out() << "\n";
for (auto const& lit : cb)
out_indent() << lit << ": " << s.lit2cnstr(lit) << '\n';
out().flush();
// if (m_conflicts == 9)
// std::exit(0);
}
void end_conflict(search_state const& search, viable const& v) {
@ -104,6 +115,7 @@ namespace polysat {
for (pvar var : m_used_vars)
out_indent() << "v" << std::setw(3) << std::left << var << ": " << viable::var_pp(v, var) << "\n";
out().flush();
LOG("End CONFLICT #" << m_conflicts);
}
bool is_relevant(search_item const& item) const {
@ -118,6 +130,11 @@ namespace polysat {
}
};
void conflict::log_var(pvar v) {
if (m_logger)
m_logger->m_used_vars.insert(v);
}
conflict::conflict(solver& s): s(s) {
ex_engines.push_back(alloc(ex_polynomial_superposition, s));
ex_engines.push_back(alloc(eq_explain, s));
@ -177,6 +194,7 @@ namespace polysat {
unset_mark(c);
m_literals.reset();
m_vars.reset();
m_var_occurrences.reset();
m_bail_vars.reset();
m_conflict_var = null_var;
m_bailout = false;
@ -252,6 +270,11 @@ namespace polysat {
SASSERT(!c->vars().empty());
set_mark(c);
m_literals.insert(c.blit().index());
for (pvar v : c->vars()) {
if (v >= m_var_occurrences.size())
m_var_occurrences.resize(v + 1, 0);
m_var_occurrences[v]++;
}
}
void conflict::propagate(signed_constraint c) {
@ -302,6 +325,10 @@ namespace polysat {
void conflict::remove(signed_constraint c) {
unset_mark(c);
m_literals.remove(c.blit().index());
for (pvar v : c->vars()) {
if (v < m_var_occurrences.size())
m_var_occurrences[v]--;
}
}
void conflict::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises) {
@ -314,6 +341,7 @@ namespace polysat {
}
bool conflict::contains(sat::literal lit) const {
SASSERT(lit != sat::null_literal);
return m_literals.contains(lit.index());
}
@ -337,8 +365,6 @@ namespace polysat {
// clause: x \/ u \/ v
// resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v
SASSERT(lit != sat::null_literal);
SASSERT(~lit != sat::null_literal);
SASSERT(contains(lit));
SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
SASSERT(!contains(~lit));
@ -368,8 +394,6 @@ namespace polysat {
// The reason for lit is conceptually:
// x1 = v1 /\ ... /\ xn = vn ==> lit
SASSERT(lit != sat::null_literal);
SASSERT(~lit != sat::null_literal);
SASSERT(contains(lit));
SASSERT(!contains(~lit));
@ -411,7 +435,7 @@ namespace polysat {
s.decay_activity();
if (m_logger)
m_logger->log_lemma(lemma);
m_logger->log_lemma(s, lemma);
return lemma;
}

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

@ -101,8 +101,8 @@ namespace polysat {
/** Conflict state, represented as core (~negation of clause). */
class conflict {
solver& s;
// signed_constraints m_constraints; // new constraints used as premises
indexed_uint_set m_literals; // set of boolean literals in the conflict
unsigned_vector m_var_occurrences; // for each variable, the number of constraints in m_literals that contain it
uint_set m_vars; // variable assignments used as premises
uint_set m_bail_vars;
@ -137,6 +137,7 @@ namespace polysat {
/// Log inference at the current state.
void log_inference(inference const& inf);
void log_inference(char const* name) { log_inference(inference_named(name)); }
void log_var(pvar v);
/// Log relevant part of search state and viable.
void end_conflict();
@ -149,6 +150,8 @@ namespace polysat {
bool empty() const;
void reset();
bool pvar_occurs_in_constraints(pvar v) const { return v < m_var_occurrences.size() && m_var_occurrences[v] > 0; }
bool contains_pvar(pvar v) const { return m_vars.contains(v) || m_bail_vars.contains(v); }
bool is_marked(signed_constraint c) const;
bool is_marked(sat::bool_var b) const;

4
src/math/polysat/explain.cpp
View file

@ -150,7 +150,9 @@ namespace polysat {
signed_constraint reducer;
inference_sup(const char* name, pvar var, signed_constraint reduced, signed_constraint reducer) : name(name), var(var), reduced(reduced), reducer(reducer) {}
std::ostream& display(std::ostream& out) const override {
return out << "Superposition " << name << ", reduced v" << var << " in " << reduced << " by " << reducer;
return out << "Superposition " << name << ", reduced v" << var
<< " in " << reduced.blit() << ": " << reduced
<< " by " << reducer.blit() << ": " << reducer;
}
};

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

@ -559,7 +559,7 @@ namespace polysat {
/**
* Conflict resolution.
*/
void solver::resolve_conflict() {
void solver::resolve_conflict() {
LOG_H2("Resolve conflict");
LOG("\n" << *this);
LOG(search_state_pp(m_search, true));
@ -572,8 +572,9 @@ namespace polysat {
pvar v = m_conflict.conflict_var();
// This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
// TODO: use unsat core from m_viable_fallback if the conflict is from there
// TODO: we could try simpler backtracking loop if we get a lemma from forbidden intervals
VERIFY(m_viable.resolve(v, m_conflict));
backtrack_fi();
return;
}
search_iterator search_it(m_search);
@ -630,6 +631,74 @@ namespace polysat {
report_unsat();
}
/**
* Simpler backracking for forbidden interval lemmas:
* since forbidden intervals already gives us a lemma where the conflict variable has been eliminated,
* we can backtrack to the last relevant decision and learn this lemma.
*/
void solver::backtrack_fi() {
uint_set relevant_vars;
search_iterator search_it(m_search);
while (search_it.next()) {
auto& item = *search_it;
search_it.set_resolved();
if (item.is_assignment()) {
// Resolve over variable assignment
pvar v = item.var();
if (!m_conflict.pvar_occurs_in_constraints(v) && !relevant_vars.contains(v)) {
m_search.pop_assignment();
continue;
}
LOG_H2("Working on " << search_item_pp(m_search, item));
LOG(m_justification[v]);
LOG("Conflict: " << m_conflict);
inc_activity(v);
justification& j = m_justification[v];
if (j.level() > base_level() && j.is_decision()) {
m_conflict.end_conflict();
revert_decision(v);
return;
}
SASSERT(j.is_propagation());
// If a variable was propagated:
// we don't really care about the constraints in this case, but just about the variables it depends on
for (auto const& c : m_viable.get_constraints(v))
for (pvar v : c->vars()) {
relevant_vars.insert(v);
m_conflict.log_var(v);
}
m_search.pop_assignment();
}
else {
// Resolve over boolean literal
SASSERT(item.is_boolean());
sat::literal const lit = item.lit();
sat::bool_var const var = lit.var();
if (!m_conflict.is_marked(var))
continue;
LOG_H2("Working on " << search_item_pp(m_search, item));
LOG(bool_justification_pp(m_bvars, lit));
LOG("Literal " << lit << " is " << lit2cnstr(lit));
LOG("Conflict: " << m_conflict);
if (m_bvars.is_assumption(var))
continue;
else if (m_bvars.is_decision(var)) {
m_conflict.end_conflict();
revert_bool_decision(lit);
return;
}
else if (m_bvars.is_bool_propagation(var))
m_conflict.resolve(lit, *m_bvars.reason(lit));
else {
SASSERT(m_bvars.is_value_propagation(var));
continue;
}
}
}
m_conflict.end_conflict();
report_unsat();
}
/**
* Variable activity accounting.
* As a placeholder we increment activity
@ -706,8 +775,6 @@ namespace polysat {
void solver::decide_on_lemma(clause& lemma) {
LOG_H3("Guessing literal in lemma: " << lemma);
IF_LOGGING(m_viable.log());
LOG("Boolean assignment: " << m_bvars);
// To make a guess, we need to find an unassigned literal that is not false in the current model.
@ -717,6 +784,7 @@ namespace polysat {
for (sat::literal lit : lemma) {
switch (m_bvars.value(lit)) {
case l_true:
LOG("Already satisfied because literal " << lit << " is true");
return;
case l_false:
break;

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

@ -72,6 +72,7 @@ namespace polysat {
friend class restart;
friend class explainer;
friend class inference_engine;
friend class inference_logger;
friend class forbidden_intervals;
friend class linear_solver;
friend class viable;
@ -203,7 +204,7 @@ namespace polysat {
unsigned base_level() const;
void resolve_conflict();
void resolve_bool(sat::literal lit);
void backtrack_fi();
void revert_decision(pvar v);
void revert_bool_decision(sat::literal lit);

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

@ -176,7 +176,7 @@ namespace polysat {
}
bool ule_constraint::is_currently_true(solver& s, assignment_t const& sub, bool is_positive) const {
return false;
return is_currently_false(s, sub, !is_positive);
}
bool ule_constraint::is_currently_true(solver& s, bool is_positive) const {