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

Polysat: use constraint_literal and begin move to core-based conflict representation (#5489)

Browse source 
* Rename solver_scope for fixplex tests

(otherwise the wrong constructor is called for polysat's solver_scope)

* Update conflict_core

* simplify

* Be clearer about constraint_literal lifetime

* remove old comment

* Remove status (positive/negative) from constraint

* Use constraint_literal in the solver

* Fix build (constraint -> get_constraint)
This commit is contained in:
Jakob Rath 2021-08-18 20:02:46 +02:00 • committed by GitHub
parent 30e9f24fa3
commit ebaea2159e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
19 changed files with 933 additions and 1004 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -52,12 +52,10 @@ namespace polysat {
m_literals.push_back(lit);
}
void clause_builder::push_new_constraint(constraint_literal c) {
void clause_builder::push_new_constraint(constraint_literal_ref c) {
// TODO: assert that constraint is new (not 'inserted' into manager yet)
SASSERT(c);
SASSERT(c->is_undef());
tmp_assign _t(c.get(), c.literal());
if (c->is_always_false())
if (c.get().is_always_false())
return;
m_level = std::max(m_level, c->level());
m_literals.push_back(c.literal());

2
src/math/polysat/clause_builder.h
View file

@ -46,7 +46,7 @@ namespace polysat {
void push_literal(sat::literal lit);
/// Add a constraint to the clause that does not yet exist in the solver so far.
void push_new_constraint(constraint_literal c);
void push_new_constraint(constraint_literal_ref c);
};
}

35
src/math/polysat/conflict_core.cpp
View file

@ -20,9 +20,40 @@ Author:
namespace polysat {
std::ostream& conflict_core::display(std::ostream& out) const {
out << "TODO: display conflict_core";
// depending on sign: A /\ B /\ C or ¬A \/ ¬B \/ ¬C
bool first = true;
for (auto c : m_constraints) {
if (first)
first = false;
else
out << " ; ";
out << c;
}
if (m_needs_model)
out << " ; + current model";
return out;
}
void conflict_core::set(std::nullptr_t) {
SASSERT(empty());
m_constraints.push_back({});
m_needs_model = false;
}
void conflict_core::set(constraint_literal c) {
LOG("Conflict: " << c);
SASSERT(empty());
m_constraints.push_back(std::move(c));
m_needs_model = true;
}
void conflict_core::set(pvar v, vector<constraint_literal> const& cjust_v) {
LOG("Conflict for v" << v << ": " << cjust_v);
SASSERT(empty());
NOT_IMPLEMENTED_YET();
m_constraints.append(cjust_v);
if (cjust_v.empty())
m_constraints.push_back({});
m_needs_model = true;
}
}

47
src/math/polysat/conflict_core.h
View file

@ -16,47 +16,38 @@ Author:
namespace polysat {
/// Represents a conflict as core (~negation of clause).
///
/// TODO: can probably move some clause_builder functionality into this class.
/** Conflict state, represented as core (~negation of clause). */
class conflict_core {
// constraint_ref_vector m_constraints;
// TODO: core needs to own the constraint literals...
vector<constraint_literal> m_constraints;
bool m_needs_model = true; ///< True iff the conflict depends on the current variable assignment. (If so, additional constraints must be added to the final learned clause.)
/** True iff the conflict depends on the current variable assignment. (If so, additional constraints must be added to the final learned clause.) */
bool m_needs_model = false;
// NOTE: for now we keep this simple implementation.
// The drawback is that we may get weaker lemmas in some cases (but they are still correct).
// For example: if we have 4x+y=2 and y=0, then we have a conflict no matter the value of x, so we should drop x=? from the core.
public:
vector<constraint_literal> const& constraints() const {
return m_constraints;
}
vector<constraint_literal> const& constraints() const { return m_constraints; }
bool needs_model() const { return m_needs_model; }
bool empty() const {
return m_constraints.empty();
return m_constraints.empty() && !m_needs_model;
}
void reset() {
m_constraints.reset();
m_needs_model = true;
}
// for bailing out with a conflict at the base level
void set(std::nullptr_t) {
SASSERT(empty());
m_constraints.push_back({});
m_needs_model = false;
SASSERT(empty());
}
// void set(
// TODO: set core from conflicting units
// TODO: set clause
// TODO: use iterator instead (this method is needed for marking so duplicates don't necessarily have to be skipped)
unsigned_vector vars(constraint_manager const& cm) const {
unsigned_vector vars;
for (auto const& c : m_constraints)
vars.append(c->vars());
return vars;
}
/** for bailing out with a conflict at the base level */
void set(std::nullptr_t);
/** conflict because the constraint c is false under current variable assignment */
void set(constraint_literal c);
/** conflict because there is no viable value for the variable v */
void set(pvar v, vector<constraint_literal> const& cjust_v);
std::ostream& display(std::ostream& out) const;
};

78
src/math/polysat/constraint.cpp
View file

@ -93,6 +93,10 @@ namespace polysat {
return get_bv2c(var);
}
constraint_literal constraint_manager::lookup(sat::literal lit) const {
return {lit, lookup(lit.var())};
}
eq_constraint& constraint::to_eq() {
return *dynamic_cast<eq_constraint*>(this);
}
@ -109,16 +113,16 @@ namespace polysat {
return *dynamic_cast<ule_constraint const*>(this);
}
constraint_literal constraint_manager::eq(unsigned lvl, pdd const& p) {
return constraint_literal{alloc(eq_constraint, *this, lvl, p)};
constraint_literal_ref constraint_manager::eq(unsigned lvl, pdd const& p) {
return constraint_literal_ref{alloc(eq_constraint, *this, lvl, p)};
}
constraint_literal constraint_manager::ule(unsigned lvl, pdd const& a, pdd const& b) {
return constraint_literal{alloc(ule_constraint, *this, lvl, a, b)};
constraint_literal_ref constraint_manager::ule(unsigned lvl, pdd const& a, pdd const& b) {
return constraint_literal_ref{alloc(ule_constraint, *this, lvl, a, b)};
}
constraint_literal constraint_manager::ult(unsigned lvl, pdd const& a, pdd const& b) {
constraint_literal_ref constraint_manager::ult(unsigned lvl, pdd const& a, pdd const& b) {
// a < b <=> !(b <= a)
return ~ule(lvl, b, a);
}
@ -139,25 +143,26 @@ namespace polysat {
//
// Argument: flipping the msb swaps the negative and non-negative blocks
//
constraint_literal constraint_manager::sle(unsigned lvl, pdd const& a, pdd const& b) {
constraint_literal_ref constraint_manager::sle(unsigned lvl, pdd const& a, pdd const& b) {
auto shift = rational::power_of_two(a.power_of_2() - 1);
return ule(lvl, a + shift, b + shift);
}
constraint_literal constraint_manager::slt(unsigned lvl, pdd const& a, pdd const& b) {
constraint_literal_ref constraint_manager::slt(unsigned lvl, pdd const& a, pdd const& b) {
auto shift = rational::power_of_two(a.power_of_2() - 1);
return ult(lvl, a + shift, b + shift);
}
std::ostream& constraint::display_extra(std::ostream& out) const {
std::ostream& constraint::display_extra(std::ostream& out, lbool status) const {
out << " @" << level() << " (b" << bvar() << ")";
if (is_positive()) out << " [pos]";
if (is_negative()) out << " [neg]";
if (is_undef()) out << " [inactive]";
(void)status;
// if (is_positive()) out << " [pos]";
// if (is_negative()) out << " [neg]";
// if (is_undef()) out << " [inactive]"; // TODO: not sure if we still need/want this... decide later
return out;
}
bool constraint::propagate(solver& s, pvar v) {
bool constraint::propagate(solver& s, bool is_positive, pvar v) {
LOG_H3("Propagate " << s.m_vars[v] << " in " << *this);
SASSERT(!vars().empty());
unsigned idx = 0;
@ -168,24 +173,35 @@ namespace polysat {
for (unsigned i = vars().size(); i-- > 2; ) {
unsigned other_v = vars()[i];
if (!s.is_assigned(other_v)) {
s.add_watch(*this, other_v);
s.add_watch({this, is_positive}, other_v);
std::swap(vars()[idx], vars()[i]);
return true;
}
}
// at most one variable remains unassigned.
unsigned other_v = vars()[idx];
propagate_core(s, v, other_v);
propagate_core(s, is_positive, v, other_v);
return false;
}
void constraint::propagate_core(solver& s, pvar v, pvar other_v) {
void constraint::propagate_core(solver& s, bool is_positive, pvar v, pvar other_v) {
(void)v;
(void)other_v;
narrow(s);
narrow(s, is_positive);
}
clause_ref clause::from_unit(constraint_literal c, p_dependency_ref d) {
std::ostream &constraint_literal::display(std::ostream &out) const {
if (*this)
return out << m_literal << "{ " << *m_constraint << " }";
else
return out << "<null>";
}
std::ostream &constraint_literal_ref::display(std::ostream &out) const {
return out << get();
}
clause_ref clause::from_unit(constraint_literal_ref c, p_dependency_ref d) {
SASSERT(c);
unsigned const lvl = c->level();
sat::literal_vector lits;
@ -201,17 +217,15 @@ namespace polysat {
bool clause::is_always_false(solver& s) const {
return std::all_of(m_literals.begin(), m_literals.end(), [&s](sat::literal lit) {
constraint *c = s.m_constraints.lookup(lit.var());
tmp_assign _t(c, lit);
return c->is_always_false();
constraint_literal c = s.m_constraints.lookup(lit);
return c.is_always_false();
});
}
bool clause::is_currently_false(solver& s) const {
return std::all_of(m_literals.begin(), m_literals.end(), [&s](sat::literal lit) {
constraint *c = s.m_constraints.lookup(lit.var());
tmp_assign _t(c, lit);
return c->is_currently_false(s);
constraint_literal c = s.m_constraints.lookup(lit);
return c.is_currently_false(s);
});
}
@ -251,22 +265,4 @@ namespace polysat {
return out;
}
std::ostream& constraints_and_clauses::display(std::ostream& out) const {
bool first = true;
for (auto c : units()) {
if (first)
first = false;
else
out << " ; ";
out << show_deref(c);
}
for (auto cl : clauses()) {
if (first)
first = false;
else
out << " ; ";
out << show_deref(cl);
}
return out;
}
}

243
src/math/polysat/constraint.h
View file

@ -26,6 +26,7 @@ namespace polysat {
enum csign_t : bool { neg_t = false, pos_t = true };
class constraint_literal;
class constraint_literal_ref;
class constraint;
class constraint_manager;
class clause;
@ -34,6 +35,7 @@ namespace polysat {
class ule_constraint;
using constraint_ref = ref<constraint>;
using constraint_ref_vector = sref_vector<constraint>;
using constraint_literal_ref_vector = vector<constraint_literal_ref>;
using clause_ref = ref<clause>;
using clause_ref_vector = sref_vector<clause>;
@ -49,7 +51,7 @@ namespace polysat {
void erase_bv2c(sat::bool_var bv) { m_bv2constraint[bv] = nullptr; }
constraint* get_bv2c(sat::bool_var bv) const { return m_bv2constraint.get(bv, nullptr); }
// Constraint storage per level; should be destructed before m_bv2constraint
// Constraint storage per level; should be destructed before m_bv2constraint because constraint's destructor calls erase_bv2c
vector<vector<constraint_ref>> m_constraints;
vector<vector<clause_ref>> m_clauses;
@ -74,13 +76,14 @@ namespace polysat {
void release_level(unsigned lvl);
constraint* lookup(sat::bool_var var) const;
constraint_literal lookup(sat::literal lit) const;
constraint* lookup_external(unsigned dep) const { return m_external_constraints.get(dep, nullptr); }
constraint_literal eq(unsigned lvl, pdd const& p);
constraint_literal ule(unsigned lvl, pdd const& a, pdd const& b);
constraint_literal ult(unsigned lvl, pdd const& a, pdd const& b);
constraint_literal sle(unsigned lvl, pdd const& a, pdd const& b);
constraint_literal slt(unsigned lvl, pdd const& a, pdd const& b);
constraint_literal_ref eq(unsigned lvl, pdd const& p);
constraint_literal_ref ule(unsigned lvl, pdd const& a, pdd const& b);
constraint_literal_ref ult(unsigned lvl, pdd const& a, pdd const& b);
constraint_literal_ref sle(unsigned lvl, pdd const& a, pdd const& b);
constraint_literal_ref slt(unsigned lvl, pdd const& a, pdd const& b);
// p_dependency_ref null_dep() const { return {nullptr, m_dm}; }
};
@ -109,12 +112,10 @@ namespace polysat {
constraint_manager* m_manager;
clause* m_unit_clause = nullptr; ///< If this constraint was asserted by a unit clause, we store that clause here.
unsigned m_ref_count = 0;
// TODO: we could remove the level on constraints and instead store constraint_refs for all literals inside the clause? (clauses will then be 4 times larger though...)
unsigned m_storage_level; ///< Controls lifetime of the constraint object. Always a base level.
ckind_t m_kind;
unsigned_vector m_vars;
sat::bool_var m_bvar; ///< boolean variable associated to this constraint; convention: a constraint itself always represents the positive sat::literal
lbool m_status = l_undef; ///< current constraint status; intended to be the same as m_manager->m_bvars.value(bvar()) if that value is set.
constraint(constraint_manager& m, unsigned lvl, ckind_t k):
m_manager(&m), m_storage_level(lvl), m_kind(k), m_bvar(m_manager->m_bvars.new_var()) {
@ -123,7 +124,7 @@ namespace polysat {
}
protected:
std::ostream& display_extra(std::ostream& out) const;
std::ostream& display_extra(std::ostream& out, lbool status) const;
public:
void inc_ref() { m_ref_count++; }
@ -140,14 +141,16 @@ namespace polysat {
bool is_eq() const { return m_kind == ckind_t::eq_t; }
bool is_ule() const { return m_kind == ckind_t::ule_t; }
ckind_t kind() const { return m_kind; }
virtual std::ostream& display(std::ostream& out) const = 0;
bool propagate(solver& s, pvar v);
virtual void propagate_core(solver& s, pvar v, pvar other_v);
virtual bool is_always_false() = 0;
virtual bool is_currently_false(solver& s) = 0;
virtual bool is_currently_true(solver& s) = 0;
virtual void narrow(solver& s) = 0;
virtual inequality as_inequality() const = 0;
virtual std::ostream& display(std::ostream& out, lbool status = l_undef) const = 0;
bool propagate(solver& s, bool is_positive, pvar v);
virtual void propagate_core(solver& s, bool is_positive, pvar v, pvar other_v);
virtual bool is_always_false(bool is_positive) = 0;
virtual bool is_currently_false(solver& s, bool is_positive) = 0;
virtual bool is_currently_true(solver& s, bool is_positive) = 0;
virtual void narrow(solver& s, bool is_positive) = 0;
virtual inequality as_inequality(bool is_positive) const = 0;
eq_constraint& to_eq();
eq_constraint const& to_eq() const;
ule_constraint& to_ule();
@ -155,27 +158,8 @@ namespace polysat {
unsigned_vector& vars() { return m_vars; }
unsigned_vector const& vars() const { return m_vars; }
unsigned level() const { return m_storage_level; }
// unsigned active_level() const {
// SASSERT(!is_undef());
// return m_manager->m_bvars.level(bvar());
// }
// unsigned active_at_base_level(solver& s) const {
// return !is_undef() && active_level() <= s.base_level();
// }
sat::bool_var bvar() const { return m_bvar; }
sat::literal blit() const { SASSERT(!is_undef()); return m_status == l_true ? sat::literal(m_bvar) : ~sat::literal(m_bvar); }
void assign(bool is_true) {
SASSERT(m_status == l_undef || m_status == to_lbool(is_true));
// SASSERT(m_status == l_undef /* || m_status == to_lbool(is_true) */);
m_status = to_lbool(is_true);
// SASSERT(m_manager->m_bvars.value(bvar()) == l_undef || m_manager->m_bvars.value(bvar()) == m_status); // TODO: is this always true? maybe we sometimes want to check the opposite phase temporarily.
}
void unassign() { m_status = l_undef; }
bool is_undef() const { return m_status == l_undef; }
bool is_positive() const { return m_status == l_true; }
bool is_negative() const { return m_status == l_false; }
clause* unit_clause() const { return m_unit_clause; }
void set_unit_clause(clause* cl) { SASSERT(cl); SASSERT(!m_unit_clause || m_unit_clause == cl); m_unit_clause = cl; }
p_dependency* unit_dep() const;
@ -186,43 +170,111 @@ namespace polysat {
* \param[out] out_neg_cond Negation of the side condition (the side condition is true when the forbidden interval is trivial). May be NULL if the condition is constant.
* \returns True iff a forbidden interval exists and the output parameters were set.
*/
virtual bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond) { return false; }
// TODO: we can probably remove this and unify the implementations for both cases by relying on as_inequality().
virtual bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, constraint_literal_ref& out_neg_cond) { return false; }
};
inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
/// Literal together with the constraint it represents.
/// (or: constraint with polarity)
/// Literal together with the constraint it represents (i.e., constraint with polarity).
/// Non-owning version.
class constraint_literal {
sat::literal m_literal = sat::null_literal;
constraint* m_constraint = nullptr;
public:
constraint_literal() {}
constraint_literal(sat::literal lit, constraint* c):
m_literal(lit), m_constraint(c) {
SASSERT(get_constraint());
SASSERT(literal().var() == get_constraint()->bvar());
}
constraint_literal(constraint* c, bool is_positive): constraint_literal(sat::literal(c->bvar(), !is_positive), c) {}
constraint_literal operator~() const {
return {~m_literal, m_constraint};
}
void negate() {
m_literal = ~m_literal;
}
bool is_positive() const { return !m_literal.sign(); }
bool is_negative() const { return m_literal.sign(); }
bool propagate(solver& s, pvar v) { return get_constraint()->propagate(s, !literal().sign(), v); }
void propagate_core(solver& s, pvar v, pvar other_v) { get_constraint()->propagate_core(s, !literal().sign(), v, other_v); }
bool is_always_false() { return get_constraint()->is_always_false(!literal().sign()); }
bool is_currently_false(solver& s) { return get_constraint()->is_currently_false(s, !literal().sign()); }
bool is_currently_true(solver& s) { return get_constraint()->is_currently_true(s, !literal().sign()); }
void narrow(solver& s) { get_constraint()->narrow(s, !literal().sign()); }
inequality as_inequality() const { return get_constraint()->as_inequality(!literal().sign()); }
sat::literal literal() const { return m_literal; }
constraint* get_constraint() const { return m_constraint; }
explicit operator bool() const { return !!m_constraint; }
bool operator!() const { return !m_constraint; }
constraint* operator->() const { return m_constraint; }
constraint const& operator*() const { return *m_constraint; }
constraint_literal& operator=(std::nullptr_t) { m_literal = sat::null_literal; m_constraint = nullptr; return *this; }
std::ostream& display(std::ostream& out) const;
};
inline std::ostream& operator<<(std::ostream& out, constraint_literal const& c) { return c.display(out); }
inline bool operator==(constraint_literal const& lhs, constraint_literal const& rhs) {
if (lhs.literal() == rhs.literal())
SASSERT(lhs.get_constraint() == rhs.get_constraint());
return lhs.literal() == rhs.literal();
}
/// Version of constraint_literal that owns the constraint.
class constraint_literal_ref {
sat::literal m_literal = sat::null_literal;
constraint_ref m_constraint = nullptr;
public:
constraint_literal() {}
constraint_literal(sat::literal lit, constraint_ref c):
constraint_literal_ref() {}
constraint_literal_ref(sat::literal lit, constraint_ref c):
m_literal(lit), m_constraint(std::move(c)) {
SASSERT(get());
SASSERT(literal().var() == get()->bvar());
SASSERT(get_constraint());
SASSERT(literal().var() == get_constraint()->bvar());
}
constraint_literal operator~() const&& {
constraint_literal_ref(constraint_literal cl): constraint_literal_ref(cl.literal(), cl.get_constraint()) {}
constraint_literal_ref operator~() const&& {
return {~m_literal, std::move(m_constraint)};
}
void negate() {
m_literal = ~m_literal;
}
sat::literal literal() const { return m_literal; }
constraint* get() const { return m_constraint.get(); }
constraint* get_constraint() const { return m_constraint.get(); }
constraint_literal get() const { return {literal(), get_constraint()}; }
constraint_ref detach() { m_literal = sat::null_literal; return std::move(m_constraint); }
explicit operator bool() const { return !!m_constraint; }
bool operator!() const { return !m_constraint; }
constraint* operator->() const { return m_constraint.get(); }
constraint* operator->() const { return m_constraint.operator->(); }
constraint const& operator*() const { return *m_constraint; }
constraint_literal& operator=(std::nullptr_t) { m_literal = sat::null_literal; m_constraint = nullptr; return *this; }
constraint_literal_ref& operator=(std::nullptr_t) { m_literal = sat::null_literal; m_constraint = nullptr; return *this; }
std::ostream& display(std::ostream& out) const;
private:
friend class constraint_manager;
explicit constraint_literal(constraint* c): constraint_literal(sat::literal(c->bvar()), c) {}
explicit constraint_literal_ref(constraint* c): constraint_literal_ref(sat::literal(c->bvar()), c) {}
};
inline std::ostream& operator<<(std::ostream& out, constraint_literal_ref const& c) { return c.display(out); }
/// Disjunction of constraints represented by boolean literals
class clause {
@ -254,7 +306,7 @@ namespace polysat {
void inc_ref() { m_ref_count++; }
void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (!m_ref_count) dealloc(this); }
static clause_ref from_unit(constraint_literal c, p_dependency_ref d);
static clause_ref from_unit(constraint_literal_ref c, p_dependency_ref d);
static clause_ref from_literals(unsigned lvl, p_dependency_ref d, sat::literal_vector literals, constraint_ref_vector new_constraints);
// Resolve with 'other' upon 'var'.
@ -286,98 +338,5 @@ namespace polysat {
inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); }
// Container for unit constraints and clauses.
class constraints_and_clauses {
constraint_ref_vector m_units;
clause_ref_vector m_clauses;
public:
constraint_ref_vector const& units() const { return m_units; }
constraint_ref_vector& units() { return m_units; }
clause_ref_vector const& clauses() const { return m_clauses; }
clause_ref_vector& clauses() { return m_clauses; }
bool is_unit() const { return units().size() == 1 && clauses().empty(); }
constraint* get_unit() const { SASSERT(is_unit()); return units()[0]; }
bool is_clause() const { return units().empty() && clauses().size() == 1; }
clause* get_clause() const { SASSERT(is_clause()); return clauses()[0]; }
unsigned size() const {
return m_units.size() + m_clauses.size();
}
bool empty() const {
return m_units.empty() && m_clauses.empty();
}
void reset() {
m_units.reset();
m_clauses.reset();
}
void append(ptr_vector<constraint> const& cs) {
for (constraint* c : cs)
m_units.push_back(c);
}
void push_back(std::nullptr_t) { m_units.push_back(nullptr); }
void push_back(constraint_ref c) { m_units.push_back(std::move(c)); }
void push_back(clause_ref cl) { m_clauses.push_back(std::move(cl)); }
// TODO: use iterator instead
unsigned_vector vars(constraint_manager const& cm) const {
unsigned_vector vars;
for (auto const& c : m_units)
vars.append(c->vars());
for (auto const& cl : m_clauses)
for (auto lit : *cl) {
constraint* c = cm.lookup(lit.var());
if (c)
vars.append(c->vars());
}
return vars;
}
std::ostream& display(std::ostream& out) const;
};
inline std::ostream& operator<<(std::ostream& out, constraints_and_clauses const& c) { return c.display(out); }
/// Temporarily assign a constraint according to the sign of the given literal.
class tmp_assign final {
constraint* m_constraint;
bool m_should_unassign = false;
public:
/// c must live longer than tmp_assign.
tmp_assign(constraint* c, sat::literal lit):
m_constraint(c) {
SASSERT(c);
SASSERT_EQ(c->bvar(), lit.var());
if (c->is_undef()) {
c->assign(!lit.sign());
m_should_unassign = true;
}
else
SASSERT_EQ(c->blit(), lit);
}
void revert() {
if (m_should_unassign) {
m_constraint->unassign();
m_should_unassign = false;
}
}
~tmp_assign() {
revert();
}
tmp_assign(tmp_assign&) = delete;
tmp_assign(tmp_assign&&) = delete;
tmp_assign& operator=(tmp_assign&) = delete;
tmp_assign& operator=(tmp_assign&&) = delete;
};
inline p_dependency* constraint::unit_dep() const { return m_unit_clause ? m_unit_clause->dep() : nullptr; }
}

70
src/math/polysat/eq_constraint.cpp
View file

@ -18,82 +18,73 @@ Author:
namespace polysat {
std::ostream& eq_constraint::display(std::ostream& out) const {
out << p() << " == 0";
return display_extra(out);
std::ostream& eq_constraint::display(std::ostream& out, lbool status) const {
out << p();
if (status == l_true) out << " == 0";
else if (status == l_false) out << " != 0";
else out << " ==/!= 0";
return display_extra(out, status);
}
void eq_constraint::narrow(solver& s) {
SASSERT(!is_undef());
void eq_constraint::narrow(solver& s, bool is_positive) {
LOG("Assignment: " << assignments_pp(s));
auto q = p().subst_val(s.assignment());
LOG("Substituted: " << p() << " := " << q);
if (q.is_zero()) {
if (is_positive())
return;
if (is_negative()) {
if (!is_positive) {
LOG("Conflict (zero under current assignment)");
s.set_conflict(*this);
return;
s.set_conflict({this, is_positive});
}
return;
}
if (q.is_never_zero()) {
if (is_positive()) {
if (is_positive) {
LOG("Conflict (never zero under current assignment)");
s.set_conflict(*this);
return;
s.set_conflict({this, is_positive});
}
if (is_negative())
return;
return;
}
if (q.is_unilinear()) {
// a*x + b == 0
pvar v = q.var();
s.push_cjust(v, this);
s.push_cjust(v, {this, is_positive});
rational a = q.hi().val();
rational b = q.lo().val();
s.m_viable.intersect_eq(a, v, b, is_positive());
s.m_viable.intersect_eq(a, v, b, is_positive);
rational val;
if (s.m_viable.find_viable(v, val) == dd::find_t::singleton)
s.propagate(v, val, *this);
s.propagate(v, val, {this, is_positive});
return;
}
// TODO: what other constraints can be extracted cheaply?
}
bool eq_constraint::is_always_false() {
if (is_positive())
bool eq_constraint::is_always_false(bool is_positive) {
if (is_positive)
return p().is_never_zero();
if (is_negative())
else
return p().is_zero();
UNREACHABLE();
return false;
}
bool eq_constraint::is_currently_false(solver& s) {
bool eq_constraint::is_currently_false(solver& s, bool is_positive) {
pdd r = p().subst_val(s.assignment());
if (is_positive())
if (is_positive)
return r.is_never_zero();
if (is_negative())
else
return r.is_zero();
UNREACHABLE();
return false;
}
bool eq_constraint::is_currently_true(solver& s) {
bool eq_constraint::is_currently_true(solver& s, bool is_positive) {
pdd r = p().subst_val(s.assignment());
if (is_positive())
if (is_positive)
return r.is_zero();
if (is_negative())
else
return r.is_never_zero();
UNREACHABLE();
return false;
}
@ -130,10 +121,8 @@ namespace polysat {
/// Compute forbidden interval for equality constraint by considering it as p <=u 0 (or p >u 0 for disequality)
bool eq_constraint::forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond)
bool eq_constraint::forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, constraint_literal_ref& out_neg_cond)
{
SASSERT(!is_undef());
// Current only works when degree(v) is at most one
unsigned const deg = p().degree(v);
if (deg > 1)
@ -182,7 +171,7 @@ namespace polysat {
rational lo_val = (1 - e1s).val();
pdd hi = -e1;
rational hi_val = (-e1s).val();
if (is_negative()) {
if (!is_positive) {
swap(lo, hi);
lo_val.swap(hi_val);
}
@ -191,10 +180,9 @@ namespace polysat {
return true;
}
inequality eq_constraint::as_inequality() const {
SASSERT(!is_undef());
inequality eq_constraint::as_inequality(bool is_positive) const {
pdd zero = p() - p();
if (is_positive())
if (is_positive)
// p <= 0
return inequality(p(), zero, false, this);
else

14
src/math/polysat/eq_constraint.h
View file

@ -26,13 +26,13 @@ namespace polysat {
}
~eq_constraint() override {}
pdd const & p() const { return m_poly; }
std::ostream& display(std::ostream& out) const override;
bool is_always_false() override;
bool is_currently_false(solver& s) override;
bool is_currently_true(solver& s) override;
void narrow(solver& s) override;
bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond) override;
inequality as_inequality() const override;
std::ostream& display(std::ostream& out, lbool status) const override;
bool is_always_false(bool is_positive) override;
bool is_currently_false(solver& s, bool is_positive) override;
bool is_currently_true(solver& s, bool is_positive) override;
void narrow(solver& s, bool is_positive) override;
bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, constraint_literal_ref& out_neg_cond) override;
inequality as_inequality(bool is_positive) const override;
unsigned hash() const override;
bool operator==(constraint const& other) const override;
};

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

File diff suppressed because it is too large Load diff

32
src/math/polysat/explain.h
View file

@ -3,7 +3,7 @@ Copyright (c) 2021 Microsoft Corporation
Module Name:
Conflict explanation / resolution
Conflict explanation
Author:
@ -15,33 +15,41 @@ Author:
#include "math/polysat/constraint.h"
#include "math/polysat/clause_builder.h"
#include "math/polysat/interval.h"
#include "math/polysat/solver.h"
namespace polysat {
// TODO: later, we probably want to update this class incrementally (adding/removing constraints as we go back through the trail)
// TODO: indexing of constraints/clauses?
class solver;
class conflict_explainer {
solver& m_solver;
constraints_and_clauses m_conflict;
ptr_vector<constraint> m_conflict_units;
pvar m_var = null_var;
ptr_vector<constraint> m_cjust_v;
// TODO: instead of listing methods, create an abstract class for explanation methods, register them in a vector and call them in turn
/* Conflict explanation methods */
clause_ref by_polynomial_superposition();
clause_ref by_ugt_x();
clause_ref by_ugt_y();
clause_ref by_ugt_z();
clause_ref y_ule_ax_and_x_ule_z();
p_dependency_ref null_dep() const { return m_solver.mk_dep_ref(null_dependency); }
p_dependency_ref null_dep();
// p_dependency_ref null_dep() const { return m_solver.mk_dep_ref(null_dependency); }
bool push_omega_mul(clause_builder& clause, unsigned level, unsigned p, pdd const& x, pdd const& y);
public:
conflict_explainer(solver& s, constraints_and_clauses const& conflict);
public:
/** Create empty conflict */
conflict_explainer(solver& s);
/** resolve conflict state against assignment to v */
clause_ref resolve(pvar v, ptr_vector<constraint> const& cjust_v);
// TODO: move conflict resolution from solver into this class.
// we have a single public method as entry point to conflict resolution.
// what do we need to return?
/** conflict resolution */
void resolve();
};
}

32
src/math/polysat/forbidden_intervals.cpp
View file

@ -22,8 +22,8 @@ namespace polysat {
struct fi_record {
eval_interval interval;
constraint_literal neg_cond; // could be multiple constraints later
constraint* src;
constraint_literal_ref neg_cond; // could be multiple constraints later
constraint_literal src;
};
/**
@ -64,24 +64,20 @@ namespace polysat {
return true;
}
bool forbidden_intervals::explain(solver& s, constraint_ref_vector const& conflict, pvar v, clause_ref& out_lemma) {
bool forbidden_intervals::explain(solver& s, vector<constraint_literal> const& conflict, pvar v, clause_ref& out_lemma) {
// Extract forbidden intervals from conflicting constraints
vector<fi_record> records;
bool has_full = false;
rational longest_len;
unsigned longest_i = UINT_MAX;
for (constraint* c : conflict) {
LOG_H3("Computing forbidden interval for: " << *c);
if (c->is_undef()) {
LOG("TODO: undef constraint in conflict... what does this mean???");
continue;
}
for (constraint_literal c : conflict) {
LOG_H3("Computing forbidden interval for: " << c);
eval_interval interval = eval_interval::full();
constraint_literal neg_cond;
if (c->forbidden_interval(s, v, interval, neg_cond)) {
constraint_literal_ref neg_cond;
if (c->forbidden_interval(s, c.is_positive(), v, interval, neg_cond)) {
LOG("interval: " << interval);
LOG("neg_cond: " << show_deref(neg_cond));
LOG("neg_cond: " << neg_cond);
if (interval.is_currently_empty())
continue;
if (interval.is_full())
@ -106,7 +102,7 @@ namespace polysat {
auto& full_record = records.back();
SASSERT(full_record.interval.is_full());
clause_builder clause(s);
clause.push_literal(~full_record.src->blit());
clause.push_literal(~full_record.src.literal());
if (full_record.neg_cond)
clause.push_new_constraint(std::move(full_record.neg_cond));
out_lemma = clause.build();
@ -134,7 +130,7 @@ namespace polysat {
unsigned lemma_lvl = 0;
for (unsigned i : seq) {
constraint* c = records[i].src;
constraint_literal const& c = records[i].src;
lemma_lvl = std::max(lemma_lvl, c->level());
}
@ -149,7 +145,7 @@ namespace polysat {
clause_builder clause(s);
// Add negation of src constraints as antecedents (may be resolved during backtracking)
for (unsigned const i : seq) {
sat::literal src_lit = records[i].src->blit();
sat::literal src_lit = records[i].src.literal();
clause.push_literal(~src_lit);
}
// Add side conditions and interval constraints
@ -163,12 +159,12 @@ namespace polysat {
auto const& next_hi = records[next_i].interval.hi();
auto const& lhs = hi - next_lo;
auto const& rhs = next_hi - next_lo;
constraint_literal c = ~s.m_constraints.ult(lemma_lvl, lhs, rhs);
LOG("constraint: " << *c);
constraint_literal_ref c = ~s.m_constraints.ult(lemma_lvl, lhs, rhs);
LOG("constraint: " << c);
clause.push_new_constraint(std::move(c));
// Side conditions
// TODO: check whether the condition is subsumed by c? maybe at the end do a "lemma reduction" step, to try and reduce branching?
constraint_literal& neg_cond = records[i].neg_cond;
constraint_literal_ref& neg_cond = records[i].neg_cond;
if (neg_cond)
clause.push_new_constraint(std::move(neg_cond));
}

2
src/math/polysat/forbidden_intervals.h
View file

@ -22,7 +22,7 @@ namespace polysat {
class forbidden_intervals {
public:
static bool explain(solver& s, constraint_ref_vector const& conflict, pvar v, clause_ref& out_lemma);
static bool explain(solver& s, vector<constraint_literal> const& conflict, pvar v, clause_ref& out_lemma);
};
}

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

@ -134,7 +134,6 @@ namespace polysat {
if (!fp)
return;
rational z(0), o(1);
SASSERT(!c.is_undef());
if (is_positive)
fp->set_bounds(v, z, z, c_dep);
else
@ -211,7 +210,6 @@ namespace polysat {
void linear_solver::activate_constraint(bool is_positive, constraint& c) {
m_active.push_back(&c);
m_trail.push_back(trail_i::set_active_i);
SASSERT(!c.is_undef());
switch (c.kind()) {
case ckind_t::eq_t:
assert_eq(is_positive, c.to_eq());

15
src/math/polysat/log_helper.h
View file

@ -40,21 +40,6 @@ show_deref_t<T> show_deref(T* ptr) {
return show_deref_t<T>{ptr};
}
// template <typename T>
// show_deref_t<T> show_deref(ref<T> const& ptr) {
// return show_deref_t<T>{ptr.get()};
// }
// template <typename T>
// show_deref_t<T> show_deref(scoped_ptr<T> const& ptr) {
// return show_deref_t<T>{ptr.get()};
// }
// template <typename Ptr, typename T = decltype(&*std::declval<Ptr>())>
// show_deref_t<T> show_deref(Ptr const& ptr) {
// return show_deref_t<T>{&*ptr};
// }
template <typename Ptr, typename T = typename std::remove_pointer<decltype(std::declval<Ptr>().get())>::type>
show_deref_t<T> show_deref(Ptr const& ptr) {
return show_deref_t<T>{ptr.get()};

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

@ -26,7 +26,6 @@ Author:
namespace polysat {
dd::pdd_manager& solver::sz2pdd(unsigned sz) {
m_pdd.reserve(sz + 1);
if (!m_pdd[sz])
@ -83,8 +82,8 @@ namespace polysat {
m_value.push_back(rational::zero());
m_justification.push_back(justification::unassigned());
m_viable.push(sz);
m_cjust.push_back(constraints());
m_watch.push_back(ptr_vector<constraint>());
m_cjust.push_back({});
m_watch.push_back({});
m_activity.push_back(0);
m_vars.push_back(sz2pdd(sz).mk_var(v));
m_size.push_back(sz);
@ -112,51 +111,52 @@ namespace polysat {
m_free_vars.del_var_eh(v);
}
constraint_literal solver::mk_eq(pdd const& p) {
constraint_literal_ref solver::mk_eq(pdd const& p) {
return m_constraints.eq(m_level, p);
}
constraint_literal solver::mk_diseq(pdd const& p) {
constraint_literal_ref solver::mk_diseq(pdd const& p) {
return ~m_constraints.eq(m_level, p);
}
constraint_literal solver::mk_ule(pdd const& p, pdd const& q) {
constraint_literal_ref solver::mk_ule(pdd const& p, pdd const& q) {
return m_constraints.ule(m_level, p, q);
}
constraint_literal solver::mk_ult(pdd const& p, pdd const& q) {
constraint_literal_ref solver::mk_ult(pdd const& p, pdd const& q) {
return m_constraints.ult(m_level, p, q);
}
constraint_literal solver::mk_sle(pdd const& p, pdd const& q) {
constraint_literal_ref solver::mk_sle(pdd const& p, pdd const& q) {
return m_constraints.sle(m_level, p, q);
}
constraint_literal solver::mk_slt(pdd const& p, pdd const& q) {
constraint_literal_ref solver::mk_slt(pdd const& p, pdd const& q) {
return m_constraints.slt(m_level, p, q);
}
void solver::new_constraint(constraint_literal cl, unsigned dep, bool activate) {
void solver::new_constraint(constraint_literal_ref cl, unsigned dep, bool activate) {
VERIFY(at_base_level());
SASSERT(cl);
SASSERT(activate || dep != null_dependency); // if we don't activate the constraint, we need the dependency to access it again later.
sat::literal lit = cl.literal();
constraint* c = cl.get();
constraint_literal c = cl.get();
clause* unit = m_constraints.store(clause::from_unit(std::move(cl), mk_dep_ref(dep)));
c->set_unit_clause(unit);
if (dep != null_dependency)
m_constraints.register_external(c);
LOG("New constraint: " << *c);
m_constraints.register_external(c.get_constraint());
LOG("New constraint: " << c);
m_original.push_back(c);
#if ENABLE_LINEAR_SOLVER
m_linear_solver.new_constraint(*c);
m_linear_solver.new_constraint(*c.constraint());
#endif
if (activate && !is_conflict())
activate_constraint_base(c, !lit.sign());
activate_constraint_base(c);
}
void solver::assign_eh(unsigned dep, bool is_true) {
VERIFY(at_base_level());
NOT_IMPLEMENTED_YET();
/*
constraint* c = m_constraints.lookup_external(dep);
if (!c) {
LOG("WARN: there is no constraint for dependency " << dep);
@ -164,7 +164,10 @@ namespace polysat {
}
if (is_conflict())
return;
activate_constraint_base(c, is_true);
// TODO: this is wrong. (e.g., if the external constraint was negative) we need to store constraint_literals
constraint_literal cl{c, is_true};
activate_constraint_base(cl);
*/
}
@ -199,10 +202,9 @@ namespace polysat {
void solver::propagate(sat::literal lit) {
LOG_H2("Propagate boolean literal " << lit);
constraint* c = m_constraints.lookup(lit.var());
constraint_literal c = m_constraints.lookup(lit);
(void)c;
SASSERT(c);
SASSERT(!c->is_undef());
// c->narrow(*this);
}
@ -211,14 +213,14 @@ namespace polysat {
auto& wlist = m_watch[v];
unsigned i = 0, j = 0, sz = wlist.size();
for (; i < sz && !is_conflict(); ++i)
if (!wlist[i]->propagate(*this, v))
if (!wlist[i].propagate(*this, v))
wlist[j++] = wlist[i];
for (; i < sz; ++i)
wlist[j++] = wlist[i];
wlist.shrink(j);
}
void solver::propagate(pvar v, rational const& val, constraint& c) {
void solver::propagate(pvar v, rational const& val, constraint_literal c) {
LOG("Propagation: " << assignment_pp(*this, v, val) << ", due to " << c);
if (m_viable.is_viable(v, val)) {
m_free_vars.del_var_eh(v);
@ -274,8 +276,8 @@ namespace polysat {
case trail_instr_t::assign_bool_i: {
sat::literal lit = m_search.back().lit();
LOG_V("Undo assign_bool_i: " << lit);
constraint* c = m_constraints.lookup(lit.var());
deactivate_constraint(*c);
constraint_literal c = m_constraints.lookup(lit);
deactivate_constraint(c);
m_bvars.unassign(lit);
m_search.pop();
break;
@ -298,42 +300,44 @@ namespace polysat {
SASSERT(m_level == target_level);
}
void solver::pop_constraints(ptr_vector<constraint>& cs) {
void solver::pop_constraints(constraint_literals& cs) {
VERIFY(invariant(cs));
while (!cs.empty() && cs.back()->level() > m_level) {
deactivate_constraint(*cs.back());
deactivate_constraint(cs.back());
cs.pop_back();
}
}
void solver::add_watch(constraint& c) {
auto const& vars = c.vars();
void solver::add_watch(constraint_literal c) {
SASSERT(c);
auto const& vars = c.get_constraint()->vars();
if (vars.size() > 0)
add_watch(c, vars[0]);
if (vars.size() > 1)
add_watch(c, vars[1]);
}
void solver::add_watch(constraint &c, pvar v) {
void solver::add_watch(constraint_literal c, pvar v) {
SASSERT(c);
LOG("Watching v" << v << " in constraint " << c);
m_watch[v].push_back(&c);
m_watch[v].push_back(c);
}
void solver::erase_watch(constraint& c) {
auto const& vars = c.vars();
void solver::erase_watch(constraint_literal c) {
auto const& vars = c.get_constraint()->vars();
if (vars.size() > 0)
erase_watch(vars[0], c);
if (vars.size() > 1)
erase_watch(vars[1], c);
}
void solver::erase_watch(pvar v, constraint& c) {
void solver::erase_watch(pvar v, constraint_literal c) {
if (v == null_var)
return;
auto& wlist = m_watch[v];
unsigned sz = wlist.size();
for (unsigned i = 0; i < sz; ++i) {
if (&c == wlist[i]) {
if (c == wlist[i]) {
wlist[i] = wlist.back();
wlist.pop_back();
return;
@ -388,49 +392,27 @@ namespace polysat {
#endif
}
void solver::set_conflict(constraint& c) {
LOG("Conflict: " << c);
LOG("\n" << *this);
SASSERT(!is_conflict());
m_conflict.push_back(&c);
}
void solver::set_conflict(clause& cl) {
LOG("Conflict: " << cl);
SASSERT(!is_conflict());
m_conflict.push_back(&cl);
void solver::set_conflict(constraint_literal c) {
m_conflict.set(c);
}
void solver::set_conflict(pvar v) {
SASSERT(!is_conflict());
m_conflict.append(m_cjust[v]);
if (m_cjust[v].empty())
m_conflict.push_back(nullptr);
LOG("Conflict for v" << v << ": " << m_conflict);
m_conflict.set(v, m_cjust[v]);
}
void solver::set_marks(conflict_core const& cc) {
for (auto c : cc.constraints())
if (c)
set_marks(*c);
}
void solver::set_marks(constraint const& c) {
LOG_V("Marking in: " << c);
if (c.bvar() != sat::null_bool_var)
m_bvars.set_mark(c.bvar());
for (auto v : c.vars())
set_mark(v);
}
void solver::set_marks(clause const& cl) {
LOG_V("Marking in: " << cl);
for (auto lit : cl)
set_marks(*m_constraints.lookup(lit.var()));
}
void solver::set_marks(constraints_and_clauses const& cc) {
for (auto c : cc.units())
if (c)
set_marks(*c);
for (auto cl : cc.clauses())
set_marks(*cl);
}
/**
* Conflict resolution.
* - m_conflict are constraints that are infeasible in the current assignment.
@ -456,6 +438,9 @@ namespace polysat {
SASSERT(is_conflict());
NOT_IMPLEMENTED_YET(); // TODO: needs to be refactored to use conflict_core, will be moved to conflict_explainer
/*
if (m_conflict.units().size() == 1 && !m_conflict.units()[0]) {
report_unsat();
return;
@ -595,9 +580,12 @@ namespace polysat {
}
}
report_unsat();
*/
}
clause_ref solver::resolve_bool(sat::literal lit) {
NOT_IMPLEMENTED_YET(); return nullptr;
/*
if (m_conflict.size() != 1)
return nullptr;
if (m_conflict.clauses().size() != 1)
@ -623,9 +611,12 @@ namespace polysat {
}
return lemma; // currently modified in-place
*/
}
void solver::backtrack(unsigned i, clause_ref lemma) {
NOT_IMPLEMENTED_YET();
/*
do {
auto const& item = m_search[i];
if (item.is_assignment()) {
@ -676,6 +667,7 @@ namespace polysat {
while (i-- > 0);
add_lemma(lemma); // TODO: this lemma is stored but otherwise "lost" because it will not be activated / not added to any watch data structures
report_unsat();
*/
}
void solver::report_unsat() {
@ -684,6 +676,8 @@ namespace polysat {
}
void solver::unsat_core(unsigned_vector& deps) {
NOT_IMPLEMENTED_YET(); // TODO: needs to be fixed to work with conflict_core
/*
deps.reset();
p_dependency_ref conflict_dep(m_dm);
for (auto& c : m_conflict.units())
@ -692,6 +686,7 @@ namespace polysat {
for (auto& c : m_conflict.clauses())
conflict_dep = m_dm.mk_join(c->dep(), conflict_dep);
m_dm.linearize(conflict_dep, deps);
*/
}
void solver::learn_lemma(pvar v, clause_ref lemma) {
@ -704,15 +699,15 @@ namespace polysat {
add_lemma(std::move(lemma));
if (cl->size() == 1) {
sat::literal lit = cl->literals()[0];
constraint* c = m_constraints.lookup(lit.var());
constraint_literal c = m_constraints.lookup(lit);
c->set_unit_clause(cl);
push_cjust(v, c);
activate_constraint_base(c, !lit.sign());
activate_constraint_base(c);
}
else {
sat::literal lit = decide_bool(*cl);
SASSERT(lit != sat::null_literal);
constraint* c = m_constraints.lookup(lit.var());
constraint_literal c = m_constraints.lookup(lit);
push_cjust(v, c);
}
}
@ -729,10 +724,9 @@ namespace polysat {
if (m_bvars.value(lit) == l_false) // already assigned => cannot decide on this (comes from either lemma LHS or previously decided literals that are now changed to propagation)
return false;
SASSERT(m_bvars.value(lit) != l_true); // cannot happen in a valid lemma
constraint* c = m_constraints.lookup(lit.var());
tmp_assign _t(c, lit);
SASSERT(!c->is_currently_true(*this)); // should not happen in a valid lemma
return !c->is_currently_false(*this);
constraint_literal c = m_constraints.lookup(lit);
SASSERT(!c.is_currently_true(*this)); // should not happen in a valid lemma
return !c.is_currently_false(*this);
};
sat::literal choice = sat::null_literal;
@ -747,11 +741,12 @@ namespace polysat {
}
LOG_V("num_choices: " << num_choices);
if (num_choices == 0)
if (num_choices == 0) {
// This case may happen when all undefined literals are false under the current variable assignment.
// TODO: The question is whether such lemmas should be generated? Check test_monot() for such a case.
set_conflict(lemma);
else if (num_choices == 1)
// set_conflict(lemma);
NOT_IMPLEMENTED_YET();
} else if (num_choices == 1)
propagate_bool(choice, &lemma);
else
decide_bool(choice, lemma);
@ -772,6 +767,8 @@ namespace polysat {
void solver::revert_decision(pvar v, clause_ref reason) {
rational val = m_value[v];
LOG_H3("Reverting decision: pvar " << v << " := " << val);
NOT_IMPLEMENTED_YET();
/*
SASSERT(m_justification[v].is_decision());
backjump(m_justification[v].level()-1);
@ -816,6 +813,7 @@ namespace polysat {
m_free_vars.del_var_eh(v);
decide(v);
}
*/
}
void solver::revert_bool_decision(sat::literal lit, clause_ref reason) {
@ -823,6 +821,9 @@ namespace polysat {
LOG_H3("Reverting boolean decision: " << lit);
SASSERT(m_bvars.is_decision(var));
NOT_IMPLEMENTED_YET();
/*
if (reason) {
LOG("Reason: " << show_deref(reason));
bool contains_var = std::any_of(reason->begin(), reason->end(), [var](sat::literal reason_lit) { return reason_lit.var() == var; });
@ -890,6 +891,7 @@ namespace polysat {
}
decide_bool(*lemma);
*/
}
void solver::decide_bool(sat::literal lit, clause& lemma) {
@ -903,9 +905,9 @@ namespace polysat {
SASSERT(reason);
if (reason->literals().size() == 1) {
SASSERT(reason->literals()[0] == lit);
constraint* c = m_constraints.lookup(lit.var());
constraint_literal c = m_constraints.lookup(lit);
// m_redundant.push_back(c);
activate_constraint_base(c, !lit.sign());
activate_constraint_base(c);
}
else
assign_bool_backtrackable(lit, reason, nullptr);
@ -919,22 +921,19 @@ namespace polysat {
m_trail.push_back(trail_instr_t::assign_bool_i);
m_search.push_boolean(lit);
constraint* c = m_constraints.lookup(lit.var());
SASSERT(c);
bool is_true = !lit.sign();
activate_constraint(*c, is_true);
constraint_literal c = m_constraints.lookup(lit);
activate_constraint(c);
}
/// Activate a constraint at the base level.
/// Used for external unit constraints and unit consequences.
void solver::activate_constraint_base(constraint* c, bool is_true) {
void solver::activate_constraint_base(constraint_literal c) {
SASSERT(c);
LOG("\n" << *this);
// c must be in m_original or m_redundant so it can be deactivated properly when popping the base level
SASSERT_EQ(std::count(m_original.begin(), m_original.end(), c) + std::count(m_redundant.begin(), m_redundant.end(), c), 1);
sat::literal lit(c->bvar(), !is_true);
assign_bool_core(lit, nullptr, nullptr);
activate_constraint(*c, is_true);
assign_bool_core(c.literal(), nullptr, nullptr);
activate_constraint(c);
}
/// Assign a boolean literal
@ -949,22 +948,21 @@ namespace polysat {
* constraints activated within the linear solver are de-activated when the linear
* solver is popped.
*/
void solver::activate_constraint(constraint& c, bool is_true) {
LOG("Activating constraint: " << c << " ; is_true = " << is_true);
SASSERT(m_bvars.value(c.bvar()) == to_lbool(is_true));
c.assign(is_true);
void solver::activate_constraint(constraint_literal c) {
SASSERT(c);
LOG("Activating constraint: " << c);
SASSERT(m_bvars.value(c.literal()) == l_true);
add_watch(c);
c.narrow(*this);
#if ENABLE_LINEAR_SOLVER
m_linear_solver.activate_constraint(c.is_positive(), c);
m_linear_solver.activate_constraint(c.is_positive(), c.constraint()); // TODO: linear solver should probably take a constraint_literal
#endif
}
/// Deactivate constraint
void solver::deactivate_constraint(constraint& c) {
void solver::deactivate_constraint(constraint_literal c) {
LOG("Deactivating constraint: " << c);
erase_watch(c);
c.unassign();
}
void solver::backjump(unsigned new_level) {
@ -973,23 +971,6 @@ namespace polysat {
if (num_levels > 0)
pop_levels(num_levels);
}
/**
* Return residue of superposing p and q with respect to v.
*/
clause_ref solver::resolve(pvar v) {
LOG_H3("Resolve v" << v);
SASSERT(!m_cjust[v].empty());
SASSERT(m_justification[v].is_propagation());
LOG("Conflict: " << m_conflict);
LOG("cjust[v" << v << "]: " << m_cjust[v]);
conflict_explainer cx(*this, m_conflict);
clause_ref res = cx.resolve(v, m_cjust[v]);
LOG("resolved: " << show_deref(res));
// SASSERT(false && "pause on explanation");
return res;
}
/**
* placeholder for factoring/gcd common factors
@ -1007,18 +988,18 @@ namespace polysat {
clause* cl = m_constraints.store(std::move(lemma));
m_redundant_clauses.push_back(cl);
if (cl->size() == 1) {
constraint* c = m_constraints.lookup(cl->literals()[0].var());
constraint_literal c = m_constraints.lookup(cl->literals()[0]);
insert_constraint(m_redundant, c);
}
}
void solver::insert_constraint(ptr_vector<constraint>& cs, constraint* c) {
void solver::insert_constraint(constraint_literals& cs, constraint_literal c) {
SASSERT(c);
LOG_V("INSERTING: " << *c);
LOG_V("INSERTING: " << c);
cs.push_back(c);
for (unsigned i = cs.size() - 1; i-- > 0; ) {
auto* c1 = cs[i + 1];
auto* c2 = cs[i];
auto c1 = cs[i + 1];
auto c2 = cs[i];
if (c1->level() >= c2->level())
break;
std::swap(cs[i], cs[i+1]);
@ -1088,11 +1069,11 @@ namespace polysat {
}
out << "Boolean assignment:\n\t" << m_bvars << "\n";
out << "Original:\n";
for (auto* c : m_original)
out << "\t" << *c << "\n";
for (auto c : m_original)
out << "\t" << c << "\n";
out << "Redundant:\n";
for (auto* c : m_redundant)
out << "\t" << *c << "\n";
for (auto c : m_redundant)
out << "\t" << c << "\n";
out << "Redundant clauses:\n";
for (auto* cl : m_redundant_clauses) {
out << "\t" << *cl << "\n";
@ -1136,7 +1117,7 @@ namespace polysat {
/**
* constraints are sorted by levels so they can be removed when levels are popped.
*/
bool solver::invariant(ptr_vector<constraint> const& cs) {
bool solver::invariant(constraint_literals const& cs) {
unsigned sz = cs.size();
for (unsigned i = 0; i + 1 < sz; ++i)
VERIFY(cs[i]->level() <= cs[i + 1]->level());
@ -1147,12 +1128,10 @@ namespace polysat {
* Check that two variables of each constraint are watched.
*/
bool solver::wlist_invariant() {
constraints cs;
constraint_literals cs;
cs.append(m_original.size(), m_original.data());
cs.append(m_redundant.size(), m_redundant.data());
for (auto* c : cs) {
if (c->is_undef())
continue;
for (auto c : cs) {
int64_t num_watches = 0;
for (auto const& wlist : m_watch) {
auto n = std::count(wlist.begin(), wlist.end(), c);
@ -1172,12 +1151,13 @@ namespace polysat {
bool solver::verify_sat() {
LOG_H1("Checking current model...");
LOG("Assignment: " << assignments_pp(*this));
for (auto* c : m_original) {
bool ok = c->is_currently_true(*this);
LOG((ok ? "PASS" : "FAIL") << ": " << show_deref(c));
if (!ok) return false;
bool all_ok = true;
for (auto c : m_original) {
bool ok = c.is_currently_true(*this);
LOG((ok ? "PASS" : "FAIL") << ": " << c);
all_ok = all_ok && ok;
}
LOG("All good!");
if (all_ok) LOG("All good!");
return true;
}
}

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

@ -21,9 +21,11 @@ Author:
#include "util/statistics.h"
#include "util/params.h"
#include "math/polysat/boolean.h"
#include "math/polysat/conflict_core.h"
#include "math/polysat/constraint.h"
#include "math/polysat/clause_builder.h"
#include "math/polysat/eq_constraint.h"
#include "math/polysat/explain.h"
#include "math/polysat/ule_constraint.h"
#include "math/polysat/justification.h"
#include "math/polysat/linear_solver.h"
@ -59,6 +61,7 @@ namespace polysat {
friend class assignments_pp;
typedef ptr_vector<constraint> constraints;
typedef vector<constraint_literal> constraint_literals;
reslimit& m_lim;
params_ref m_params;
@ -68,7 +71,7 @@ namespace polysat {
small_object_allocator m_alloc;
poly_dep_manager m_dm;
linear_solver m_linear_solver;
constraints_and_clauses m_conflict;
conflict_core m_conflict;
// constraints m_stash_just;
var_queue m_free_vars;
stats m_stats;
@ -81,8 +84,8 @@ namespace polysat {
// Per constraint state
constraint_manager m_constraints;
ptr_vector<constraint> m_original;
ptr_vector<constraint> m_redundant;
constraint_literals m_original;
constraint_literals m_redundant;
ptr_vector<clause> m_redundant_clauses;
svector<sat::bool_var> m_disjunctive_lemma;
@ -90,8 +93,8 @@ namespace polysat {
// Per variable information
vector<rational> m_value; // assigned value
vector<justification> m_justification; // justification for variable assignment
vector<constraints> m_cjust; // constraints justifying variable range.
vector<constraints> m_watch; // watch list datastructure into constraints.
vector<constraint_literals> m_cjust; // constraints justifying variable range.
vector<constraint_literals> m_watch; // watch list datastructure into constraints.
unsigned_vector m_activity;
vector<pdd> m_vars;
unsigned_vector m_size; // store size of variables.
@ -125,12 +128,12 @@ namespace polysat {
m_qhead_trail.pop_back();
}
void push_cjust(pvar v, constraint* c) {
void push_cjust(pvar v, constraint_literal c) {
if (m_cjust[v].contains(c)) // TODO: better check (flag on constraint?)
return;
LOG_V("cjust[v" << v << "] += " << show_deref(c));
LOG_V("cjust[v" << v << "] += " << c);
SASSERT(c);
m_cjust[v].push_back(c);
m_cjust[v].push_back(c);
m_trail.push_back(trail_instr_t::just_i);
m_cjust_trail.push_back(v);
}
@ -148,14 +151,14 @@ namespace polysat {
void push_level();
void pop_levels(unsigned num_levels);
void pop_constraints(ptr_vector<constraint>& cs);
void pop_constraints(constraint_literals& cs);
void assign_bool_backtrackable(sat::literal lit, clause* reason, clause* lemma);
void activate_constraint_base(constraint* c, bool is_true);
void activate_constraint_base(constraint_literal c);
void assign_bool_core(sat::literal lit, clause* reason, clause* lemma);
// void assign_bool_base(sat::literal lit);
void activate_constraint(constraint& c, bool is_true);
void deactivate_constraint(constraint& c);
void activate_constraint(constraint_literal c);
void deactivate_constraint(constraint_literal c);
sat::literal decide_bool(clause& lemma);
void decide_bool(sat::literal lit, clause& lemma);
void propagate_bool(sat::literal lit, clause* reason);
@ -168,14 +171,13 @@ namespace polysat {
void propagate(sat::literal lit);
void propagate(pvar v);
void propagate(pvar v, rational const& val, constraint& c);
void erase_watch(pvar v, constraint& c);
void erase_watch(constraint& c);
void add_watch(constraint& c);
void add_watch(constraint& c, pvar v);
void propagate(pvar v, rational const& val, constraint_literal c);
void erase_watch(pvar v, constraint_literal c);
void erase_watch(constraint_literal c);
void add_watch(constraint_literal c);
void add_watch(constraint_literal c, pvar v);
void set_conflict(constraint& c);
void set_conflict(clause& cl);
void set_conflict(constraint_literal c);
void set_conflict(pvar v);
unsigned_vector m_marks;
@ -184,13 +186,11 @@ namespace polysat {
bool is_marked(pvar v) const { return m_clock == m_marks[v]; }
void set_mark(pvar v) { LOG_V("Marking: v" << v); m_marks[v] = m_clock; }
void set_marks(constraints_and_clauses const& cc);
void set_marks(conflict_core const& cc);
void set_marks(constraint const& c);
void set_marks(clause const& cl);
unsigned m_conflict_level { 0 };
clause_ref resolve(pvar v);
clause_ref resolve_bool(sat::literal lit);
bool can_decide() const { return !m_free_vars.empty(); }
@ -219,17 +219,17 @@ namespace polysat {
void backjump(unsigned new_level);
void add_lemma(clause_ref lemma);
constraint_literal mk_eq(pdd const& p);
constraint_literal mk_diseq(pdd const& p);
constraint_literal mk_ule(pdd const& p, pdd const& q);
constraint_literal mk_ult(pdd const& p, pdd const& q);
constraint_literal mk_sle(pdd const& p, pdd const& q);
constraint_literal mk_slt(pdd const& p, pdd const& q);
void new_constraint(constraint_literal c, unsigned dep, bool activate);
static void insert_constraint(ptr_vector<constraint>& cs, constraint* c);
constraint_literal_ref mk_eq(pdd const& p);
constraint_literal_ref mk_diseq(pdd const& p);
constraint_literal_ref mk_ule(pdd const& p, pdd const& q);
constraint_literal_ref mk_ult(pdd const& p, pdd const& q);
constraint_literal_ref mk_sle(pdd const& p, pdd const& q);
constraint_literal_ref mk_slt(pdd const& p, pdd const& q);
void new_constraint(constraint_literal_ref c, unsigned dep, bool activate);
static void insert_constraint(constraint_literals& cs, constraint_literal c);
bool invariant();
static bool invariant(ptr_vector<constraint> const& cs);
static bool invariant(constraint_literals const& cs);
bool wlist_invariant();
bool verify_sat();

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

@ -18,12 +18,16 @@ Author:
namespace polysat {
std::ostream& ule_constraint::display(std::ostream& out) const {
out << m_lhs << " <= " << m_rhs;
return display_extra(out);
std::ostream& ule_constraint::display(std::ostream& out, lbool status) const {
out << m_lhs;
if (status == l_true) out << " <= ";
else if (status == l_false) out << " > ";
else out << " <=/> ";
out << m_rhs;
return display_extra(out, status);
}
void ule_constraint::narrow(solver& s) {
void ule_constraint::narrow(solver& s, bool is_positive) {
LOG_H3("Narrowing " << *this);
LOG("Assignment: " << assignments_pp(s));
auto p = lhs().subst_val(s.assignment());
@ -31,15 +35,13 @@ namespace polysat {
auto q = rhs().subst_val(s.assignment());
LOG("Substituted RHS: " << rhs() << " := " << q);
SASSERT(!is_undef());
if (is_always_false(p, q)) {
s.set_conflict(*this);
if (is_always_false(is_positive, p, q)) {
s.set_conflict({this, is_positive});
return;
}
if (p.is_val() && q.is_val()) {
SASSERT(!is_positive() || p.val() <= q.val());
SASSERT(!is_negative() || p.val() > q.val());
SASSERT(!is_positive || p.val() <= q.val());
SASSERT(is_positive || p.val() > q.val());
return;
}
@ -70,13 +72,13 @@ namespace polysat {
d = q.lo().val();
}
if (v != null_var) {
s.push_cjust(v, this);
s.push_cjust(v, {this, is_positive});
s.m_viable.intersect_ule(v, a, b, c, d, is_positive());
s.m_viable.intersect_ule(v, a, b, c, d, is_positive);
rational val;
if (s.m_viable.find_viable(v, val) == dd::find_t::singleton)
s.propagate(v, val, *this);
s.propagate(v, val, {this, is_positive});
return;
}
@ -84,39 +86,35 @@ namespace polysat {
// TODO: other cheap constraints possible?
}
bool ule_constraint::is_always_false(pdd const& lhs, pdd const& rhs) {
bool ule_constraint::is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) {
// TODO: other conditions (e.g. when forbidden interval would be full)
VERIFY(!is_undef());
if (is_positive())
if (is_positive)
return lhs.is_val() && rhs.is_val() && lhs.val() > rhs.val();
else
return (lhs.is_val() && rhs.is_val() && lhs.val() <= rhs.val()) || (lhs == rhs);
}
bool ule_constraint::is_always_false() {
return is_always_false(lhs(), rhs());
bool ule_constraint::is_always_false(bool is_positive) {
return is_always_false(is_positive, lhs(), rhs());
}
bool ule_constraint::is_currently_false(solver& s) {
bool ule_constraint::is_currently_false(solver& s, bool is_positive) {
auto p = lhs().subst_val(s.assignment());
auto q = rhs().subst_val(s.assignment());
return is_always_false(p, q);
return is_always_false(is_positive, p, q);
}
bool ule_constraint::is_currently_true(solver& s) {
bool ule_constraint::is_currently_true(solver& s, bool is_positive) {
auto p = lhs().subst_val(s.assignment());
auto q = rhs().subst_val(s.assignment());
VERIFY(!is_undef());
if (is_positive())
if (is_positive)
return p.is_val() && q.is_val() && p.val() <= q.val();
else
return p.is_val() && q.is_val() && p.val() > q.val();
}
bool ule_constraint::forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond)
bool ule_constraint::forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, constraint_literal_ref& out_neg_cond)
{
SASSERT(!is_undef());
// Current only works when degree(v) is at most one on both sides
unsigned const deg1 = lhs().degree(v);
unsigned const deg2 = rhs().degree(v);
@ -249,7 +247,7 @@ namespace polysat {
out_neg_cond = s.m_constraints.eq(level(), condition_body);
if (is_trivial) {
if (is_positive())
if (is_positive)
// TODO: we cannot use empty intervals for interpolation. So we
// can remove the empty case (make it represent 'full' instead),
// and return 'false' here. Then we do not need the proper/full
@ -276,7 +274,7 @@ namespace polysat {
else
SASSERT(y_coeff.is_one());
if (is_negative()) {
if (!is_positive) {
swap(lo, hi);
lo_val.swap(hi_val);
}
@ -286,9 +284,8 @@ namespace polysat {
return true;
}
inequality ule_constraint::as_inequality() const {
SASSERT(!is_undef());
if (is_positive())
inequality ule_constraint::as_inequality(bool is_positive) const {
if (is_positive)
return inequality(lhs(), rhs(), false, this);
else
return inequality(rhs(), lhs(), true, this);

16
src/math/polysat/ule_constraint.h
View file

@ -31,14 +31,14 @@ namespace polysat {
~ule_constraint() override {}
pdd const& lhs() const { return m_lhs; }
pdd const& rhs() const { return m_rhs; }
std::ostream& display(std::ostream& out) const override;
bool is_always_false(pdd const& lhs, pdd const& rhs);
bool is_always_false() override;
bool is_currently_false(solver& s) override;
bool is_currently_true(solver& s) override;
void narrow(solver& s) override;
bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond) override;
inequality as_inequality() const override;
std::ostream& display(std::ostream& out, lbool status) const override;
bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs);
bool is_always_false(bool is_positive) override;
bool is_currently_false(solver& s, bool is_positive) override;
bool is_currently_true(solver& s, bool is_positive) override;
void narrow(solver& s, bool is_positive) override;
bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, constraint_literal_ref& out_neg_cond) override;
inequality as_inequality(bool is_positive) const override;
unsigned hash() const override;
bool operator==(constraint const& other) const override;
};

5
src/test/fixplex.cpp
View file

@ -11,11 +11,12 @@ namespace polysat {
typedef uint64_ext::numeral numeral;
struct solver_scope {
struct fp_scope {
params_ref p;
reslimit lim;
};
struct scoped_fp : public solver_scope, public fixplex<uint64_ext> {
struct scoped_fp : public fp_scope, public fixplex<uint64_ext> {
scoped_fp(): fixplex<uint64_ext>(p, lim) {}