mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 00:55:31 +00:00
rename conflict_core to conflict:
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
1e3ff3179e
commit
bb5ff8db24
13 changed files with 98 additions and 97 deletions
|
|
@ -3,7 +3,7 @@ z3_add_component(polysat
|
|||
boolean.cpp
|
||||
clause.cpp
|
||||
clause_builder.cpp
|
||||
conflict_core.cpp
|
||||
conflict.cpp
|
||||
constraint.cpp
|
||||
explain.cpp
|
||||
forbidden_intervals.cpp
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ TODO: If we have e.g. 4x+y=2 and y=0, then we have a conflict no matter the valu
|
|||
|
||||
--*/
|
||||
|
||||
#include "math/polysat/conflict_core.h"
|
||||
#include "math/polysat/conflict.h"
|
||||
#include "math/polysat/solver.h"
|
||||
#include "math/polysat/log.h"
|
||||
#include "math/polysat/log_helper.h"
|
||||
|
|
@ -33,7 +33,7 @@ TODO: If we have e.g. 4x+y=2 and y=0, then we have a conflict no matter the valu
|
|||
|
||||
namespace polysat {
|
||||
|
||||
conflict_core::conflict_core(solver& s) {
|
||||
conflict::conflict(solver& s) {
|
||||
m_solver = &s;
|
||||
ex_engines.push_back(alloc(ex_polynomial_superposition));
|
||||
for (auto* engine : ex_engines)
|
||||
|
|
@ -44,11 +44,11 @@ namespace polysat {
|
|||
engine->set_solver(s);
|
||||
}
|
||||
|
||||
conflict_core::~conflict_core() {}
|
||||
conflict::~conflict() {}
|
||||
|
||||
constraint_manager& conflict_core::cm() const { return s().m_constraints; }
|
||||
constraint_manager& conflict::cm() const { return s().m_constraints; }
|
||||
|
||||
std::ostream& conflict_core::display(std::ostream& out) const {
|
||||
std::ostream& conflict::display(std::ostream& out) const {
|
||||
char const* sep = "";
|
||||
for (auto c : *this)
|
||||
out << sep << c->bvar2string() << " " << c, sep = " ; ";
|
||||
|
|
@ -59,7 +59,7 @@ namespace polysat {
|
|||
return out;
|
||||
}
|
||||
|
||||
void conflict_core::reset() {
|
||||
void conflict::reset() {
|
||||
for (auto c : *this)
|
||||
unset_mark(c);
|
||||
m_constraints.reset();
|
||||
|
|
@ -75,7 +75,7 @@ namespace polysat {
|
|||
* The constraint is false under the current assignment of variables.
|
||||
* The core is then the conjuction of this constraint and assigned variables.
|
||||
*/
|
||||
void conflict_core::set(signed_constraint c) {
|
||||
void conflict::set(signed_constraint c) {
|
||||
LOG("Conflict: " << c);
|
||||
SASSERT(empty());
|
||||
c->set_var_dependent();
|
||||
|
|
@ -91,7 +91,7 @@ namespace polysat {
|
|||
* A consistent approach could be to add these constraints to the core and then also include the
|
||||
* variable assignments.
|
||||
*/
|
||||
void conflict_core::set(pvar v) {
|
||||
void conflict::set(pvar v) {
|
||||
LOG("Conflict: v" << v);
|
||||
SASSERT(empty());
|
||||
m_conflict_var = v;
|
||||
|
|
@ -102,7 +102,7 @@ namespace polysat {
|
|||
SASSERT(!empty());
|
||||
}
|
||||
|
||||
void conflict_core::set(clause const& cl) {
|
||||
void conflict::set(clause const& cl) {
|
||||
LOG("Conflict: " << cl);
|
||||
SASSERT(empty());
|
||||
for (auto lit : cl) {
|
||||
|
|
@ -113,7 +113,7 @@ namespace polysat {
|
|||
SASSERT(!empty());
|
||||
}
|
||||
|
||||
void conflict_core::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)
|
||||
|
|
@ -128,12 +128,12 @@ namespace polysat {
|
|||
m_constraints.push_back(c);
|
||||
}
|
||||
|
||||
void conflict_core::insert(signed_constraint c, vector<signed_constraint> premises) {
|
||||
void conflict::insert(signed_constraint c, vector<signed_constraint> premises) {
|
||||
insert(c);
|
||||
m_saturation_premises.insert(c, std::move(premises)); // TODO: map doesn't have move-insertion, so this still copies the vector.
|
||||
}
|
||||
|
||||
void conflict_core::remove(signed_constraint c) {
|
||||
void conflict::remove(signed_constraint c) {
|
||||
unset_mark(c);
|
||||
if (c->has_bvar()) {
|
||||
SASSERT(std::count(m_constraints.begin(), m_constraints.end(), c) == 0);
|
||||
|
|
@ -143,18 +143,18 @@ namespace polysat {
|
|||
m_constraints.erase(c);
|
||||
}
|
||||
|
||||
void conflict_core::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> c_new_premises) {
|
||||
void conflict::replace(signed_constraint c_old, signed_constraint c_new, vector<signed_constraint> c_new_premises) {
|
||||
remove(c_old);
|
||||
insert(c_new, c_new_premises);
|
||||
}
|
||||
|
||||
void conflict_core::set_bailout() {
|
||||
void conflict::set_bailout() {
|
||||
SASSERT(!is_bailout());
|
||||
m_bailout = true;
|
||||
s().m_stats.m_num_bailouts++;
|
||||
}
|
||||
|
||||
void conflict_core::resolve(constraint_manager const& m, sat::bool_var var, clause const& cl) {
|
||||
void conflict::resolve(constraint_manager const& m, sat::bool_var var, 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
|
||||
|
|
@ -185,7 +185,7 @@ namespace polysat {
|
|||
}
|
||||
|
||||
/** If the constraint c is a temporary constraint derived by core saturation, insert it (and recursively, its premises) into \Gamma */
|
||||
void conflict_core::keep(signed_constraint c) {
|
||||
void conflict::keep(signed_constraint c) {
|
||||
if (!c->has_bvar()) {
|
||||
remove(c);
|
||||
cm().ensure_bvar(c.get());
|
||||
|
|
@ -215,7 +215,7 @@ namespace polysat {
|
|||
s().assign_bool(s().level(*lemma), c.blit(), lemma.get(), nullptr);
|
||||
}
|
||||
|
||||
clause_builder conflict_core::build_lemma() {
|
||||
clause_builder conflict::build_lemma() {
|
||||
LOG_H3("Build lemma from core");
|
||||
LOG("core: " << *this);
|
||||
clause_builder lemma(s());
|
||||
|
|
@ -244,7 +244,7 @@ namespace polysat {
|
|||
}
|
||||
|
||||
|
||||
bool conflict_core::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) {
|
||||
bool conflict::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) {
|
||||
// NOTE:
|
||||
// In the "standard" case where "v = val" is on the stack:
|
||||
// - cjust_v contains true constraints
|
||||
|
|
@ -281,7 +281,7 @@ namespace polysat {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool conflict_core::try_eliminate(pvar v) {
|
||||
bool conflict::try_eliminate(pvar v) {
|
||||
bool has_v = false;
|
||||
for (auto c : *this)
|
||||
has_v |= c->contains_var(v);
|
||||
|
|
@ -293,14 +293,14 @@ namespace polysat {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool conflict_core::try_saturate(pvar v) {
|
||||
bool conflict::try_saturate(pvar v) {
|
||||
for (auto* engine : inf_engines)
|
||||
if (engine->perform(v, *this))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
void conflict_core::set_mark(signed_constraint c) {
|
||||
void conflict::set_mark(signed_constraint c) {
|
||||
if (c->is_marked())
|
||||
return;
|
||||
c->set_mark();
|
||||
|
|
@ -315,7 +315,7 @@ namespace polysat {
|
|||
}
|
||||
}
|
||||
|
||||
void conflict_core::unset_mark(signed_constraint c) {
|
||||
void conflict::unset_mark(signed_constraint c) {
|
||||
if (!c->is_marked())
|
||||
return;
|
||||
c->unset_mark();
|
||||
|
|
@ -328,46 +328,46 @@ namespace polysat {
|
|||
}
|
||||
}
|
||||
|
||||
void conflict_core::inc_pref(pvar v) {
|
||||
void conflict::inc_pref(pvar v) {
|
||||
if (v >= m_pvar2count.size())
|
||||
m_pvar2count.resize(v + 1);
|
||||
m_pvar2count[v]++;
|
||||
}
|
||||
|
||||
void conflict_core::dec_pref(pvar v) {
|
||||
void conflict::dec_pref(pvar v) {
|
||||
SASSERT(m_pvar2count[v] > 0);
|
||||
m_pvar2count[v]--;
|
||||
}
|
||||
|
||||
bool conflict_core::is_pmarked(pvar v) const {
|
||||
bool conflict::is_pmarked(pvar v) const {
|
||||
return m_pvar2count.get(v, 0) > 0;
|
||||
}
|
||||
|
||||
void conflict_core::set_bmark(sat::bool_var b) {
|
||||
void conflict::set_bmark(sat::bool_var b) {
|
||||
if (b >= m_bvar2mark.size())
|
||||
m_bvar2mark.resize(b + 1);
|
||||
SASSERT(!m_bvar2mark[b]);
|
||||
m_bvar2mark[b] = true;
|
||||
}
|
||||
|
||||
void conflict_core::unset_bmark(sat::bool_var b) {
|
||||
void conflict::unset_bmark(sat::bool_var b) {
|
||||
SASSERT(m_bvar2mark[b]);
|
||||
m_bvar2mark[b] = false;
|
||||
}
|
||||
|
||||
bool conflict_core::is_bmarked(sat::bool_var b) const {
|
||||
bool conflict::is_bmarked(sat::bool_var b) const {
|
||||
return m_bvar2mark.get(b, false);
|
||||
}
|
||||
|
||||
bool conflict_core::contains_literal(sat::literal lit) const {
|
||||
bool conflict::contains_literal(sat::literal lit) const {
|
||||
return m_literals.contains(lit.to_uint());
|
||||
}
|
||||
|
||||
void conflict_core::insert_literal(sat::literal lit) {
|
||||
void conflict::insert_literal(sat::literal lit) {
|
||||
m_literals.insert(lit.to_uint());
|
||||
}
|
||||
|
||||
void conflict_core::remove_literal(sat::literal lit) {
|
||||
void conflict::remove_literal(sat::literal lit) {
|
||||
m_literals.remove(lit.to_uint());
|
||||
}
|
||||
|
||||
|
|
@ -22,10 +22,10 @@ namespace polysat {
|
|||
class explainer;
|
||||
class inference_engine;
|
||||
class variable_elimination_engine;
|
||||
class conflict_core_iterator;
|
||||
class conflict_iterator;
|
||||
|
||||
/** Conflict state, represented as core (~negation of clause). */
|
||||
class conflict_core {
|
||||
class conflict {
|
||||
signed_constraints m_constraints; // new constraints used as premises
|
||||
indexed_uint_set m_literals; // set of boolean literals in the conflict
|
||||
uint_set m_vars; // variable assignments used as premises
|
||||
|
|
@ -62,8 +62,8 @@ namespace polysat {
|
|||
// ptr_addr_map<constraint, vector<signed_constraint>> m_saturation_premises;
|
||||
map<signed_constraint, vector<signed_constraint>, obj_hash<signed_constraint>, default_eq<signed_constraint>> m_saturation_premises;
|
||||
public:
|
||||
conflict_core(solver& s);
|
||||
~conflict_core();
|
||||
conflict(solver& s);
|
||||
~conflict();
|
||||
|
||||
pvar conflict_var() const { return m_conflict_var; }
|
||||
|
||||
|
|
@ -109,18 +109,18 @@ namespace polysat {
|
|||
bool try_eliminate(pvar v);
|
||||
bool try_saturate(pvar v);
|
||||
|
||||
using const_iterator = conflict_core_iterator;
|
||||
using const_iterator = conflict_iterator;
|
||||
const_iterator begin() const;
|
||||
const_iterator end() const;
|
||||
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, conflict_core const& c) { return c.display(out); }
|
||||
inline std::ostream& operator<<(std::ostream& out, conflict const& c) { return c.display(out); }
|
||||
|
||||
|
||||
class conflict_core_iterator {
|
||||
friend class conflict_core;
|
||||
class conflict_iterator {
|
||||
friend class conflict;
|
||||
|
||||
using it1_t = signed_constraints::const_iterator;
|
||||
using it2_t = indexed_uint_set::iterator;
|
||||
|
|
@ -130,14 +130,14 @@ namespace polysat {
|
|||
it1_t m_end1;
|
||||
it2_t m_it2;
|
||||
|
||||
conflict_core_iterator(constraint_manager& cm, it1_t it1, it1_t end1, it2_t it2):
|
||||
conflict_iterator(constraint_manager& cm, it1_t it1, it1_t end1, it2_t it2):
|
||||
m_cm(&cm), m_it1(it1), m_end1(end1), m_it2(it2) {}
|
||||
|
||||
static conflict_core_iterator begin(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
|
||||
static conflict_iterator begin(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
|
||||
return {cm, cs.begin(), cs.end(), lits.begin()};
|
||||
}
|
||||
|
||||
static conflict_core_iterator end(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
|
||||
static conflict_iterator end(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
|
||||
return {cm, cs.end(), cs.end(), lits.end()};
|
||||
}
|
||||
|
||||
|
|
@ -148,7 +148,7 @@ namespace polysat {
|
|||
using reference = signed_constraint const&;
|
||||
using iterator_category = std::input_iterator_tag;
|
||||
|
||||
conflict_core_iterator& operator++() {
|
||||
conflict_iterator& operator++() {
|
||||
if (m_it1 != m_end1)
|
||||
++m_it1;
|
||||
else
|
||||
|
|
@ -163,14 +163,14 @@ namespace polysat {
|
|||
return m_cm->lookup(sat::to_literal(*m_it2));
|
||||
}
|
||||
|
||||
bool operator==(conflict_core_iterator const& other) const {
|
||||
bool operator==(conflict_iterator const& other) const {
|
||||
return m_it1 == other.m_it1 && m_it2 == other.m_it2;
|
||||
}
|
||||
|
||||
bool operator!=(conflict_core_iterator const& other) const { return !operator==(other); }
|
||||
bool operator!=(conflict_iterator const& other) const { return !operator==(other); }
|
||||
};
|
||||
|
||||
|
||||
inline conflict_core::const_iterator conflict_core::begin() const { return conflict_core_iterator::begin(cm(), m_constraints, m_literals); }
|
||||
inline conflict_core::const_iterator conflict_core::end() const { return conflict_core_iterator::end(cm(), m_constraints, m_literals); }
|
||||
inline conflict::const_iterator conflict::begin() const { return conflict_iterator::begin(cm(), m_constraints, m_literals); }
|
||||
inline conflict::const_iterator conflict::end() const { return conflict_iterator::end(cm(), m_constraints, m_literals); }
|
||||
}
|
||||
|
|
@ -274,6 +274,7 @@ namespace polysat {
|
|||
if (!s.is_assigned(other_v)) {
|
||||
s.add_watch({this, is_positive}, other_v);
|
||||
std::swap(vars()[idx], vars()[i]);
|
||||
// narrow(s, is_positive);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -46,7 +46,7 @@ namespace polysat {
|
|||
|
||||
// c2 ... constraint that is currently false
|
||||
// Try to replace it with a new false constraint (derived from superposition with a true constraint)
|
||||
signed_constraint ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict_core& core) {
|
||||
signed_constraint ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict& core) {
|
||||
for (auto c1 : core) {
|
||||
if (!is_positive_equality_over(v, c1))
|
||||
continue;
|
||||
|
|
@ -67,7 +67,7 @@ namespace polysat {
|
|||
|
||||
// TODO(later): check superposition into disequality again (see notes)
|
||||
// true = done, false = abort, undef = continue
|
||||
lbool ex_polynomial_superposition::try_explain1(pvar v, conflict_core& core) {
|
||||
lbool ex_polynomial_superposition::try_explain1(pvar v, conflict& core) {
|
||||
for (auto c2 : core) {
|
||||
if (!is_positive_equality_over(v, c2))
|
||||
continue;
|
||||
|
|
@ -92,7 +92,7 @@ namespace polysat {
|
|||
return l_false;
|
||||
}
|
||||
|
||||
void ex_polynomial_superposition::reduce_by(pvar v, conflict_core& core) {
|
||||
void ex_polynomial_superposition::reduce_by(pvar v, conflict& core) {
|
||||
//return;
|
||||
bool progress = true;
|
||||
while (progress) {
|
||||
|
|
@ -106,7 +106,7 @@ namespace polysat {
|
|||
}
|
||||
}
|
||||
|
||||
bool ex_polynomial_superposition::reduce_by(pvar v, signed_constraint eq, conflict_core& core) {
|
||||
bool ex_polynomial_superposition::reduce_by(pvar v, signed_constraint eq, conflict& core) {
|
||||
pdd p = eq->to_ule().p();
|
||||
for (auto c : core) {
|
||||
if (c == eq)
|
||||
|
|
@ -136,7 +136,7 @@ namespace polysat {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool ex_polynomial_superposition::try_explain(pvar v, conflict_core& core) {
|
||||
bool ex_polynomial_superposition::try_explain(pvar v, conflict& core) {
|
||||
LOG_H3("Trying polynomial superposition...");
|
||||
reduce_by(v, core);
|
||||
lbool result = l_undef;
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ Author:
|
|||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "math/polysat/conflict_core.h"
|
||||
#include "math/polysat/conflict.h"
|
||||
#include "math/polysat/constraint.h"
|
||||
#include "math/polysat/clause_builder.h"
|
||||
#include "math/polysat/interval.h"
|
||||
|
|
@ -22,26 +22,26 @@ namespace polysat {
|
|||
class solver;
|
||||
|
||||
class explainer {
|
||||
friend class conflict_core;
|
||||
friend class conflict;
|
||||
solver* m_solver = nullptr;
|
||||
void set_solver(solver& s) { m_solver = &s; }
|
||||
protected:
|
||||
solver& s() { return *m_solver; }
|
||||
public:
|
||||
virtual ~explainer() {}
|
||||
virtual bool try_explain(pvar v, /* vector<signed_constraint> const& cjust_v, */ conflict_core& core) = 0;
|
||||
virtual bool try_explain(pvar v, /* vector<signed_constraint> const& cjust_v, */ conflict& core) = 0;
|
||||
};
|
||||
|
||||
class ex_polynomial_superposition : public explainer {
|
||||
private:
|
||||
bool is_positive_equality_over(pvar v, signed_constraint const& c);
|
||||
signed_constraint resolve1(pvar v, signed_constraint c1, signed_constraint c2);
|
||||
signed_constraint find_replacement(signed_constraint c2, pvar v, conflict_core& core);
|
||||
void reduce_by(pvar v, conflict_core& core);
|
||||
bool reduce_by(pvar, signed_constraint c, conflict_core& core);
|
||||
lbool try_explain1(pvar v, conflict_core& core);
|
||||
signed_constraint find_replacement(signed_constraint c2, pvar v, conflict& core);
|
||||
void reduce_by(pvar v, conflict& core);
|
||||
bool reduce_by(pvar, signed_constraint c, conflict& core);
|
||||
lbool try_explain1(pvar v, conflict& core);
|
||||
public:
|
||||
bool try_explain(pvar v, conflict_core& core) override;
|
||||
bool try_explain(pvar v, conflict& core) override;
|
||||
};
|
||||
|
||||
|
||||
|
|
@ -54,7 +54,7 @@ namespace polysat {
|
|||
class conflict_explainer {
|
||||
solver& m_solver;
|
||||
|
||||
// conflict_core m_conflict;
|
||||
// conflict m_conflict;
|
||||
vector<constraint> m_new_assertions; // to be inserted into Gamma (conclusions from saturation)
|
||||
|
||||
scoped_ptr_vector<inference_engine> inference_engines;
|
||||
|
|
@ -64,7 +64,7 @@ namespace polysat {
|
|||
// Gamma
|
||||
// search_state& search() { return m_solver.m_search; }
|
||||
// Core
|
||||
// conflict_core& conflict() { return m_solver.m_conflict; }
|
||||
// conflict& conflict() { return m_solver.m_conflict; }
|
||||
public:
|
||||
/** Create empty conflict */
|
||||
conflict_explainer(solver& s);
|
||||
|
|
|
|||
|
|
@ -72,7 +72,7 @@ namespace polysat {
|
|||
* We assume that neg_cond is a consequence of src that
|
||||
* does not mention the variable v to be eliminated.
|
||||
*/
|
||||
void forbidden_intervals::full_interval_conflict(signed_constraint src, signed_constraint neg_cond, conflict_core& core) {
|
||||
void forbidden_intervals::full_interval_conflict(signed_constraint src, signed_constraint neg_cond, conflict& core) {
|
||||
SASSERT(neg_cond);
|
||||
core.reset();
|
||||
core.insert(~neg_cond);
|
||||
|
|
@ -80,7 +80,7 @@ namespace polysat {
|
|||
core.set_bailout();
|
||||
}
|
||||
|
||||
bool forbidden_intervals::perform(solver& s, pvar v, vector<signed_constraint> const& just, conflict_core& core) {
|
||||
bool forbidden_intervals::perform(solver& s, pvar v, vector<signed_constraint> const& just, conflict& core) {
|
||||
|
||||
// Extract forbidden intervals from conflicting constraints
|
||||
vector<fi_record> records;
|
||||
|
|
|
|||
|
|
@ -20,9 +20,9 @@ Author:
|
|||
namespace polysat {
|
||||
|
||||
class forbidden_intervals {
|
||||
void full_interval_conflict(signed_constraint c, signed_constraint neg_cond, conflict_core& core);
|
||||
void full_interval_conflict(signed_constraint c, signed_constraint neg_cond, conflict& core);
|
||||
bool get_interval(solver& s, signed_constraint const& c, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond);
|
||||
public:
|
||||
bool perform(solver& s, pvar v, vector<signed_constraint> const& just, conflict_core& core);
|
||||
bool perform(solver& s, pvar v, vector<signed_constraint> const& just, conflict& core);
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -29,7 +29,7 @@ TODO: when we check that 'x' is "unary":
|
|||
|
||||
namespace polysat {
|
||||
|
||||
bool inf_saturate::perform(pvar v, conflict_core& core) {
|
||||
bool inf_saturate::perform(pvar v, conflict& core) {
|
||||
for (auto c1 : core) {
|
||||
if (!c1->is_ule())
|
||||
continue;
|
||||
|
|
@ -57,7 +57,7 @@ namespace polysat {
|
|||
* Propagate c. It is added to reason and core all other literals in reason are false in current stack.
|
||||
* The lemmas outlined in the rules are valid and therefore c is implied.
|
||||
*/
|
||||
bool inf_saturate::propagate(conflict_core& core, inequality const& crit1, inequality const& crit2, signed_constraint& c, vector<signed_constraint>& new_constraints) {
|
||||
bool inf_saturate::propagate(conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint& c, vector<signed_constraint>& new_constraints) {
|
||||
bool crit1_false = crit1.as_signed_constraint().is_currently_false(s());
|
||||
bool crit2_false = crit2.as_signed_constraint().is_currently_false(s());
|
||||
if (!crit1_false && !crit2_false)
|
||||
|
|
@ -83,7 +83,7 @@ namespace polysat {
|
|||
return true;
|
||||
}
|
||||
|
||||
bool inf_saturate::propagate(conflict_core& core, inequality const& crit1, inequality const& crit2, bool is_strict, pdd const& lhs, pdd const& rhs, vector<signed_constraint>& new_constraints) {
|
||||
bool inf_saturate::propagate(conflict& core, inequality const& crit1, inequality const& crit2, bool is_strict, pdd const& lhs, pdd const& rhs, vector<signed_constraint>& new_constraints) {
|
||||
signed_constraint c = ineq(is_strict, lhs, rhs);
|
||||
return propagate(core, crit1, crit2, c, new_constraints);
|
||||
}
|
||||
|
|
@ -263,7 +263,7 @@ namespace polysat {
|
|||
* [x] zx > yx ==> Ω*(x,y) \/ z > y
|
||||
* [x] yx <= zx ==> Ω*(x,y) \/ y <= z \/ x = 0
|
||||
*/
|
||||
bool inf_saturate::try_ugt_x(pvar v, conflict_core& core, inequality const& c) {
|
||||
bool inf_saturate::try_ugt_x(pvar v, conflict& core, inequality const& c) {
|
||||
pdd x = s().var(v);
|
||||
pdd y = x;
|
||||
pdd z = x;
|
||||
|
|
@ -283,7 +283,7 @@ namespace polysat {
|
|||
|
||||
/// [y] z' <= y /\ zx > yx ==> Ω*(x,y) \/ zx > z'x
|
||||
/// [y] z' <= y /\ yx <= zx ==> Ω*(x,y) \/ z'x <= zx
|
||||
bool inf_saturate::try_ugt_y(pvar v, conflict_core& core, inequality const& le_y, inequality const& yx_l_zx, pdd const& x, pdd const& z) {
|
||||
bool inf_saturate::try_ugt_y(pvar v, conflict& core, inequality const& le_y, inequality const& yx_l_zx, pdd const& x, pdd const& z) {
|
||||
pdd const y = s().var(v);
|
||||
|
||||
SASSERT(is_l_v(v, le_y));
|
||||
|
|
@ -301,7 +301,7 @@ namespace polysat {
|
|||
return propagate(core, le_y, yx_l_zx, yx_l_zx.is_strict || le_y.is_strict, z_prime * x, z * x, new_constraints);
|
||||
}
|
||||
|
||||
bool inf_saturate::try_ugt_y(pvar v, conflict_core& core, inequality const& c) {
|
||||
bool inf_saturate::try_ugt_y(pvar v, conflict& core, inequality const& c) {
|
||||
if (!is_l_v(v, c))
|
||||
return false;
|
||||
pdd x = s().var(v);
|
||||
|
|
@ -319,7 +319,7 @@ namespace polysat {
|
|||
|
||||
/// [x] y <= ax /\ x <= z (non-overflow case)
|
||||
/// ==> Ω*(a, z) \/ y <= az
|
||||
bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict_core& core, inequality const& c) {
|
||||
bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& c) {
|
||||
if (!is_g_v(x, c))
|
||||
return false;
|
||||
pdd y = s().var(x);
|
||||
|
|
@ -334,7 +334,7 @@ namespace polysat {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict_core& core, inequality const& x_l_z, inequality const& y_l_ax, pdd const& a, pdd const& y) {
|
||||
bool inf_saturate::try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& x_l_z, inequality const& y_l_ax, pdd const& a, pdd const& y) {
|
||||
|
||||
SASSERT(is_g_v(x, x_l_z));
|
||||
SASSERT(verify_Y_l_Ax(x, y_l_ax, a, y));
|
||||
|
|
@ -351,7 +351,7 @@ namespace polysat {
|
|||
|
||||
/// [z] z <= y' /\ zx > yx ==> Ω*(x,y') \/ y'x > yx
|
||||
/// [z] z <= y' /\ yx <= zx ==> Ω*(x,y') \/ yx <= y'x
|
||||
bool inf_saturate::try_ugt_z(pvar z, conflict_core& core, inequality const& c) {
|
||||
bool inf_saturate::try_ugt_z(pvar z, conflict& core, inequality const& c) {
|
||||
if (!is_g_v(z, c))
|
||||
return false;
|
||||
pdd y = s().var(z);
|
||||
|
|
@ -366,7 +366,7 @@ namespace polysat {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool inf_saturate::try_ugt_z(pvar z, conflict_core& core, inequality const& z_l_y, inequality const& yx_l_zx, pdd const& x, pdd const& y) {
|
||||
bool inf_saturate::try_ugt_z(pvar z, conflict& core, inequality const& z_l_y, inequality const& yx_l_zx, pdd const& x, pdd const& y) {
|
||||
SASSERT(is_g_v(z, z_l_y));
|
||||
SASSERT(verify_YX_l_zX(z, yx_l_zx, x, y));
|
||||
pdd const& y_prime = z_l_y.rhs;
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ Author:
|
|||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "math/polysat/conflict_core.h"
|
||||
#include "math/polysat/conflict.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
|
|
@ -20,7 +20,7 @@ namespace polysat {
|
|||
class constraint_manager;
|
||||
|
||||
class inference_engine {
|
||||
friend class conflict_core;
|
||||
friend class conflict;
|
||||
solver* m_solver = nullptr;
|
||||
void set_solver(solver& s) { m_solver = &s; }
|
||||
protected:
|
||||
|
|
@ -31,7 +31,7 @@ namespace polysat {
|
|||
* Derive new constraints from constraints containing the variable v (i.e., at least one premise must contain v).
|
||||
* Returns true if a new constraint was added to the core.
|
||||
*/
|
||||
virtual bool perform(pvar v, conflict_core& core) = 0;
|
||||
virtual bool perform(pvar v, conflict& core) = 0;
|
||||
};
|
||||
|
||||
class inf_saturate : public inference_engine {
|
||||
|
|
@ -40,19 +40,19 @@ namespace polysat {
|
|||
void push_omega(vector<signed_constraint>& new_constraints, pdd const& x, pdd const& y);
|
||||
void push_omega_bisect(vector<signed_constraint>& new_constraints, pdd const& x, rational x_max, pdd const& y, rational y_max);
|
||||
signed_constraint ineq(bool strict, pdd const& lhs, pdd const& rhs);
|
||||
bool propagate(conflict_core& core, inequality const& crit1, inequality const& crit2, signed_constraint& c, vector<signed_constraint>& new_constraints);
|
||||
bool propagate(conflict_core& core, inequality const& crit1, inequality const& crit2, bool strict, pdd const& lhs, pdd const& rhs, vector<signed_constraint>& new_constraints);
|
||||
bool propagate(conflict& core, inequality const& crit1, inequality const& crit2, signed_constraint& c, vector<signed_constraint>& new_constraints);
|
||||
bool propagate(conflict& core, inequality const& crit1, inequality const& crit2, bool strict, pdd const& lhs, pdd const& rhs, vector<signed_constraint>& new_constraints);
|
||||
|
||||
bool try_ugt_x(pvar v, conflict_core& core, inequality const& c);
|
||||
bool try_ugt_x(pvar v, conflict& core, inequality const& c);
|
||||
|
||||
bool try_ugt_y(pvar v, conflict_core& core, inequality const& c);
|
||||
bool try_ugt_y(pvar v, conflict_core& core, inequality const& l_y, inequality const& yx_l_zx, pdd const& x, pdd const& z);
|
||||
bool try_ugt_y(pvar v, conflict& core, inequality const& c);
|
||||
bool try_ugt_y(pvar v, conflict& core, inequality const& l_y, inequality const& yx_l_zx, pdd const& x, pdd const& z);
|
||||
|
||||
bool try_y_l_ax_and_x_l_z(pvar x, conflict_core& core, inequality const& c);
|
||||
bool try_y_l_ax_and_x_l_z(pvar x, conflict_core& core, inequality const& x_l_z, inequality const& y_l_ax, pdd const& a, pdd const& y);
|
||||
bool try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& c);
|
||||
bool try_y_l_ax_and_x_l_z(pvar x, conflict& core, inequality const& x_l_z, inequality const& y_l_ax, pdd const& a, pdd const& y);
|
||||
|
||||
bool try_ugt_z(pvar z, conflict_core& core, inequality const& c);
|
||||
bool try_ugt_z(pvar z, conflict_core& core, inequality const& x_l_z0, inequality const& yz_l_xz, pdd const& y, pdd const& x);
|
||||
bool try_ugt_z(pvar z, conflict& core, inequality const& c);
|
||||
bool try_ugt_z(pvar z, conflict& core, inequality const& x_l_z0, inequality const& yz_l_xz, pdd const& y, pdd const& x);
|
||||
|
||||
// c := lhs ~ v
|
||||
// where ~ is < or <=
|
||||
|
|
@ -90,7 +90,7 @@ namespace polysat {
|
|||
|
||||
public:
|
||||
|
||||
bool perform(pvar v, conflict_core& core) override;
|
||||
bool perform(pvar v, conflict& core) override;
|
||||
};
|
||||
|
||||
/*
|
||||
|
|
|
|||
|
|
@ -21,7 +21,7 @@ Author:
|
|||
#include "util/statistics.h"
|
||||
#include "util/params.h"
|
||||
#include "math/polysat/boolean.h"
|
||||
#include "math/polysat/conflict_core.h"
|
||||
#include "math/polysat/conflict.h"
|
||||
#include "math/polysat/constraint.h"
|
||||
#include "math/polysat/clause_builder.h"
|
||||
#include "math/polysat/explain.h"
|
||||
|
|
@ -52,7 +52,7 @@ namespace polysat {
|
|||
friend class signed_constraint;
|
||||
friend class clause;
|
||||
friend class clause_builder;
|
||||
friend class conflict_core;
|
||||
friend class conflict;
|
||||
friend class conflict_explainer;
|
||||
friend class explainer;
|
||||
friend class inference_engine;
|
||||
|
|
@ -73,7 +73,7 @@ namespace polysat {
|
|||
small_object_allocator m_alloc;
|
||||
poly_dep_manager m_dm;
|
||||
linear_solver m_linear_solver;
|
||||
conflict_core m_conflict;
|
||||
conflict m_conflict;
|
||||
bool_var_manager m_bvars; // Map boolean variables to constraints
|
||||
var_queue m_free_pvars; // free poly vars
|
||||
stats m_stats;
|
||||
|
|
|
|||
|
|
@ -17,7 +17,7 @@ Author:
|
|||
|
||||
namespace polysat {
|
||||
|
||||
bool ve_reduction::perform(solver& s, pvar v, conflict_core& core) {
|
||||
bool ve_reduction::perform(solver& s, pvar v, conflict& core) {
|
||||
// without any further hints, we just do core reduction with the stronger premise "C contains a c' that evaluates to false",
|
||||
// and kick out all other constraints.
|
||||
auto pred = [&s, v](signed_constraint c) -> bool {
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ Author:
|
|||
|
||||
--*/
|
||||
#pragma once
|
||||
#include "math/polysat/conflict_core.h"
|
||||
#include "math/polysat/conflict.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
|
|
@ -21,12 +21,12 @@ namespace polysat {
|
|||
class variable_elimination_engine {
|
||||
public:
|
||||
virtual ~variable_elimination_engine() {}
|
||||
virtual bool perform(solver& s, pvar v, conflict_core& core) = 0;
|
||||
virtual bool perform(solver& s, pvar v, conflict& core) = 0;
|
||||
};
|
||||
|
||||
class ve_reduction : public variable_elimination_engine {
|
||||
public:
|
||||
bool perform(solver& s, pvar v, conflict_core& core) override;
|
||||
bool perform(solver& s, pvar v, conflict& core) override;
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue