mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

Separate constraint creation from activation; add sign/polarity to constraints (#5217)

Browse source 
* Separate constraint creation from activation

* Basic recursive handling of disjunctive lemmas for unit tests

* Set learned constraint to true immediately

* Preliminary support for negated constraints
This commit is contained in:
Jakob Rath 2021-04-26 18:55:58 +02:00 • committed by GitHub
parent 2fac9e6e66
commit 9e505d60f0
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
12 changed files with 244 additions and 73 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -29,16 +29,16 @@ namespace polysat {
return *dynamic_cast<eq_constraint const*>(this);
}
constraint* constraint::eq(unsigned lvl, pdd const& p, p_dependency_ref& d) {
return alloc(eq_constraint, lvl, p, d);
constraint* constraint::eq(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref& d) {
return alloc(eq_constraint, lvl, bvar, sign, p, d);
}
constraint* constraint::viable(unsigned lvl, pvar v, bdd const& b, p_dependency_ref& d) {
return alloc(var_constraint, lvl, v, b, d);
constraint* constraint::viable(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const& b, p_dependency_ref& d) {
return alloc(var_constraint, lvl, bvar, sign, v, b, d);
}
constraint* constraint::ule(unsigned lvl, pdd const& a, pdd const& b, p_dependency_ref& d) {
return alloc(ule_constraint, lvl, a, b, d);
constraint* constraint::ule(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref& d) {
return alloc(ule_constraint, lvl, bvar, sign, a, b, d);
}
}

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

@ -17,6 +17,7 @@ Author:
namespace polysat {
enum ckind_t { eq_t, ule_t, sle_t, bit_t };
enum csign_t : bool { neg_t = false, pos_t = true };
class eq_constraint;
class var_constraint;
@ -30,12 +31,15 @@ namespace polysat {
ckind_t m_kind;
p_dependency_ref m_dep;
unsigned_vector m_vars;
constraint(unsigned lvl, p_dependency_ref& dep, ckind_t k):
m_level(lvl), m_kind(k), m_dep(dep) {}
bool_var m_bool_var;
csign_t m_sign; ///< sign/polarity
lbool m_status = l_undef; ///< current constraint status, computed from value of m_bool_var and m_sign
constraint(unsigned lvl, bool_var bvar, csign_t sign, p_dependency_ref& dep, ckind_t k):
m_level(lvl), m_kind(k), m_dep(dep), m_bool_var(bvar), m_sign(sign) {}
public:
static constraint* eq(unsigned lvl, pdd const& p, p_dependency_ref& d);
static constraint* viable(unsigned lvl, pvar v, bdd const& b, p_dependency_ref& d);
static constraint* ule(unsigned lvl, pdd const& a, pdd const& b, p_dependency_ref& d);
static constraint* eq(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref& d);
static constraint* viable(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const& b, p_dependency_ref& d);
static constraint* ule(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref& d);
virtual ~constraint() {}
bool is_eq() const { return m_kind == ckind_t::eq_t; }
bool is_ule() const { return m_kind == ckind_t::ule_t; }
@ -46,12 +50,18 @@ namespace polysat {
virtual constraint* resolve(solver& s, pvar v) = 0;
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;
eq_constraint& to_eq();
eq_constraint const& to_eq() const;
p_dependency* dep() const { return m_dep; }
unsigned_vector& vars() { return m_vars; }
unsigned level() const { return m_level; }
bool_var bvar() const { return m_bool_var; }
bool sign() const { return m_sign; }
void assign_eh(bool is_true) { m_status = (is_true ^ !m_sign) ? l_true : l_false; }
bool is_positive() const { return m_status == l_true; }
bool is_negative() const { return m_status == l_false; }
};
inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }

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

@ -19,7 +19,7 @@ Author:
namespace polysat {
std::ostream& eq_constraint::display(std::ostream& out) const {
return out << p() << " == 0";
return out << p() << (sign() == pos_t ? " == 0" : " != 0") << " [" << m_status << "]";
}
bool eq_constraint::propagate(solver& s, pvar v) {
@ -43,9 +43,56 @@ namespace polysat {
}
constraint* eq_constraint::resolve(solver& s, pvar v) {
if (is_positive())
return eq_resolve(s, v);
if (is_negative())
return diseq_resolve(s, v);
UNREACHABLE();
}
void eq_constraint::narrow(solver& s) {
if (is_positive())
eq_narrow(s);
if (is_negative())
diseq_narrow(s);
}
bool eq_constraint::is_always_false() {
if (is_positive())
return p().is_never_zero();
if (is_negative())
return p().is_zero();
UNREACHABLE();
}
bool eq_constraint::is_currently_false(solver& s) {
pdd r = p().subst_val(s.m_search);
if (is_positive())
return r.is_never_zero();
if (is_negative())
return r.is_zero();
UNREACHABLE();
}
bool eq_constraint::is_currently_true(solver& s) {
pdd r = p().subst_val(s.m_search);
if (is_positive())
return r.is_zero();
if (is_negative())
return r.is_never_zero();
UNREACHABLE();
}
/**
* Equality constraints
*/
constraint* eq_constraint::eq_resolve(solver& s, pvar v) {
SASSERT(is_currently_true(s));
if (s.m_conflict.size() != 1)
return nullptr;
constraint* c = s.m_conflict[0];
SASSERT(c->is_currently_false(s));
if (c->is_eq()) {
pdd a = c->to_eq().p();
pdd b = p();
@ -54,12 +101,14 @@ namespace polysat {
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 constraint::eq(lvl, r, d);
constraint* lemma = constraint::eq(lvl, s.m_next_bvar++, pos_t, r, d);
lemma->assign_eh(true);
return lemma;
}
return nullptr;
}
void eq_constraint::narrow(solver& s) {
void eq_constraint::eq_narrow(solver& s) {
LOG("Assignment: " << s.m_search);
auto q = p().subst_val(s.m_search);
LOG("Substituted: " << p() << " := " << q);
@ -92,13 +141,17 @@ namespace polysat {
// TODO: what other constraints can be extracted cheaply?
}
bool eq_constraint::is_always_false() {
return p().is_never_zero();
/**
* Disequality constraints
*/
constraint* eq_constraint::diseq_resolve(solver& s, pvar v) {
NOT_IMPLEMENTED_YET();
}
bool eq_constraint::is_currently_false(solver& s) {
pdd r = p().subst_val(s.m_search);
return r.is_never_zero();
void eq_constraint::diseq_narrow(solver& s) {
NOT_IMPLEMENTED_YET();
}
}

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

@ -20,8 +20,8 @@ namespace polysat {
class eq_constraint : public constraint {
pdd m_poly;
public:
eq_constraint(unsigned lvl, pdd const& p, p_dependency_ref& dep):
constraint(lvl, dep, ckind_t::eq_t), m_poly(p) {
eq_constraint(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref& dep):
constraint(lvl, bvar, sign, dep, ckind_t::eq_t), m_poly(p) {
m_vars.append(p.free_vars());
}
~eq_constraint() override {}
@ -31,7 +31,14 @@ namespace polysat {
constraint* 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;
private:
constraint* eq_resolve(solver& s, pvar v);
void eq_narrow(solver& s);
constraint* diseq_resolve(solver& s, pvar v);
void diseq_narrow(solver& s);
};
}

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

@ -148,58 +148,76 @@ namespace polysat {
m_free_vars.del_var_eh(v);
}
void solver::add_constraint(constraint* c) {
void solver::new_constraint(constraint* c) {
SASSERT(c);
LOG("Adding constraint: " << *c);
LOG("New constraint: " << *c);
m_constraints.push_back(c);
c->narrow(*this);
SASSERT(!get_bv2c(c->bvar()));
insert_bv2c(c->bvar(), c);
}
void solver::add_eq(pdd const& p, unsigned dep) {
bool_var solver::new_eq(pdd const& p, unsigned dep) {
p_dependency_ref d(mk_dep(dep), m_dm);
constraint* c = constraint::eq(m_level, p, d);
add_watch(*c);
add_constraint(c);
constraint* c = constraint::eq(m_level, m_next_bvar++, pos_t, p, d);
new_constraint(c);
return c->bvar();
}
void solver::add_diseq(pdd const& p, unsigned dep) {
if (p.is_val()) {
if (!p.is_zero())
return;
// set conflict.
NOT_IMPLEMENTED_YET();
return;
}
bool_var solver::new_diseq(pdd const& p, unsigned dep) {
// if (p.is_val()) {
// if (!p.is_zero())
// return;
// // set conflict.
// NOT_IMPLEMENTED_YET(); // TODO: not here, only when activated
// return;
// }
unsigned sz = size(p.var());
auto slack = add_var(sz);
auto q = p + var(slack);
add_eq(q, dep);
auto non_zero = sz2bits(sz).non_zero();
p_dependency_ref d(mk_dep(dep), m_dm);
constraint* c = constraint::viable(m_level, slack, non_zero, d);
add_constraint(c);
constraint* c = constraint::viable(m_level, m_next_bvar++, pos_t, slack, non_zero, d);
new_constraint(c);
return c->bvar();
}
void solver::add_ule(pdd const& p, pdd const& q, unsigned dep) {
bool_var solver::new_ule(pdd const& p, pdd const& q, unsigned dep, csign_t sign) {
p_dependency_ref d(mk_dep(dep), m_dm);
constraint* c = constraint::ule(m_level, p, q, d);
constraint* c = constraint::ule(m_level, m_next_bvar++, sign, p, q, d);
new_constraint(c);
return c->bvar();
}
bool_var solver::new_sle(pdd const& p, pdd const& q, unsigned dep, csign_t sign) {
auto shift = rational::power_of_two(p.power_of_2() - 1);
return new_ule(p + shift, q + shift, dep, sign);
}
bool_var solver::new_ult(pdd const& p, pdd const& q, unsigned dep) {
return new_ule(q, p, dep, neg_t);
}
bool_var solver::new_slt(pdd const& p, pdd const& q, unsigned dep) {
return new_sle(q, p, dep, neg_t);
}
void solver::add_eq(pdd const& p, unsigned dep) { assign_eh(new_eq(p, dep), true); }
void solver::add_diseq(pdd const& p, unsigned dep) { assign_eh(new_diseq(p, dep), true); }
void solver::add_ule(pdd const& p, pdd const& q, unsigned dep) { assign_eh(new_ule(p, q, dep), true); }
void solver::add_ult(pdd const& p, pdd const& q, unsigned dep) { assign_eh(new_ult(p, q, dep), true); }
void solver::add_sle(pdd const& p, pdd const& q, unsigned dep) { assign_eh(new_sle(p, q, dep), true); }
void solver::add_slt(pdd const& p, pdd const& q, unsigned dep) { assign_eh(new_slt(p, q, dep), true); }
void solver::assign_eh(bool_var v, bool is_true) {
constraint* c = get_bv2c(v);
if (!c) {
LOG("WARN: there is no constraint for bool_var " << v);
return;
}
c->assign_eh(is_true);
add_watch(*c);
add_constraint(c);
}
void solver::add_sle(pdd const& p, pdd const& q, unsigned dep) {
// save for later
NOT_IMPLEMENTED_YET();
}
void solver::add_ult(pdd const& p, pdd const& q, unsigned dep) {
// save for later
NOT_IMPLEMENTED_YET();
}
void solver::add_slt(pdd const& p, pdd const& q, unsigned dep) {
// save for later
NOT_IMPLEMENTED_YET();
c->narrow(*this);
}
@ -566,6 +584,8 @@ namespace polysat {
if (!c)
return;
LOG("Lemma: " << *c);
SASSERT(!get_bv2c(c->bvar()));
insert_bv2c(c->bvar(), c);
add_watch(*c);
m_redundant.push_back(c);
for (unsigned i = m_redundant.size() - 1; i-- > 0; ) {

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

@ -65,6 +65,13 @@ namespace polysat {
scoped_ptr_vector<constraint> m_constraints;
scoped_ptr_vector<constraint> m_redundant;
// Map boolean variables to constraints
bool_var m_next_bvar = 2; // TODO: later, bool vars come from external supply
ptr_vector<constraint> m_bv2constraint;
void insert_bv2c(bool_var bv, constraint* c) { m_bv2constraint.setx(bv, c, nullptr); }
void erase_bv2c(bool_var bv) { m_bv2constraint[bv] = nullptr; }
constraint* get_bv2c(bool_var bv) const { return m_bv2constraint.get(bv, nullptr); }
// Per variable information
vector<bdd> m_viable; // set of viable values.
vector<rational> m_value; // assigned value
@ -204,7 +211,7 @@ namespace polysat {
void backjump(unsigned new_level);
void add_lemma(constraint* c);
void add_constraint(constraint* c);
void new_constraint(constraint* c);
bool invariant();
bool invariant(scoped_ptr_vector<constraint> const& cs);
@ -222,9 +229,20 @@ namespace polysat {
/**
* End-game satisfiability checker.
*
* Returns l_undef if the search cannot proceed.
* Possible reasons:
* - Resource limits are exhausted.
* - A disjunctive lemma should be learned. The disjunction needs to be handled externally.
*/
lbool check_sat();
/**
* Returns the disjunctive lemma that should be learned,
* or an empty vector if check_sat() terminated for a different reason.
*/
bool_var_vector get_lemma() { NOT_IMPLEMENTED_YET(); return {}; };
/**
* retrieve unsat core dependencies
*/
@ -241,10 +259,17 @@ namespace polysat {
pdd var(pvar v) { return m_vars[v]; }
/**
* Add polynomial constraints
* Create polynomial constraints (but do not activate them).
* Each constraint is tracked by a dependency.
* assign sets the 'index'th bit of var.
*/
bool_var new_eq(pdd const& p, unsigned dep = null_dependency);
bool_var new_diseq(pdd const& p, unsigned dep = null_dependency);
bool_var new_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency, csign_t sign = pos_t);
bool_var new_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency);
bool_var new_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency, csign_t sign = pos_t);
bool_var new_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency);
/** Create and activate polynomial constraints. */
void add_eq(pdd const& p, unsigned dep = null_dependency);
void add_diseq(pdd const& p, unsigned dep = null_dependency);
void add_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency);
@ -252,6 +277,11 @@ namespace polysat {
void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency);
void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency);
/**
* Activate the constraint corresponding to the given boolean variable.
* Note: to deactivate, use push/pop.
*/
void assign_eh(bool_var v, bool is_true);
/**
* main state transitions.
@ -264,7 +294,7 @@ namespace polysat {
* Adds so-called user-scope.
*/
void push();
void pop(unsigned num_scopes);
void pop(unsigned num_scopes = 1);
std::ostream& display(std::ostream& out) const;

3
src/math/polysat/types.h
View file

@ -51,4 +51,7 @@ namespace polysat {
typedef obj_ref<p_dependency, poly_dep_manager> p_dependency_ref;
typedef ref_vector<p_dependency, poly_dep_manager> p_dependency_refv;
typedef int bool_var; // see smt_types.h
typedef svector<bool_var> bool_var_vector; // see smt_types.h
}

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

@ -19,7 +19,7 @@ Author:
namespace polysat {
std::ostream& ule_constraint::display(std::ostream& out) const {
return out << m_lhs << " <=u " << m_rhs;
return out << m_lhs << (sign() == pos_t ? " <=u " : " >u ") << m_rhs << " [" << m_status << "]";
}
bool ule_constraint::propagate(solver& s, pvar v) {
@ -57,7 +57,8 @@ namespace polysat {
return;
}
if (p.is_val() && q.is_val()) {
SASSERT(p.val() <= q.val());
SASSERT(!is_positive() || p.val() <= q.val());
SASSERT(!is_negative() || p.val() > q.val());
return;
}
@ -89,7 +90,9 @@ namespace polysat {
}
if (v != null_var) {
bddv const& x = s.var2bits(v).var();
bdd xs = (a * x + b <= c * x + d);
bddv l = a * x + b;
bddv r = c * x + d;
bdd xs = is_positive() ? (l <= r) : (l > r);
s.push_cjust(v, this);
s.intersect_viable(v, xs);
@ -106,7 +109,11 @@ namespace polysat {
bool ule_constraint::is_always_false(pdd const& lhs, pdd const& rhs) {
// TODO: other conditions (e.g. when forbidden interval would be full)
return lhs.is_val() && rhs.is_val() && !(lhs.val() <= rhs.val());
if (is_positive())
return lhs.is_val() && rhs.is_val() && !(lhs.val() <= rhs.val());
if (is_negative())
return lhs.is_val() && rhs.is_val() && !(lhs.val() > rhs.val());
UNREACHABLE();
}
bool ule_constraint::is_always_false() {
@ -119,4 +126,14 @@ namespace polysat {
return is_always_false(p, q);
}
bool ule_constraint::is_currently_true(solver& s) {
auto p = lhs().subst_val(s.m_search);
auto q = rhs().subst_val(s.m_search);
if (is_positive())
return p.is_val() && q.is_val() && p.val() <= q.val();
if (is_negative())
return p.is_val() && q.is_val() && p.val() > q.val();
UNREACHABLE();
}
}

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

@ -21,8 +21,8 @@ namespace polysat {
pdd m_lhs;
pdd m_rhs;
public:
ule_constraint(unsigned lvl, pdd const& l, pdd const& r, p_dependency_ref& dep):
constraint(lvl, dep, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
ule_constraint(unsigned lvl, bool_var bvar, csign_t sign, pdd const& l, pdd const& r, p_dependency_ref& dep):
constraint(lvl, bvar, sign, dep, 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))
@ -34,9 +34,10 @@ namespace polysat {
std::ostream& display(std::ostream& out) const override;
bool propagate(solver& s, pvar v) override;
constraint* resolve(solver& s, pvar v) override;
static bool is_always_false(pdd const& lhs, pdd const& rhs);
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;
};

4
src/math/polysat/var_constraint.cpp
View file

@ -39,6 +39,10 @@ namespace polysat {
return s.m_viable[m_var].is_false();
}
bool var_constraint::is_currently_true(solver& s) {
return !s.m_viable[m_var].is_false();
}
void var_constraint::narrow(solver& s) {
s.intersect_viable(m_var, m_viable);
}

5
src/math/polysat/var_constraint.h
View file

@ -29,8 +29,8 @@ namespace polysat {
pvar m_var;
bdd m_viable;
public:
var_constraint(unsigned lvl, pvar v, bdd const & b, p_dependency_ref& dep):
constraint(lvl, dep, ckind_t::bit_t), m_var(v), m_viable(b) {}
var_constraint(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const & b, p_dependency_ref& dep):
constraint(lvl, bvar, sign, dep, ckind_t::bit_t), m_var(v), m_viable(b) {}
~var_constraint() override {}
std::ostream& display(std::ostream& out) const override;
bool propagate(solver& s, pvar v) override;
@ -38,5 +38,6 @@ namespace polysat {
void narrow(solver& s) override;
bool is_always_false() override;
bool is_currently_false(solver& s) override;
bool is_currently_true(solver& s) override;
};
}

33
src/test/polysat.cpp
View file

@ -12,8 +12,33 @@ namespace polysat {
struct scoped_solver : public solver_scope, public solver {
scoped_solver(): solver(lim) {}
lbool check_rec() {
lbool result = check_sat();
if (result != l_undef)
return result;
auto const& new_lemma = get_lemma();
// Empty lemma => check_sat() terminated for another reason, e.g., resource limits
if (new_lemma.empty())
return l_undef;
for (auto lit : new_lemma) {
push();
assign_eh(lit, true);
result = check_rec();
pop();
// Found a model => done
if (result == l_true)
return l_true;
if (result == l_undef)
return l_undef;
// Unsat => try next literal
SASSERT(result == l_false);
}
// No literal worked? unsat
return l_false;
}
void check() {
std::cout << check_sat() << "\n";
std::cout << check_rec() << "\n";
statistics st;
collect_statistics(st);
std::cout << st << "\n";
@ -113,9 +138,9 @@ namespace polysat {
auto v = s.var(s.add_var(5));
auto q = s.var(s.add_var(5));
auto r = s.var(s.add_var(5));
s.add_eq(u - (v*q) - r, 0);
s.add_ult(r, u, 0);
s.add_ult(u, v*q, 0);
s.add_eq(u - (v*q) - r);
s.add_ult(r, u);
s.add_ult(u, v*q);
s.check();
}