mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 11:42:28 +00:00
Add functionality for BDD vectors (#5198)
* Fix XOR over BDDs * Add operator<< for find_int_t * Add equality assertion macro that prints expression values on failure * Adapt contains_int and find_int to take externally-defined bits * Add more operations on BDD vectors * Remove old functions * Additional bddv functions * Rename some things * Make bddv a class and add operators * Fix find_num/contains_num calls
This commit is contained in:
Jakob Rath
GitHub
parent
981839ee73
commit
4da1b7b03c
8 changed files with 499 additions and 138 deletions
|
|
@ -23,6 +23,19 @@ Revision History:
|
|||
|
||||
namespace dd {
|
||||
|
||||
std::ostream& operator<<(std::ostream& out, find_result x) {
|
||||
switch (x) {
|
||||
case find_result::empty:
|
||||
return out << "empty";
|
||||
case find_result::singleton:
|
||||
return out << "singleton";
|
||||
case find_result::multiple:
|
||||
return out << "multiple";
|
||||
}
|
||||
UNREACHABLE();
|
||||
return out;
|
||||
}
|
||||
|
||||
bdd_manager::bdd_manager(unsigned num_vars) {
|
||||
m_cost_metric = bdd_cost;
|
||||
m_cost_bdd = 0;
|
||||
|
|
@ -142,6 +155,8 @@ namespace dd {
|
|||
if (a == b) return false_bdd;
|
||||
if (is_false(a)) return b;
|
||||
if (is_false(b)) return a;
|
||||
if (is_true(a)) return mk_not_rec(b);
|
||||
if (is_true(b)) return mk_not_rec(a);
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
|
|
@ -896,87 +911,54 @@ namespace dd {
|
|||
std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); }
|
||||
|
||||
|
||||
// NSB code review:
|
||||
// this function should be removed and replaced by functionality where the
|
||||
// client maintains what are the variables.
|
||||
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) {
|
||||
bool bdd_manager::contains_num(BDD b, rational const& val, unsigned_vector const& bits) {
|
||||
DEBUG_CODE(for (unsigned i = 1; i < bits.size(); ++i) { SASSERT(bits[i-1] < bits[i]); });
|
||||
unsigned var_idx = bits.size();
|
||||
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);
|
||||
VERIFY(var_idx-- > 0);
|
||||
SASSERT(var(b) <= bits[var_idx]);
|
||||
while (var(b) < bits[var_idx]) {
|
||||
VERIFY(var_idx-- > 0);
|
||||
}
|
||||
SASSERT(var(b) == bits[var_idx]);
|
||||
b = val.get_bit(var_idx) ? hi(b) : lo(b);
|
||||
}
|
||||
return is_true(b);
|
||||
}
|
||||
|
||||
find_int_t bdd_manager::find_int(BDD b, unsigned w, rational& val) {
|
||||
find_result bdd_manager::find_num(BDD b, unsigned_vector bits, rational& val) {
|
||||
DEBUG_CODE(for (unsigned i = 1; i < bits.size(); ++i) { SASSERT(bits[i-1] < bits[i]); });
|
||||
val = 0;
|
||||
if (is_false(b))
|
||||
return find_int_t::empty;
|
||||
return find_result::empty;
|
||||
bool is_unique = true;
|
||||
unsigned num_vars = 0;
|
||||
unsigned var_idx = bits.size();
|
||||
while (!is_true(b)) {
|
||||
++num_vars;
|
||||
VERIFY(var_idx-- > 0);
|
||||
SASSERT(var(b) <= bits[var_idx]);
|
||||
while (var(b) < bits[var_idx]) {
|
||||
is_unique = false;
|
||||
VERIFY(var_idx-- > 0);
|
||||
}
|
||||
if (!is_false(lo(b)) && !is_false(hi(b)))
|
||||
is_unique = false;
|
||||
if (is_false(lo(b))) {
|
||||
val += rational::power_of_two(var(b));
|
||||
SASSERT(var(b) == bits[var_idx]);
|
||||
val += rational::power_of_two(var_idx);
|
||||
b = hi(b);
|
||||
}
|
||||
else
|
||||
b = lo(b);
|
||||
}
|
||||
is_unique &= (num_vars == w);
|
||||
if (var_idx > 0)
|
||||
is_unique = false;
|
||||
|
||||
return is_unique ? find_int_t::singleton : find_int_t::multiple;
|
||||
return is_unique ? find_result::singleton : find_result::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);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
bdd bdd_manager::mk_eq(bddv const& a, bddv const& b) {
|
||||
SASSERT(a.size() == b.size());
|
||||
bdd eq = mk_true();
|
||||
for (unsigned i = a.size(); i-- > 0; ) {
|
||||
eq &= !(a[i] ^ b[i]);
|
||||
|
|
@ -1014,13 +996,132 @@ namespace dd {
|
|||
bdd bdd_manager::mk_ult(bddv const& a, bddv const& b) { return mk_ule(a, b) && !mk_eq(a, b); }
|
||||
bdd bdd_manager::mk_ugt(bddv const& a, bddv const& b) { return mk_ult(b, a); }
|
||||
|
||||
bdd_manager::bddv bdd_manager::mk_add(bddv const& a, bddv const& b) {
|
||||
bddv bdd_manager::mk_add(bddv const& a, bddv const& b) {
|
||||
SASSERT(a.size() == b.size());
|
||||
bdd carry = mk_false();
|
||||
bddv result;
|
||||
bddv result(this);
|
||||
#if 0
|
||||
for (unsigned i = 0; i < a.size(); ++i) {
|
||||
carry = (carry && a[i]) || (carry && b[i]) || (a[i] && b[i]);
|
||||
result.push_back(carry ^ a[i] ^ b[i]);
|
||||
carry = (carry && a[i]) || (carry && b[i]) || (a[i] && b[i]);
|
||||
}
|
||||
#else
|
||||
if (a.size() > 0) {
|
||||
result.push_back(a[0] ^ b[0]);
|
||||
}
|
||||
for (unsigned i = 1; i < a.size(); ++i) {
|
||||
carry = (carry && a[i-1]) || (carry && b[i-1]) || (a[i-1] && b[i-1]);
|
||||
result.push_back(carry ^ a[i] ^ b[i]);
|
||||
}
|
||||
#endif
|
||||
return result;
|
||||
}
|
||||
|
||||
void bdd_manager::bddv_shl(bddv &a) {
|
||||
for (unsigned j = a.size(); j-- > 1; ) {
|
||||
a[j] = a[j - 1];
|
||||
}
|
||||
a[0] = mk_false();
|
||||
}
|
||||
|
||||
bddv bdd_manager::mk_mul(bddv const& a, bddv const& b) {
|
||||
SASSERT(a.size() == b.size());
|
||||
bddv a_shifted = a;
|
||||
bddv result = mk_zero(a.size());
|
||||
for (unsigned i = 0; i < b.size(); ++i) {
|
||||
#if 1
|
||||
bddv s = a_shifted;
|
||||
for (unsigned j = i; j < b.size(); ++j) {
|
||||
s[j] &= b[i];
|
||||
}
|
||||
result = mk_add(result, s);
|
||||
#else
|
||||
// From BuDDy's bvec_mul. It seems to compute more intermediate BDDs than the version above?
|
||||
bddv added = mk_add(result, a_shifted);
|
||||
for (unsigned j = 0; j < result.size(); ++j) {
|
||||
result[j] = mk_ite(b[i], added[j], result[j]);
|
||||
}
|
||||
#endif
|
||||
bddv_shl(a_shifted);
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
template <class GetBitFn>
|
||||
bddv bdd_manager::mk_mul(bddv const& a, GetBitFn get_bit) {
|
||||
bddv a_shifted = a;
|
||||
bddv result = mk_zero(a.size());
|
||||
for (unsigned i = 0; i < a.size(); ++i) {
|
||||
if (get_bit(i)) {
|
||||
result = mk_add(result, a_shifted);
|
||||
}
|
||||
bddv_shl(a_shifted);
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
bddv bdd_manager::mk_mul(bddv const& a, rational const& val) {
|
||||
SASSERT(val.is_int() && val >= 0 && val < rational::power_of_two(a.size()));
|
||||
return mk_mul(a, [val](unsigned i) { return val.get_bit(i); });
|
||||
}
|
||||
|
||||
bddv bdd_manager::mk_mul(bddv const& a, bool_vector const& b) {
|
||||
SASSERT(a.size() == b.size());
|
||||
return mk_mul(a, [b](unsigned i) { return b[i]; });
|
||||
}
|
||||
|
||||
bddv bdd_manager::mk_num(rational const& n, unsigned num_bits) {
|
||||
SASSERT(n.is_int() && n >= 0 && n < rational::power_of_two(num_bits));
|
||||
bddv result(this);
|
||||
for (unsigned i = 0; i < num_bits; ++i) {
|
||||
result.push_back(n.get_bit(i) ? mk_true() : mk_false());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
bddv bdd_manager::mk_ones(unsigned num_bits) {
|
||||
bddv result(this);
|
||||
for (unsigned i = 0; i < num_bits; ++i) {
|
||||
result.push_back(mk_true());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
bddv bdd_manager::mk_zero(unsigned num_bits) {
|
||||
bddv result(this);
|
||||
for (unsigned i = 0; i < num_bits; ++i) {
|
||||
result.push_back(mk_false());
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
bddv bdd_manager::mk_var(unsigned num_bits, unsigned const* vars) {
|
||||
bddv result(this);
|
||||
for (unsigned i = 0; i < num_bits; ++i) {
|
||||
result.push_back(mk_var(vars[i]));
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
bddv bdd_manager::mk_var(unsigned_vector const& vars) {
|
||||
return mk_var(vars.size(), vars.data());
|
||||
}
|
||||
|
||||
bool bdd_manager::is_constv(bddv const& a) {
|
||||
for (bdd const& bit : a.bits)
|
||||
if (!is_const(bit.root))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
rational bdd_manager::to_val(bddv const& a) {
|
||||
rational result = rational::zero();
|
||||
for (unsigned i = 0; i < a.size(); ++i) {
|
||||
bdd const &bit = a[i];
|
||||
SASSERT(is_const(bit.root));
|
||||
if (bit.is_true()) {
|
||||
result += rational::power_of_two(i);
|
||||
}
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
|
@ -1030,16 +1131,8 @@ namespace dd {
|
|||
bdd bdd_manager::mk_sge(bddv const& a, bddv const& b) { return mk_sle(b, a); }
|
||||
bdd bdd_manager::mk_slt(bddv const& a, bddv const& b) { return mk_sle(a, b) && !mk_eq(a, b); }
|
||||
bdd bdd_manager::mk_sgt(bddv const& a, bddv const& b) { return mk_slt(b, a); }
|
||||
bdd_manager::bddv bdd_manager::mk_num(rational const& n, unsigned num_bits);
|
||||
bdd_manager::bddv bdd_manager::mk_ones(unsigned num_bits);
|
||||
bdd_manager::bddv bdd_manager::mk_zero(unsigned num_bits);
|
||||
bdd_manager::bddv bdd_manager::mk_var(unsigned num_bits, unsigned const* vars);
|
||||
bdd_manager::bddv bdd_manager::mk_var(unsigned_vector const& vars);
|
||||
bdd_manager::bddv bdd_manager::mk_sub(bddv const& a, bddv const& b);
|
||||
bdd_manager::bddv bdd_manager::mk_mul(bddv const& a, bddv const& b);
|
||||
bdd_manager::bddv bdd_manager::mk_mul(bddv const& a, bool_vector const& b);
|
||||
void bdd_manager::mk_quot_rem(bddv const& a, bddv const& b, bddv& quot, bddv& rem);
|
||||
rational bdd_manager::to_val(bddv const& a);
|
||||
#endif
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -26,13 +26,17 @@ Revision History:
|
|||
namespace dd {
|
||||
|
||||
class bdd;
|
||||
class bddv;
|
||||
|
||||
enum class find_int_t { empty, singleton, multiple };
|
||||
enum class find_result { empty, singleton, multiple };
|
||||
std::ostream& operator<<(std::ostream& out, find_result x);
|
||||
|
||||
class bdd_manager {
|
||||
friend bdd;
|
||||
friend bddv;
|
||||
|
||||
typedef unsigned BDD;
|
||||
typedef svector<BDD> BDDV;
|
||||
|
||||
const BDD null_bdd = UINT_MAX;
|
||||
|
||||
|
|
@ -192,9 +196,6 @@ 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();
|
||||
|
||||
|
|
@ -205,6 +206,12 @@ namespace dd {
|
|||
~scoped_push() { m.m_bdd_stack.shrink(m_size); }
|
||||
};
|
||||
|
||||
bool contains_num(BDD b, rational const& val, unsigned_vector const& bits);
|
||||
find_result find_num(BDD b, unsigned_vector bits, rational& val);
|
||||
|
||||
void bddv_shl(bddv& a);
|
||||
template <class GetBitFn> bddv mk_mul(bddv const& a, GetBitFn get_bit);
|
||||
|
||||
public:
|
||||
struct mem_out {};
|
||||
|
||||
|
|
@ -225,8 +232,10 @@ namespace dd {
|
|||
bdd mk_forall(unsigned v, bdd const& b);
|
||||
bdd mk_ite(bdd const& c, bdd const& t, bdd const& e);
|
||||
|
||||
/* BDD vector operations */
|
||||
typedef vector<bdd> bddv;
|
||||
/* BDD vector operations
|
||||
* - Fixed-width arithmetic, i.e., modulo 2^size
|
||||
* - The lowest index is the LSB
|
||||
*/
|
||||
bdd mk_ule(bddv const& a, bddv const& b);
|
||||
bdd mk_uge(bddv const& a, bddv const& b); // { return mk_ule(b, a); }
|
||||
bdd mk_ult(bddv const& a, bddv const& b); // { return mk_ule(a, b) && !mk_eq(a, b); }
|
||||
|
|
@ -247,23 +256,10 @@ namespace dd {
|
|||
bddv mk_sub(bddv const& a, bddv const& b);
|
||||
bddv mk_mul(bddv const& a, bddv const& b);
|
||||
bddv mk_mul(bddv const& a, bool_vector const& b);
|
||||
bddv mk_mul(bddv const& a, rational const& val);
|
||||
void mk_quot_rem(bddv const& a, bddv const& b, bddv& quot, bddv& rem);
|
||||
rational to_val(bddv const& a);
|
||||
|
||||
|
||||
/** 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);
|
||||
bool is_constv(bddv const& a);
|
||||
rational to_val(bddv const& a);
|
||||
|
||||
std::ostream& display(std::ostream& out);
|
||||
std::ostream& display(std::ostream& out, bdd const& b);
|
||||
|
|
@ -303,17 +299,102 @@ namespace dd {
|
|||
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). */
|
||||
// NSB code review: this API needs to be changed: bit-position to variable mapping is external
|
||||
bool contains_int(rational const& val, unsigned w) { return m->contains_int(root, val, w); }
|
||||
/** Checks whether the integer val is contained in the BDD when viewed as set of integers.
|
||||
*
|
||||
* Preconditions:
|
||||
* - bits are sorted in ascending order,
|
||||
* - the bdd only contains variables from bits.
|
||||
*/
|
||||
bool contains_num(rational const& val, unsigned_vector const& bits) const { return m->contains_num(root, val, bits); }
|
||||
|
||||
/** Returns an integer contained in the BDD, if any, and whether the BDD is a singleton. */
|
||||
// NSB code review: this API needs to be changed: bit-position to variable mapping is external
|
||||
find_int_t find_int(unsigned w, rational& val) { return m->find_int(root, w, val); }
|
||||
/** Returns an integer contained in the BDD, if any, and whether the BDD is a singleton.
|
||||
*
|
||||
* Preconditions:
|
||||
* - bits are sorted in ascending order,
|
||||
* - the bdd only contains variables from bits.
|
||||
*/
|
||||
find_result find_num(unsigned_vector const& bits, rational& val) const { return m->find_num(root, bits, val); }
|
||||
};
|
||||
|
||||
std::ostream& operator<<(std::ostream& out, bdd const& b);
|
||||
|
||||
class bddv {
|
||||
friend bdd_manager;
|
||||
|
||||
// TODO: currently we repeat the pointer to the manager in every entry of bits.
|
||||
// Should use BDDV instead (drawback: the functions in bdd_manager aren't as nice and they need to be careful about reference counting if they work with BDD directly).
|
||||
vector<bdd> bits;
|
||||
bdd_manager& m;
|
||||
|
||||
bddv(vector<bdd> bits, bdd_manager* m): bits(bits), m(*m) { inc_bits_ref(); }
|
||||
bddv(vector<bdd>&& bits, bdd_manager* m): bits(std::move(bits)), m(*m) { inc_bits_ref(); }
|
||||
void inc_bits_ref() {
|
||||
// NOTE: necessary if we switch to BDDV as storage
|
||||
// for (BDD b : bits) { m.inc_ref(b); }
|
||||
}
|
||||
|
||||
// NOTE: these should probably be removed if we switch to BDDV
|
||||
bddv(bdd_manager* m): bits(), m(*m) { }
|
||||
bdd const& operator[](unsigned i) const { return bits[i]; }
|
||||
bdd& operator[](unsigned i) { return bits[i]; }
|
||||
void push_back(bdd const& a) { bits.push_back(a); }
|
||||
void push_back(bdd&& a) { bits.push_back(a); }
|
||||
public:
|
||||
bddv(bddv const& other): bits(other.bits), m(other.m) { inc_bits_ref(); }
|
||||
bddv(bddv&& other): bits(), m(other.m) { std::swap(bits, other.bits); }
|
||||
bddv& operator=(bddv const& other) {
|
||||
if (this != &other) {
|
||||
bddv old(std::move(*this));
|
||||
bits = other.bits;
|
||||
inc_bits_ref();
|
||||
}
|
||||
return *this;
|
||||
}
|
||||
bddv& operator=(bddv&& other) {
|
||||
if (this != &other) {
|
||||
bddv old(std::move(*this));
|
||||
SASSERT(bits.empty());
|
||||
std::swap(bits, other.bits);
|
||||
}
|
||||
return *this;
|
||||
}
|
||||
~bddv() {
|
||||
// NOTE: necessary if we switch to BDDV as storage
|
||||
// for (BDD b : bits) { m.dec_ref(b); }
|
||||
}
|
||||
|
||||
unsigned size() const { return bits.size(); }
|
||||
vector<bdd> const& get_bits() const { return bits; }
|
||||
|
||||
bdd operator<=(bddv const& other) const { return m.mk_ule(*this, other); }
|
||||
bdd operator>=(bddv const& other) const { return m.mk_uge(*this, other); }
|
||||
bdd operator<(bddv const& other) const { return m.mk_ult(*this, other); }
|
||||
bdd operator>(bddv const& other) const { return m.mk_ugt(*this, other); }
|
||||
// TODO: what about the signed versions?
|
||||
// bdd mk_sle(bddv const& a, bddv const& b);
|
||||
// bdd mk_sge(bddv const& a, bddv const& b); // { return mk_sle(b, a); }
|
||||
// bdd mk_slt(bddv const& a, bddv const& b); // { return mk_sle(a, b) && !mk_eq(a, b); }
|
||||
// bdd mk_sgt(bddv const& a, bddv const& b); // { return mk_slt(b, a); }
|
||||
|
||||
bdd operator==(bddv const& other) const { return m.mk_eq(*this, other); }
|
||||
bdd operator==(rational const& other) const { return m.mk_eq(*this, other); }
|
||||
bdd operator!=(bddv const& other) const { return !m.mk_eq(*this, other); }
|
||||
bdd operator!=(rational const& other) const { return !m.mk_eq(*this, other); }
|
||||
bddv operator+(bddv const& other) const { return m.mk_add(*this, other); }
|
||||
bddv operator+(rational const& other) const { return m.mk_add(*this, m.mk_num(other, size())); }
|
||||
bddv operator-(bddv const& other) const { return m.mk_sub(*this, other); }
|
||||
bddv operator*(bddv const& other) const { return m.mk_mul(*this, other); }
|
||||
bddv operator*(rational const& other) const { return m.mk_mul(*this, other); }
|
||||
bddv operator*(bool_vector const& other) const { return m.mk_mul(*this, other); }
|
||||
|
||||
// void mk_quot_rem(bddv const& a, bddv const& b, bddv& quot, bddv& rem);
|
||||
|
||||
bool is_const() const { return m.is_constv(*this); }
|
||||
rational to_val() const { return m.to_val(*this); }
|
||||
};
|
||||
|
||||
inline bddv operator*(rational const& r, bddv const& a) { return a * r; }
|
||||
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -57,13 +57,13 @@ namespace polysat {
|
|||
if (try_narrow_with(q, s)) {
|
||||
rational val;
|
||||
switch (s.find_viable(other_var, val)) {
|
||||
case dd::find_int_t::empty:
|
||||
case dd::find_result::empty:
|
||||
s.set_conflict(*this);
|
||||
return false;
|
||||
case dd::find_int_t::singleton:
|
||||
case dd::find_result::singleton:
|
||||
s.propagate(other_var, val, *this);
|
||||
return false;
|
||||
case dd::find_int_t::multiple:
|
||||
case dd::find_result::multiple:
|
||||
/* do nothing */
|
||||
break;
|
||||
}
|
||||
|
|
@ -95,7 +95,8 @@ namespace polysat {
|
|||
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));
|
||||
bddv const& x = s.m_bdd.mk_var(s.sz2bits(s.size(v)));
|
||||
bdd xs = (a * x + b == rational(0));
|
||||
s.intersect_viable(v, xs);
|
||||
s.push_cjust(v, this);
|
||||
return true;
|
||||
|
|
|
|||
|
|
@ -29,20 +29,20 @@ namespace polysat {
|
|||
return *m_pdd[sz];
|
||||
}
|
||||
|
||||
vector<bdd>& solver::sz2bits(unsigned sz) {
|
||||
unsigned_vector const& solver::sz2bits(unsigned sz) {
|
||||
m_bits.reserve(sz + 1);
|
||||
auto* bits = m_bits[sz];
|
||||
if (!bits) {
|
||||
m_bits.set(sz, alloc(vector<bdd>));
|
||||
m_bits.set(sz, alloc(unsigned_vector));
|
||||
bits = m_bits[sz];
|
||||
for (unsigned i = 0; i < sz; ++i)
|
||||
bits->push_back(m_bdd.mk_var(i));
|
||||
bits->push_back(i);
|
||||
}
|
||||
return *bits;
|
||||
}
|
||||
|
||||
bool solver::is_viable(pvar v, rational const& val) {
|
||||
return m_viable[v].contains_int(val, size(v));
|
||||
return m_viable[v].contains_num(val, sz2bits(size(v)));
|
||||
}
|
||||
|
||||
void solver::add_non_viable(pvar v, rational const& val) {
|
||||
|
|
@ -60,8 +60,8 @@ namespace polysat {
|
|||
set_conflict(v);
|
||||
}
|
||||
|
||||
dd::find_int_t solver::find_viable(pvar v, rational & val) {
|
||||
return m_viable[v].find_int(size(v), val);
|
||||
dd::find_result solver::find_viable(pvar v, rational & val) {
|
||||
return m_viable[v].find_num(sz2bits(size(v)), val);
|
||||
}
|
||||
|
||||
solver::solver(reslimit& lim):
|
||||
|
|
@ -323,15 +323,15 @@ namespace polysat {
|
|||
IF_LOGGING(log_viable(v));
|
||||
rational val;
|
||||
switch (find_viable(v, val)) {
|
||||
case dd::find_int_t::empty:
|
||||
case dd::find_result::empty:
|
||||
LOG("Conflict: no value for pvar " << v);
|
||||
set_conflict(v);
|
||||
break;
|
||||
case dd::find_int_t::singleton:
|
||||
case dd::find_result::singleton:
|
||||
LOG("Propagation: pvar " << v << " := " << val << " (due to unique value)");
|
||||
assign_core(v, val, justification::propagation(m_level));
|
||||
break;
|
||||
case dd::find_int_t::multiple:
|
||||
case dd::find_result::multiple:
|
||||
LOG("Decision: pvar " << v << " := " << val);
|
||||
push_level();
|
||||
assign_core(v, val, justification::decision(m_level));
|
||||
|
|
|
|||
|
|
@ -45,7 +45,7 @@ namespace polysat {
|
|||
|
||||
reslimit& m_lim;
|
||||
scoped_ptr_vector<dd::pdd_manager> m_pdd;
|
||||
scoped_ptr_vector<vector<bdd>> m_bits;
|
||||
scoped_ptr_vector<unsigned_vector> m_bits;
|
||||
dd::bdd_manager m_bdd;
|
||||
dep_value_manager m_value_manager;
|
||||
small_object_allocator m_alloc;
|
||||
|
|
@ -132,7 +132,7 @@ namespace polysat {
|
|||
/**
|
||||
* Find a next viable value for variable.
|
||||
*/
|
||||
dd::find_int_t find_viable(pvar v, rational & val);
|
||||
dd::find_result find_viable(pvar v, rational & val);
|
||||
|
||||
/** Log all viable values for the given variable.
|
||||
* (Inefficient, but useful for debugging small instances.)
|
||||
|
|
@ -147,7 +147,7 @@ namespace polysat {
|
|||
void del_var();
|
||||
|
||||
dd::pdd_manager& sz2pdd(unsigned sz);
|
||||
vector<bdd>& sz2bits(unsigned sz);
|
||||
unsigned_vector const& sz2bits(unsigned sz);
|
||||
|
||||
void push_level();
|
||||
void pop_levels(unsigned num_levels);
|
||||
|
|
|
|||
|
|
@ -26,6 +26,7 @@ namespace polysat {
|
|||
class solver;
|
||||
typedef dd::pdd pdd;
|
||||
typedef dd::bdd bdd;
|
||||
typedef dd::bddv bddv;
|
||||
typedef unsigned pvar;
|
||||
|
||||
const unsigned null_dependency = UINT_MAX;
|
||||
|
|
|
|||
226
src/test/bdd.cpp
226
src/test/bdd.cpp
|
|
@ -74,44 +74,217 @@ namespace dd {
|
|||
std::cout << c1.bdd_size() << "\n";
|
||||
}
|
||||
|
||||
static void test_xor() {
|
||||
bdd_manager m(4);
|
||||
bdd v0 = m.mk_var(0);
|
||||
bdd v1 = m.mk_var(0);
|
||||
SASSERT((m.mk_false() ^ v0) == v0);
|
||||
SASSERT((v0 ^ m.mk_false()) == v0);
|
||||
SASSERT((m.mk_true() ^ v0) == !v0);
|
||||
SASSERT((v0 ^ m.mk_true()) == !v0);
|
||||
SASSERT((v0 ^ v1) == ((v0 && !v1) || (!v0 && v1)));
|
||||
}
|
||||
|
||||
static void test_bddv_ops_on_constants() {
|
||||
unsigned const num_bits = 4;
|
||||
rational const modulus = rational::power_of_two(num_bits);
|
||||
bdd_manager m(num_bits);
|
||||
|
||||
SASSERT_EQ(m.to_val(m.mk_zero(num_bits)), rational(0));
|
||||
SASSERT_EQ(m.to_val(m.mk_ones(num_bits)), modulus - 1);
|
||||
|
||||
for (unsigned n = 0; n < 16; ++n) {
|
||||
rational const nr(n);
|
||||
SASSERT_EQ(m.to_val(m.mk_num(nr, num_bits)), nr);
|
||||
}
|
||||
|
||||
for (unsigned n = 0; n < 16; ++n) {
|
||||
for (unsigned k = 0; k < 16; ++k) {
|
||||
rational const nr(n);
|
||||
rational const kr(k);
|
||||
bddv const nv = m.mk_num(nr, num_bits);
|
||||
bddv const kv = m.mk_num(kr, num_bits);
|
||||
SASSERT_EQ((nv + kv).to_val(), (nr + kr) % modulus);
|
||||
SASSERT_EQ((nv * kr).to_val(), (nr * kr) % modulus);
|
||||
SASSERT_EQ((nv * kv).to_val(), (nr * kr) % modulus);
|
||||
bdd eq = m.mk_eq(nv, kv);
|
||||
SASSERT((eq.is_true() || eq.is_false()) && (eq.is_true() == (n == k)));
|
||||
eq = m.mk_eq(nv, kr);
|
||||
SASSERT((eq.is_true() || eq.is_false()) && (eq.is_true() == (n == k)));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
static void test_bddv_eqfind_small() {
|
||||
bdd_manager m(4);
|
||||
unsigned_vector bits;
|
||||
bits.push_back(0);
|
||||
bddv const x = m.mk_var(bits);
|
||||
bddv const one = m.mk_num(rational(1), bits.size());
|
||||
bdd x_is_one = m.mk_eq(x, one);
|
||||
std::cout << "x_is_one:\n" << x_is_one << "\n";
|
||||
rational r;
|
||||
auto res = x_is_one.find_num(bits, r);
|
||||
SASSERT_EQ(res, find_result::singleton);
|
||||
SASSERT_EQ(r, rational(1));
|
||||
}
|
||||
|
||||
static void test_bddv_eqfind() {
|
||||
unsigned const num_bits = 4;
|
||||
bdd_manager m(num_bits);
|
||||
|
||||
unsigned_vector bits;
|
||||
bits.push_back(0);
|
||||
bits.push_back(1);
|
||||
bits.push_back(4);
|
||||
bits.push_back(27);
|
||||
|
||||
bddv const x = m.mk_var(bits);
|
||||
bddv const zero = m.mk_zero(num_bits);
|
||||
bddv const one = m.mk_num(rational(1), num_bits);
|
||||
bddv const five = m.mk_num(rational(5), num_bits);
|
||||
|
||||
SASSERT(m.mk_eq(one, rational(1)).is_true());
|
||||
SASSERT(m.mk_eq(five, rational(5)).is_true());
|
||||
SASSERT(m.mk_eq(five, rational(4)).is_false());
|
||||
SASSERT(m.mk_eq(five, five).is_true());
|
||||
SASSERT(m.mk_eq(five, one).is_false());
|
||||
|
||||
{
|
||||
bdd const x_is_five = m.mk_eq(x, rational(5));
|
||||
rational r;
|
||||
auto res = x_is_five.find_num(bits, r);
|
||||
SASSERT_EQ(res, find_result::singleton);
|
||||
SASSERT_EQ(r, rational(5));
|
||||
}
|
||||
|
||||
{
|
||||
bdd const x_is_five = m.mk_eq(bits, rational(5));
|
||||
rational r;
|
||||
auto res = x_is_five.find_num(bits, r);
|
||||
SASSERT_EQ(res, find_result::singleton);
|
||||
SASSERT_EQ(r, rational(5));
|
||||
}
|
||||
|
||||
{
|
||||
bdd const x_is_five = m.mk_eq(x, five);
|
||||
rational r;
|
||||
auto res = x_is_five.find_num(bits, r);
|
||||
SASSERT_EQ(res, find_result::singleton);
|
||||
SASSERT_EQ(r, rational(5));
|
||||
}
|
||||
}
|
||||
|
||||
static void test_bddv_mul() {
|
||||
unsigned const num_bits = 4;
|
||||
bdd_manager m(num_bits);
|
||||
|
||||
unsigned_vector bits;
|
||||
bits.push_back(0);
|
||||
bits.push_back(1);
|
||||
bits.push_back(4);
|
||||
bits.push_back(27);
|
||||
|
||||
bddv const x = m.mk_var(bits);
|
||||
bddv const zero = m.mk_zero(num_bits);
|
||||
bddv const one = m.mk_num(rational(1), num_bits);
|
||||
bddv const five = m.mk_num(rational(5), num_bits);
|
||||
bddv const six = m.mk_num(rational(6), num_bits);
|
||||
|
||||
{
|
||||
// 5*x == 1 (mod 16) => x == 13 (mod 16)
|
||||
bdd const five_inv = x * five == one;
|
||||
rational r;
|
||||
auto res = five_inv.find_num(bits, r);
|
||||
SASSERT_EQ(res, find_result::singleton);
|
||||
SASSERT_EQ(r, rational(13));
|
||||
}
|
||||
|
||||
{
|
||||
// 6*x == 1 (mod 16) => no solution for x
|
||||
bdd const six_inv = x * six == one;
|
||||
rational r;
|
||||
auto res = six_inv.find_num(bits, r);
|
||||
SASSERT_EQ(res, find_result::empty);
|
||||
SASSERT(six_inv.is_false());
|
||||
}
|
||||
|
||||
{
|
||||
// 6*x == 0 (mod 16) => x is either 0 or 8 (mod 16)
|
||||
bdd const b = six * x == zero;
|
||||
rational r;
|
||||
SASSERT(b.contains_num(rational(0), bits));
|
||||
SASSERT(b.contains_num(rational(8), bits));
|
||||
SASSERT((b && (x != rational(0)) && (x != rational(8))).is_false());
|
||||
SASSERT((b && (x != rational(0))) == (x == rational(8)));
|
||||
}
|
||||
|
||||
SASSERT_EQ((x * zero).get_bits(), (x * rational(0)).get_bits());
|
||||
SASSERT_EQ((x * one).get_bits(), (x * rational(1)).get_bits());
|
||||
SASSERT_EQ((x * five).get_bits(), (x * rational(5)).get_bits());
|
||||
SASSERT_EQ((x * six).get_bits(), (x * rational(6)).get_bits());
|
||||
}
|
||||
|
||||
static void test_int() {
|
||||
unsigned const w = 3; // bit width
|
||||
unsigned_vector bits;
|
||||
bits.push_back(0);
|
||||
bits.push_back(1);
|
||||
bits.push_back(2);
|
||||
bdd_manager m(w);
|
||||
|
||||
bddv const x = m.mk_var(bits);
|
||||
|
||||
// Encodes the values x satisfying a*x + b == 0 (mod 2^w) as BDD.
|
||||
auto mk_affine = [] (rational const& a, bddv const& x, rational const& b) {
|
||||
return (a*x + b == rational(0));
|
||||
};
|
||||
|
||||
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));
|
||||
num.push_back(m.mk_eq(x, rational(n)));
|
||||
|
||||
for (unsigned k = 0; k < (1 << w); ++k) {
|
||||
for (unsigned n = 0; n < (1 << w); ++n) {
|
||||
SASSERT(num[k].contains_num(rational(n), bits) == (n == k));
|
||||
rational r;
|
||||
SASSERT_EQ((num[n] || num[k]).find_num(bits, r), (n == k) ? find_result::singleton : find_result::multiple);
|
||||
SASSERT(r == n || r == 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));
|
||||
SASSERT(s0127.contains_num(rational(0), bits));
|
||||
SASSERT(s0127.contains_num(rational(1), bits));
|
||||
SASSERT(s0127.contains_num(rational(2), bits));
|
||||
SASSERT(!s0127.contains_num(rational(3), bits));
|
||||
SASSERT(!s0127.contains_num(rational(4), bits));
|
||||
SASSERT(!s0127.contains_num(rational(5), bits));
|
||||
SASSERT(!s0127.contains_num(rational(6), bits));
|
||||
SASSERT(s0127.contains_num(rational(7), bits));
|
||||
|
||||
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));
|
||||
SASSERT(mk_affine(rational(0), x, rational(0)).is_true());
|
||||
SASSERT(mk_affine(rational(0), x, rational(1)).is_false());
|
||||
// 2*x == 0 (mod 2^3) has the solutions 0, 4
|
||||
SASSERT(mk_affine(rational(2), x, rational(0)) == (num[0] || num[4]));
|
||||
|
||||
// 4*x + 2 == 0 (mod 2^3) has no solutions
|
||||
SASSERT(m.mk_affine(rational(4), rational(2), 3).is_false());
|
||||
SASSERT(mk_affine(rational(4), x, rational(2)).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]);
|
||||
SASSERT(mk_affine(rational(3), x, rational(2)) == 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(mk_affine(rational(2), x, rational(2)) == (num[3] || num[7]));
|
||||
|
||||
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]));
|
||||
unsigned_vector bits4 = bits;
|
||||
bits4.push_back(10);
|
||||
bddv const x4 = m.mk_var(bits4);
|
||||
|
||||
// 12*x + 8 == 0 (mod 2^4) has the solutions 2, 6, 10, 14
|
||||
bdd expected = m.mk_eq(x4, rational(2)) || m.mk_eq(x4, rational(6)) || m.mk_eq(x4, rational(10)) || m.mk_eq(x4, rational(14));
|
||||
SASSERT(mk_affine(rational(12), x4, rational(8)) == expected);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -120,5 +293,10 @@ void tst_bdd() {
|
|||
dd::test2();
|
||||
dd::test3();
|
||||
dd::test4();
|
||||
dd::test_xor();
|
||||
dd::test_bddv_ops_on_constants();
|
||||
dd::test_bddv_eqfind_small();
|
||||
dd::test_bddv_eqfind();
|
||||
dd::test_bddv_mul();
|
||||
dd::test_int();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -63,6 +63,13 @@ bool is_debug_enabled(const char * tag);
|
|||
#define CASSERT(TAG, COND) DEBUG_CODE(if (assertions_enabled() && is_debug_enabled(TAG) && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); })
|
||||
#define XASSERT(COND, EXTRA_CODE) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); { EXTRA_CODE } INVOKE_DEBUGGER(); })
|
||||
|
||||
#define SASSERT_EQ(LHS, RHS) \
|
||||
DEBUG_CODE(if (assertions_enabled() && !((LHS) == (RHS))) { \
|
||||
notify_assertion_violation(__FILE__, __LINE__, #LHS " == " #RHS); \
|
||||
std::cerr << "LHS value: " << (LHS) << "\nRHS value: " << (RHS) << "\n"; \
|
||||
INVOKE_DEBUGGER(); \
|
||||
})
|
||||
|
||||
#ifdef Z3DEBUG
|
||||
# define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); INVOKE_DEBUGGER();)
|
||||
#else
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue