mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 09:35:32 +00:00
Remove old file
This commit is contained in:
Jakob Rath
parent
d3f70c0fb8
commit
fc773ef19e
2 changed files with 0 additions and 858 deletions
|
|
@ -1,605 +0,0 @@
|
|||
#if 0
|
||||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat conflict
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-6
|
||||
|
||||
Notes:
|
||||
|
||||
TODO: try a final core reduction step or other core minimization
|
||||
|
||||
TODO: revert(pvar v) is too weak.
|
||||
It should apply saturation rules currently only available for propagated values.
|
||||
|
||||
TODO: dependency tracking for constraints evaluating to false should be minimized.
|
||||
|
||||
--*/
|
||||
|
||||
#include "math/polysat/conflict.h"
|
||||
#include "math/polysat/solver.h"
|
||||
#include "math/polysat/log.h"
|
||||
#include "math/polysat/log_helper.h"
|
||||
#include "math/polysat/explain.h"
|
||||
#include "math/polysat/eq_explain.h"
|
||||
#include "math/polysat/forbidden_intervals.h"
|
||||
#include "math/polysat/saturation.h"
|
||||
#include "math/polysat/variable_elimination.h"
|
||||
#include <algorithm>
|
||||
#include <fstream>
|
||||
|
||||
namespace polysat {
|
||||
|
||||
class old_inference_logger {
|
||||
uint_set m_used_constraints;
|
||||
uint_set m_used_vars;
|
||||
scoped_ptr<std::ostream> m_out = nullptr;
|
||||
unsigned m_conflicts = 0;
|
||||
|
||||
friend class conflict;
|
||||
|
||||
std::ostream& out() {
|
||||
SASSERT(m_out);
|
||||
return *m_out;
|
||||
}
|
||||
|
||||
std::ostream& out_indent() { return out() << " "; }
|
||||
|
||||
std::string hline() const { return std::string(70, '-'); }
|
||||
|
||||
public:
|
||||
void begin_conflict(char const* text) {
|
||||
++m_conflicts;
|
||||
if (text)
|
||||
LOG("Begin CONFLICT #" << m_conflicts << " (" << text << ")");
|
||||
else
|
||||
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 << " (" << text << ")" << "\n";
|
||||
}
|
||||
|
||||
void log_inference(conflict const& core, inference const* inf) {
|
||||
out() << hline() << "\n";
|
||||
if (inf)
|
||||
out() << *inf << "\n";
|
||||
if (core.conflict_var() != null_var) {
|
||||
out_indent() << "Conflict var: " << core.conflict_var() << "\n";
|
||||
m_used_vars.insert(core.conflict_var());
|
||||
}
|
||||
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() << assignment_pp(core.s, v, core.s.get_value(v)) << "\n";
|
||||
m_used_vars.insert(v);
|
||||
}
|
||||
for (auto v : core.bail_vars()) {
|
||||
out_indent() << assignment_pp(core.s, v, core.s.get_value(v)) << " (bail)\n";
|
||||
m_used_vars.insert(v);
|
||||
}
|
||||
if (core.is_bailout())
|
||||
out_indent() << "(bailout)\n";
|
||||
out().flush();
|
||||
}
|
||||
|
||||
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();
|
||||
}
|
||||
|
||||
void end_conflict(search_state const& search, viable const& v) {
|
||||
out() << "\n" << hline() << "\n\n";
|
||||
out() << "Search state (part):\n";
|
||||
for (auto const& item : search)
|
||||
if (is_relevant(item))
|
||||
out_indent() << search_item_pp(search, item, true) << "\n";
|
||||
out() << hline() << "\nViable (part):\n";
|
||||
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 {
|
||||
switch (item.kind()) {
|
||||
case search_item_k::assignment:
|
||||
return m_used_vars.contains(item.var());
|
||||
case search_item_k::boolean:
|
||||
return m_used_constraints.contains(item.lit().index());
|
||||
}
|
||||
UNREACHABLE();
|
||||
return false;
|
||||
}
|
||||
};
|
||||
|
||||
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));
|
||||
ve_engines.push_back(alloc(ve_reduction));
|
||||
inf_engines.push_back(alloc(inf_saturate, s));
|
||||
// TODO: how to set this on the CLI? "polysat.log_conflicts=true" doesn't seem to work although z3 accepts it
|
||||
if (true || s.get_config().m_log_conflicts)
|
||||
m_logger = alloc(old_inference_logger);
|
||||
}
|
||||
|
||||
conflict::~conflict() {}
|
||||
|
||||
void conflict::begin_conflict(char const* text) {
|
||||
if (m_logger) {
|
||||
m_logger->begin_conflict(text);
|
||||
// log initial conflict state
|
||||
m_logger->log_inference(*this, nullptr);
|
||||
}
|
||||
}
|
||||
|
||||
void conflict::log_inference(inference const& inf) {
|
||||
if (m_logger)
|
||||
m_logger->log_inference(*this, &inf);
|
||||
}
|
||||
|
||||
void conflict::end_conflict() {
|
||||
if (m_logger)
|
||||
m_logger->end_conflict(s.m_search, s.m_viable);
|
||||
}
|
||||
|
||||
constraint_manager& conflict::cm() const { return s.m_constraints; }
|
||||
|
||||
std::ostream& conflict::display(std::ostream& out) const {
|
||||
char const* sep = "";
|
||||
for (auto c : *this)
|
||||
out << sep << c->bvar2string() << " " << c, sep = " ; ";
|
||||
if (!m_vars.empty())
|
||||
out << " vars";
|
||||
for (auto v : m_vars)
|
||||
out << " v" << v;
|
||||
if (!m_bail_vars.empty())
|
||||
out << " bail vars";
|
||||
for (auto v : m_bail_vars)
|
||||
out << " v" << v;
|
||||
return out;
|
||||
}
|
||||
|
||||
bool conflict::empty() const {
|
||||
return m_literals.empty()
|
||||
&& m_vars.empty()
|
||||
&& m_bail_vars.empty()
|
||||
&& m_conflict_var == null_var;
|
||||
}
|
||||
|
||||
void conflict::reset() {
|
||||
for (auto c : *this)
|
||||
unset_mark(c);
|
||||
m_literals.reset();
|
||||
m_vars.reset();
|
||||
m_var_occurrences.reset();
|
||||
m_bail_vars.reset();
|
||||
m_conflict_var = null_var;
|
||||
m_kind = conflict_kind_t::ok;
|
||||
SASSERT(empty());
|
||||
}
|
||||
|
||||
/**
|
||||
* The constraint is false under the current assignment of variables.
|
||||
* The core is then the conjuction of this constraint and assigned variables.
|
||||
*/
|
||||
void conflict::set(signed_constraint c) {
|
||||
LOG("Conflict: " << c << " " << c.bvalue(s));
|
||||
SASSERT(empty());
|
||||
if (c.bvalue(s) == l_false) {
|
||||
auto* cl = s.m_bvars.reason(c.blit().var());
|
||||
if (cl)
|
||||
set(*cl);
|
||||
else
|
||||
insert(c);
|
||||
}
|
||||
else {
|
||||
SASSERT(c.is_currently_false(s));
|
||||
// TBD: fails with test_subst SASSERT(c.bvalue(s) == l_true);
|
||||
insert_vars(c);
|
||||
insert(c);
|
||||
}
|
||||
SASSERT(!empty());
|
||||
}
|
||||
|
||||
/**
|
||||
* The variable v cannot be assigned.
|
||||
* The conflict is the set of justifications accumulated for the viable values for v.
|
||||
* These constraints are (in the current form) not added to the core, but passed directly
|
||||
* to the forbidden interval module.
|
||||
* A consistent approach could be to add these constraints to the core and then also include the
|
||||
* variable assignments.
|
||||
*/
|
||||
void conflict::set(pvar v) {
|
||||
LOG("Conflict: v" << v);
|
||||
SASSERT(empty());
|
||||
m_conflict_var = v;
|
||||
SASSERT(!empty());
|
||||
}
|
||||
|
||||
/**
|
||||
* The clause is conflicting in the current search state.
|
||||
*/
|
||||
void conflict::set(clause const& cl) {
|
||||
if (!empty())
|
||||
return;
|
||||
LOG("Conflict: " << cl);
|
||||
SASSERT(empty());
|
||||
for (auto lit : cl) {
|
||||
auto c = s.lit2cnstr(lit);
|
||||
SASSERT(c.bvalue(s) == l_false);
|
||||
insert(~c);
|
||||
}
|
||||
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) {
|
||||
if (c.is_always_true())
|
||||
return;
|
||||
if (is_marked(c))
|
||||
return;
|
||||
LOG("inserting: " << c);
|
||||
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) {
|
||||
switch (c.bvalue(s)) {
|
||||
case l_undef:
|
||||
s.assign_eval(c.blit());
|
||||
break;
|
||||
case l_true:
|
||||
break;
|
||||
case l_false:
|
||||
break;
|
||||
}
|
||||
insert(c);
|
||||
}
|
||||
|
||||
void conflict::insert_vars(signed_constraint c) {
|
||||
for (pvar v : c->vars())
|
||||
if (s.is_assigned(v))
|
||||
m_vars.insert(v);
|
||||
}
|
||||
|
||||
/**
|
||||
* Premises can either be justified by a Clause or by a value assignment.
|
||||
* Premises that are justified by value assignments are not assigned (the bvalue is l_undef)
|
||||
* The justification for those premises are based on the free assigned variables.
|
||||
*
|
||||
* NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c?
|
||||
* Ensure that c is assigned and justified
|
||||
*/
|
||||
// TODO: rename this; it pushes onto \Gamma and doesn't insert into the core
|
||||
void conflict::insert(signed_constraint c, vector<signed_constraint> const& premises) {
|
||||
// keep(c);
|
||||
clause_builder c_lemma(s);
|
||||
for (auto premise : premises) {
|
||||
LOG_H3("premise: " << premise);
|
||||
// keep(premise);
|
||||
SASSERT(premise.bvalue(s) != l_false);
|
||||
c_lemma.push(~premise.blit());
|
||||
}
|
||||
c_lemma.push(c.blit());
|
||||
clause_ref lemma = c_lemma.build();
|
||||
SASSERT(lemma);
|
||||
cm().store(lemma.get(), s, false);
|
||||
if (c.bvalue(s) == l_undef)
|
||||
s.assign_propagate(c.blit(), *lemma);
|
||||
}
|
||||
|
||||
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) {
|
||||
remove(c_old);
|
||||
insert(c_new, c_new_premises);
|
||||
}
|
||||
|
||||
bool conflict::contains(signed_constraint c) const {
|
||||
return m_literals.contains(c.blit().index());
|
||||
}
|
||||
|
||||
bool conflict::contains(sat::literal lit) const {
|
||||
SASSERT(lit != sat::null_literal);
|
||||
return m_literals.contains(lit.index());
|
||||
}
|
||||
|
||||
void conflict::set_bailout_gave_up() {
|
||||
SASSERT(m_kind == conflict_kind_t::ok);
|
||||
m_kind = conflict_kind_t::bailout_gave_up;
|
||||
s.m_stats.m_num_bailouts++;
|
||||
}
|
||||
|
||||
void conflict::set_bailout_lemma() {
|
||||
SASSERT(m_kind == conflict_kind_t::ok);
|
||||
m_kind = conflict_kind_t::bailout_lemma;
|
||||
// s.m_stats.m_num_bailouts++;
|
||||
}
|
||||
|
||||
struct inference_resolve : public inference {
|
||||
sat::literal m_lit;
|
||||
clause const& m_clause;
|
||||
inference_resolve(sat::literal lit, clause const& cl) : m_lit(lit), m_clause(cl) {}
|
||||
std::ostream& display(std::ostream& out) const override {
|
||||
return out << "Resolve upon " << m_lit << " with " << m_clause;
|
||||
}
|
||||
};
|
||||
|
||||
void conflict::resolve(sat::literal lit, clause const& cl) {
|
||||
// Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
|
||||
// clause: x \/ u \/ v
|
||||
// resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v
|
||||
|
||||
SASSERT(contains(lit));
|
||||
SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
|
||||
SASSERT(!contains(~lit));
|
||||
SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
|
||||
|
||||
remove(s.lit2cnstr(lit));
|
||||
for (sat::literal lit2 : cl)
|
||||
if (lit2 != lit)
|
||||
insert(s.lit2cnstr(~lit2));
|
||||
log_inference(inference_resolve(lit, cl));
|
||||
}
|
||||
|
||||
struct inference_resolve_with_assignment : public inference {
|
||||
solver& s;
|
||||
sat::literal lit;
|
||||
signed_constraint c;
|
||||
inference_resolve_with_assignment(solver& s, sat::literal lit, signed_constraint c) : s(s), lit(lit), c(c) {}
|
||||
std::ostream& display(std::ostream& out) const override {
|
||||
out << "Resolve upon " << lit << " with assignment:";
|
||||
for (pvar v : c->vars())
|
||||
if (s.is_assigned(v))
|
||||
out << " " << assignment_pp(s, v, s.get_value(v), true);
|
||||
return out;
|
||||
}
|
||||
};
|
||||
|
||||
void conflict::resolve_with_assignment(sat::literal lit, unsigned lvl) {
|
||||
// The reason for lit is conceptually:
|
||||
// x1 = v1 /\ ... /\ xn = vn ==> lit
|
||||
|
||||
SASSERT(contains(lit));
|
||||
SASSERT(!contains(~lit));
|
||||
|
||||
signed_constraint c = s.lit2cnstr(lit);
|
||||
bool has_decision = false;
|
||||
for (pvar v : c->vars())
|
||||
if (s.is_assigned(v) && s.m_justification[v].is_decision())
|
||||
m_bail_vars.insert(v), has_decision = true;
|
||||
|
||||
if (!has_decision) {
|
||||
remove(c);
|
||||
for (pvar v : c->vars())
|
||||
if (s.is_assigned(v)) {
|
||||
// TODO: 'lit' was propagated at level 'lvl'; can we here ignore variables above that?
|
||||
SASSERT(s.get_level(v) <= lvl);
|
||||
m_vars.insert(v);
|
||||
}
|
||||
}
|
||||
log_inference(inference_resolve_with_assignment(s, lit, c));
|
||||
}
|
||||
|
||||
clause_builder conflict::build_lemma() {
|
||||
LOG_H3("Build lemma from core");
|
||||
LOG("core: " << *this);
|
||||
clause_builder lemma(s);
|
||||
|
||||
for (auto c : *this)
|
||||
minimize_vars(c);
|
||||
|
||||
for (auto c : *this)
|
||||
lemma.push(~c);
|
||||
|
||||
for (unsigned v : m_vars) {
|
||||
auto eq = s.eq(s.var(v), s.get_value(v));
|
||||
if (eq.bvalue(s) == l_undef)
|
||||
s.assign_eval(eq.blit());
|
||||
lemma.push(~eq);
|
||||
}
|
||||
s.decay_activity();
|
||||
|
||||
if (m_logger)
|
||||
m_logger->log_lemma(s, lemma);
|
||||
|
||||
return lemma;
|
||||
}
|
||||
|
||||
void conflict::minimize_vars(signed_constraint c) {
|
||||
if (m_vars.empty())
|
||||
return;
|
||||
if (!c.is_currently_false(s))
|
||||
return;
|
||||
|
||||
assignment_t a;
|
||||
for (auto v : m_vars)
|
||||
a.push_back(std::make_pair(v, s.get_value(v)));
|
||||
for (unsigned i = 0; i < a.size(); ++i) {
|
||||
std::pair<pvar, rational> save = a[i];
|
||||
std::pair<pvar, rational> last = a.back();
|
||||
a[i] = last;
|
||||
a.pop_back();
|
||||
if (c.is_currently_false(s, a))
|
||||
--i;
|
||||
else {
|
||||
a.push_back(last);
|
||||
a[i] = save;
|
||||
}
|
||||
}
|
||||
if (a.size() == m_vars.num_elems())
|
||||
return;
|
||||
m_vars.reset();
|
||||
for (auto const& [v, val] : a)
|
||||
m_vars.insert(v);
|
||||
log_inference("minimize vars");
|
||||
LOG("reduced " << m_vars);
|
||||
}
|
||||
|
||||
|
||||
struct inference_resolve_value : public inference {
|
||||
solver& s;
|
||||
pvar v;
|
||||
inference_resolve_value(solver& s, pvar v) : s(s), v(v) {}
|
||||
std::ostream& display(std::ostream& out) const override {
|
||||
return out << "Value resolution with " << assignment_pp(s, v, s.get_value(v), true);
|
||||
}
|
||||
};
|
||||
|
||||
bool conflict::resolve_value(pvar v) {
|
||||
// NOTE:
|
||||
// In the "standard" case where "v = val" is on the stack:
|
||||
// forbidden interval projection is performed at top level
|
||||
|
||||
SASSERT(v != conflict_var());
|
||||
|
||||
bool has_saturated = false;
|
||||
|
||||
auto const& j = s.m_justification[v];
|
||||
|
||||
if (j.is_decision() && m_bail_vars.contains(v))
|
||||
return false;
|
||||
|
||||
s.inc_activity(v);
|
||||
m_vars.remove(v);
|
||||
|
||||
if (j.is_propagation()) {
|
||||
for (auto const& c : s.m_viable.get_constraints(v))
|
||||
propagate(c);
|
||||
for (auto const& i : s.m_viable.units(v)) {
|
||||
propagate(s.eq(i.lo(), i.lo_val()));
|
||||
propagate(s.eq(i.hi(), i.hi_val()));
|
||||
}
|
||||
}
|
||||
|
||||
if (is_bailout())
|
||||
goto bailout;
|
||||
|
||||
LOG("try-explain v" << v);
|
||||
if (try_explain(v))
|
||||
return true;
|
||||
|
||||
// No value resolution method was successful => fall back to saturation and variable elimination
|
||||
while (s.inc()) {
|
||||
LOG("try-eliminate v" << v);
|
||||
// TODO: as a last resort, substitute v by m_value[v]?
|
||||
if (try_eliminate(v))
|
||||
return true;
|
||||
LOG("try-saturate v" << v);
|
||||
if (try_saturate(v))
|
||||
has_saturated = true;
|
||||
else
|
||||
break;
|
||||
}
|
||||
LOG("bailout v" << v);
|
||||
if (has_saturated) {
|
||||
// NOTE: current saturation rules create valid lemmas that do not depend on the variable assignment
|
||||
set_bailout_lemma();
|
||||
return true;
|
||||
}
|
||||
else
|
||||
set_bailout_gave_up();
|
||||
bailout:
|
||||
if (s.is_assigned(v) && j.is_decision())
|
||||
m_vars.insert(v);
|
||||
log_inference(inference_resolve_value(s, v));
|
||||
return false;
|
||||
}
|
||||
|
||||
bool conflict::try_eliminate(pvar v) {
|
||||
LOG("try v" << v << " contains " << m_vars.contains(v));
|
||||
if (m_vars.contains(v))
|
||||
return false;
|
||||
bool has_v = false;
|
||||
for (auto c : *this)
|
||||
has_v |= c->contains_var(v);
|
||||
if (!has_v)
|
||||
return true;
|
||||
for (auto* engine : ve_engines)
|
||||
if (engine->perform(s, v, *this))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
bool conflict::try_saturate(pvar v) {
|
||||
for (auto* engine : inf_engines)
|
||||
if (engine->perform(v, *this))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
bool conflict::try_explain(pvar v) {
|
||||
for (auto* engine : ex_engines)
|
||||
if (engine->try_explain(v, *this))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
void conflict::set_mark(signed_constraint c) {
|
||||
sat::bool_var b = c->bvar();
|
||||
if (b >= m_bvar2mark.size())
|
||||
m_bvar2mark.resize(b + 1);
|
||||
SASSERT(!m_bvar2mark[b]);
|
||||
m_bvar2mark[b] = true;
|
||||
}
|
||||
|
||||
/**
|
||||
* unset marking on the constraint, but keep variable dependencies.
|
||||
*/
|
||||
void conflict::unset_mark(signed_constraint c) {
|
||||
sat::bool_var b = c->bvar();
|
||||
SASSERT(m_bvar2mark[b]);
|
||||
m_bvar2mark[b] = false;
|
||||
}
|
||||
|
||||
bool conflict::is_marked(signed_constraint c) const {
|
||||
return is_marked(c->bvar());
|
||||
}
|
||||
|
||||
bool conflict::is_marked(sat::bool_var b) const {
|
||||
return m_bvar2mark.get(b, false);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
|
@ -1,253 +0,0 @@
|
|||
#if 0
|
||||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
polysat conflict
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-6
|
||||
|
||||
Notes:
|
||||
|
||||
A conflict state is of the form <Vars, Constraints>
|
||||
Where Vars are shorthand for the constraints v = value(v) for v in Vars and value(v) is the assignent.
|
||||
|
||||
The conflict state is unsatisfiable under background clauses F.
|
||||
Dually, the negation is a consequence of F.
|
||||
|
||||
Conflict resolution resolves an assignment in the search stack against the conflict state.
|
||||
|
||||
Assignments are of the form:
|
||||
|
||||
lit <- D => lit - lit is propagated by the clause D => lit
|
||||
lit <- ? - lit is a decision literal.
|
||||
lit <- asserted - lit is asserted
|
||||
lit <- Vars - lit is propagated from variable evaluation.
|
||||
|
||||
v = value <- D - v is assigned value by constraints D
|
||||
v = value <- ? - v is a decision literal.
|
||||
|
||||
- All literals should be assigned in the stack prior to their use.
|
||||
|
||||
l <- D => l, < Vars, { l } u C > ===> < Vars, C u D >
|
||||
l <- ?, < Vars, { l } u C > ===> ~l <- (C & Vars = value(Vars) => ~l)
|
||||
l <- asserted, < Vars, { l } u C > ===> < Vars, { l } u C >
|
||||
l <- Vars', < Vars, { l } u C > ===> < Vars u Vars', C > if all Vars' are propagated
|
||||
l <- Vars', < Vars, { l } u C > ===> Mark < Vars, { l } u C > as bailout
|
||||
|
||||
v = value <- D, < Vars u { v }, C > ===> < Vars, D u C >
|
||||
v = value <- ?, < Vars u { v }, C > ===> v != value <- (C & Vars = value(Vars) => v != value)
|
||||
|
||||
|
||||
Example derivations:
|
||||
|
||||
Trail: z <= y <- asserted
|
||||
xz > xy <- asserted
|
||||
x = a <- ?
|
||||
y = b <- ?
|
||||
z = c <- ?
|
||||
Conflict: < {x, y, z}, xz > xy > when ~O(a,b) and c <= b
|
||||
Append x <= a <- { x }
|
||||
Append y <= b <- { y }
|
||||
Conflict: < {}, y >= z, xz > xy, x <= a, y <= b >
|
||||
Based on: z <= y & x <= a & y <= b => xz <= xy
|
||||
Resolve: y <= b <- { y }, y is a decision variable.
|
||||
Bailout: lemma ~(y >= z & xz > xy & x <= a & y <= b) at decision level of lemma
|
||||
|
||||
With overflow predicate:
|
||||
Append ~O(x, y) <- { x, y }
|
||||
Conflict: < {}, y >= z, xz > xy, ~O(x,y) >
|
||||
Based on z <= y & ~O(x,y) => xz <= xy
|
||||
Resolve: ~O(x, y) <- { x, y } both x, y are decision variables
|
||||
Lemma: y < z or xz <= xy or O(x,y)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "math/polysat/constraint.h"
|
||||
#include "math/polysat/clause_builder.h"
|
||||
#include "math/polysat/inference_logger.h"
|
||||
#include <optional>
|
||||
|
||||
namespace polysat {
|
||||
|
||||
class solver;
|
||||
class explainer;
|
||||
class inference_engine;
|
||||
class variable_elimination_engine;
|
||||
class conflict_iterator;
|
||||
class old_inference_logger;
|
||||
|
||||
enum class conflict_kind_t {
|
||||
ok,
|
||||
bailout_gave_up,
|
||||
bailout_lemma,
|
||||
};
|
||||
|
||||
/** Conflict state, represented as core (~negation of clause). */
|
||||
class conflict {
|
||||
solver& s;
|
||||
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;
|
||||
|
||||
// If this is not null_var, the conflict was due to empty viable set for this variable.
|
||||
// Can be treated like "v = x" for any value x.
|
||||
pvar m_conflict_var = null_var;
|
||||
|
||||
/** Whether we are in a bailout state.
|
||||
* We enter a bailout state when we give up on proper conflict resolution,
|
||||
* or want to learn a lemma without fine-grained backtracking.
|
||||
*/
|
||||
conflict_kind_t m_kind = conflict_kind_t::ok;
|
||||
|
||||
friend class old_inference_logger;
|
||||
scoped_ptr<old_inference_logger> m_logger;
|
||||
|
||||
bool_vector m_bvar2mark; // mark of Boolean variables
|
||||
|
||||
void set_mark(signed_constraint c);
|
||||
void unset_mark(signed_constraint c);
|
||||
|
||||
void minimize_vars(signed_constraint c);
|
||||
|
||||
constraint_manager& cm() const;
|
||||
scoped_ptr_vector<explainer> ex_engines;
|
||||
scoped_ptr_vector<variable_elimination_engine> ve_engines;
|
||||
scoped_ptr_vector<inference_engine> inf_engines;
|
||||
|
||||
public:
|
||||
conflict(solver& s);
|
||||
~conflict();
|
||||
|
||||
/// Begin next conflict
|
||||
void begin_conflict(char const* text = nullptr);
|
||||
/// 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();
|
||||
|
||||
pvar conflict_var() const { return m_conflict_var; }
|
||||
|
||||
bool is_bailout() const { return m_kind != conflict_kind_t::ok; }
|
||||
bool is_bailout_lemma() const { return m_kind == conflict_kind_t::bailout_lemma; }
|
||||
void set_bailout_gave_up();
|
||||
void set_bailout_lemma();
|
||||
|
||||
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;
|
||||
|
||||
/** conflict because the constraint c is false under current variable assignment */
|
||||
void set(signed_constraint c);
|
||||
/** conflict because there is no viable value for the variable v */
|
||||
void set(pvar v);
|
||||
/** all literals in clause are false */
|
||||
void set(clause const& cl);
|
||||
|
||||
void propagate(signed_constraint c);
|
||||
void insert(signed_constraint c);
|
||||
void insert_vars(signed_constraint c);
|
||||
void insert(signed_constraint c, vector<signed_constraint> const& premises);
|
||||
void remove(signed_constraint c);
|
||||
void replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> const& c_new_premises);
|
||||
|
||||
bool contains(signed_constraint c) const;
|
||||
bool contains(sat::literal lit) const;
|
||||
|
||||
/** Perform boolean resolution with the clause upon variable 'var'.
|
||||
* Precondition: core/clause contain complementary 'var'-literals.
|
||||
*/
|
||||
void resolve(sat::literal lit, clause const& cl);
|
||||
|
||||
/** lit was fully evaluated under the assignment up to level 'lvl'.
|
||||
*/
|
||||
void resolve_with_assignment(sat::literal lit, unsigned lvl);
|
||||
|
||||
/** Perform value resolution by applying various inference rules.
|
||||
* Returns true if it was possible to eliminate the variable 'v'.
|
||||
*/
|
||||
bool resolve_value(pvar v);
|
||||
|
||||
/** Convert the core into a lemma to be learned. */
|
||||
clause_builder build_lemma();
|
||||
|
||||
bool try_eliminate(pvar v);
|
||||
bool try_saturate(pvar v);
|
||||
bool try_explain(pvar v);
|
||||
|
||||
using const_iterator = conflict_iterator;
|
||||
const_iterator begin() const;
|
||||
const_iterator end() const;
|
||||
|
||||
uint_set const& vars() const { return m_vars; }
|
||||
uint_set const& bail_vars() const { return m_bail_vars; }
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, conflict const& c) { return c.display(out); }
|
||||
|
||||
|
||||
class conflict_iterator {
|
||||
friend class conflict;
|
||||
|
||||
using inner_t = indexed_uint_set::iterator;
|
||||
|
||||
constraint_manager* m_cm;
|
||||
inner_t m_inner;
|
||||
|
||||
conflict_iterator(constraint_manager& cm, inner_t inner):
|
||||
m_cm(&cm), m_inner(inner) {}
|
||||
|
||||
static conflict_iterator begin(constraint_manager& cm, indexed_uint_set const& lits) {
|
||||
return {cm, lits.begin()};
|
||||
}
|
||||
|
||||
static conflict_iterator end(constraint_manager& cm, indexed_uint_set const& lits) {
|
||||
return {cm, lits.end()};
|
||||
}
|
||||
|
||||
public:
|
||||
using value_type = signed_constraint;
|
||||
using difference_type = unsigned;
|
||||
using pointer = signed_constraint const*;
|
||||
using reference = signed_constraint const&;
|
||||
using iterator_category = std::input_iterator_tag;
|
||||
|
||||
conflict_iterator& operator++() {
|
||||
++m_inner;
|
||||
return *this;
|
||||
}
|
||||
|
||||
signed_constraint operator*() const {
|
||||
return m_cm->lookup(sat::to_literal(*m_inner));
|
||||
}
|
||||
|
||||
bool operator==(conflict_iterator const& other) const {
|
||||
return m_inner == other.m_inner;
|
||||
}
|
||||
|
||||
bool operator!=(conflict_iterator const& other) const { return !operator==(other); }
|
||||
};
|
||||
|
||||
|
||||
inline conflict::const_iterator conflict::begin() const { return conflict_iterator::begin(cm(), m_literals); }
|
||||
inline conflict::const_iterator conflict::end() const { return conflict_iterator::end(cm(), m_literals); }
|
||||
}
|
||||
#endif
|
||||
Loading…
Add table
Add a link
Reference in a new issue