mirror of
https://github.com/Z3Prover/z3
synced 2025-04-25 10:05:32 +00:00
Add BDD utilities; use them for narrowing/propagation of linear equality constraints (#5192)
* Add a few helper methods for encoding sets of integers as BDDs * Use BDD functions in solver * Add bdd::find_int * Use bdd::find_int in solver * Add narrowing for linear equality constraints * Simplify code for linear propagation * Add test for later * Narrowing can only handle linear constraints with a single variable * Need to push_cjust
This commit is contained in:
Jakob Rath
GitHub
parent
e970fe5034
commit
f72e30e539
10 changed files with 208 additions and 104 deletions
|
|
@ -895,4 +895,81 @@ namespace dd {
|
|||
bdd& bdd::operator=(bdd const& other) { unsigned r1 = root; root = other.root; m->inc_ref(root); m->dec_ref(r1); return *this; }
|
||||
std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); }
|
||||
|
||||
|
||||
bdd bdd_manager::mk_int(rational const& val, unsigned w) {
|
||||
bdd b = mk_true();
|
||||
for (unsigned k = w; k-- > 0;)
|
||||
b &= val.get_bit(k) ? mk_var(k) : mk_nvar(k);
|
||||
return b;
|
||||
}
|
||||
|
||||
bool bdd_manager::contains_int(BDD b, rational const& val, unsigned w) {
|
||||
while (!is_const(b)) {
|
||||
unsigned const var = m_level2var[level(b)];
|
||||
if (var >= w)
|
||||
b = lo(b);
|
||||
else
|
||||
b = val.get_bit(var) ? hi(b) : lo(b);
|
||||
}
|
||||
return is_true(b);
|
||||
}
|
||||
|
||||
find_int_t bdd_manager::find_int(BDD b, unsigned w, rational& val) {
|
||||
val = 0;
|
||||
if (is_false(b))
|
||||
return find_int_t::empty;
|
||||
bool is_unique = true;
|
||||
unsigned num_vars = 0;
|
||||
while (!is_true(b)) {
|
||||
++num_vars;
|
||||
if (!is_false(lo(b)) && !is_false(hi(b)))
|
||||
is_unique = false;
|
||||
if (is_false(lo(b))) {
|
||||
val += rational::power_of_two(var(b));
|
||||
b = hi(b);
|
||||
}
|
||||
else
|
||||
b = lo(b);
|
||||
}
|
||||
is_unique &= (num_vars == w);
|
||||
|
||||
return is_unique ? find_int_t::singleton : find_int_t::multiple;
|
||||
}
|
||||
|
||||
bdd bdd_manager::mk_affine(rational const& a, rational const& b, unsigned w) {
|
||||
if (a.is_zero())
|
||||
return b.is_zero() ? mk_true() : mk_false();
|
||||
// a*x + b == 0 (mod 2^w)
|
||||
unsigned const rank_a = a.trailing_zeros();
|
||||
unsigned const rank_b = b.is_zero() ? w : b.trailing_zeros();
|
||||
// We have a', b' odd such that:
|
||||
// 2^rank(a) * a'* x + 2^rank(b) * b' == 0 (mod 2^w)
|
||||
if (rank_a > rank_b) {
|
||||
// <=> 2^(rank(a)-rank(b)) * a' * x + b' == 0 (mod 2^(w-rank(b)))
|
||||
// LHS is always odd => equation cannot be true
|
||||
return mk_false();
|
||||
}
|
||||
else if (b.is_zero()) {
|
||||
// this is just a specialization of the else-branch below
|
||||
return mk_int(rational::zero(), w - rank_a);
|
||||
}
|
||||
else {
|
||||
unsigned const j = w - rank_a;
|
||||
// Let b'' := 2^(rank(b)-rank(a)) * b', then we have:
|
||||
// <=> a' * x + b'' == 0 (mod 2^j)
|
||||
// <=> x == -b'' * inverse_j(a') (mod 2^j)
|
||||
// Now the question is, for what x in Z_{2^w} does this hold?
|
||||
// Answer: for all x where the lower j bits are the same as in the RHS of the last equation,
|
||||
// so we just fix those bits and leave the others unconstrained
|
||||
// (which we can do simply by encoding the RHS as a j-width integer).
|
||||
rational const pow2_rank_a = rational::power_of_two(rank_a);
|
||||
rational const aa = a / pow2_rank_a; // a'
|
||||
rational const bb = b / pow2_rank_a; // b''
|
||||
rational inv_aa;
|
||||
VERIFY(aa.mult_inverse(j, inv_aa));
|
||||
rational const cc = mod(inv_aa * -bb, rational::power_of_two(j));
|
||||
return mk_int(cc, j);
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -21,11 +21,14 @@ Revision History:
|
|||
#include "util/vector.h"
|
||||
#include "util/map.h"
|
||||
#include "util/small_object_allocator.h"
|
||||
#include "util/rational.h"
|
||||
|
||||
namespace dd {
|
||||
|
||||
class bdd;
|
||||
|
||||
enum class find_int_t { empty, singleton, multiple };
|
||||
|
||||
class bdd_manager {
|
||||
friend bdd;
|
||||
|
||||
|
|
@ -189,6 +192,9 @@ namespace dd {
|
|||
bdd mk_or(bdd const& a, bdd const& b);
|
||||
bdd mk_xor(bdd const& a, bdd const& b);
|
||||
|
||||
bool contains_int(BDD b, rational const& val, unsigned w);
|
||||
find_int_t find_int(BDD b, unsigned w, rational& val);
|
||||
|
||||
void reserve_var(unsigned v);
|
||||
bool well_formed();
|
||||
|
||||
|
|
@ -219,6 +225,20 @@ namespace dd {
|
|||
bdd mk_forall(unsigned v, bdd const& b);
|
||||
bdd mk_ite(bdd const& c, bdd const& t, bdd const& e);
|
||||
|
||||
/** Encodes the lower w bits of val as BDD, using variable indices 0 to w-1.
|
||||
* The least-significant bit is encoded as variable 0.
|
||||
* val must be an integer.
|
||||
*/
|
||||
bdd mk_int(rational const& val, unsigned w);
|
||||
|
||||
/** Encodes the solutions of the affine relation
|
||||
*
|
||||
* a*x + b == 0 (mod 2^w)
|
||||
*
|
||||
* as BDD.
|
||||
*/
|
||||
bdd mk_affine(rational const& a, rational const& b, unsigned w);
|
||||
|
||||
std::ostream& display(std::ostream& out);
|
||||
std::ostream& display(std::ostream& out, bdd const& b);
|
||||
|
||||
|
|
@ -256,6 +276,12 @@ namespace dd {
|
|||
double cnf_size() const { return m->cnf_size(root); }
|
||||
double dnf_size() const { return m->dnf_size(root); }
|
||||
unsigned bdd_size() const { return m->bdd_size(*this); }
|
||||
|
||||
/** Checks whether the integer val is contained in the BDD when viewed as set of integers (see also mk_int). */
|
||||
bool contains_int(rational const& val, unsigned w) { return m->contains_int(root, val, w); }
|
||||
|
||||
/** Returns an integer contained in the BDD, if any, and whether the BDD is a singleton. */
|
||||
find_int_t find_int(unsigned w, rational& val) { return m->find_int(root, w, val); }
|
||||
};
|
||||
|
||||
std::ostream& operator<<(std::ostream& out, bdd const& b);
|
||||
|
|
|
|||
|
|
@ -36,7 +36,6 @@ namespace polysat {
|
|||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
LOG("Assignments: " << s.m_search);
|
||||
auto q = p().subst_val(s.m_search);
|
||||
|
|
@ -52,71 +51,24 @@ namespace polysat {
|
|||
|
||||
// at most one variable remains unassigned.
|
||||
auto other_var = vars()[1 - idx];
|
||||
SASSERT(!q.is_val() && q.var() == other_var);
|
||||
|
||||
// Detect and apply unit propagation.
|
||||
|
||||
if (!q.is_linear())
|
||||
return false;
|
||||
|
||||
// a*x + b == 0
|
||||
rational a = q.hi().val();
|
||||
rational b = q.lo().val();
|
||||
rational inv_a;
|
||||
if (a.is_odd()) {
|
||||
// v1 = -b * inverse(a)
|
||||
unsigned sz = q.power_of_2();
|
||||
VERIFY(a.mult_inverse(sz, inv_a));
|
||||
rational val = mod(inv_a * -b, rational::power_of_two(sz));
|
||||
s.m_cjust[other_var].push_back(this);
|
||||
s.propagate(other_var, val, *this);
|
||||
return false;
|
||||
}
|
||||
|
||||
SASSERT(!b.is_odd()); // otherwise p.is_never_zero() would have been true above
|
||||
|
||||
// TBD
|
||||
// constrain viable using condition on x
|
||||
// 2*x + 2 == 0 mod 4 => x is odd
|
||||
//
|
||||
// We have:
|
||||
// 2^j*a'*x + 2^j*b' == 0 mod m, where a' is odd (but not necessarily b')
|
||||
// <=> 2^j*(a'*x + b') == 0 mod m
|
||||
// <=> a'*x + b' == 0 mod (m-j)
|
||||
// <=> x == -b' * inverse_{m-j}(a') mod (m-j)
|
||||
// ( <=> 2^j*x == 2^j * -b' * inverse_{m-j}(a') mod m )
|
||||
//
|
||||
// x == c mod (m-j)
|
||||
// Which x in 2^m satisfy this?
|
||||
// => x \in { c + k * 2^(m-j) | k = 0, ..., 2^j - 1 }
|
||||
unsigned rank_a = a.trailing_zeros(); // j
|
||||
SASSERT(b == 0 || rank_a <= b.trailing_zeros());
|
||||
rational aa = a / rational::power_of_two(rank_a); // a'
|
||||
rational bb = b / rational::power_of_two(rank_a); // b'
|
||||
rational inv_aa;
|
||||
unsigned small_sz = q.power_of_2() - rank_a; // m - j
|
||||
VERIFY(aa.mult_inverse(small_sz, inv_aa));
|
||||
rational cc = mod(inv_aa * -bb, rational::power_of_two(small_sz));
|
||||
LOG(m_vars[other_var] << " = " << cc << " + k * 2^" << small_sz);
|
||||
// TODO: better way to update the BDD, e.g. construct new one (only if rank_a is small?)
|
||||
vector<rational> viable;
|
||||
for (rational k = rational::zero(); k < rational::power_of_two(rank_a); k += 1) {
|
||||
rational val = cc + k * rational::power_of_two(small_sz);
|
||||
viable.push_back(val);
|
||||
}
|
||||
LOG_V("still viable: " << viable);
|
||||
unsigned i = 0;
|
||||
for (rational r = rational::zero(); r < rational::power_of_two(q.power_of_2()); r += 1) {
|
||||
while (i < viable.size() && viable[i] < r)
|
||||
++i;
|
||||
if (i < viable.size() && viable[i] == r)
|
||||
continue;
|
||||
if (s.is_viable(other_var, r)) {
|
||||
s.add_non_viable(other_var, r);
|
||||
if (try_narrow_with(q, s)) {
|
||||
rational val;
|
||||
switch (s.find_viable(other_var, val)) {
|
||||
case dd::find_int_t::empty:
|
||||
s.set_conflict(*this);
|
||||
return false;
|
||||
case dd::find_int_t::singleton:
|
||||
s.propagate(other_var, val, *this);
|
||||
return false;
|
||||
case dd::find_int_t::multiple:
|
||||
/* do nothing */
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
LOG("TODO");
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
|
|
@ -137,10 +89,23 @@ namespace polysat {
|
|||
return nullptr;
|
||||
}
|
||||
|
||||
bool eq_constraint::try_narrow_with(pdd const& q, solver& s) {
|
||||
if (q.is_linear() && q.free_vars().size() == 1) {
|
||||
// a*x + b == 0
|
||||
pvar v = q.var();
|
||||
rational a = q.hi().val();
|
||||
rational b = q.lo().val();
|
||||
bdd xs = s.m_bdd.mk_affine(a, b, s.size(v));
|
||||
s.intersect_viable(v, xs);
|
||||
s.push_cjust(v, this);
|
||||
return true;
|
||||
}
|
||||
// TODO: what other constraints can be extracted cheaply?
|
||||
return false;
|
||||
}
|
||||
|
||||
void eq_constraint::narrow(solver& s) {
|
||||
if (!p().is_linear())
|
||||
return;
|
||||
// TODO apply affine constraints and other that can be extracted cheaply
|
||||
(void)try_narrow_with(p(), s);
|
||||
}
|
||||
|
||||
bool eq_constraint::is_always_false() {
|
||||
|
|
|
|||
|
|
@ -35,6 +35,7 @@ namespace polysat {
|
|||
bool is_always_false() override;
|
||||
bool is_currently_false(solver& s) override;
|
||||
void narrow(solver& s) override;
|
||||
bool try_narrow_with(pdd const& q, solver& s);
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -30,44 +30,23 @@ namespace polysat {
|
|||
}
|
||||
|
||||
bool solver::is_viable(pvar v, rational const& val) {
|
||||
bdd b = m_viable[v];
|
||||
for (unsigned k = size(v); k-- > 0 && !b.is_false(); )
|
||||
b &= val.get_bit(k) ? m_bdd.mk_var(k) : m_bdd.mk_nvar(k);
|
||||
return !b.is_false();
|
||||
return m_viable[v].contains_int(val, size(v));
|
||||
}
|
||||
|
||||
void solver::add_non_viable(pvar v, rational const& val) {
|
||||
LOG("pvar " << v << " /= " << val);
|
||||
TRACE("polysat", tout << "v" << v << " /= " << val << "\n";);
|
||||
bdd value = m_bdd.mk_true();
|
||||
for (unsigned k = size(v); k-- > 0; )
|
||||
value &= val.get_bit(k) ? m_bdd.mk_var(k) : m_bdd.mk_nvar(k);
|
||||
SASSERT((value && !m_viable[v]).is_false());
|
||||
push_viable(v);
|
||||
m_viable[v] &= !value;
|
||||
SASSERT(is_viable(v, val));
|
||||
intersect_viable(v, !m_bdd.mk_int(val, size(v)));
|
||||
}
|
||||
|
||||
lbool solver::find_viable(pvar v, rational & val) {
|
||||
val = 0;
|
||||
bdd viable = m_viable[v];
|
||||
if (viable.is_false())
|
||||
return l_false;
|
||||
bool is_unique = true;
|
||||
unsigned num_vars = 0;
|
||||
while (!viable.is_true()) {
|
||||
++num_vars;
|
||||
if (!viable.lo().is_false() && !viable.hi().is_false())
|
||||
is_unique = false;
|
||||
if (viable.lo().is_false()) {
|
||||
val += rational::power_of_two(viable.var());
|
||||
viable = viable.hi();
|
||||
}
|
||||
else
|
||||
viable = viable.lo();
|
||||
}
|
||||
is_unique &= num_vars == size(v);
|
||||
TRACE("polysat", tout << "v" << v << " := " << val << " unique " << is_unique << "\n";);
|
||||
return is_unique ? l_true : l_undef;
|
||||
void solver::intersect_viable(pvar v, bdd vals) {
|
||||
push_viable(v);
|
||||
m_viable[v] &= vals;
|
||||
}
|
||||
|
||||
dd::find_int_t solver::find_viable(pvar v, rational & val) {
|
||||
return m_viable[v].find_int(size(v), val);
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -312,15 +291,15 @@ namespace polysat {
|
|||
IF_LOGGING(log_viable(v));
|
||||
rational val;
|
||||
switch (find_viable(v, val)) {
|
||||
case l_false:
|
||||
case dd::find_int_t::empty:
|
||||
LOG("Conflict: no value for pvar " << v);
|
||||
set_conflict(v);
|
||||
break;
|
||||
case l_true:
|
||||
case dd::find_int_t::singleton:
|
||||
LOG("Propagation: pvar " << v << " := " << val << " (due to unique value)");
|
||||
assign_core(v, val, justification::propagation(m_level));
|
||||
break;
|
||||
case l_undef:
|
||||
case dd::find_int_t::multiple:
|
||||
LOG("Decision: pvar " << v << " := " << val);
|
||||
push_level();
|
||||
assign_core(v, val, justification::decision(m_level));
|
||||
|
|
|
|||
|
|
@ -111,6 +111,11 @@ namespace polysat {
|
|||
*/
|
||||
void add_non_viable(pvar v, rational const& val);
|
||||
|
||||
/**
|
||||
* Register all values that are not contained in vals as non-viable.
|
||||
*/
|
||||
void intersect_viable(pvar v, bdd vals);
|
||||
|
||||
/**
|
||||
* Add dependency for variable viable range.
|
||||
*/
|
||||
|
|
@ -119,11 +124,8 @@ namespace polysat {
|
|||
|
||||
/**
|
||||
* Find a next viable value for variable.
|
||||
* l_false - there are no viable values.
|
||||
* l_true - there is only one viable value left.
|
||||
* l_undef - there are multiple viable values, return a guess
|
||||
*/
|
||||
lbool find_viable(pvar v, rational & val);
|
||||
dd::find_int_t find_viable(pvar v, rational & val);
|
||||
|
||||
/** Log all viable values for the given variable.
|
||||
* (Inefficient, but useful for debugging small instances.)
|
||||
|
|
|
|||
|
|
@ -73,6 +73,46 @@ namespace dd {
|
|||
std::cout << c1 << "\n";
|
||||
std::cout << c1.bdd_size() << "\n";
|
||||
}
|
||||
|
||||
static void test_int() {
|
||||
unsigned const w = 3; // bit width
|
||||
bdd_manager m(w);
|
||||
vector<bdd> num;
|
||||
for (unsigned n = 0; n < (1<<w); ++n)
|
||||
num.push_back(m.mk_int(rational(n), w));
|
||||
for (unsigned k = 0; k < (1 << w); ++k)
|
||||
for (unsigned n = 0; n < (1 << w); ++n)
|
||||
SASSERT(num[k].contains_int(rational(n), w) == (n == k));
|
||||
bdd s0127 = num[0] || num[1] || num[2] || num[7];
|
||||
SASSERT(s0127.contains_int(rational(0), w));
|
||||
SASSERT(s0127.contains_int(rational(1), w));
|
||||
SASSERT(s0127.contains_int(rational(2), w));
|
||||
SASSERT(!s0127.contains_int(rational(3), w));
|
||||
SASSERT(!s0127.contains_int(rational(4), w));
|
||||
SASSERT(!s0127.contains_int(rational(5), w));
|
||||
SASSERT(!s0127.contains_int(rational(6), w));
|
||||
SASSERT(s0127.contains_int(rational(7), w));
|
||||
bdd s123 = num[1] || num[2] || num[3];
|
||||
SASSERT((s0127 && s123) == (num[1] || num[2]));
|
||||
|
||||
// larger width constrains additional bits
|
||||
SASSERT(m.mk_int(rational(6), 3) != m.mk_int(rational(6), 4));
|
||||
|
||||
// 4*x + 2 == 0 (mod 2^3) has no solutions
|
||||
SASSERT(m.mk_affine(rational(4), rational(2), 3).is_false());
|
||||
// 3*x + 2 == 0 (mod 2^3) has the unique solution 2
|
||||
SASSERT(m.mk_affine(rational(3), rational(2), 3) == num[2]);
|
||||
// 2*x + 2 == 0 (mod 2^3) has the solutions 3, 7
|
||||
SASSERT(m.mk_affine(rational(2), rational(2), 3) == (num[3] || num[7]));
|
||||
// 12*x + 8 == 0 (mod 2^4) has the solutions 2, 6, 10, 14
|
||||
bdd expected = m.mk_int(rational(2), 4) || m.mk_int(rational(6), 4) || m.mk_int(rational(10), 4) || m.mk_int(rational(14), 4);
|
||||
SASSERT(m.mk_affine(rational(12), rational(8), 4) == expected);
|
||||
|
||||
SASSERT(m.mk_affine(rational(0), rational(0), 3).is_true());
|
||||
SASSERT(m.mk_affine(rational(0), rational(1), 3).is_false());
|
||||
// 2*x == 0 (mod 2^3) has the solutions 0, 4
|
||||
SASSERT(m.mk_affine(rational(2), rational(0), 3) == (num[0] || num[4]));
|
||||
}
|
||||
}
|
||||
|
||||
void tst_bdd() {
|
||||
|
|
@ -80,4 +120,5 @@ void tst_bdd() {
|
|||
dd::test2();
|
||||
dd::test3();
|
||||
dd::test4();
|
||||
dd::test_int();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -141,6 +141,19 @@ namespace polysat {
|
|||
s.check();
|
||||
}
|
||||
|
||||
// Goal: we probably mix up polysat variables and PDD variables at several points; try to uncover such cases
|
||||
// NOTE: actually, add_var seems to keep them in sync, so this is not an issue at the moment (but we should still test it later)
|
||||
// static void test_mixed_vars() {
|
||||
// scoped_solver s;
|
||||
// auto a = s.var(s.add_var(2));
|
||||
// auto b = s.var(s.add_var(4));
|
||||
// auto c = s.var(s.add_var(2));
|
||||
// s.add_eq(a + 2*c + 4);
|
||||
// s.add_eq(3*b + 4);
|
||||
// s.check();
|
||||
// // Expected result:
|
||||
// }
|
||||
|
||||
// convert assertions into internal solver state
|
||||
// support small grammar of formulas.
|
||||
void internalize(solver& s, expr_ref_vector& fmls) {
|
||||
|
|
|
|||
|
|
@ -130,7 +130,7 @@ bool rational::limit_denominator(rational &num, rational const& limit) {
|
|||
return false;
|
||||
}
|
||||
|
||||
bool rational::mult_inverse(unsigned num_bits, rational & result) {
|
||||
bool rational::mult_inverse(unsigned num_bits, rational & result) const {
|
||||
rational const& n = *this;
|
||||
if (n.is_one()) {
|
||||
result = n;
|
||||
|
|
|
|||
|
|
@ -343,7 +343,7 @@ public:
|
|||
return m().is_power_of_two(m_val, shift);
|
||||
}
|
||||
|
||||
bool mult_inverse(unsigned num_bits, rational & result);
|
||||
bool mult_inverse(unsigned num_bits, rational & result) const;
|
||||
|
||||
static rational const & zero() {
|
||||
return m_zero;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue