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

Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-30 01:05:42 -04:00
commit 1defbc8aa4
16 changed files with 435 additions and 325 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/CMakeLists.txt
View file

@ -1,6 +1,7 @@
z3_add_component(polysat
SOURCES
boolean.cpp
clause_builder.cpp
constraint.cpp
eq_constraint.cpp
explain.cpp

68
src/math/polysat/clause_builder.cpp Normal file
View file

@ -0,0 +1,68 @@
/*++
Copyright (c) 2021 Microsoft Corporation
Module Name:
polysat clause builder
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
--*/
#include "math/polysat/clause_builder.h"
#include "math/polysat/solver.h"
#include "math/polysat/log.h"
namespace polysat {
clause_builder::clause_builder(solver& s):
m_solver(s), m_dep(nullptr, s.m_dm)
{}
void clause_builder::reset() {
m_literals.reset();
m_new_constraints.reset();
m_level = 0;
m_dep = nullptr;
SASSERT(empty());
}
clause_ref clause_builder::build() {
// TODO: here we could set all the levels of the new constraints. so we do not have to compute the max at every use site.
clause_ref cl = clause::from_literals(m_level, std::move(m_dep), std::move(m_literals), std::move(m_new_constraints));
m_level = 0;
SASSERT(empty());
return cl;
}
void clause_builder::add_dependency(p_dependency* d) {
m_dep = m_solver.m_dm.mk_join(m_dep, d);
}
void clause_builder::push_literal(sat::literal lit) {
constraint* c = m_solver.m_constraints.lookup(lit.var());
SASSERT(c);
if (c->unit_clause()) {
add_dependency(c->unit_clause()->dep());
return;
}
m_level = std::max(m_level, c->level());
m_literals.push_back(lit);
}
void clause_builder::push_new_constraint(constraint_literal 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())
return;
m_level = std::max(m_level, c->level());
m_literals.push_back(c.literal());
m_new_constraints.push_back(c.detach());
}
}

49
src/math/polysat/clause_builder.h Normal file
View file

@ -0,0 +1,49 @@
/*++
Copyright (c) 2021 Microsoft Corporation
Module Name:
polysat clause builder
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
--*/
#pragma once
#include "math/polysat/constraint.h"
#include "math/polysat/types.h"
namespace polysat {
/// Builds a clause from literals and constraints.
/// Takes care to
/// - resolve with unit clauses and accumulate their dependencies,
/// - skip trivial new constraints such as "4 <= 1".
class clause_builder {
solver& m_solver;
sat::literal_vector m_literals;
constraint_ref_vector m_new_constraints;
p_dependency_ref m_dep;
unsigned m_level = 0;
public:
clause_builder(solver& s);
bool empty() const { return m_literals.empty() && m_new_constraints.empty() && m_dep == nullptr && m_level == 0; }
void reset();
/// Build the clause. This will reset the clause builder so it can be reused.
clause_ref build();
void add_dependency(p_dependency* d);
/// Add a literal to the clause.
/// Intended to be used for literals representing a constraint that already exists.
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);
};
}

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

@ -21,17 +21,11 @@ Author:
namespace polysat {
constraint* constraint_manager::insert(constraint_ref c) {
LOG_V("Inserting constraint: " << show_deref(c));
constraint* constraint_manager::store(constraint_ref c) {
LOG_V("Store constraint: " << show_deref(c));
SASSERT(c);
SASSERT(c->bvar() != sat::null_bool_var);
SASSERT(get_bv2c(c->bvar()) == c.get());
// TODO: use explicit insert_external(constraint* c, unsigned dep) for that.
if (c->dep() && c->dep()->is_leaf()) {
unsigned dep = c->dep()->leaf_value();
SASSERT(!m_external_constraints.contains(dep));
m_external_constraints.insert(dep, c.get());
}
while (m_constraints.size() <= c->level())
m_constraints.push_back({});
constraint* pc = c.get();
@ -39,12 +33,12 @@ namespace polysat {
return pc;
}
clause* constraint_manager::insert(clause_ref cl) {
clause* constraint_manager::store(clause_ref cl) {
LOG_V("Store clause: " << show_deref(cl));
SASSERT(cl);
// Insert new constraints
for (constraint* c : cl->m_new_constraints)
// TODO: if (!inserted) ?
insert(c);
store(c);
cl->m_new_constraints = {}; // free vector memory
// Insert clause
while (m_clauses.size() <= cl->level())
@ -54,14 +48,17 @@ namespace polysat {
return pcl;
}
void constraint_manager::register_external(constraint* c) {
SASSERT(c);
SASSERT(c->unit_dep());
SASSERT(c->unit_dep()->is_leaf());
unsigned const dep = c->unit_dep()->leaf_value();
SASSERT(!m_external_constraints.contains(dep));
m_external_constraints.insert(dep, c);
}
// Release constraints at the given level and above.
void constraint_manager::release_level(unsigned lvl) {
for (unsigned l = m_clauses.size(); l-- > lvl; ) {
for (auto const& cl : m_clauses[l]) {
SASSERT_EQ(cl->m_ref_count, 1); // otherwise there is a leftover reference somewhere
}
m_clauses[l].reset();
}
for (unsigned l = m_constraints.size(); l-- > lvl; ) {
for (auto const& c : m_constraints[l]) {
LOG_V("Removing constraint: " << show_deref(c));
@ -69,14 +66,21 @@ namespace polysat {
// NOTE: ref count could be two if the constraint was added twice (once as part of clause, and later as unit constraint)
LOG_H1("Expected ref_count 1 or 2, got " << c->m_ref_count << " for " << *c);
}
if (c->dep() && c->dep()->is_leaf()) {
unsigned dep = c->dep()->leaf_value();
auto* d = c->unit_dep();
if (d && d->is_leaf()) {
unsigned const dep = d->leaf_value();
SASSERT(m_external_constraints.contains(dep));
m_external_constraints.remove(dep);
}
}
m_constraints[l].reset();
}
for (unsigned l = m_clauses.size(); l-- > lvl; ) {
for (auto const& cl : m_clauses[l]) {
SASSERT_EQ(cl->m_ref_count, 1); // otherwise there is a leftover reference somewhere
}
m_clauses[l].reset();
}
}
constraint_manager::~constraint_manager() {
@ -105,18 +109,18 @@ namespace polysat {
return *dynamic_cast<ule_constraint const*>(this);
}
constraint_ref constraint_manager::eq(unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& d) {
return alloc(eq_constraint, *this, lvl, sign, p, d);
constraint_literal constraint_manager::eq(unsigned lvl, pdd const& p) {
return constraint_literal{alloc(eq_constraint, *this, lvl, p)};
}
constraint_ref constraint_manager::ule(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) {
return alloc(ule_constraint, *this, lvl, sign, a, b, d);
constraint_literal constraint_manager::ule(unsigned lvl, pdd const& a, pdd const& b) {
return constraint_literal{alloc(ule_constraint, *this, lvl, a, b)};
}
constraint_ref constraint_manager::ult(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) {
constraint_literal constraint_manager::ult(unsigned lvl, pdd const& a, pdd const& b) {
// a < b <=> !(b <= a)
return ule(lvl, static_cast<csign_t>(!sign), b, a, d);
return ~ule(lvl, b, a);
}
// To do signed comparison of bitvectors, flip the msb and do unsigned comparison:
@ -135,14 +139,14 @@ namespace polysat {
//
// Argument: flipping the msb swaps the negative and non-negative blocks
//
constraint_ref constraint_manager::sle(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) {
constraint_literal 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, sign, a + shift, b + shift, d);
return ule(lvl, a + shift, b + shift);
}
constraint_ref constraint_manager::slt(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) {
constraint_literal 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, sign, a + shift, b + shift, d);
return ult(lvl, a + shift, b + shift);
}
std::ostream& constraint::display_extra(std::ostream& out) const {
@ -180,19 +184,18 @@ namespace polysat {
narrow(s);
}
clause_ref clause::from_unit(constraint_ref c) {
clause_ref clause::from_unit(constraint_literal c, p_dependency_ref d) {
SASSERT(c);
unsigned const lvl = c->level();
auto const& dep = c->m_dep;
sat::literal_vector lits;
lits.push_back(sat::literal(c->bvar()));
lits.push_back(c.literal());
constraint_ref_vector cs;
cs.push_back(std::move(c));
return clause::from_literals(lvl, dep, std::move(lits), std::move(cs));
cs.push_back(c.detach());
return clause::from_literals(lvl, std::move(d), std::move(lits), std::move(cs));
}
clause_ref clause::from_literals(unsigned lvl, p_dependency_ref const& d, sat::literal_vector literals, constraint_ref_vector constraints) {
return alloc(clause, lvl, d, std::move(literals), std::move(constraints));
clause_ref clause::from_literals(unsigned lvl, p_dependency_ref d, sat::literal_vector literals, constraint_ref_vector constraints) {
return alloc(clause, lvl, std::move(d), std::move(literals), std::move(constraints));
}
bool clause::is_always_false(solver& s) const {
@ -247,35 +250,6 @@ namespace polysat {
return out;
}
void clause_builder::reset() {
m_literals.reset();
m_new_constraints.reset();
SASSERT(empty());
}
clause_ref clause_builder::build(unsigned lvl, p_dependency_ref const& d) {
clause_ref cl = clause::from_literals(lvl, d, std::move(m_literals), std::move(m_new_constraints));
SASSERT(empty());
return cl;
}
void clause_builder::push_literal(sat::literal lit) {
if (m_solver.active_at_base_level(lit))
return;
m_literals.push_back(lit);
}
void clause_builder::push_new_constraint(constraint_ref c) {
SASSERT(c);
SASSERT(c->is_undef());
sat::literal lit{c->bvar()};
tmp_assign _t(c, lit);
if (c->is_always_false())
return;
m_literals.push_back(lit);
m_new_constraints.push_back(std::move(c));
}
std::ostream& constraints_and_clauses::display(std::ostream& out) const {
bool first = true;
for (auto c : units()) {

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

@ -25,6 +25,7 @@ namespace polysat {
enum ckind_t { eq_t, ule_t };
enum csign_t : bool { neg_t = false, pos_t = true };
class constraint_literal;
class constraint;
class constraint_manager;
class clause;
@ -41,6 +42,7 @@ namespace polysat {
friend class constraint;
bool_var_manager& m_bvars;
// poly_dep_manager& m_dm;
// Association to boolean variables
ptr_vector<constraint> m_bv2constraint;
@ -59,24 +61,29 @@ namespace polysat {
public:
constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {}
// constraint_manager(bool_var_manager& bvars, poly_dep_manager& dm): m_bvars(bvars), m_dm(dm) {}
~constraint_manager();
// Start managing lifetime of the given constraint
// TODO: rename to "store", or "keep"... because the bvar->constraint mapping is already inserted at creation.
constraint* insert(constraint_ref c);
clause* insert(clause_ref cl);
constraint* store(constraint_ref c);
clause* store(clause_ref cl);
// Release constraints at the given level and above.
/// Register a unit clause with an external dependency.
void register_external(constraint* c);
/// Release constraints at the given level and above.
void release_level(unsigned lvl);
constraint* lookup(sat::bool_var var) const;
constraint* lookup_external(unsigned dep) const { return m_external_constraints.get(dep, nullptr); }
constraint_ref eq(unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& d);
constraint_ref ule(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d);
constraint_ref ult(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d);
constraint_ref sle(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d);
constraint_ref slt(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d);
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);
// p_dependency_ref null_dep() const { return {nullptr, m_dm}; }
};
@ -101,20 +108,17 @@ namespace polysat {
friend class ule_constraint;
constraint_manager* m_manager;
unsigned m_ref_count = 0;
// bool m_stored = false; ///< Whether it has been inserted into the constraint_manager to be tracked by level
unsigned m_storage_level; ///< Controls lifetime of the constraint object. Always a base level (for external dependencies the level at which it was created, and for others the maximum storage level of its external dependencies).
// unsigned m_active_level = UINT_MAX; ///< Level at which the constraint was activated. Possibly different from m_storage_level because constraints in lemmas may become activated only at a higher level. NOTE: this is actually the level of the corresponding bool_var.
ckind_t m_kind;
p_dependency_ref m_dep;
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
csign_t m_sign; ///< sign/polarity
lbool m_status = l_undef; ///< current constraint status, computed from value of m_lit and m_sign
lbool m_bvalue = l_undef; ///< TODO: remove m_sign and m_bvalue, use m_status as current value. the constraint itself is always the positive literal. use unit clauses for unit/external constraints; negation may come in through there.
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, csign_t sign, p_dependency_ref const& dep, ckind_t k):
m_manager(&m), m_storage_level(lvl), m_kind(k), m_dep(dep), m_bvar(m_manager->m_bvars.new_var()), m_sign(sign) {
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()) {
SASSERT_EQ(m_manager->get_bv2c(bvar()), nullptr);
m_manager->insert_bv2c(bvar(), this);
}
@ -146,7 +150,6 @@ namespace polysat {
eq_constraint const& to_eq() const;
ule_constraint& to_ule();
ule_constraint const& to_ule() const;
p_dependency* dep() const { return m_dep; }
unsigned_vector& vars() { return m_vars; }
unsigned_vector const& vars() const { return m_vars; }
unsigned level() const { return m_storage_level; }
@ -158,22 +161,21 @@ namespace polysat {
// return !is_undef() && active_level() <= s.base_level();
// }
sat::bool_var bvar() const { return m_bvar; }
sat::literal blit() const { SASSERT(m_bvalue != l_undef); return m_bvalue == l_true ? sat::literal(m_bvar) : ~sat::literal(m_bvar); }
bool sign() const { return m_sign; }
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_bvalue == l_undef || m_bvalue == to_lbool(is_true));
m_bvalue = to_lbool(is_true);
lbool new_status = (is_true ^ !m_sign) ? l_true : l_false;
SASSERT(is_undef() || new_status == m_status);
m_status = new_status;
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; m_bvalue = l_undef; }
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; }
// TODO: must return a 'clause_ref' instead. If we resolve with a non-base constraint, we need to keep it in the clause (or should we track those as dependencies? the level needs to be higher then.)
virtual constraint_ref resolve(solver& s, pvar v) = 0;
clause* unit_clause() const { return m_unit_clause; }
void set_unit_clause(clause* cl) { SASSERT(cl); SASSERT(!m_unit_clause); m_unit_clause = cl; }
p_dependency* unit_dep() const;
/** Precondition: all variables other than v are assigned.
*
@ -181,18 +183,50 @@ 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_ref& out_neg_cond) { return false; }
virtual bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond) { return false; }
};
inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
// Disjunction of constraints represented by boolean literals
/// Literal together with the constraint it represents.
/// (or: constraint with polarity)
class constraint_literal {
sat::literal m_literal = sat::null_literal;
constraint_ref m_constraint = nullptr;
public:
constraint_literal() {}
constraint_literal(sat::literal lit, constraint_ref c):
m_literal(lit), m_constraint(std::move(c)) {
SASSERT(get());
SASSERT(literal().var() == get()->bvar());
}
constraint_literal operator~() const&& {
return {~m_literal, std::move(m_constraint)};
}
sat::literal literal() const { return m_literal; }
constraint* get() const { return m_constraint.get(); }
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; }
polysat::constraint* operator->() const { return m_constraint.get(); }
polysat::constraint const& operator*() const { return *m_constraint; }
constraint_literal& operator=(nullptr_t) { m_literal = sat::null_literal; m_constraint = nullptr; return *this; }
private:
friend class constraint_manager;
explicit constraint_literal(polysat::constraint* c): constraint_literal(sat::literal(c->bvar()), c) {}
};
/// Disjunction of constraints represented by boolean literals
class clause {
friend class constraint_manager;
unsigned m_ref_count = 0;
unsigned m_level; // TODO: this is "storage" level, rename accordingly
// unsigned m_next_guess = UINT_MAX; // next guess for enumerative backtracking
unsigned m_level;
unsigned m_next_guess = 0; // next guess for enumerative backtracking
p_dependency_ref m_dep;
sat::literal_vector m_literals;
@ -207,8 +241,8 @@ namespace polysat {
}
*/
clause(unsigned lvl, p_dependency_ref const& d, sat::literal_vector literals, constraint_ref_vector new_constraints):
m_level(lvl), m_dep(d), m_literals(std::move(literals)), m_new_constraints(std::move(new_constraints))
clause(unsigned lvl, p_dependency_ref d, sat::literal_vector literals, constraint_ref_vector new_constraints):
m_level(lvl), m_dep(std::move(d)), m_literals(std::move(literals)), m_new_constraints(std::move(new_constraints))
{
SASSERT(std::count(m_literals.begin(), m_literals.end(), sat::null_literal) == 0);
}
@ -217,8 +251,8 @@ 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_ref c);
static clause_ref from_literals(unsigned lvl, p_dependency_ref const& d, sat::literal_vector literals, constraint_ref_vector new_constraints);
static clause_ref from_unit(constraint_literal 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'.
bool resolve(sat::bool_var var, clause const& other);
@ -249,32 +283,6 @@ namespace polysat {
inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); }
/// Builds a clause from literals and constraints.
/// Takes care to
/// - skip literals that are active at the base level,
/// - skip trivial new constraints such as "4 <= 1".
class clause_builder {
solver& m_solver;
sat::literal_vector m_literals;
constraint_ref_vector m_new_constraints;
public:
clause_builder(solver& s): m_solver(s) {}
bool empty() const { return m_literals.empty() && m_new_constraints.empty(); }
void reset();
/// Build the clause. This will reset the clause builder so it can be reused.
clause_ref build(unsigned lvl, p_dependency_ref const& d);
/// Add a literal to the clause.
/// Intended to be used for literals representing a constraint that already exists.
void push_literal(sat::literal lit);
/// Add a constraint to the clause that does not yet exist in the solver so far.
/// By convention, this will add the positive literal for this constraint.
/// (TODO: we might need to change this later; but then we will add a second argument for the literal or the sign.)
void push_new_constraint(constraint_ref c);
};
// Container for unit constraints and clauses.
class constraints_and_clauses {
@ -344,13 +352,13 @@ namespace polysat {
tmp_assign(constraint* c, sat::literal lit):
m_constraint(c) {
SASSERT(c);
SASSERT(c->bvar() == lit.var());
SASSERT_EQ(c->bvar(), lit.var());
if (c->is_undef()) {
c->assign(!lit.sign());
m_should_unassign = true;
}
else
SASSERT(c->blit() == lit);
SASSERT_EQ(c->blit(), lit);
}
tmp_assign(constraint_ref const& c, sat::literal lit): tmp_assign(c.get(), lit) {}
void revert() {
@ -368,4 +376,5 @@ namespace polysat {
tmp_assign& operator=(tmp_assign&&) = delete;
};
inline p_dependency* constraint::unit_dep() const { return m_unit_clause ? m_unit_clause->dep() : nullptr; }
}

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

@ -19,19 +19,10 @@ Author:
namespace polysat {
std::ostream& eq_constraint::display(std::ostream& out) const {
out << p() << (sign() == pos_t ? " == 0" : " != 0");
out << p() << " == 0 ";
return display_extra(out);
}
constraint_ref eq_constraint::resolve(solver& s, pvar v) {
if (is_positive())
return eq_resolve(s, v);
if (is_negative())
return diseq_resolve(s, v);
UNREACHABLE();
return nullptr;
}
void eq_constraint::narrow(solver& s) {
SASSERT(!is_undef());
LOG("Assignment: " << assignments_pp(s));
@ -110,47 +101,36 @@ namespace polysat {
* Equality constraints
*/
constraint_ref eq_constraint::eq_resolve(solver& s, pvar v) {
LOG("Resolve " << *this << " upon v" << v);
if (s.m_conflict.size() != 1)
return nullptr;
if (!s.m_conflict.clauses().empty())
return nullptr;
constraint* c = s.m_conflict.units()[0];
SASSERT(c->is_currently_false(s));
// 'c == this' can happen if propagation was from decide() with only one value left
// (e.g., if there's an unsatisfiable clause and we try all values).
// Resolution would give us '0 == 0' in this case, which is useless.
if (c == this)
return nullptr;
SASSERT(is_currently_true(s)); // TODO: might not always hold (due to similar case as in comment above?)
if (c->is_eq() && c->is_positive()) {
pdd a = c->to_eq().p();
pdd b = p();
pdd r = a;
if (!a.resolve(v, b, r))
return nullptr;
p_dependency_ref d(s.m_dm.mk_join(c->dep(), dep()), s.m_dm);
unsigned lvl = std::max(c->level(), level());
return s.m_constraints.eq(lvl, pos_t, r, d);
}
return nullptr;
}
/**
* Disequality constraints
*/
constraint_ref eq_constraint::diseq_resolve(solver& s, pvar v) {
NOT_IMPLEMENTED_YET();
return nullptr;
}
// constraint_ref eq_constraint::eq_resolve(solver& s, pvar v) {
// LOG("Resolve " << *this << " upon v" << v);
// if (s.m_conflict.size() != 1)
// return nullptr;
// if (!s.m_conflict.clauses().empty())
// return nullptr;
// constraint* c = s.m_conflict.units()[0];
// SASSERT(c->is_currently_false(s));
// // 'c == this' can happen if propagation was from decide() with only one value left
// // (e.g., if there's an unsatisfiable clause and we try all values).
// // Resolution would give us '0 == 0' in this case, which is useless.
// if (c == this)
// return nullptr;
// SASSERT(is_currently_true(s)); // TODO: might not always hold (due to similar case as in comment above?)
// if (c->is_eq() && c->is_positive()) {
// pdd a = c->to_eq().p();
// pdd b = p();
// pdd r = a;
// if (!a.resolve(v, b, r))
// return nullptr;
// p_dependency_ref d(s.m_dm.mk_join(c->dep(), dep()), s.m_dm);
// unsigned lvl = std::max(c->level(), level());
// return s.m_constraints.eq(lvl, pos_t, r, d);
// }
// return nullptr;
// }
/// 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_ref& out_neg_cond)
bool eq_constraint::forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond)
{
SASSERT(!is_undef());

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

@ -20,24 +20,19 @@ namespace polysat {
class eq_constraint : public constraint {
pdd m_poly;
public:
eq_constraint(constraint_manager& m, unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& dep):
constraint(m, lvl, sign, dep, ckind_t::eq_t), m_poly(p) {
eq_constraint(constraint_manager& m, unsigned lvl, pdd const& p):
constraint(m, lvl, ckind_t::eq_t), m_poly(p) {
m_vars.append(p.free_vars());
}
~eq_constraint() override {}
pdd const & p() const { return m_poly; }
std::ostream& display(std::ostream& out) const override;
constraint_ref resolve(solver& s, pvar v) 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_ref& out_neg_cond) override;
bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond) override;
inequality as_inequality() const override;
private:
constraint_ref eq_resolve(solver& s, pvar v);
constraint_ref diseq_resolve(solver& s, pvar v);
};
}

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

@ -32,6 +32,15 @@ namespace polysat {
for (auto* c : m_conflict.clauses())
LOG("Clause: " << show_deref(c));
// TODO: this is a temporary workaround! we should not get any undef constraints at this point
constraints_and_clauses confl = std::move(m_conflict);
SASSERT(m_conflict.empty());
for (auto* c : confl.units())
if (!c->is_undef())
m_conflict.push_back(c);
for (auto* c : confl.clauses())
m_conflict.push_back(c);
// TODO: we should share work done for examining constraints between different resolution methods
clause_ref lemma;
if (!lemma) lemma = by_polynomial_superposition();
@ -40,15 +49,32 @@ namespace polysat {
if (!lemma) lemma = by_ugt_z();
if (!lemma) lemma = y_ule_ax_and_x_ule_z();
if (lemma) {
LOG("New lemma: " << *lemma);
for (auto* c : lemma->new_constraints()) {
LOG("New constraint: " << show_deref(c));
DEBUG_CODE({
if (lemma) {
LOG("New lemma: " << *lemma);
for (auto* c : lemma->new_constraints()) {
LOG("New constraint: " << show_deref(c));
}
// All constraints in the lemma must be false in the conflict state
for (auto lit : lemma->literals()) {
if (m_solver.m_bvars.value(lit.var()) == l_false)
continue;
SASSERT(m_solver.m_bvars.value(lit.var()) != l_true);
constraint* c = m_solver.m_constraints.lookup(lit.var());
SASSERT(c);
tmp_assign _t(c, lit);
// if (c->is_currently_true(m_solver)) {
// LOG("ERROR: constraint is true: " << show_deref(c));
// SASSERT(false);
// }
// SASSERT(!c->is_currently_true(m_solver));
// SASSERT(c->is_currently_false(m_solver)); // TODO: pvar v may not have a value at this point...
}
}
}
else {
LOG("No lemma");
}
else {
LOG("No lemma");
}
});
m_var = null_var;
m_cjust_v.reset();
@ -70,11 +96,12 @@ namespace polysat {
pdd r = a;
if (!a.resolve(m_var, b, r) && !b.resolve(m_var, a, r))
return nullptr;
p_dependency_ref d(m_solver.m_dm.mk_join(c1->dep(), c2->dep()), m_solver.m_dm);
unsigned lvl = std::max(c1->level(), c2->level());
constraint_ref c = m_solver.m_constraints.eq(lvl, pos_t, r, d);
c->assign(true);
return clause::from_unit(c);
unsigned const lvl = std::max(c1->level(), c2->level());
clause_builder clause(m_solver);
clause.push_literal(~c1->blit());
clause.push_literal(~c2->blit());
clause.push_new_constraint(m_solver.m_constraints.eq(lvl, r));
return clause.build();
}
return nullptr;
}
@ -108,19 +135,19 @@ namespace polysat {
unsigned const lvl = c.src->level();
clause_builder clause(m_solver);
clause.push_literal(~c.src->blit());
// Omega^*(x, y)
if (!push_omega_mul(clause, lvl, sz, x, y))
continue;
constraint_ref y_le_z;
constraint_literal y_le_z;
if (c.is_strict)
y_le_z = m_solver.m_constraints.ult(lvl, pos_t, y, z, null_dep());
y_le_z = m_solver.m_constraints.ult(lvl, y, z);
else
y_le_z = m_solver.m_constraints.ule(lvl, pos_t, y, z, null_dep());
y_le_z = m_solver.m_constraints.ule(lvl, y, z);
LOG("z>y: " << show_deref(y_le_z));
clause.push_new_constraint(std::move(y_le_z));
p_dependency_ref dep(c.src->dep(), m_solver.m_dm);
return clause.build(lvl, dep);
return clause.build();
}
return nullptr;
}
@ -181,20 +208,21 @@ namespace polysat {
pdd const& z_prime = d.lhs;
clause_builder clause(m_solver);
clause.push_literal(~c.src->blit());
clause.push_literal(~d.src->blit());
// Omega^*(x, y)
if (!push_omega_mul(clause, lvl, sz, x, y))
continue;
// z'x <= zx
constraint_ref zpx_le_zx;
constraint_literal zpx_le_zx;
if (c.is_strict || d.is_strict)
zpx_le_zx = m_solver.m_constraints.ult(lvl, pos_t, z_prime*x, z*x, null_dep());
zpx_le_zx = m_solver.m_constraints.ult(lvl, z_prime*x, z*x);
else
zpx_le_zx = m_solver.m_constraints.ule(lvl, pos_t, z_prime*x, z*x, null_dep());
zpx_le_zx = m_solver.m_constraints.ule(lvl, z_prime*x, z*x);
LOG("zx>z'x: " << show_deref(zpx_le_zx));
clause.push_new_constraint(std::move(zpx_le_zx));
p_dependency_ref dep(m_solver.m_dm.mk_join(c.src->dep(), d.src->dep()), m_solver.m_dm);
return clause.build(lvl, dep);
return clause.build();
}
}
return nullptr;
@ -256,20 +284,21 @@ namespace polysat {
pdd const& y_prime = d.rhs;
clause_builder clause(m_solver);
clause.push_literal(~c.src->blit());
clause.push_literal(~d.src->blit());
// Omega^*(x, y')
if (!push_omega_mul(clause, lvl, sz, x, y_prime))
continue;
// yx <= y'x
constraint_ref yx_le_ypx;
constraint_literal yx_le_ypx;
if (c.is_strict || d.is_strict)
yx_le_ypx = m_solver.m_constraints.ult(lvl, pos_t, y*x, y_prime*x, null_dep());
yx_le_ypx = m_solver.m_constraints.ult(lvl, y*x, y_prime*x);
else
yx_le_ypx = m_solver.m_constraints.ule(lvl, pos_t, y*x, y_prime*x, null_dep());
yx_le_ypx = m_solver.m_constraints.ule(lvl, y*x, y_prime*x);
LOG("y'x>yx: " << show_deref(yx_le_ypx));
clause.push_new_constraint(std::move(yx_le_ypx));
p_dependency_ref dep(m_solver.m_dm.mk_join(c.src->dep(), d.src->dep()), m_solver.m_dm);
return clause.build(lvl, dep);
return clause.build();
}
}
return nullptr;
@ -316,20 +345,21 @@ namespace polysat {
pdd const& z = d.rhs;
clause_builder clause(m_solver);
clause.push_literal(~c.src->blit());
clause.push_literal(~d.src->blit());
// Omega^*(a, z)
if (!push_omega_mul(clause, lvl, sz, a, z))
continue;
// y'x > yx
constraint_ref y_ule_az;
constraint_literal y_ule_az;
if (c.is_strict || d.is_strict)
y_ule_az = m_solver.m_constraints.ult(lvl, pos_t, y, a*z, null_dep());
y_ule_az = m_solver.m_constraints.ult(lvl, y, a*z);
else
y_ule_az = m_solver.m_constraints.ule(lvl, pos_t, y, a*z, null_dep());
y_ule_az = m_solver.m_constraints.ule(lvl, y, a*z);
LOG("y<=az: " << show_deref(y_ule_az));
clause.push_new_constraint(std::move(y_ule_az));
p_dependency_ref dep(m_solver.m_dm.mk_join(c1->dep(), d.src->dep()), m_solver.m_dm);
return clause.build(lvl, dep);
return clause.build();
}
}
return nullptr;
@ -382,9 +412,9 @@ namespace polysat {
SASSERT(min_k <= k && k <= max_k);
// x >= 2^k
constraint_ref c1 = m_solver.m_constraints.ult(level, pos_t, pddm.mk_val(rational::power_of_two(k)), x, null_dep());
auto c1 = m_solver.m_constraints.ule(level, pddm.mk_val(rational::power_of_two(k)), x);
// y > 2^{p-k}
constraint_ref c2 = m_solver.m_constraints.ule(level, pos_t, pddm.mk_val(rational::power_of_two(p-k)), y, null_dep());
auto c2 = m_solver.m_constraints.ult(level, pddm.mk_val(rational::power_of_two(p-k)), y);
clause.push_new_constraint(std::move(c1));
clause.push_new_constraint(std::move(c2));
return true;

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

@ -13,6 +13,7 @@ Author:
--*/
#pragma once
#include "math/polysat/constraint.h"
#include "math/polysat/clause_builder.h"
#include "math/polysat/interval.h"
#include "math/polysat/solver.h"

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

@ -14,13 +14,15 @@ Author:
--*/
#include "math/polysat/forbidden_intervals.h"
#include "math/polysat/clause_builder.h"
#include "math/polysat/interval.h"
#include "math/polysat/log.h"
namespace polysat {
struct fi_record {
eval_interval interval;
constraint_ref neg_cond; // could be multiple constraints later
constraint_literal neg_cond; // could be multiple constraints later
constraint* src;
};
@ -76,7 +78,7 @@ namespace polysat {
continue;
}
eval_interval interval = eval_interval::full();
constraint_ref neg_cond;
constraint_literal neg_cond;
if (c->forbidden_interval(s, v, interval, neg_cond)) {
LOG("interval: " << interval);
LOG("neg_cond: " << show_deref(neg_cond));
@ -107,9 +109,7 @@ namespace polysat {
clause.push_literal(~full_record.src->blit());
if (full_record.neg_cond)
clause.push_new_constraint(std::move(full_record.neg_cond));
unsigned lemma_lvl = full_record.src->level();
p_dependency_ref lemma_dep(full_record.src->dep(), s.m_dm);
out_lemma = clause.build(lemma_lvl, lemma_dep);
out_lemma = clause.build();
return true;
}
@ -132,14 +132,11 @@ namespace polysat {
LOG("seq: " << seq);
SASSERT(seq.size() >= 2); // otherwise has_full should have been true
p_dependency* d = nullptr;
unsigned lemma_lvl = 0;
for (unsigned i : seq) {
constraint* c = records[i].src;
d = s.m_dm.mk_join(d, c->dep());
lemma_lvl = std::max(lemma_lvl, c->level());
}
p_dependency_ref lemma_dep(d, s.m_dm);
// Create lemma
// Idea:
@ -166,16 +163,16 @@ 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_ref c = s.m_constraints.ult(lemma_lvl, neg_t, lhs, rhs, s.mk_dep_ref(null_dependency));
constraint_literal 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_ref& neg_cond = records[i].neg_cond;
constraint_literal& neg_cond = records[i].neg_cond;
if (neg_cond)
clause.push_new_constraint(std::move(neg_cond));
}
out_lemma = clause.build(lemma_lvl, lemma_dep);
out_lemma = clause.build();
return true;
}

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

@ -15,7 +15,6 @@ Author:
--*/
#pragma once
#include "math/polysat/constraint.h"
#include "math/polysat/interval.h"
#include "math/polysat/solver.h"
namespace polysat {

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

@ -61,7 +61,7 @@ namespace polysat {
m_disjunctive_lemma.reset();
while (m_lim.inc()) {
m_stats.m_num_iterations++;
LOG_H1("Next solving loop iteration");
LOG_H1("Next solving loop iteration (#" << m_stats.m_num_iterations << ")");
LOG("Free variables: " << m_free_vars);
LOG("Assignment: " << assignments_pp(*this));
if (!m_conflict.empty()) LOG("Conflict: " << m_conflict);
@ -112,42 +112,47 @@ namespace polysat {
m_free_vars.del_var_eh(v);
}
constraint_ref solver::mk_eq(pdd const& p, unsigned dep) {
return m_constraints.eq(m_level, pos_t, p, mk_dep_ref(dep));
constraint_literal solver::mk_eq(pdd const& p) {
return m_constraints.eq(m_level, p);
}
constraint_ref solver::mk_diseq(pdd const& p, unsigned dep) {
return m_constraints.eq(m_level, neg_t, p, mk_dep_ref(dep));
constraint_literal solver::mk_diseq(pdd const& p) {
return ~m_constraints.eq(m_level, p);
}
constraint_ref solver::mk_ule(pdd const& p, pdd const& q, unsigned dep) {
return m_constraints.ule(m_level, pos_t, p, q, mk_dep_ref(dep));
constraint_literal solver::mk_ule(pdd const& p, pdd const& q) {
return m_constraints.ule(m_level, p, q);
}
constraint_ref solver::mk_ult(pdd const& p, pdd const& q, unsigned dep) {
return m_constraints.ult(m_level, pos_t, p, q, mk_dep_ref(dep));
constraint_literal solver::mk_ult(pdd const& p, pdd const& q) {
return m_constraints.ult(m_level, p, q);
}
constraint_ref solver::mk_sle(pdd const& p, pdd const& q, unsigned dep) {
return m_constraints.sle(m_level, pos_t, p, q, mk_dep_ref(dep));
constraint_literal solver::mk_sle(pdd const& p, pdd const& q) {
return m_constraints.sle(m_level, p, q);
}
constraint_ref solver::mk_slt(pdd const& p, pdd const& q, unsigned dep) {
return m_constraints.slt(m_level, pos_t, p, q, mk_dep_ref(dep));
constraint_literal solver::mk_slt(pdd const& p, pdd const& q) {
return m_constraints.slt(m_level, p, q);
}
void solver::new_constraint(constraint_ref cr, bool activate) {
void solver::new_constraint(constraint_literal cl, unsigned dep, bool activate) {
VERIFY(at_base_level());
SASSERT(cr);
SASSERT(activate || cr->dep()); // if we don't activate the constraint, we need the dependency to access it again later.
constraint* c = m_constraints.insert(std::move(cr));
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();
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_original.push_back(c);
#if ENABLE_LINEAR_SOLVER
m_linear_solver.new_constraint(*c);
#endif
if (activate && !is_conflict())
activate_constraint_base(c);
activate_constraint_base(c, !lit.sign());
}
void solver::assign_eh(unsigned dep, bool is_true) {
@ -159,7 +164,7 @@ namespace polysat {
}
if (is_conflict())
return;
activate_constraint_base(c);
activate_constraint_base(c, is_true);
}
@ -382,7 +387,7 @@ namespace polysat {
void solver::set_conflict(constraint& c) {
LOG("Conflict: " << c);
LOG(*this);
LOG("\n" << *this);
SASSERT(!is_conflict());
m_conflict.push_back(&c);
}
@ -442,7 +447,7 @@ namespace polysat {
void solver::resolve_conflict() {
IF_VERBOSE(1, verbose_stream() << "resolve conflict\n");
LOG_H2("Resolve conflict");
LOG(*this);
LOG("\n" << *this);
LOG("search state: " << m_search);
++m_stats.m_num_conflicts;
@ -489,6 +494,7 @@ namespace polysat {
conflict_explainer cx(*this, m_conflict);
lemma = cx.resolve(conflict_var, {});
LOG("resolved: " << show_deref(lemma));
// SASSERT(false && "pause on explanation");
}
}
@ -678,7 +684,7 @@ namespace polysat {
p_dependency_ref conflict_dep(m_dm);
for (auto& c : m_conflict.units())
if (c)
conflict_dep = m_dm.mk_join(c->dep(), conflict_dep);
conflict_dep = m_dm.mk_join(c->unit_dep(), conflict_dep);
for (auto& c : m_conflict.clauses())
conflict_dep = m_dm.mk_join(c->dep(), conflict_dep);
m_dm.linearize(conflict_dep, deps);
@ -706,21 +712,15 @@ namespace polysat {
c = m_constraints.lookup(lemma->literals()[0].var());
}
SASSERT_EQ(lemma->literals()[0].var(), c->bvar());
SASSERT(!lemma->literals()[0].sign()); // TODO: that case is handled incorrectly atm
learn_lemma_unit(v, std::move(c));
SASSERT(c);
add_lemma_unit(c);
push_cjust(v, c.get());
activate_constraint_base(c.get(), !lemma->literals()[0].sign());
}
else
learn_lemma_clause(v, std::move(lemma));
}
void solver::learn_lemma_unit(pvar v, constraint_ref lemma) {
SASSERT(lemma);
constraint* c = lemma.get();
add_lemma_unit(std::move(lemma));
push_cjust(v, c);
activate_constraint_base(c);
}
void solver::learn_lemma_clause(pvar v, clause_ref lemma) {
SASSERT(lemma);
sat::literal lit = decide_bool(*lemma);
@ -744,6 +744,7 @@ namespace polysat {
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);
};
@ -863,19 +864,19 @@ namespace polysat {
// * the reason for reverting this decision then needs to be the (negation of the) conflicting literals. Or we give up on resolving this lemma?
SASSERT(m_conflict.clauses().empty()); // not sure how to handle otherwise
clause_builder clause(*this);
unsigned reason_lvl = m_constraints.lookup(lit.var())->level();
p_dependency_ref reason_dep(m_constraints.lookup(lit.var())->dep(), m_dm);
// unsigned reason_lvl = m_constraints.lookup(lit.var())->level();
// p_dependency_ref reason_dep(m_constraints.lookup(lit.var())->dep(), m_dm);
clause.push_literal(~lit); // propagated literal
for (auto c : m_conflict.units()) {
if (c->bvar() == var)
continue;
if (c->is_undef()) // TODO: see revert_decision for a note on this.
continue;
reason_lvl = std::max(reason_lvl, c->level());
reason_dep = m_dm.mk_join(reason_dep, c->dep());
// reason_lvl = std::max(reason_lvl, c->level());
// reason_dep = m_dm.mk_join(reason_dep, c->dep());
clause.push_literal(c->blit());
}
reason = clause.build(reason_lvl, reason_dep);
reason = clause.build();
LOG("Made-up reason: " << show_deref(reason));
}
@ -923,7 +924,7 @@ namespace polysat {
SASSERT(reason->literals()[0] == lit);
constraint* c = m_constraints.lookup(lit.var());
m_redundant.push_back(c);
activate_constraint_base(c);
activate_constraint_base(c, !lit.sign());
}
else
assign_bool_backtrackable(lit, reason, nullptr);
@ -945,15 +946,16 @@ namespace polysat {
/// Activate a constraint at the base level.
/// Used for external unit constraints and unit consequences.
void solver::activate_constraint_base(constraint* c) {
void solver::activate_constraint_base(constraint* c, bool is_true) {
SASSERT(c);
assign_bool_core(sat::literal(c->bvar()), nullptr, nullptr);
activate_constraint(*c, true);
// 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 a boolean literal and activate the corresponding constraint
/// Assign a boolean literal
void solver::assign_bool_core(sat::literal lit, clause* reason, clause* lemma) {
LOG("Assigning boolean literal: " << lit);
m_bvars.assign(lit, m_level, reason, lemma);
@ -976,6 +978,9 @@ namespace polysat {
LOG("Deactivating constraint: " << c);
erase_watch(c);
c.unassign();
#if ENABLE_LINEAR_SOLVER
m_linear_solver.deactivate_constraint(c); // TODO add this method to linear solver?
#endif
}
void solver::backjump(unsigned new_level) {
@ -998,6 +1003,7 @@ namespace polysat {
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;
}
@ -1013,20 +1019,22 @@ namespace polysat {
if (!lemma)
return;
LOG("Lemma: " << show_deref(lemma));
constraint* c = m_constraints.insert(std::move(lemma));
constraint* c = m_constraints.store(std::move(lemma));
insert_constraint(m_redundant, c);
// TODO: create unit clause
}
// Add lemma to storage but do not activate it
void solver::add_lemma_clause(clause_ref lemma) {
if (!lemma)
return;
// TODO: check for unit clauses!
LOG("Lemma: " << show_deref(lemma));
if (lemma->size() < 2) {
LOG_H1("TODO: this should be treated as unit constraint and asserted at the base level!");
}
// SASSERT(lemma->size() > 1);
clause* cl = m_constraints.insert(std::move(lemma));
clause* cl = m_constraints.store(std::move(lemma));
m_redundant_clauses.push_back(cl);
}
@ -1074,7 +1082,15 @@ namespace polysat {
}
bool solver::active_at_base_level(sat::bool_var bvar) const {
return m_bvars.is_assigned(bvar) && m_bvars.level(bvar) <= base_level();
// NOTE: this active_at_base_level is actually not what we want!!!
// first of all, it might not really be a base level: could be a non-base level between previous base levels.
// in that case, how do we determine the right dependencies???
// secondly, we are interested in "unit clauses", not as much whether we assigned something on the base level...
// TODO: however, propagating stuff at the base level... need to be careful with dependencies there... might need to turn all base-level propagations into unit clauses...
VERIFY(false);
// bool res = m_bvars.is_assigned(bvar) && m_bvars.level(bvar) <= base_level();
// SASSERT_EQ(res, !!m_constraints.lookup(bvar)->unit_clause());
// return res;
}
bool solver::try_eval(pdd const& p, rational& out_value) const {
@ -1085,14 +1101,16 @@ namespace polysat {
}
std::ostream& solver::display(std::ostream& out) const {
out << "Assignment:\n";
for (auto [v, val] : assignment()) {
auto j = m_justification[v];
out << assignment_pp(*this, v, val) << " @" << j.level();
out << "\t" << assignment_pp(*this, v, val) << " @" << j.level();
if (j.is_propagation())
out << " " << m_cjust[v];
out << "\n";
// out << m_viable[v] << "\n";
}
out << "Boolean assignment:\n\t" << m_bvars << "\n";
out << "Original:\n";
for (auto* c : m_original)
out << "\t" << *c << "\n";

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

@ -21,6 +21,7 @@ Author:
#include "util/statistics.h"
#include "math/polysat/boolean.h"
#include "math/polysat/constraint.h"
#include "math/polysat/clause_builder.h"
#include "math/polysat/eq_constraint.h"
#include "math/polysat/ule_constraint.h"
#include "math/polysat/justification.h"
@ -96,14 +97,6 @@ namespace polysat {
search_state m_search;
assignment_t const& assignment() const { return m_search.assignment(); }
// (old, remove later)
// using bool_clauses = ptr_vector<bool_clause>;
// vector<lbool> m_bool_value; // value of boolean literal (indexed by literal)
// vector<bool_clauses> m_bool_watch; // watch list into clauses (indexed by literal)
// // scoped_ptr_vector<bool_clause> m_bool_clauses; // NOTE: as of now, external clauses will only be units! So this is not needed.
// svector<sat::literal> m_bool_units; // externally asserted unit clauses, via assign_eh
// scoped_ptr_vector<bool_clause> m_bool_redundant; // learned clause storage
unsigned m_qhead { 0 }; // next item to propagate (index into m_search)
unsigned m_level { 0 };
@ -155,7 +148,7 @@ namespace polysat {
void pop_constraints(ptr_vector<constraint>& cs);
void assign_bool_backtrackable(sat::literal lit, clause* reason, clause* lemma);
void activate_constraint_base(constraint* c);
void activate_constraint_base(constraint* c, bool is_true);
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);
@ -224,19 +217,18 @@ namespace polysat {
void revert_decision(pvar v, clause_ref reason);
void revert_bool_decision(sat::literal lit, clause_ref reason);
void learn_lemma(pvar v, clause_ref lemma);
void learn_lemma_unit(pvar v, constraint_ref lemma);
void learn_lemma_clause(pvar v, clause_ref lemma);
void backjump(unsigned new_level);
void add_lemma_unit(constraint_ref lemma);
void add_lemma_clause(clause_ref lemma);
constraint_ref mk_eq(pdd const& p, unsigned dep);
constraint_ref mk_diseq(pdd const& p, unsigned dep);
constraint_ref mk_ule(pdd const& p, pdd const& q, unsigned dep);
constraint_ref mk_ult(pdd const& p, pdd const& q, unsigned dep);
constraint_ref mk_sle(pdd const& p, pdd const& q, unsigned dep);
constraint_ref mk_slt(pdd const& p, pdd const& q, unsigned dep);
void new_constraint(constraint_ref c, bool activate);
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);
bool invariant();
@ -301,20 +293,20 @@ namespace polysat {
* Create polynomial constraints (but do not activate them).
* Each constraint is tracked by a dependency.
*/
void new_eq(pdd const& p, unsigned dep) { new_constraint(mk_eq(p, dep), false); }
void new_diseq(pdd const& p, unsigned dep) { new_constraint(mk_diseq(p, dep), false); }
void new_ule(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ule(p, q, dep), false); }
void new_ult(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ult(p, q, dep), false); }
void new_sle(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_sle(p, q, dep), false); }
void new_slt(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_slt(p, q, dep), false); }
void new_eq(pdd const& p, unsigned dep) { new_constraint(mk_eq(p), dep, false); }
void new_diseq(pdd const& p, unsigned dep) { new_constraint(mk_diseq(p), dep, false); }
void new_ule(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ule(p, q), dep, false); }
void new_ult(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ult(p, q), dep, false); }
void new_sle(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_sle(p, q), dep, false); }
void new_slt(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_slt(p, q), dep, false); }
/** Create and activate polynomial constraints. */
void add_eq(pdd const& p, unsigned dep = null_dependency) { new_constraint(mk_eq(p, dep), true); }
void add_diseq(pdd const& p, unsigned dep = null_dependency) { new_constraint(mk_diseq(p, dep), true); }
void add_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_ule(p, q, dep), true); }
void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_ult(p, q, dep), true); }
void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_sle(p, q, dep), true); }
void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_slt(p, q, dep), true); }
void add_eq(pdd const& p, unsigned dep = null_dependency) { new_constraint(mk_eq(p), dep, true); }
void add_diseq(pdd const& p, unsigned dep = null_dependency) { new_constraint(mk_diseq(p), dep, true); }
void add_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_ule(p, q), dep, true); }
void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_ult(p, q), dep, true); }
void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_sle(p, q), dep, true); }
void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_slt(p, q), dep, true); }
/**
* Activate the constraint corresponding to the given boolean variable.

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

@ -19,14 +19,10 @@ Author:
namespace polysat {
std::ostream& ule_constraint::display(std::ostream& out) const {
out << m_lhs << (sign() == pos_t ? " <= " : " > ") << m_rhs;
out << m_lhs << " <= " << m_rhs;
return display_extra(out);
}
constraint_ref ule_constraint::resolve(solver& s, pvar v) {
return nullptr;
}
void ule_constraint::narrow(solver& s) {
LOG_H3("Narrowing " << *this);
LOG("Assignment: " << assignments_pp(s));
@ -117,7 +113,7 @@ namespace polysat {
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_ref& out_neg_cond)
bool ule_constraint::forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond)
{
SASSERT(!is_undef());
@ -247,8 +243,10 @@ namespace polysat {
SASSERT(is_trivial == condition_body.is_zero());
out_neg_cond = nullptr;
}
else if (is_trivial)
out_neg_cond = ~s.m_constraints.eq(level(), condition_body);
else
out_neg_cond = s.m_constraints.eq(level(), is_trivial ? neg_t : pos_t, condition_body, s.mk_dep_ref(null_dependency));
out_neg_cond = s.m_constraints.eq(level(), condition_body);
if (is_trivial) {
if (is_positive())

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

@ -21,8 +21,8 @@ namespace polysat {
pdd m_lhs;
pdd m_rhs;
public:
ule_constraint(constraint_manager& m, unsigned lvl, csign_t sign, pdd const& l, pdd const& r, p_dependency_ref const& dep):
constraint(m, lvl, sign, dep, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
ule_constraint(constraint_manager& m, unsigned lvl, pdd const& l, pdd const& r):
constraint(m, lvl, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
m_vars.append(l.free_vars());
for (auto v : r.free_vars())
if (!m_vars.contains(v))
@ -32,13 +32,12 @@ namespace polysat {
pdd const& lhs() const { return m_lhs; }
pdd const& rhs() const { return m_rhs; }
std::ostream& display(std::ostream& out) const override;
constraint_ref resolve(solver& s, pvar v) 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_ref& out_neg_cond) override;
bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_literal& out_neg_cond) override;
inequality as_inequality() const override;
};

4
src/test/polysat.cpp
View file

@ -833,8 +833,8 @@ namespace polysat {
void tst_polysat() {
polysat::test_monot_bounds(8);
// polysat::test_monot_bounds_simple(8);
// polysat::test_monot_bounds(8);
polysat::test_monot_bounds_simple(8);
return;
polysat::test_add_conflicts();