mirror of
https://github.com/Z3Prover/z3
synced 2025-04-25 01:55:32 +00:00
adding Boolean propagation, watch; and factoring
This commit is contained in:
Nikolaj Bjorner
parent
f01da40e49
commit
fa3886136b
15 changed files with 341 additions and 134 deletions
|
|
@ -914,14 +914,10 @@ namespace dd {
|
|||
bool pdd_manager::resolve(unsigned v, pdd const& p, pdd const& q, pdd& r) {
|
||||
unsigned const l = p.degree(v);
|
||||
unsigned const m = q.degree(v);
|
||||
if (l < m) {
|
||||
// no reduction
|
||||
// no reduction
|
||||
if (l < m || m == 0)
|
||||
return false;
|
||||
}
|
||||
if (m == 0) {
|
||||
// no reduction (result would still contain v^l)
|
||||
return false;
|
||||
}
|
||||
|
||||
pdd a = zero();
|
||||
pdd b = zero();
|
||||
pdd c = zero();
|
||||
|
|
@ -938,6 +934,100 @@ namespace dd {
|
|||
return true;
|
||||
}
|
||||
|
||||
/**
|
||||
* Reduce polynomial a with respect to b by eliminating terms using v
|
||||
*
|
||||
* a := a1*v^l + a2
|
||||
* b := b1*v^m + b2
|
||||
* l >= m
|
||||
* q, r := quot_rem(a1, b1)
|
||||
* r = 0
|
||||
* result := reduce(v, q*b2*v^{l-m}, b) + reduce(v, a2, b)
|
||||
*/
|
||||
pdd pdd_manager::reduce(unsigned v, pdd const& a, pdd const& b) {
|
||||
unsigned const l = a.degree(v);
|
||||
unsigned const m = b.degree(v);
|
||||
// no reduction
|
||||
if (l < m || m == 0)
|
||||
return a;
|
||||
|
||||
pdd a1 = zero();
|
||||
pdd a2 = zero();
|
||||
pdd b1 = zero();
|
||||
pdd b2 = zero();
|
||||
pdd q = zero();
|
||||
pdd r = zero();
|
||||
a.factor(v, l, a1, a2);
|
||||
b.factor(v, m, b1, b2);
|
||||
|
||||
quot_rem(a1, b1, q, r);
|
||||
if (r.is_zero()) {
|
||||
std::cout << a1 << " " << b1 << " " << q << "\n";
|
||||
SASSERT(q * b1 == a1);
|
||||
a1 = -q * pow(mk_var(v), l - m) * b2;
|
||||
if (l > m)
|
||||
a1 = reduce(v, a1, b);
|
||||
}
|
||||
else
|
||||
a1 = a1 * pow(mk_var(v), l);
|
||||
a2 = a2.reduce(v, b);
|
||||
|
||||
pdd result = a1 + a2;
|
||||
return result;
|
||||
}
|
||||
|
||||
/**
|
||||
* quotient/remainder of 'a' divided by 'b'
|
||||
* a := x*hi + lo
|
||||
* x > level(b):
|
||||
* hi = q1*b + r1
|
||||
* lo = q2*b + r2
|
||||
* x*hi + lo = (x*q1 + q2)*b + (x*r1 + r2)
|
||||
* q := x*q1 + q2
|
||||
* r := x*r1 + r2
|
||||
* Some special cases.
|
||||
* General multi-variable polynomial division is TBD.
|
||||
*/
|
||||
void pdd_manager::quot_rem(pdd const& a, pdd const& b, pdd& q, pdd& r) {
|
||||
if (level(a.root) > level(b.root)) {
|
||||
pdd q1(*this), q2(*this), r1(*this), r2(*this);
|
||||
quot_rem(a.hi(), b, q1, r1);
|
||||
quot_rem(a.lo(), b, q2, r2);
|
||||
q = mk_var(a.var()) * q1 + q2;
|
||||
r = mk_var(a.var()) * r1 + r2;
|
||||
}
|
||||
else if (level(a.root) < level(b.root)) {
|
||||
q = zero();
|
||||
r = a;
|
||||
}
|
||||
else if (a == b) {
|
||||
q = one();
|
||||
r = zero();
|
||||
}
|
||||
else if (a.is_val() && b.is_val() && divides(b.val(), a.val())) {
|
||||
q = mk_val(a.val() / b.val());
|
||||
r = zero();
|
||||
}
|
||||
else if (a.is_val() || b.is_val()) {
|
||||
q = zero();
|
||||
r = a;
|
||||
}
|
||||
else {
|
||||
SASSERT(level(a.root) == level(b.root));
|
||||
pdd q1(*this), q2(*this), r1(*this), r2(*this);
|
||||
quot_rem(a.hi(), b.hi(), q1, r1);
|
||||
quot_rem(a.lo(), b.lo(), q2, r2);
|
||||
if (q1 == q2 && r1.is_zero() && r2.is_zero()) {
|
||||
q = q1;
|
||||
r = zero();
|
||||
}
|
||||
else {
|
||||
q = zero();
|
||||
r = a;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns the largest j such that 2^j divides p.
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -23,6 +23,11 @@ Abstract:
|
|||
|
||||
- try_spoly(a, b, c) returns true if lt(a) and lt(b) have a non-trivial overlap. c is the resolvent (S polynomial).
|
||||
|
||||
- reduce(v, a, b) reduces 'a' using b = 0 with respect to eliminating v.
|
||||
Given b = v^l*b1 + b2, where l is the leading coefficient of v in b
|
||||
Given a = v^m*a1 + b2, where m >= l is the leading coefficient of v in b.
|
||||
reduce(a1, b1)*v^{m - l} + reduce(v, a2, b);
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2019-12-17
|
||||
|
|
@ -333,6 +338,8 @@ namespace dd {
|
|||
pdd subst_val(pdd const& a, vector<std::pair<unsigned, rational>> const& s);
|
||||
pdd subst_val(pdd const& a, unsigned v, rational const& val);
|
||||
bool resolve(unsigned v, pdd const& p, pdd const& q, pdd& r);
|
||||
pdd reduce(unsigned v, pdd const& a, pdd const& b);
|
||||
void quot_rem(pdd const& a, pdd const& b, pdd& q, pdd& r);
|
||||
pdd pow(pdd const& p, unsigned j);
|
||||
|
||||
bool is_linear(PDD p) { return degree(p) == 1; }
|
||||
|
|
@ -419,6 +426,7 @@ namespace dd {
|
|||
void factor(unsigned v, unsigned degree, pdd& lc, pdd& rest) const { m.factor(*this, v, degree, lc, rest); }
|
||||
bool factor(unsigned v, unsigned degree, pdd& lc) const { return m.factor(*this, v, degree, lc); }
|
||||
bool resolve(unsigned v, pdd const& other, pdd& result) { return m.resolve(v, *this, other, result); }
|
||||
pdd reduce(unsigned v, pdd const& other) const { return m.reduce(v, *this, other); }
|
||||
|
||||
pdd subst_val(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val(*this, s); }
|
||||
pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); }
|
||||
|
|
|
|||
|
|
@ -17,8 +17,9 @@ Author:
|
|||
namespace polysat {
|
||||
|
||||
sat::bool_var bool_var_manager::new_var() {
|
||||
sat::bool_var var;
|
||||
if (m_unused.empty()) {
|
||||
sat::bool_var var = size();
|
||||
var = size();
|
||||
m_value.push_back(l_undef);
|
||||
m_value.push_back(l_undef);
|
||||
m_level.push_back(UINT_MAX);
|
||||
|
|
@ -26,18 +27,19 @@ namespace polysat {
|
|||
m_lemma.push_back(nullptr);
|
||||
m_watch.push_back({});
|
||||
m_watch.push_back({});
|
||||
return var;
|
||||
m_activity.push_back(0);
|
||||
}
|
||||
else {
|
||||
sat::bool_var var = m_unused.back();
|
||||
var = m_unused.back();
|
||||
m_unused.pop_back();
|
||||
SASSERT_EQ(m_level[var], UINT_MAX);
|
||||
SASSERT_EQ(m_value[2*var], l_undef);
|
||||
SASSERT_EQ(m_value[2*var+1], l_undef);
|
||||
SASSERT_EQ(m_reason[var], nullptr);
|
||||
SASSERT_EQ(m_lemma[var], nullptr);
|
||||
return var;
|
||||
}
|
||||
m_free_vars.mk_var_eh(var);
|
||||
return var;
|
||||
}
|
||||
|
||||
void bool_var_manager::del_var(sat::bool_var var) {
|
||||
|
|
@ -50,6 +52,7 @@ namespace polysat {
|
|||
m_lemma[var] = nullptr;
|
||||
m_watch[lit.index()].reset();
|
||||
m_watch[(~lit).index()].reset();
|
||||
m_free_vars.del_var_eh(var);
|
||||
// TODO: this is disabled for now, since re-using variables for different constraints may be confusing during debugging. Should be enabled later.
|
||||
// m_unused.push_back(var);
|
||||
}
|
||||
|
|
@ -61,6 +64,7 @@ namespace polysat {
|
|||
m_level[lit.var()] = lvl;
|
||||
m_reason[lit.var()] = reason;
|
||||
m_lemma[lit.var()] = lemma;
|
||||
m_free_vars.del_var_eh(lit.var());
|
||||
}
|
||||
|
||||
void bool_var_manager::unassign(sat::literal lit) {
|
||||
|
|
@ -70,6 +74,7 @@ namespace polysat {
|
|||
m_level[lit.var()] = UINT_MAX;
|
||||
m_reason[lit.var()] = nullptr;
|
||||
m_lemma[lit.var()] = nullptr;
|
||||
m_free_vars.unassign_var_eh(lit.var());
|
||||
}
|
||||
|
||||
std::ostream& bool_var_manager::display(std::ostream& out) const {
|
||||
|
|
|
|||
|
|
@ -28,9 +28,13 @@ namespace polysat {
|
|||
// For enumerative backtracking we store the lemma we're handling with a certain decision
|
||||
svector<clause*> m_lemma;
|
||||
|
||||
var_queue m_free_vars; // free Boolean variables
|
||||
vector<ptr_vector<clause>> m_watch; // watch list for literals into clauses
|
||||
|
||||
public:
|
||||
|
||||
bool_var_manager(): m_free_vars(m_activity) {}
|
||||
|
||||
// allocated size (not the number of active variables)
|
||||
unsigned size() const { return m_level.size(); }
|
||||
|
||||
|
|
@ -52,8 +56,16 @@ namespace polysat {
|
|||
|
||||
clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_lemma[var]; }
|
||||
|
||||
|
||||
|
||||
ptr_vector<clause>& watch(sat::literal lit) { return m_watch[lit.index()]; }
|
||||
unsigned_vector& activity() { return m_activity; }
|
||||
bool can_decide() const { return !m_free_vars.empty(); }
|
||||
sat::bool_var next_var() { return m_free_vars.next_var(); }
|
||||
|
||||
// TODO connect activity updates with solver
|
||||
void inc_activity(sat::literal lit) { m_activity[lit.var()]++; }
|
||||
void dec_activity(sat::literal lit) { m_activity[lit.var()] /= 2; }
|
||||
|
||||
/// Set the given literal to true
|
||||
void assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma);
|
||||
|
|
|
|||
|
|
@ -51,7 +51,7 @@ namespace polysat {
|
|||
std::ostream& conflict_core::display(std::ostream& out) const {
|
||||
char const* sep = "";
|
||||
for (auto c : *this)
|
||||
out << sep << c, sep = " ; ";
|
||||
out << sep << c->bvar2string() << " " << c, sep = " ; ";
|
||||
if (!m_vars.empty())
|
||||
out << " vars";
|
||||
for (auto v : m_vars)
|
||||
|
|
@ -102,8 +102,19 @@ namespace polysat {
|
|||
SASSERT(!empty());
|
||||
}
|
||||
|
||||
void conflict_core::set(clause const& cl) {
|
||||
LOG("Conflict: " << cl);
|
||||
SASSERT(empty());
|
||||
for (auto lit : cl) {
|
||||
auto c = s().lit2cnstr(lit);
|
||||
c->set_var_dependent();
|
||||
insert(~c);
|
||||
}
|
||||
SASSERT(!empty());
|
||||
}
|
||||
|
||||
void conflict_core::insert(signed_constraint c) {
|
||||
LOG("inserting: " << c << " " << c.is_always_true() << " " << c->is_marked() << " " << c->has_bvar());
|
||||
LOG("inserting: " << c);
|
||||
// Skip trivial constraints
|
||||
// (e.g., constant ones such as "4 > 1"... only true ones should appear, otherwise the lemma would be a tautology)
|
||||
if (c.is_always_true())
|
||||
|
|
@ -152,6 +163,8 @@ namespace polysat {
|
|||
SASSERT(std::all_of(m_constraints.begin(), m_constraints.end(), [](auto c){ return !c->has_bvar(); }));
|
||||
bool core_has_pos = contains_literal(sat::literal(var));
|
||||
bool core_has_neg = contains_literal(~sat::literal(var));
|
||||
std::cout << cl << "\n";
|
||||
std::cout << *this << "\n";
|
||||
DEBUG_CODE({
|
||||
bool clause_has_pos = std::count(cl.begin(), cl.end(), sat::literal(var)) > 0;
|
||||
bool clause_has_neg = std::count(cl.begin(), cl.end(), ~sat::literal(var)) > 0;
|
||||
|
|
@ -183,23 +196,23 @@ namespace polysat {
|
|||
auto it = m_saturation_premises.find_iterator(c);
|
||||
if (it == m_saturation_premises.end())
|
||||
return;
|
||||
unsigned active_level = 0;
|
||||
auto& premises = it->m_value;
|
||||
clause_builder c_lemma(s());
|
||||
for (auto premise : premises) {
|
||||
LOG_H3("premise: " << premise);
|
||||
keep(premise);
|
||||
SASSERT(premise->has_bvar());
|
||||
SASSERT(premise->has_bvar());
|
||||
SASSERT(premise.is_currently_true(s()) || premise.bvalue(s()) == l_true);
|
||||
// otherwise the propagation doesn't make sense
|
||||
c_lemma.push(~premise.blit());
|
||||
active_level = std::max(active_level, premise.level(s()));
|
||||
}
|
||||
c_lemma.push(c.blit());
|
||||
clause* cl = cm().store(c_lemma.build());
|
||||
if (cl->size() == 1)
|
||||
c->set_unit_clause(cl);
|
||||
s().propagate_bool_at(active_level, c.blit(), cl);
|
||||
clause_ref lemma = c_lemma.build();
|
||||
cm().store(lemma.get(), s());
|
||||
if (lemma->size() == 1)
|
||||
c->set_unit_clause(lemma.get());
|
||||
if (s().m_bvars.value(c.blit()) == l_undef)
|
||||
s().propagate_bool_at(s().level(*lemma), c.blit(), lemma.get());
|
||||
}
|
||||
|
||||
clause_builder conflict_core::build_core_lemma() {
|
||||
|
|
@ -207,7 +220,8 @@ namespace polysat {
|
|||
LOG("core: " << *this);
|
||||
clause_builder lemma(s());
|
||||
|
||||
for (auto c : m_constraints) {
|
||||
while (!m_constraints.empty()) {
|
||||
signed_constraint c = m_constraints.back();
|
||||
SASSERT(!c->has_bvar());
|
||||
keep(c);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -83,6 +83,8 @@ namespace polysat {
|
|||
void set(signed_constraint c);
|
||||
/** conflict because there is no viable value for the variable v */
|
||||
void set(pvar v);
|
||||
/** all literals in clause are false */
|
||||
void set(clause const& cl);
|
||||
|
||||
void insert(signed_constraint c);
|
||||
void insert(signed_constraint c, vector<signed_constraint> premises);
|
||||
|
|
|
|||
|
|
@ -55,13 +55,11 @@ namespace polysat {
|
|||
m_constraints.push_back(c);
|
||||
}
|
||||
|
||||
|
||||
clause* constraint_manager::store(clause_ref cl_ref) {
|
||||
clause* cl = cl_ref.get();
|
||||
void constraint_manager::store(clause* cl, solver& s) {
|
||||
while (m_clauses.size() <= cl->level())
|
||||
m_clauses.push_back({});
|
||||
m_clauses[cl->level()].push_back(std::move(cl_ref));
|
||||
return cl;
|
||||
m_clauses[cl->level()].push_back(cl);
|
||||
watch(*cl, s);
|
||||
}
|
||||
|
||||
void constraint_manager::register_external(signed_constraint c) {
|
||||
|
|
@ -94,13 +92,48 @@ namespace polysat {
|
|||
// 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]) {
|
||||
for (auto& cl : m_clauses[l]) {
|
||||
unwatch(*cl);
|
||||
SASSERT_EQ(cl->m_ref_count, 1); // otherwise there is a leftover reference somewhere
|
||||
}
|
||||
m_clauses[l].reset();
|
||||
}
|
||||
}
|
||||
|
||||
// find literals that are not propagated to false
|
||||
// if clause is unsat then assign arbitrary
|
||||
// solver handles unsat clauses by creating a conflict.
|
||||
// solver also can propagate, but need to check that it does indeed.
|
||||
void constraint_manager::watch(clause& cl, solver& s) {
|
||||
if (cl.size() <= 1)
|
||||
return;
|
||||
bool first = true;
|
||||
for (unsigned i = 0; i < cl.size(); ++i) {
|
||||
if (m_bvars.is_false(cl[i]))
|
||||
continue;
|
||||
m_bvars.watch(cl[i]).push_back(&cl);
|
||||
std::swap(cl[!first], cl[i]);
|
||||
if (!first)
|
||||
return;
|
||||
first = false;
|
||||
}
|
||||
|
||||
if (first)
|
||||
m_bvars.watch(cl[0]).push_back(&cl);
|
||||
m_bvars.watch(cl[1]).push_back(&cl);
|
||||
if (first)
|
||||
s.set_conflict(cl);
|
||||
else
|
||||
s.propagate_bool_at(s.level(cl), cl[0], &cl);
|
||||
}
|
||||
|
||||
void constraint_manager::unwatch(clause& cl) {
|
||||
if (cl.size() <= 1)
|
||||
return;
|
||||
m_bvars.watch(~cl[0]).erase(&cl);
|
||||
m_bvars.watch(~cl[1]).erase(&cl);
|
||||
}
|
||||
|
||||
constraint_manager::~constraint_manager() {
|
||||
// Release explicitly to check for leftover references in debug mode,
|
||||
// and to make sure all constraints are destructed before the bvar->constraint mapping.
|
||||
|
|
@ -219,11 +252,12 @@ namespace polysat {
|
|||
return *dynamic_cast<ule_constraint const*>(this);
|
||||
}
|
||||
|
||||
std::ostream& constraint::display_extra(std::ostream& out) const {
|
||||
std::string constraint::bvar2string() const {
|
||||
std::stringstream out;
|
||||
out << " (b";
|
||||
if (has_bvar()) { out << bvar(); } else { out << "_"; }
|
||||
out << ")";
|
||||
return out;
|
||||
return out.str();
|
||||
}
|
||||
|
||||
bool constraint::propagate(solver& s, bool is_positive, pvar v) {
|
||||
|
|
@ -265,7 +299,8 @@ namespace polysat {
|
|||
return s.m_bvars.level(bvar());
|
||||
unsigned level = 0;
|
||||
for (auto v : vars())
|
||||
level = std::max(level, s.get_level(v));
|
||||
if (s.is_assigned(v))
|
||||
level = std::max(level, s.get_level(v));
|
||||
return level;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -64,6 +64,9 @@ namespace polysat {
|
|||
void gc_constraints(solver& s);
|
||||
void gc_clauses(solver& s);
|
||||
|
||||
void watch(clause& cl, solver& s);
|
||||
void unwatch(clause& cl);
|
||||
|
||||
public:
|
||||
constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {}
|
||||
~constraint_manager();
|
||||
|
|
@ -72,7 +75,7 @@ namespace polysat {
|
|||
void erase_bvar(constraint* c);
|
||||
// sat::literal get_or_assign_blit(signed_constraint& c);
|
||||
|
||||
clause* store(clause_ref cl);
|
||||
void store(clause* cl, solver& s);
|
||||
|
||||
/// Register a unit clause with an external dependency.
|
||||
void register_external(signed_constraint c);
|
||||
|
|
@ -146,9 +149,7 @@ namespace polysat {
|
|||
sat::bool_var m_bvar = sat::null_bool_var;
|
||||
|
||||
constraint(constraint_manager& m, ckind_t k): m_kind(k) {}
|
||||
|
||||
protected:
|
||||
std::ostream& display_extra(std::ostream& out) const;
|
||||
|
||||
|
||||
public:
|
||||
virtual ~constraint() {}
|
||||
|
|
@ -179,6 +180,7 @@ namespace polysat {
|
|||
bool contains_var(pvar v) const { return m_vars.contains(v); }
|
||||
bool has_bvar() const { return m_bvar != sat::null_bool_var; }
|
||||
sat::bool_var bvar() const { return m_bvar; }
|
||||
std::string bvar2string() const;
|
||||
unsigned level(solver& s) const;
|
||||
|
||||
clause* unit_clause() const { return m_unit_clause; }
|
||||
|
|
|
|||
|
|
@ -92,8 +92,48 @@ namespace polysat {
|
|||
return l_false;
|
||||
}
|
||||
|
||||
void ex_polynomial_superposition::reduce_by(pvar v, conflict_core& core) {
|
||||
return;
|
||||
bool progress = true;
|
||||
while (progress) {
|
||||
progress = false;
|
||||
for (auto c : core) {
|
||||
if (is_positive_equality_over(v, c) && reduce_by(v, c, core)) {
|
||||
progress = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool ex_polynomial_superposition::reduce_by(pvar v, signed_constraint eq, conflict_core& core) {
|
||||
pdd p = eq->to_ule().p();
|
||||
for (auto c : core) {
|
||||
if (c == eq)
|
||||
continue;
|
||||
if (c->is_ule()) {
|
||||
auto lhs = c->to_ule().lhs();
|
||||
auto rhs = c->to_ule().rhs();
|
||||
auto a = lhs.reduce(v, p);
|
||||
auto b = rhs.reduce(v, p);
|
||||
if (a == lhs && b == rhs)
|
||||
continue;
|
||||
auto c2 = s().ule(a, b);
|
||||
if (!c.is_positive())
|
||||
c2 = ~c2;
|
||||
vector<signed_constraint> premises;
|
||||
premises.push_back(eq);
|
||||
premises.push_back(c);
|
||||
core.replace(c, c2, premises);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool ex_polynomial_superposition::try_explain(pvar v, conflict_core& core) {
|
||||
LOG_H3("Trying polynomial superposition...");
|
||||
reduce_by(v, core);
|
||||
lbool result = l_undef;
|
||||
while (result == l_undef)
|
||||
result = try_explain1(v, core);
|
||||
|
|
|
|||
|
|
@ -37,6 +37,8 @@ namespace polysat {
|
|||
bool is_positive_equality_over(pvar v, signed_constraint const& c);
|
||||
signed_constraint resolve1(pvar v, signed_constraint c1, signed_constraint c2);
|
||||
signed_constraint find_replacement(signed_constraint c2, pvar v, conflict_core& core);
|
||||
void reduce_by(pvar v, conflict_core& core);
|
||||
bool reduce_by(pvar, signed_constraint c, conflict_core& core);
|
||||
lbool try_explain1(pvar v, conflict_core& core);
|
||||
public:
|
||||
bool try_explain(pvar v, conflict_core& core) override;
|
||||
|
|
|
|||
|
|
@ -42,7 +42,6 @@ namespace polysat {
|
|||
m_conflict(*this),
|
||||
m_bvars(),
|
||||
m_free_pvars(m_activity),
|
||||
m_free_bvars(m_bvars.activity()),
|
||||
m_constraints(m_bvars) {
|
||||
}
|
||||
|
||||
|
|
@ -144,8 +143,9 @@ namespace polysat {
|
|||
if (is_conflict())
|
||||
return; // no need to do anything if we already have a conflict at base level
|
||||
m_constraints.ensure_bvar(c.get());
|
||||
clause* unit = m_constraints.store(clause::from_unit(m_level, c, mk_dep_ref(dep)));
|
||||
c->set_unit_clause(unit);
|
||||
clause_ref unit = clause::from_unit(m_level, c, mk_dep_ref(dep));
|
||||
m_constraints.store(unit.get(), *this);
|
||||
c->set_unit_clause(unit.get());
|
||||
if (dep != null_dependency && !c->is_external()) {
|
||||
m_constraints.register_external(c);
|
||||
m_trail.push_back(trail_instr_t::ext_constraint_i);
|
||||
|
|
@ -203,16 +203,16 @@ namespace polysat {
|
|||
}
|
||||
|
||||
void solver::propagate_watch(sat::literal lit) {
|
||||
LOG("propagate " << lit);
|
||||
auto& wlist = m_bvars.watch(~lit);
|
||||
unsigned end = 0;
|
||||
unsigned j = 0, end = 0;
|
||||
unsigned sz = wlist.size();
|
||||
bool flush = false;
|
||||
for (unsigned j = 0; j < sz && !is_conflict(); ++j) {
|
||||
for (; j < sz && !is_conflict(); ++j) {
|
||||
clause& cl = *wlist[j];
|
||||
SASSERT(cl.size() >= 2);
|
||||
unsigned idx = cl[0] == lit ? 1 : 0;
|
||||
SASSERT(cl[1 - idx] == lit);
|
||||
if (flush || m_bvars.is_true(cl[idx])) {
|
||||
unsigned idx = cl[0] == ~lit ? 1 : 0;
|
||||
SASSERT(cl[1 - idx] == ~lit);
|
||||
if (m_bvars.is_true(cl[idx])) {
|
||||
wlist[end++] = &cl;
|
||||
continue;
|
||||
}
|
||||
|
|
@ -226,15 +226,13 @@ namespace polysat {
|
|||
wlist[end++] = &cl;
|
||||
if (m_bvars.is_false(cl[idx])) {
|
||||
set_conflict(cl);
|
||||
flush = true;
|
||||
continue;
|
||||
++j;
|
||||
break;
|
||||
}
|
||||
unsigned level = 0;
|
||||
for (i = 0; i < cl.size(); ++i)
|
||||
if (cl[i] != lit)
|
||||
level = std::max(level, m_bvars.level(cl[i]));
|
||||
assign_bool(level, cl[1 - idx], &cl, nullptr);
|
||||
assign_bool(level(cl), cl[idx], &cl, nullptr);
|
||||
}
|
||||
for (; j < sz; ++j)
|
||||
wlist[end++] = wlist[j];
|
||||
wlist.shrink(end);
|
||||
}
|
||||
|
||||
|
|
@ -252,7 +250,7 @@ namespace polysat {
|
|||
|
||||
void solver::propagate(sat::literal lit) {
|
||||
LOG_H2("Propagate bool " << lit);
|
||||
signed_constraint c = m_constraints.lookup(lit);
|
||||
signed_constraint c = lit2cnstr(lit);
|
||||
SASSERT(c);
|
||||
activate_constraint(c);
|
||||
propagate_watch(lit);
|
||||
|
|
@ -289,6 +287,8 @@ namespace polysat {
|
|||
}
|
||||
|
||||
void solver::pop_levels(unsigned num_levels) {
|
||||
if (num_levels == 0)
|
||||
return;
|
||||
SASSERT(m_level >= num_levels);
|
||||
unsigned const target_level = m_level - num_levels;
|
||||
vector<sat::literal> replay;
|
||||
|
|
@ -301,10 +301,8 @@ namespace polysat {
|
|||
case trail_instr_t::qhead_i: {
|
||||
pop_qhead();
|
||||
for (unsigned i = m_search.size(); i-- > m_qhead; )
|
||||
if (m_search[i].is_boolean()) {
|
||||
auto c = m_constraints.lookup(m_search[i].lit());
|
||||
deactivate_constraint(c);
|
||||
}
|
||||
if (m_search[i].is_boolean())
|
||||
deactivate_constraint(lit2cnstr(m_search[i].lit()));
|
||||
break;
|
||||
}
|
||||
case trail_instr_t::add_var_i: {
|
||||
|
|
@ -407,8 +405,8 @@ namespace polysat {
|
|||
void solver::decide() {
|
||||
LOG_H2("Decide");
|
||||
SASSERT(can_decide());
|
||||
if (!m_free_bvars.empty())
|
||||
bdecide(m_free_bvars.next_var());
|
||||
if (m_bvars.can_decide())
|
||||
bdecide(m_bvars.next_var());
|
||||
else
|
||||
pdecide(m_free_pvars.next_var());
|
||||
}
|
||||
|
|
@ -434,10 +432,10 @@ namespace polysat {
|
|||
assign_core(v, val, justification::decision(m_level));
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void solver::bdecide(sat::bool_var b) {
|
||||
|
||||
decide_bool(sat::literal(b), nullptr);
|
||||
}
|
||||
|
||||
void solver::assign_core(pvar v, rational const& val, justification const& j) {
|
||||
|
|
@ -467,8 +465,7 @@ namespace polysat {
|
|||
}
|
||||
|
||||
void solver::set_conflict(clause& cl) {
|
||||
for (auto lit : cl)
|
||||
set_conflict(~m_constraints.lookup(lit));
|
||||
m_conflict.set(cl);
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -498,8 +495,6 @@ namespace polysat {
|
|||
|
||||
SASSERT(is_conflict());
|
||||
|
||||
// TODO: subsequent changes to the conflict should update the marks incrementally
|
||||
|
||||
if (m_conflict.conflict_var() != null_var) {
|
||||
// This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
|
||||
resolve_value(m_conflict.conflict_var());
|
||||
|
|
@ -584,12 +579,12 @@ namespace polysat {
|
|||
}
|
||||
|
||||
void solver::learn_lemma(pvar v, clause_ref lemma) {
|
||||
LOG("Learning: " << show_deref(lemma));
|
||||
if (!lemma)
|
||||
return;
|
||||
LOG("Learning: " << show_deref(lemma));
|
||||
SASSERT(lemma->size() > 0);
|
||||
lemma->set_justified_var(v);
|
||||
add_lemma(lemma);
|
||||
add_lemma(*lemma);
|
||||
decide_bool(*lemma);
|
||||
}
|
||||
|
||||
|
|
@ -600,24 +595,24 @@ namespace polysat {
|
|||
LOG("Boolean assignment: " << m_bvars);
|
||||
|
||||
// To make a guess, we need to find an unassigned literal that is not false in the current model.
|
||||
auto is_suitable = [this](sat::literal lit) -> bool {
|
||||
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
|
||||
signed_constraint 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;
|
||||
unsigned num_choices = 0; // TODO: should probably cache this? (or rather the suitability of each literal... it won't change until we backtrack beyond the current point)
|
||||
|
||||
for (sat::literal lit : lemma) {
|
||||
if (is_suitable(lit)) {
|
||||
num_choices++;
|
||||
if (choice == sat::null_literal)
|
||||
choice = lit;
|
||||
switch (m_bvars.value(lit)) {
|
||||
case l_true:
|
||||
return;
|
||||
case l_false:
|
||||
continue;
|
||||
default:
|
||||
if (lit2cnstr(lit).is_currently_false(*this))
|
||||
continue;
|
||||
break;
|
||||
}
|
||||
num_choices++;
|
||||
if (choice == sat::null_literal)
|
||||
choice = lit;
|
||||
}
|
||||
LOG_V("num_choices: " << num_choices);
|
||||
if (choice == sat::null_literal) {
|
||||
|
|
@ -627,13 +622,13 @@ namespace polysat {
|
|||
return;
|
||||
}
|
||||
|
||||
signed_constraint c = m_constraints.lookup(choice);
|
||||
signed_constraint c = lit2cnstr(choice);
|
||||
push_cjust(lemma.justified_var(), c);
|
||||
|
||||
if (num_choices == 1)
|
||||
propagate_bool(choice, &lemma);
|
||||
else
|
||||
decide_bool(choice, lemma);
|
||||
decide_bool(choice, &lemma);
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -710,23 +705,23 @@ namespace polysat {
|
|||
// The lemma where 'lit' comes from.
|
||||
// Currently, boolean decisions always come from guessing a literal of a learned non-unit lemma.
|
||||
clause* lemma = m_bvars.lemma(var); // need to grab this while 'lit' is still assigned
|
||||
SASSERT(lemma);
|
||||
|
||||
backjump(m_bvars.level(var) - 1);
|
||||
|
||||
add_lemma(reason);
|
||||
propagate_bool(~lit, reason.get());
|
||||
add_lemma(*reason);
|
||||
// propagate_bool(~lit, reason.get());
|
||||
if (is_conflict()) {
|
||||
LOG_H1("Conflict during revert_bool_decision/propagate_bool!");
|
||||
return;
|
||||
}
|
||||
decide_bool(*lemma);
|
||||
if (lemma)
|
||||
decide_bool(*lemma);
|
||||
}
|
||||
|
||||
void solver::decide_bool(sat::literal lit, clause& lemma) {
|
||||
void solver::decide_bool(sat::literal lit, clause* lemma) {
|
||||
push_level();
|
||||
LOG_H2("Decide boolean literal " << lit << " @ " << m_level);
|
||||
assign_bool(m_level, lit, nullptr, &lemma);
|
||||
assign_bool(m_level, lit, nullptr, lemma);
|
||||
}
|
||||
|
||||
void solver::propagate_bool(sat::literal lit, clause* reason) {
|
||||
|
|
@ -740,8 +735,19 @@ namespace polysat {
|
|||
assign_bool(level, lit, reason, nullptr);
|
||||
}
|
||||
|
||||
unsigned solver::level(clause const& cl) {
|
||||
unsigned lvl = 0;
|
||||
for (auto lit : cl) {
|
||||
auto c = lit2cnstr(lit);
|
||||
if (m_bvars.is_false(lit) || c.is_currently_false(*this))
|
||||
lvl = std::max(lvl, c.level(*this));
|
||||
}
|
||||
return lvl;
|
||||
}
|
||||
|
||||
/// Assign a boolean literal and put it on the search stack
|
||||
void solver::assign_bool(unsigned level, sat::literal lit, clause* reason, clause* lemma) {
|
||||
SASSERT(!m_bvars.is_true(lit));
|
||||
LOG("Assigning boolean literal: " << lit);
|
||||
m_bvars.assign(lit, level, reason, lemma);
|
||||
m_trail.push_back(trail_instr_t::assign_bool_i);
|
||||
|
|
@ -773,9 +779,7 @@ namespace polysat {
|
|||
|
||||
void solver::backjump(unsigned new_level) {
|
||||
LOG_H3("Backjumping to level " << new_level << " from level " << m_level);
|
||||
unsigned num_levels = m_level - new_level;
|
||||
if (num_levels > 0)
|
||||
pop_levels(num_levels);
|
||||
pop_levels(m_level - new_level);
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -786,30 +790,23 @@ namespace polysat {
|
|||
}
|
||||
|
||||
// Add lemma to storage but do not activate it
|
||||
void solver::add_lemma(clause_ref lemma) {
|
||||
if (!lemma)
|
||||
return;
|
||||
bool non_propagated_literal = false;
|
||||
LOG("Lemma: " << show_deref(lemma));
|
||||
for (sat::literal lit : *lemma) {
|
||||
LOG(" Literal " << lit << " is: " << m_constraints.lookup(lit));
|
||||
signed_constraint c = m_constraints.lookup(lit);
|
||||
void solver::add_lemma(clause& lemma) {
|
||||
|
||||
LOG("Lemma: " << lemma);
|
||||
for (sat::literal lit : lemma) {
|
||||
LOG(" Literal " << lit << " is: " << lit2cnstr(lit));
|
||||
// Check that fully evaluated constraints are on the stack
|
||||
SASSERT(!c.is_currently_true(*this));
|
||||
SASSERT(!lit2cnstr(lit).is_currently_true(*this));
|
||||
// literals that are added from m_conflict.m_vars have not been assigned.
|
||||
// they are false in the current model.
|
||||
if (!m_bvars.is_assigned(lit) && c.is_currently_false(*this)) {
|
||||
non_propagated_literal = true;
|
||||
}
|
||||
// SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_false(*this));
|
||||
// TODO: work out invariant for the lemma. It should be impossible to extend the model in a way that makes the lemma true.
|
||||
}
|
||||
// SASSERT(!non_propagated_literal);
|
||||
SASSERT(lemma->size() > 0);
|
||||
clause* cl = m_constraints.store(std::move(lemma));
|
||||
if (cl->size() == 1) {
|
||||
signed_constraint c = m_constraints.lookup((*cl)[0]);
|
||||
c->set_unit_clause(cl);
|
||||
SASSERT(lemma.size() > 0);
|
||||
m_constraints.store(&lemma, *this);
|
||||
if (lemma.size() == 1) {
|
||||
signed_constraint c = lit2cnstr(lemma[0]);
|
||||
c->set_unit_clause(&lemma);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -854,7 +851,7 @@ namespace polysat {
|
|||
if (item.is_assignment()) {
|
||||
pvar v = item.var();
|
||||
auto j = m_justification[v];
|
||||
out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level();
|
||||
out << "\t" << assignment_pp(*this, v, get_value(v)) << " @" << j.level();
|
||||
if (j.is_propagation())
|
||||
out << " " << m_cjust[v];
|
||||
out << "\n";
|
||||
|
|
@ -869,15 +866,13 @@ namespace polysat {
|
|||
}
|
||||
out << "Constraints:\n";
|
||||
for (auto c : m_constraints)
|
||||
out << "\t" << *c << "\n";
|
||||
out << "\t" << c->bvar2string() << ": " << *c << "\n";
|
||||
out << "Clauses:\n";
|
||||
for (auto cls : m_constraints.clauses()) {
|
||||
for (auto cl : cls) {
|
||||
out << "\t" << *cl << "\n";
|
||||
for (auto lit : *cl) {
|
||||
auto c = m_constraints.lookup(lit);
|
||||
out << "\t\t" << lit << ": " << c << "\n";
|
||||
}
|
||||
for (auto lit : *cl)
|
||||
out << "\t\t" << lit << ": " << lit2cnstr(lit) << "\n";
|
||||
}
|
||||
}
|
||||
return out;
|
||||
|
|
@ -959,7 +954,7 @@ namespace polysat {
|
|||
bool ok = true;
|
||||
for (sat::bool_var v = m_bvars.size(); v-- > 0; ) {
|
||||
sat::literal lit(v);
|
||||
auto c = m_constraints.lookup(lit);
|
||||
auto c = lit2cnstr(lit);
|
||||
if (!std::all_of(c->vars().begin(), c->vars().end(), [&](auto v) { return is_assigned(v); }))
|
||||
continue;
|
||||
ok &= (m_bvars.value(lit) != l_true) || !c.is_currently_false(*this);
|
||||
|
|
@ -979,7 +974,7 @@ namespace polysat {
|
|||
bool all_ok = true;
|
||||
for (auto s : m_search) {
|
||||
if (s.is_boolean()) {
|
||||
bool ok = m_constraints.lookup(s.lit()).is_currently_true(*this);
|
||||
bool ok = lit2cnstr(s.lit()).is_currently_true(*this);
|
||||
LOG((ok ? "PASS" : "FAIL") << ": " << s.lit());
|
||||
all_ok = all_ok && ok;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -76,7 +76,6 @@ namespace polysat {
|
|||
conflict_core m_conflict;
|
||||
bool_var_manager m_bvars; // Map boolean variables to constraints
|
||||
var_queue m_free_pvars; // free poly vars
|
||||
var_queue m_free_bvars; // free Boolean variables
|
||||
stats m_stats;
|
||||
|
||||
uint64_t m_max_conflicts = std::numeric_limits<uint64_t>::max();
|
||||
|
|
@ -155,9 +154,10 @@ namespace polysat {
|
|||
void activate_constraint(signed_constraint c);
|
||||
void deactivate_constraint(signed_constraint c);
|
||||
void decide_bool(clause& lemma);
|
||||
void decide_bool(sat::literal lit, clause& lemma);
|
||||
void decide_bool(sat::literal lit, clause* lemma);
|
||||
void propagate_bool(sat::literal lit, clause* reason);
|
||||
void propagate_bool_at(unsigned level, sat::literal lit, clause* reason);
|
||||
unsigned level(clause const& cl);
|
||||
|
||||
void assign_core(pvar v, rational const& val, justification const& j);
|
||||
bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); }
|
||||
|
|
@ -179,7 +179,7 @@ namespace polysat {
|
|||
void set_conflict(clause& cl);
|
||||
void set_conflict(pvar v);
|
||||
|
||||
bool can_decide() const { return !m_free_pvars.empty() || !m_free_bvars.empty(); }
|
||||
bool can_decide() const { return !m_free_pvars.empty() || m_bvars.can_decide(); }
|
||||
void decide();
|
||||
void pdecide(pvar v);
|
||||
void bdecide(sat::bool_var b);
|
||||
|
|
@ -206,7 +206,7 @@ namespace polysat {
|
|||
void report_unsat();
|
||||
void learn_lemma(pvar v, clause_ref lemma);
|
||||
void backjump(unsigned new_level);
|
||||
void add_lemma(clause_ref lemma);
|
||||
void add_lemma(clause& lemma);
|
||||
|
||||
signed_constraint eq(pdd const& p);
|
||||
signed_constraint diseq(pdd const& p);
|
||||
|
|
@ -218,6 +218,7 @@ namespace polysat {
|
|||
signed_constraint ult(pdd const& p, pdd const& q);
|
||||
signed_constraint sle(pdd const& p, pdd const& q);
|
||||
signed_constraint slt(pdd const& p, pdd const& q);
|
||||
signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); }
|
||||
void ext_constraint(signed_constraint c, unsigned dep, bool activate);
|
||||
static void insert_constraint(signed_constraints& cs, signed_constraint c);
|
||||
void assert_ext_constraint(signed_constraint c);
|
||||
|
|
|
|||
|
|
@ -38,18 +38,11 @@ namespace polysat {
|
|||
else if (status == l_true) out << " <= ";
|
||||
else if (status == l_false) out << " > ";
|
||||
else out << " <=/> ";
|
||||
out << m_rhs;
|
||||
return display_extra(out);
|
||||
return out << m_rhs;
|
||||
}
|
||||
|
||||
std::ostream& ule_constraint::display(std::ostream& out) const {
|
||||
out << m_lhs;
|
||||
if (is_eq())
|
||||
out << " == ";
|
||||
else
|
||||
out << " <= ";
|
||||
out << m_rhs;
|
||||
return display_extra(out);
|
||||
return out << m_lhs << (is_eq() ? " == " : " <= ") << m_rhs;
|
||||
}
|
||||
|
||||
void ule_constraint::narrow(solver& s, bool is_positive) {
|
||||
|
|
|
|||
|
|
@ -867,29 +867,35 @@ namespace polysat {
|
|||
|
||||
|
||||
void tst_polysat() {
|
||||
|
||||
polysat::test_p3();
|
||||
|
||||
polysat::test_l2();
|
||||
|
||||
// polysat::test_subst();
|
||||
// return;
|
||||
// not working
|
||||
// polysat::test_fixed_point_arith_div_mul_inverse();
|
||||
// polysat::test_cjust();
|
||||
polysat::test_monot_bounds_simple(8);
|
||||
return;
|
||||
|
||||
//polysat::test_monot_bounds_simple(8);
|
||||
|
||||
|
||||
// working
|
||||
polysat::test_fixed_point_arith_mul_div_inverse();
|
||||
|
||||
polysat::test_subst();
|
||||
|
||||
polysat::test_monot_bounds(8);
|
||||
|
||||
polysat::test_add_conflicts();
|
||||
polysat::test_wlist();
|
||||
polysat::test_l1();
|
||||
polysat::test_l2();
|
||||
|
||||
polysat::test_l3();
|
||||
polysat::test_l4();
|
||||
polysat::test_l5();
|
||||
polysat::test_p1();
|
||||
polysat::test_p2();
|
||||
polysat::test_p3();
|
||||
|
||||
polysat::test_ineq_basic1();
|
||||
polysat::test_ineq_basic2();
|
||||
polysat::test_ineq_basic3();
|
||||
|
|
@ -897,6 +903,8 @@ void tst_polysat() {
|
|||
polysat::test_ineq_basic5();
|
||||
polysat::test_ineq_basic6();
|
||||
polysat::test_monot_bounds(2);
|
||||
polysat::test_cjust();
|
||||
|
||||
|
||||
// inefficient conflicts:
|
||||
// Takes time: polysat::test_monot_bounds_full();
|
||||
|
|
|
|||
|
|
@ -52,7 +52,7 @@ public:
|
|||
|
||||
void mk_var_eh(var v) {
|
||||
m_queue.reserve(v+1);
|
||||
m_queue.insert(v);
|
||||
unassign_var_eh(v);
|
||||
}
|
||||
|
||||
void del_var_eh(var v) {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue