From 42233ab5c875409d9952b890ab70e0289e9fbba3 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 1 Aug 2022 12:30:34 +0200 Subject: [PATCH] Additional BDD operations; BDD vectors and finite domain abstraction --- src/math/dd/CMakeLists.txt | 1 + src/math/dd/dd_bdd.cpp | 363 ++++++++++++++++++++++++++- src/math/dd/dd_bdd.h | 133 +++++++++- src/math/dd/dd_fdd.cpp | 366 +++++++++++++++++++++++++++ src/math/dd/dd_fdd.h | 108 ++++++++ src/test/bdd.cpp | 493 +++++++++++++++++++++++++++++++++++-- 6 files changed, 1432 insertions(+), 32 deletions(-) create mode 100644 src/math/dd/dd_fdd.cpp create mode 100644 src/math/dd/dd_fdd.h diff --git a/src/math/dd/CMakeLists.txt b/src/math/dd/CMakeLists.txt index ac9d28b0d..3f25a8406 100644 --- a/src/math/dd/CMakeLists.txt +++ b/src/math/dd/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(dd SOURCES dd_bdd.cpp + dd_fdd.cpp dd_pdd.cpp COMPONENT_DEPENDENCIES util diff --git a/src/math/dd/dd_bdd.cpp b/src/math/dd/dd_bdd.cpp index 86f2b9408..ee0f1600c 100644 --- a/src/math/dd/dd_bdd.cpp +++ b/src/math/dd/dd_bdd.cpp @@ -142,6 +142,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(); @@ -571,7 +573,63 @@ namespace dd { e1->m_result = r; return r; } + + /** + * co-factor a using b. + * b must be a variable bdd (it can be generalized to a cube) + */ + + bdd bdd_manager::mk_cofactor(bdd const& a, bdd const& b) { + bool first = true; + scoped_push _sp(*this); + SASSERT(!b.is_const() && b.lo().is_const() && b.hi().is_const()); + while (true) { + try { + return bdd(mk_cofactor_rec(a.root, b.root), this); + } + catch (const mem_out &) { + if (!first) throw; + try_reorder(); + first = false; + } + } + } + + bdd_manager::BDD bdd_manager::mk_cofactor_rec(BDD a, BDD b) { + if (is_const(a)) return a; + if (is_const(b)) return a; + unsigned la = level(a), lb = level(b); + // cases where b is a single literal + if (la == lb && is_const(lo(b)) && is_const(hi(b))) + return is_true(hi(b)) ? hi(a) : lo(a); + if (la < lb && is_const(lo(b)) && is_const(hi(b))) + return a; + // cases where b is a proper cube (with more than one literal + if (la == lb) { + if (is_false(lo(b))) + a = hi(a), b = hi(b); + else + a = lo(a), b = lo(b); + return mk_cofactor_rec(a, b); + } + if (la < lb) + return mk_cofactor_rec(a, is_false(lo(b)) ? hi(b) : lo(b)); + + op_entry* e1 = pop_entry(a, b, bdd_cofactor_op); + op_entry const* e2 = m_op_cache.insert_if_not_there(e1); + if (check_result(e1, e2, a, b, bdd_cofactor_op)) + return e2->m_result; + + SASSERT(la > lb); + push(mk_cofactor_rec(lo(a), b)); + push(mk_cofactor_rec(hi(a), b)); + BDD r = make_node(la, read(2), read(1)); + pop(2); + e1->m_result = r; + return r; + } + bdd bdd_manager::mk_ite(bdd const& c, bdd const& t, bdd const& e) { bool first = true; scoped_push _sp(*this); @@ -587,14 +645,15 @@ namespace dd { } } + bdd_manager::BDD bdd_manager::mk_ite_rec(BDD a, BDD b, BDD c) { if (is_true(a)) return b; if (is_false(a)) return c; if (b == c) return b; - if (is_true(b)) return apply(a, c, bdd_or_op); - if (is_false(c)) return apply(a, b, bdd_and_op); - if (is_false(b)) return apply(mk_not_rec(a), c, bdd_and_op); - if (is_true(c)) return apply(mk_not_rec(a), b, bdd_or_op); + if (is_true(b)) return apply_rec(a, c, bdd_or_op); + if (is_false(c)) return apply_rec(a, b, bdd_and_op); + if (is_false(b)) return apply_rec(mk_not_rec(a), c, bdd_and_op); + if (is_true(c)) return apply_rec(mk_not_rec(a), b, bdd_or_op); SASSERT(!is_const(a) && !is_const(b) && !is_const(c)); op_entry * e1 = pop_entry(a, b, c); op_entry const* e2 = m_op_cache.insert_if_not_there(e1); @@ -644,6 +703,7 @@ namespace dd { bdd_manager::BDD bdd_manager::mk_quant(unsigned n, unsigned const* vars, BDD b, bdd_op op) { BDD result = b; + // TODO: should this method catch mem_out like the other non-rec mk_ methods? for (unsigned i = 0; i < n; ++i) { result = mk_quant_rec(m_var2level[vars[i]], result, op); } @@ -895,4 +955,299 @@ 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_eq(bddv const& a, bddv const& b) { + SASSERT(a.size() == b.size()); + bdd eq = mk_true(); + for (unsigned i = 0; i < a.size(); ++i) + eq &= !(a[i] ^ b[i]); + return eq; + } + + bdd bdd_manager::mk_eq(bddv const& a, rational const& n) { + SASSERT(n.is_int() && n >= 0 && n < rational(2).expt(a.size())); + bdd b = mk_true(); + for (unsigned i = 0; i < a.size(); ++i) + b &= n.get_bit(i) ? a[i] : !a[i]; + return b; + } + + bdd bdd_manager::mk_eq(unsigned_vector const& vars, rational const& n) { + SASSERT(n.is_int() && n >= 0 && n < rational(2).expt(vars.size())); + bdd b = mk_true(); + for (unsigned i = 0; i < vars.size(); ++i) + b &= n.get_bit(i) ? mk_var(vars[i]) : mk_nvar(vars[i]); + return b; + } + + bdd bdd_manager::mk_ule(bddv const& a, bddv const& b) { + SASSERT(a.size() == b.size()); + bdd lt = mk_false(); + bdd eq = mk_true(); + for (unsigned i = a.size(); i-- > 0 && !eq.is_false(); ) { + lt |= eq && (!a[i] && b[i]); + eq &= !(a[i] ^ b[i]); + } + return lt || eq; + } + bdd bdd_manager::mk_uge(bddv const& a, bddv const& b) { return mk_ule(b, a); } + 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 bdd_manager::mk_sle(bddv const& a, bddv const& b) { + SASSERT(a.size() == b.size()); + // Note: sle can be reduced to ule by flipping the sign bits of both arguments + bdd lt = mk_false(); + bdd eq = mk_true(); + unsigned const sz = a.size(); + if (sz > 0) { + lt = a[sz - 1] && !b[sz - 1]; + eq = !(a[sz - 1] ^ b[sz - 1]); + for (unsigned i = sz - 1; i-- > 0; ) { + lt |= eq && (!a[i] && b[i]); + eq &= !(a[i] ^ b[i]); + } + } + return lt || eq; + } + 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); } + + bddv bdd_manager::mk_add(bddv const& a, bddv const& b) { + SASSERT(a.size() == b.size()); + bdd carry = mk_false(); + bddv result(this); +#if 0 + for (unsigned i = 0; i < a.size(); ++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; + } + + bddv bdd_manager::mk_add(bddv const& a, std::function& b) { + bdd carry = mk_false(); + bddv result(this); + if (a.size() > 0) + result.push_back(a[0] ^ b(0)); + for (unsigned i = 1; i < a.size(); ++i) { + auto bi1 = b(i-1); + carry = (carry && a[i-1]) || (carry && bi1) || (a[i-1] && bi1); + result.push_back(carry ^ a[i] ^ b(i)); + } + return result; + } + + + bddv bdd_manager::mk_sub(bddv const& a, bddv const& b) { + SASSERT(a.size() == b.size()); + bdd carry = mk_false(); + bddv result(this); + if (a.size() > 0) + result.push_back(a[0] ^ b[0]); + for (unsigned i = 1; i < a.size(); ++i) { + // carry = (a[i-1] && b[i-1] && carry) || (!a[i-1] && (b[i-1] || carry)); + carry = mk_ite(a[i-1], b[i-1] && carry, b[i-1] || carry); + result.push_back(carry ^ a[i] ^ b[i]); + } + return result; + } + + bddv bdd_manager::mk_usub(bddv const& a) { + bddv result(this); + bdd carry = mk_false(); + result.push_back(a[0]); + for (unsigned i = 1; i < a.size(); ++i) { + carry = a[i-1] || carry; + result.push_back(carry ^ a[i]); + } + return result; + } + + bool_vector bdd_manager::mk_usub(bool_vector const& b) { + bool_vector result; + if (b.empty()) + return result; + bool carry = false; + result.push_back(b[0]); + for (unsigned i = 1; i < b.size(); ++i) { + carry = carry || b[i-1]; + result.push_back(carry ^ b[i]); + } + return result; + } + + + bddv bdd_manager::mk_mul(bddv const& a, bddv const& b) { + SASSERT(a.size() == b.size()); + bddv result = mk_zero(a.size()); + for (unsigned i = 0; i < b.size(); ++i) { + std::function get_a = [&](unsigned k) { + if (k < i) + return mk_false(); + else + return a[k - i] && b[i]; + }; + result = mk_add(result, get_a); + } + 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())); + bool_vector b; + for (unsigned i = 0; i < a.size(); ++i) + b.push_back(val.get_bit(i)); + return mk_mul(a, b); + } + + bddv bdd_manager::mk_mul(bddv const& a, bool_vector const& b) { + SASSERT(a.size() == b.size()); + bddv result = mk_zero(a.size()); + + // use identity (bvmul a b) == (bvneg (bvmul (bvneg a) b)) + unsigned cnt = 0; + for (auto v : b) if (v) cnt++; + if (cnt*2 > b.size()+1) + return mk_usub(mk_mul(a, mk_usub(b))); + + for (unsigned i = 0; i < a.size(); ++i) { + std::function get_a = [&](unsigned k) { + if (k < i) + return mk_false(); + else + return a[k - i]; + }; + if (b[i]) + result = mk_add(result, get_a); + } + return result; + } + + bddv bdd_manager::mk_concat(bddv const& a, bddv const& b) { + bddv result = a; + result.m_bits.append(b.m_bits); + return result; + } + + + /** + * Quotient remainder + * + * rem, div have size 2*|a| = worksize. + * Initialization: + * rem := a ++ false + * div := false ++ b + */ + void bdd_manager::mk_quot_rem(bddv const& a, bddv const& b, bddv& quot, bddv& rem) { + SASSERT(a.size() == b.size()); + quot = mk_zero(a.size()); + unsigned worksize = a.size() + b.size(); + rem = a.append(mk_zero(b.size())); + bddv div = mk_zero(a.size()).append(b); + // + // Keep shifting divisor to the right and subtract whenever it is + // smaller than the remaining value + // + for (unsigned i = 0; i <= b.size(); ++i) { + bdd divLteRem = div <= rem; + bddv remSubDiv = rem - div; + + for (unsigned j = 0; j < worksize; ++j) + rem[j] = mk_ite(divLteRem, remSubDiv[j], rem[j]); + + if (i > 0) + quot[b.size() - i] = divLteRem; + + div.shr(); + } + rem.m_bits.shrink(b.size()); + } + + 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; + } + + void bddv::shl() { + for (unsigned j = size(); j-- > 1;) + m_bits[j] = m_bits[j - 1]; + m_bits[0] = m->mk_false(); + } + + void bddv::shr() { + for (unsigned j = 1; j < size(); ++j) + m_bits[j - 1] = m_bits[j]; + m_bits[size() - 1] = m->mk_false(); + } + + bdd bddv::all0() const { + bdd r = m->mk_true(); + for (unsigned i = 0; i < size() && !r.is_false(); ++i) + r &= !m_bits[i]; + return r; + } + + bdd bddv::all1() const { + bdd r = m->mk_true(); + for (unsigned i = 0; i < size() && !r.is_false(); ++i) + r &= m_bits[i]; + return r; + } + } diff --git a/src/math/dd/dd_bdd.h b/src/math/dd/dd_bdd.h index 1892c5317..109f3dc19 100644 --- a/src/math/dd/dd_bdd.h +++ b/src/math/dd/dd_bdd.h @@ -21,13 +21,18 @@ Revision History: #include "util/vector.h" #include "util/map.h" #include "util/small_object_allocator.h" +#include "util/rational.h" namespace dd { class bdd; + class bddv; + class test_bdd; class bdd_manager { friend bdd; + friend bddv; + friend test_bdd; typedef unsigned BDD; @@ -40,7 +45,8 @@ namespace dd { bdd_not_op = 5, bdd_and_proj_op = 6, bdd_or_proj_op = 7, - bdd_no_op = 8, + bdd_cofactor_op = 8, + bdd_no_op = 9, }; struct bdd_node { @@ -141,6 +147,7 @@ namespace dd { BDD mk_not_rec(BDD b); BDD mk_ite_rec(BDD a, BDD b, BDD c); BDD mk_quant_rec(unsigned lvl, BDD b, bdd_op op); + BDD mk_cofactor_rec(BDD a, BDD b); void push(BDD b); void pop(unsigned num_scopes); @@ -188,6 +195,7 @@ namespace dd { bdd mk_and(bdd const& a, bdd const& b); bdd mk_or(bdd const& a, bdd const& b); bdd mk_xor(bdd const& a, bdd const& b); + bdd mk_cofactor(bdd const& a, bdd const& b); void reserve_var(unsigned v); bool well_formed(); @@ -199,10 +207,13 @@ namespace dd { ~scoped_push() { m.m_bdd_stack.shrink(m_size); } }; + bool_vector mk_usub(bool_vector const& b); + + public: struct mem_out {}; - bdd_manager(unsigned nodes); + bdd_manager(unsigned num_vars); ~bdd_manager(); void set_max_num_nodes(unsigned n) { m_max_num_bdd_nodes = n; } @@ -219,6 +230,39 @@ 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 + * - 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); } + bdd mk_ugt(bddv const& a, bddv const& b); // { return mk_ult(b, a); } + 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 mk_eq(bddv const& a, bddv const& b); + bdd mk_eq(bddv const& a, rational const& v); + bdd mk_eq(unsigned_vector const& vars, rational const& v); + bddv mk_num(rational const& n, unsigned num_bits); + bddv mk_ones(unsigned num_bits); + bddv mk_zero(unsigned num_bits); + bddv mk_var(unsigned num_bits, unsigned const* vars); + bddv mk_var(unsigned_vector const& vars); + bddv mk_add(bddv const& a, bddv const& b); + bddv mk_add(bddv const& a, std::function& get_bit); + bddv mk_sub(bddv const& a, bddv const& b); + bddv mk_usub(bddv const& a); + 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); + bddv mk_concat(bddv const& a, bddv const& b); + void mk_quot_rem(bddv const& a, bddv const& b, bddv& quot, bddv& rem); + 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); @@ -242,14 +286,16 @@ namespace dd { unsigned var() const { return m->var(root); } bool is_true() const { return root == bdd_manager::true_bdd; } - bool is_false() const { return root == bdd_manager::false_bdd; } + bool is_false() const { return root == bdd_manager::false_bdd; } + bool is_const() const { return is_false() || is_true(); } - bdd operator!() { return m->mk_not(*this); } - bdd operator&&(bdd const& other) { return m->mk_and(*this, other); } - bdd operator||(bdd const& other) { return m->mk_or(*this, other); } - bdd operator^(bdd const& other) { return m->mk_xor(*this, other); } + bdd operator!() const { return m->mk_not(*this); } + bdd operator&&(bdd const& other) const { return m->mk_and(*this, other); } + bdd operator||(bdd const& other) const { return m->mk_or(*this, other); } + bdd operator^(bdd const& other) const { return m->mk_xor(*this, other); } bdd operator|=(bdd const& other) { return *this = *this || other; } bdd operator&=(bdd const& other) { return *this = *this && other; } + bdd cofactor(bdd const& cube) { return m->mk_cofactor(*this, cube); } std::ostream& display(std::ostream& out) const { return m->display(out, *this); } bool operator==(bdd const& other) const { return root == other.root; } bool operator!=(bdd const& other) const { return root != other.root; } @@ -260,6 +306,79 @@ namespace dd { std::ostream& operator<<(std::ostream& out, bdd const& b); + class bddv { + friend bdd_manager; + + vector m_bits; + bdd_manager* m; + + bddv(vector const& bits, bdd_manager* m): m_bits(bits), m(m) { SASSERT(m); } + bddv(vector&& bits, bdd_manager* m): m_bits(std::move(bits)), m(m) { SASSERT(m); } + + bddv(bdd_manager* m): m_bits(), m(m) { SASSERT(m); } + bdd const& operator[](unsigned i) const { return m_bits[i]; } + bdd& operator[](unsigned i) { return m_bits[i]; } + void push_back(bdd const& a) { m_bits.push_back(a); } + void push_back(bdd&& a) { m_bits.push_back(std::move(a)); } + void shl(); + void shr(); + + public: + unsigned size() const { return m_bits.size(); } + vector const& bits() const { return m_bits; } + + /* unsigned comparison operators */ + bdd operator<=(bddv const& other) const { return m->mk_ule(*this, other); } ///< unsigned comparison + bdd operator>=(bddv const& other) const { return m->mk_uge(*this, other); } ///< unsigned comparison + bdd operator< (bddv const& other) const { return m->mk_ult(*this, other); } ///< unsigned comparison + bdd operator> (bddv const& other) const { return m->mk_ugt(*this, other); } ///< unsigned comparison + bdd operator<=(rational const& other) const { return m->mk_ule(*this, m->mk_num(other, size())); } ///< unsigned comparison + bdd operator>=(rational const& other) const { return m->mk_uge(*this, m->mk_num(other, size())); } ///< unsigned comparison + bdd operator< (rational const& other) const { return m->mk_ult(*this, m->mk_num(other, size())); } ///< unsigned comparison + bdd operator> (rational const& other) const { return m->mk_ugt(*this, m->mk_num(other, size())); } ///< unsigned comparison + + /* signed comparison operators */ + bdd sle(bddv const& other) const { return m->mk_sle(*this, other); } + bdd sge(bddv const& other) const { return m->mk_sge(*this, other); } + bdd slt(bddv const& other) const { return m->mk_slt(*this, other); } + bdd sgt(bddv const& other) const { return m->mk_sgt(*this, other); } + + bdd all0() const; + bdd all1() const; + + 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-(rational const& other) const { return m->mk_sub(*this, m->mk_num(other, size())); } + bddv rev_sub(rational const& other) const { return m->mk_sub(m->mk_num(other, size()), *this); } + 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); } + bddv append(bddv const& other) const { return m->mk_concat(*this, other); } + void quot_rem(bddv const& divisor, bddv& quot, bddv& rem) const { m->mk_quot_rem(*this, divisor, quot, rem); } + + bool is_const() const { return m->is_constv(*this); } + rational to_val() const { return m->to_val(*this); } + }; + + inline bdd operator<=(rational const& r, bddv const& a) { return a >= r; } ///< unsigned comparison + inline bdd operator>=(rational const& r, bddv const& a) { return a <= r; } ///< unsigned comparison + inline bdd operator< (rational const& r, bddv const& a) { return a > r; } ///< unsigned comparison + inline bdd operator> (rational const& r, bddv const& a) { return a < r; } ///< unsigned comparison + inline bdd operator==(rational const& r, bddv const& a) { return a == r; } + inline bdd operator!=(rational const& r, bddv const& a) { return a != r; } + inline bddv operator*(rational const& r, bddv const& a) { return a * r; } + inline bddv operator+(rational const& r, bddv const& a) { return a + r; } + inline bddv operator-(rational const& r, bddv const& a) { return a.rev_sub(r); } + inline bdd operator<=(int i, bddv const& a) { return a >= rational(i); } + inline bdd operator<=(bddv const& a, int i) { return a <= rational(i); } + + } diff --git a/src/math/dd/dd_fdd.cpp b/src/math/dd/dd_fdd.cpp new file mode 100644 index 000000000..21ec82fd1 --- /dev/null +++ b/src/math/dd/dd_fdd.cpp @@ -0,0 +1,366 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + dd_fdd + +Abstract: + + Finite domain abstraction for using BDDs as sets of integers, inspired by BuDDy's fdd module. + +Author: + + Nikolaj Bjorner (nbjorner) 2021-04-20 + Jakob Rath 2021-04-20 + +--*/ + +#include "math/dd/dd_fdd.h" + +namespace dd { + + fdd::fdd(bdd_manager& manager, unsigned_vector&& vars) + : m_pos2var(std::move(vars)) + , m_var2pos() + , m(&manager) + , m_var(manager.mk_var(m_pos2var)) + { + for (unsigned pos = 0; pos < m_pos2var.size(); ++pos) { + unsigned const var = m_pos2var[pos]; + while (var >= m_var2pos.size()) + m_var2pos.push_back(UINT_MAX); + m_var2pos[var] = pos; + } + } + + bdd fdd::non_zero() const { + bdd non_zero = m->mk_false(); + for (unsigned var : m_pos2var) { + non_zero |= m->mk_var(var); + } + return non_zero; + } + + unsigned fdd::var2pos(unsigned var) const { + return var < m_var2pos.size() ? m_var2pos[var] : UINT_MAX; + } + + bool fdd::contains(bdd b, rational const& val) const { + while (!b.is_const()) { + unsigned const pos = var2pos(b.var()); + SASSERT(pos != UINT_MAX && "Unexpected BDD variable"); + b = val.get_bit(pos) ? b.hi() : b.lo(); + } + return b.is_true(); + } + + find_t fdd::find(bdd b, rational& out_val) const { + return find_hint(b, rational::zero(), out_val); + } + + find_t fdd::find_hint(bdd b, rational const& hint, rational& out_val) const { + out_val = 0; + if (b.is_false()) + return find_t::empty; + bool is_unique = true; + bool hint_ok = !hint.is_zero(); // since we choose the 'lo' branch by default, we don't need to check the hint when it is 0. + unsigned num_vars = 0; + while (!b.is_true()) { + ++num_vars; + unsigned const pos = var2pos(b.var()); + SASSERT(pos != UINT_MAX && "Unexpected BDD variable"); + + bool go_hi = false; + if (b.lo().is_false()) { + go_hi = true; + if (hint_ok && !hint.get_bit(pos)) + hint_ok = false; + } + else if (b.hi().is_false()) { + if (hint_ok && hint.get_bit(pos)) + hint_ok = false; + } + else { + // This is the only case where we have a choice + // => follow the hint + SASSERT(!b.lo().is_false() && !b.hi().is_false()); + is_unique = false; + if (hint_ok && hint.get_bit(pos)) + go_hi = true; + } + + if (go_hi) { + out_val += rational::power_of_two(pos); + b = b.hi(); + } + else + b = b.lo(); + } + if (num_vars != num_bits()) + is_unique = false; + // If a variable corresponding to a 1-bit in hint does not appear in the BDD, + // out_val is wrong at this point, so we set it explicitly. + if (hint_ok) + out_val = hint; + // TODO: instead of computing out_val incrementally, we could mark the visited 'hi'-positions and only compute out_val from the marks when !hint_ok. + return is_unique ? find_t::singleton : find_t::multiple; + } + + std::ostream& operator<<(std::ostream& out, find_t x) { + switch (x) { + case find_t::empty: + return out << "empty"; + case find_t::singleton: + return out << "singleton"; + case find_t::multiple: + return out << "multiple"; + } + UNREACHABLE(); + return out; + } + + bool fdd::contains(bdd const& x, bool_vector const& value) const { + bdd b = x; + while (!b.is_true()) { + unsigned const pos = var2pos(b.var()); + SASSERT(pos != UINT_MAX && "Unexpected BDD variable"); + if (value[pos] && b.hi().is_false()) + return false; + if (!value[pos] && b.lo().is_false()) + return false; + if (value[pos]) + b = b.hi(); + else + b = b.lo(); + } + return true; + } + + + // subtract one from x + static void dec(bool_vector& x) { + for (auto& b : x) { + b = !b; + if (!b) + break; + } + } + + // add one to x + static void inc(bool_vector& x) { + for (auto& b : x) { + b = !b; + if (b) + break; + } + } + + static void reset(bool_vector& x, bool value) { + for (auto& b : x) + b = value; + } + + + bool fdd::sup(bdd const& x, bool_vector& lo) const { + SASSERT(lo.size() == num_bits()); + // + // Assumption: common case is that high-order bits are before lower-order bits also + // after re-ordering. Then co-factoring is relatively cheap. + // + + if (!contains(x, lo)) + return false; + + // + // find minimal index where b is false for some + // value larger than lo. + // + // Let ua(x lo) be shorthand for "unbounded-above" of variable + // x with bit-string lo. + // + // we have the following identities: + // ua(_ []) = true + // ua(x 1 ++ lo) = hi(x) = T or ua(hi(x), lo) + // ua(x 0 ++ lo) = hi(x) = T and ua(lo(x), lo) + // + // the least significant bit where ua is false + // represents the position where the smallest number above + // lo resides that violates x. + + unsigned idx = UINT_MAX; + vector trail; + bdd b = x; + for (unsigned i = lo.size(); i-- > 0; ) { + trail.push_back(b); + unsigned v = m_pos2var[i]; + bdd w = m->mk_var(v); + bdd hi = b.cofactor(w); + if (lo[i]) { + if (hi.is_true()) + break; + SASSERT(!hi.is_false()); + b = hi; + } + else { + if (!hi.is_true()) + idx = i; + b = b.cofactor(m->mk_nvar(v)); + } + } + if (idx == UINT_MAX) { + // all values above lo satisfy x + reset(lo, true); + return true; + } + + SASSERT(!lo[idx]); + lo[idx] = true; + unsigned v = m_pos2var[idx]; + b = trail[lo.size() - idx - 1].cofactor(m->mk_var(v)); + for (unsigned i = idx; i-- > 0; ) { + SASSERT(!b.is_true()); + if (b.is_false()) { + for (unsigned j = 0; j <= i; ++j) + lo[j] = false; + break; + } + lo[i] = b.lo().is_true(); + if (lo[i]) + b = b.hi(); + else + b = b.lo(); + } + + dec(lo); + + return true; + } + + bool fdd::inf(bdd const& x, bool_vector& hi) const { + SASSERT(hi.size() == num_bits()); + if (!contains(x, hi)) + return false; + + // Let ub(x hi) be shorthand for "unbounded-below" of variable + // x with bit-string hi. + // + // we have the following identities: + // ub(_ []) = true + // ub(x 0 ++ hi) = lo(x) = T or ub(lo(x), hi) + // ub(x 1 ++ hi) = lo(x) = T and ub(hi(x), hi) + // + + unsigned idx = UINT_MAX; + vector trail; + bdd b = x; + for (unsigned i = hi.size(); i-- > 0; ) { + trail.push_back(b); + unsigned v = m_pos2var[i]; + bdd nw = m->mk_nvar(v); + bdd lo = b.cofactor(nw); + if (!hi[i]) { + if (lo.is_true()) + break; + SASSERT(!lo.is_false()); + b = lo; + } + else { + if (!lo.is_true()) + idx = i; + b = b.cofactor(m->mk_var(v)); + } + } + if (idx == UINT_MAX) { + // all values below hi satisfy x + reset(hi, false); + return true; + } + + SASSERT(hi[idx]); + hi[idx] = false; + unsigned v = m_pos2var[idx]; + b = trail[hi.size() - idx - 1].cofactor(m->mk_nvar(v)); + + for (unsigned i = idx; i-- > 0; ) { + SASSERT(!b.is_true()); + if (b.is_false()) { + for (unsigned j = 0; j <= i; ++j) + hi[j] = true; + break; + } + hi[i] = !b.hi().is_true(); + if (!hi[i]) + b = b.lo(); + else + b = b.hi(); + } + + inc(hi); + + return true; + } + + bool_vector fdd::rational2bits(rational const& r) const { + bool_vector result; + for (unsigned i = 0; i < num_bits(); ++i) + result.push_back(r.get_bit(i)); + return result; + } + + rational fdd::bits2rational(bool_vector const& v) const { + rational result(0); + for (unsigned i = 0; i < num_bits(); ++i) + if (v[i]) + result += rational::power_of_two(i); + return result; + } + + bool fdd::sup(bdd const& b, rational& _lo) const { + bool_vector lo = rational2bits(_lo); + if (!sup(b, lo)) + return false; + _lo = bits2rational(lo); + return true; + } + + bool fdd::inf(bdd const& b, rational& _hi) const { + bool_vector hi = rational2bits(_hi); + if (!inf(b, hi)) + return false; + _hi = bits2rational(hi); + return true; + } + + rational fdd::max(bdd b) const { + SASSERT(!b.is_false()); + rational result(0); + for (unsigned i = num_bits(); i-- > 0; ) { + unsigned v = m_pos2var[i]; + bdd w = m->mk_var(v); + bdd hi = b.cofactor(w); + if (!hi.is_false()) { + b = hi; + result += rational::power_of_two(i); + } + } + return result; + } + + rational fdd::min(bdd b) const { + SASSERT(!b.is_false()); + rational result(0); + for (unsigned i = num_bits(); i-- > 0; ) { + unsigned v = m_pos2var[i]; + bdd nw = m->mk_nvar(v); + bdd lo = b.cofactor(nw); + if (lo.is_false()) + result += rational::power_of_two(i); + else + b = lo; + } + return result; + } + + +} diff --git a/src/math/dd/dd_fdd.h b/src/math/dd/dd_fdd.h new file mode 100644 index 000000000..e17233aa4 --- /dev/null +++ b/src/math/dd/dd_fdd.h @@ -0,0 +1,108 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + dd_fdd + +Abstract: + + Finite domain abstraction for using BDDs as sets of integers, inspired by BuDDy's fdd module. + +Author: + + Jakob Rath 2021-04-20 + Nikolaj Bjorner (nbjorner) 2021-04-20 + +--*/ +#pragma once + +#include "math/dd/dd_bdd.h" +#include "util/vector.h" +#include "util/rational.h" + +namespace dd { + + enum class find_t { empty, singleton, multiple }; + std::ostream& operator<<(std::ostream& out, find_t x); + + /** + * Finite domain abstraction over BDDs. + */ + class fdd { + unsigned_vector m_pos2var; // pos -> BDD var + unsigned_vector m_var2pos; // var -> pos (pos = place number in the bit representation, 0 is LSB's place) + bdd_manager* m; + bddv m_var; + + static unsigned_vector seq(unsigned count, unsigned start = 0, unsigned step = 1) { + unsigned_vector result; + unsigned k = start; + for (unsigned i = 0; i < count; ++i, k += step) + result.push_back(k); + return result; + } + + unsigned var2pos(unsigned var) const; + + bool contains(bdd const& b, bool_vector const& value) const; + + rational bits2rational(bool_vector const& v) const; + + bool_vector rational2bits(rational const& r) const; + + public: + /** Initialize FDD using BDD variables from 0 to num_bits-1. */ + fdd(bdd_manager& manager, unsigned num_bits, unsigned start = 0, unsigned step = 1) : fdd(manager, seq(num_bits, start, step)) { } + fdd(bdd_manager& manager, unsigned_vector const& vars) : fdd(manager, unsigned_vector(vars)) { } + fdd(bdd_manager& manager, unsigned_vector&& vars); + + unsigned num_bits() const { return m_pos2var.size(); } + unsigned_vector const& bdd_vars() const { return m_pos2var; } + + bddv const& var() const { return m_var; } + + /** Equivalent to var() != 0 */ + bdd non_zero() const; + + /** Checks whether the integer val is contained in the BDD when viewed as set of integers. + * Precondition: the bdd only contains variables managed by this fdd. + */ + bool contains(bdd b, rational const& val) const; + + /** Returns an integer contained in the BDD, if any, and whether the BDD is a singleton. + * Precondition: the bdd only contains variables managed by this fdd. + */ + find_t find(bdd b, rational& out_val) const; + + /** Like find, but returns hint if it is contained in the BDD. */ + find_t find_hint(bdd b, rational const& hint, rational& out_val) const; + + /* + * find largest value at lo or above such that bdd b evaluates to true + * at lo and all values between. + * dually, find smallest value below hi that evaluates b to true + * and all values between the value and hi also evaluate b to true. + * \param b - a bdd using variables from this + * \param lo/hi - bound to be traversed. + * \return false if b is false at lo/hi + * \pre variables in b are a subset of variables from the fdd + */ + bool sup(bdd const& b, bool_vector& lo) const; + + bool inf(bdd const& b, bool_vector& hi) const; + + bool sup(bdd const& b, rational& lo) const; + + bool inf(bdd const& b, rational& hi) const; + + /* + * Find the min-max satisfying assignment. + * \pre b is not false. + */ + rational max(bdd b) const; + + rational min(bdd b) const; + }; + +} diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp index d08d10a11..12d5b27d8 100644 --- a/src/test/bdd.cpp +++ b/src/test/bdd.cpp @@ -1,7 +1,12 @@ #include "math/dd/dd_bdd.h" +#include "math/dd/dd_fdd.h" #include namespace dd { + +class test_bdd { +public: + static void test1() { bdd_manager m(20); bdd v0 = m.mk_var(0); @@ -10,13 +15,13 @@ namespace dd { bdd c1 = v0 && v1 && v2; bdd c2 = v2 && v0 && v1; std::cout << c1 << "\n"; - SASSERT(c1 == c2); + VERIFY(c1 == c2); std::cout << "cnf size: " << c1.cnf_size() << "\n"; c1 = v0 || v1 || v2; c2 = v2 || v1 || v0; std::cout << c1 << "\n"; - SASSERT(c1 == c2); + VERIFY(c1 == c2); std::cout << "cnf size: " << c1.cnf_size() << "\n"; } @@ -25,14 +30,14 @@ namespace dd { bdd v0 = m.mk_var(0); bdd v1 = m.mk_var(1); bdd v2 = m.mk_var(2); - SASSERT(m.mk_ite(v0,v0,v1) == (v0 || v1)); - SASSERT(m.mk_ite(v0,v1,v1) == v1); - SASSERT(m.mk_ite(v1,v0,v1) == (v0 && v1)); - SASSERT(m.mk_ite(v1,v0,v0) == v0); - SASSERT(m.mk_ite(v0,!v0,v1) == (!v0 && v1)); - SASSERT(m.mk_ite(v0,v1,!v0) == (!v0 || v1)); - SASSERT((!(v0 && v1)) == (!v0 || !v1)); - SASSERT((!(v0 || v1)) == (!v0 && !v1)); + VERIFY(m.mk_ite(v0,v0,v1) == (v0 || v1)); + VERIFY(m.mk_ite(v0,v1,v1) == v1); + VERIFY(m.mk_ite(v1,v0,v1) == (v0 && v1)); + VERIFY(m.mk_ite(v1,v0,v0) == v0); + VERIFY(m.mk_ite(v0,!v0,v1) == (!v0 && v1)); + VERIFY(m.mk_ite(v0,v1,!v0) == (!v0 || v1)); + VERIFY((!(v0 && v1)) == (!v0 || !v1)); + VERIFY((!(v0 || v1)) == (!v0 && !v1)); } static void test3() { @@ -44,19 +49,19 @@ namespace dd { bdd c2 = m.mk_exists(0, c1); std::cout << c1 << "\n"; std::cout << c2 << "\n"; - SASSERT(c2 == (v1 || v2)); + VERIFY(c2 == (v1 || v2)); c2 = m.mk_exists(1, c1); - SASSERT(c2 == (v0 || v2)); + VERIFY(c2 == (v0 || v2)); c2 = m.mk_exists(2, c1); - SASSERT(c2.is_true()); - SASSERT(m.mk_exists(3, c1) == c1); + VERIFY(c2.is_true()); + VERIFY(m.mk_exists(3, c1) == c1); c1 = (v0 && v1) || (v1 && v2) || (!v0 && !v2); c2 = m.mk_exists(0, c1); - SASSERT(c2 == (v1 || (v1 && v2) || !v2)); + VERIFY(c2 == (v1 || (v1 && v2) || !v2)); c2 = m.mk_exists(1, c1); - SASSERT(c2 == (v0 || v2 || (!v0 && !v2))); + VERIFY(c2 == (v0 || v2 || (!v0 && !v2))); c2 = m.mk_exists(2, c1); - SASSERT(c2 == ((v0 && v1) || v1 || !v0)); + VERIFY(c2 == ((v0 && v1) || v1 || !v0)); } static void test4() { @@ -74,11 +79,457 @@ namespace dd { std::cout << c1 << "\n"; 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); + VERIFY((m.mk_false() ^ v0) == v0); + VERIFY((v0 ^ m.mk_false()) == v0); + VERIFY((m.mk_true() ^ v0) == !v0); + VERIFY((v0 ^ m.mk_true()) == !v0); + VERIFY((v0 ^ v1) == ((v0 && !v1) || (!v0 && v1))); + } + + static void test_bddv_ops_on_constants() { + std::cout << "test_bddv_ops_on_constants\n"; + unsigned const num_bits = 3; + rational const modulus = rational::power_of_two(num_bits); + bdd_manager m(num_bits); + + VERIFY_EQ(m.to_val(m.mk_zero(num_bits)), rational(0)); + VERIFY_EQ(m.to_val(m.mk_ones(num_bits)), modulus - 1); + + for (unsigned n = 0; n < 8; ++n) { + rational const nr(n); + VERIFY_EQ(m.to_val(m.mk_num(nr, num_bits)), nr); + } + + for (unsigned n = 0; n < 8; ++n) { + for (unsigned k = 0; k < 8; ++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); + VERIFY_EQ((nv + kv).to_val(), (nr + kr) % modulus); + VERIFY_EQ((nv - kv).to_val(), (nr - kr + modulus) % modulus); + VERIFY_EQ((nv * kr).to_val(), (nr * kr) % modulus); + VERIFY_EQ((nv * kv).to_val(), (nr * kr) % modulus); + bdd eq = m.mk_eq(nv, kv); + VERIFY(eq.is_const() && (eq.is_true() == (n == k))); + eq = m.mk_eq(nv, kr); + VERIFY(eq.is_const() && (eq.is_true() == (n == k))); + + VERIFY(m.mk_usub(nv).to_val() == (m.mk_zero(num_bits) - nv).to_val()); + + bdd cmp = nv <= kv; + VERIFY(cmp.is_const() && (cmp.is_true() == (nr <= kr))); + cmp = nv >= kv; + VERIFY(cmp.is_const() && (cmp.is_true() == (nr >= kr))); + cmp = nv < kv; + VERIFY(cmp.is_const() && (cmp.is_true() == (nr < kr))); + cmp = nv > kv; + VERIFY(cmp.is_const() && (cmp.is_true() == (nr > kr))); + + // signed versions + rational const nrs = (nr < modulus / 2) ? nr : nr - modulus; + rational const krs = (kr < modulus / 2) ? kr : kr - modulus; + cmp = nv.sle(kv); + VERIFY(cmp.is_const() && (cmp.is_true() == (nrs <= krs))); + cmp = nv.sge(kv); + VERIFY(cmp.is_const() && (cmp.is_true() == (nrs >= krs))); + cmp = nv.slt(kv); + VERIFY(cmp.is_const() && (cmp.is_true() == (nrs < krs))); + cmp = nv.sgt(kv); + VERIFY(cmp.is_const() && (cmp.is_true() == (nrs > krs))); + + bddv quotv = m.mk_zero(num_bits); + bddv remv = m.mk_zero(num_bits); + nv.quot_rem(kv, quotv, remv); + if (k != 0) { + VERIFY_EQ(quotv.to_val(), rational(n / k)); + VERIFY_EQ(remv.to_val(), rational(n % k)); + } else { + // std::cout << "n=" << n << " k=" << k << "\n"; + // std::cout << " quot: " << quotv.to_val() << "\n"; + // std::cout << " rem: " << remv.to_val() << "\n"; + } + } + } + } + + static void test_bddv_eqfind_small() { + std::cout << "test_bddv_eqfind_small\n"; + bdd_manager m(4); + fdd const x_dom(m, 1); + bddv const x = x_dom.var(); + bdd x_is_one = (x == rational(1)); + std::cout << "x_is_one:\n" << x_is_one << "\n"; + rational r; + auto res = x_dom.find(x_is_one, r); + VERIFY_EQ(res, find_t::singleton); + VERIFY_EQ(r, rational(1)); + } + + static void test_bddv_eqfind() { + std::cout << "test_bddv_eqfind\n"; + bdd_manager m(4); + + unsigned_vector bits; + bits.push_back(0); + bits.push_back(1); + bits.push_back(4); + bits.push_back(27); + + fdd const x_dom(m, bits); + bddv const x = x_dom.var(); + bddv const zero = m.mk_zero(x_dom.num_bits()); + bddv const one = m.mk_num(rational(1), x_dom.num_bits()); + bddv const five = m.mk_num(rational(5), x_dom.num_bits()); + + VERIFY((one == rational(1)).is_true()); + VERIFY((five == rational(5)).is_true()); + VERIFY((five == rational(4)).is_false()); + VERIFY((five == five).is_true()); + VERIFY((five == one).is_false()); + + // Test the three different mk_eq overloads + { + bdd const x_is_five = m.mk_eq(x, rational(5)); + rational r; + auto res = x_dom.find(x_is_five, r); + VERIFY_EQ(res, find_t::singleton); + VERIFY_EQ(r, 5); + } + + { + bdd const x_is_five = m.mk_eq(bits, rational(5)); + rational r; + auto res = x_dom.find(x_is_five, r); + VERIFY_EQ(res, find_t::singleton); + VERIFY_EQ(r, 5); + } + + { + bdd const x_is_five = m.mk_eq(x, five); + rational r; + auto res = x_dom.find(x_is_five, r); + VERIFY_EQ(res, find_t::singleton); + VERIFY_EQ(r, 5); + } + } + + static void test_bddv_addsub() { + std::cout << "test_bddv_addsub\n"; + unsigned_vector bits; + bits.push_back(0); + bits.push_back(1); + bits.push_back(2); + bdd_manager m(bits.size()); + bddv const x = m.mk_var(bits); + VERIFY_EQ(x - rational(3) == rational(2), x == rational(5)); + VERIFY_EQ(x + rational(3) == rational(5), x == rational(2)); + VERIFY_EQ(x - rational(3) == rational(6), x == rational(1)); + VERIFY_EQ(x + rational(3) == rational(2), x == rational(7)); + } + + static void test_bddv_mul() { + std::cout << "test_bddv_mul\n"; + 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; + VERIFY_EQ(five_inv, x == rational(13)); + + // 6*x == 1 (mod 16) => no solution for x + bdd const six_inv = x * six == one; + VERIFY(six_inv.is_false()); + + // 6*x == 0 (mod 16) => x is either 0 or 8 (mod 16) + bdd const b = six * x == zero; + VERIFY_EQ(b, x == rational(0) || x == rational(8)); + VERIFY((b && (x != rational(0)) && (x != rational(8))).is_false()); + VERIFY_EQ(b && (x != rational(0)), x == rational(8)); + + VERIFY_EQ((x * zero).bits(), (x * rational(0)).bits()); + VERIFY_EQ((x * one).bits(), (x * rational(1)).bits()); + VERIFY_EQ((x * five).bits(), (x * rational(5)).bits()); + VERIFY_EQ((x * six).bits(), (x * rational(6)).bits()); + } + + static void test_bddv_ule() { + std::cout << "test_bddv_ule\n"; + unsigned const num_bits = 4; + bdd_manager m(num_bits); + + unsigned_vector bits; + bits.push_back(0); + bits.push_back(1); + bits.push_back(2); + bits.push_back(3); + + bddv const x = m.mk_var(bits); + bddv const three = m.mk_num(rational(3), num_bits); + bddv const four = m.mk_num(rational(4), num_bits); + bddv const five = m.mk_num(rational(5), num_bits); + + VERIFY_EQ(x >= four && x < five, x == four); + VERIFY_EQ(four <= x && x < five, x == four); + VERIFY_EQ(three < x && x < five, x == four); + VERIFY_EQ(three < x && x <= four, x == four); + VERIFY_EQ(three <= x && x < five, x == four || x == three); + } + + static void test_fdd3() { + std::cout << "test_fdd3\n"; + unsigned const w = 3; // bit width + bdd_manager m(w); + + fdd const x_dom(m, w); + bddv const& x = x_dom.var(); + + // Encodes the values x satisfying a*x + b == 0 (mod 2^w) as BDD. + auto mk_affine = [] (unsigned a, bddv const& x, unsigned b) { + return (rational(a)*x + rational(b) == rational(0)); + }; + + vector num; + for (unsigned n = 0; n < (1< num; + for (unsigned n = 0; n < (1ul << x_dom.num_bits()); ++n) { + num.push_back(x == rational(n)); + VERIFY(x_dom.contains(num[n], rational(n))); + rational r; + VERIFY_EQ(x_dom.find(num[n], r), find_t::singleton); + VERIFY_EQ(r, n); + } + + // need something extra to skew costs and trigger a reorder + bdd atleast3 = (x >= rational(3)); + VERIFY(x_dom.contains(atleast3, rational(3))); + + auto const old_levels = m.m_var2level; + std::cout << "old levels: " << old_levels << "\n"; + m.gc(); + m.try_reorder(); + std::cout << "new levels: " << m.m_var2level << "\n"; + VERIFY(old_levels != m.m_var2level); // ensure that reorder actually did something. + + // Should still give the correct answer after reordering + for (unsigned n = 0; n < (1ul << x_dom.num_bits()); ++n) { + VERIFY(x_dom.contains(num[n], rational(n))); + rational r; + VERIFY_EQ(x_dom.find(num[n], r), find_t::singleton); + VERIFY_EQ(r, n); + } + } + + static void test_fdd_twovars() { + std::cout << "test_fdd_twovars\n"; + bdd_manager m(6); + fdd const x_dom(m, 3, 0, 2); + fdd const y_dom(m, 3, 1, 2); + bddv const& x = x_dom.var(); + bddv const& y = y_dom.var(); + VERIFY_EQ(x - y <= rational(0), x == y); + } + + static void test_fdd_find_hint() { + std::cout << "test_fdd_find_hint\n"; + bdd_manager m(4); + fdd const x_dom(m, 4); + bddv const& x = x_dom.var(); + + bdd s358 = x == rational(3) || x == rational(5) || x == rational(8); + rational r; + VERIFY_EQ(x_dom.find_hint(s358, rational(8), r), find_t::multiple); + VERIFY_EQ(r, 8); + VERIFY_EQ(x_dom.find_hint(s358, rational(5), r), find_t::multiple); + VERIFY_EQ(r, 5); + VERIFY_EQ(x_dom.find_hint(s358, rational(3), r), find_t::multiple); + VERIFY_EQ(r, 3); + VERIFY_EQ(x_dom.find_hint(s358, rational(7), r), find_t::multiple); + VERIFY(r == 3 || r == 5 || r == 8); + + VERIFY_EQ(x_dom.find_hint(x == rational(5), rational(3), r), find_t::singleton); + VERIFY_EQ(r, 5); + VERIFY_EQ(x_dom.find_hint(x == rational(5), rational(5), r), find_t::singleton); + VERIFY_EQ(r, 5); + + VERIFY_EQ(x_dom.find_hint(s358 && (x == rational(4)), rational(5), r), find_t::empty); + } + + static void test_cofactor() { + std::cout << "test_cofactor\n"; + bdd_manager m(20); + bdd v0 = m.mk_var(0); + bdd v1 = m.mk_var(1); + bdd v2 = m.mk_var(2); + bdd c1 = v0 && v1 && v2; + VERIFY(c1.cofactor(v0) == (v1 && v2)); + VERIFY(c1.cofactor(v1) == (v0 && v2)); + VERIFY(c1.cofactor(v2) == (v0 && v1)); + VERIFY(c1.cofactor(!v1) == m.mk_false()); + } + + static void inc(bool_vector& x) { + for (auto& b : x) { + b = !b; + if (b) + break; + } + } + + static void dec(bool_vector& x) { + for (auto& b : x) { + b = !b; + if (!b) + break; + } + } + + static unsigned value(bool_vector const& x) { + unsigned p = 1; + unsigned v = 0; + for (auto b : x) { + v += p*b; + p <<= 1; + } + return v; + } + + static void test_sup() { + std::cout << "test_sup\n"; + bdd_manager m(20); + fdd const x_dom(m, 10); + bddv const& x = x_dom.var(); + bdd c = (1 <= x && x <= 5) || (11 <= x && x <= 13) || (29 <= x && x <= 33); + bool_vector lo(10, false); + for (unsigned i = 0; i < 20; ++i) { + unsigned v = value(lo); + bool found = x_dom.sup(c, lo); + std::cout << found << ": " << v << " - " << value(lo) << "\n"; + if (found) + std::cout << x_dom.sup(c, lo) << ": " << value(lo) << "\n"; + c = !c; + inc(lo); + } + } + + static void test_inf() { + std::cout << "test_inf\n"; + bdd_manager m(20); + fdd const x_dom(m, 10); + bddv const& x = x_dom.var(); + bdd c = (1 <= x && x <= 5) || (11 <= x && x <= 13) || (29 <= x && x <= 33); + bool_vector hi(10, true); + for (unsigned i = 0; i < 10; ++i) { + bool found = x_dom.inf(c, hi); + std::cout << found << ": " << value(hi) << "\n"; + if (found) { + std::cout << x_dom.inf(c, hi) << ": " << value(hi) << "\n"; + VERIFY(value(hi) == 0 || value(hi) == 1 || value(hi) == 5 || value(hi) == 6 || + value(hi) == 10 || value(hi) == 11 || + value(hi) == 13 || value(hi) == 14 || + value(hi) == 28 || value(hi) == 29 || + value(hi) == 33 || value(hi) == 34 || value(hi) == 1023); + } + c = !c; + dec(hi); + } + } + + + +}; + } void tst_bdd() { - dd::test1(); - dd::test2(); - dd::test3(); - dd::test4(); + dd::test_bdd::test1(); + dd::test_bdd::test2(); + dd::test_bdd::test3(); + dd::test_bdd::test4(); + dd::test_bdd::test_xor(); + dd::test_bdd::test_bddv_ops_on_constants(); + dd::test_bdd::test_bddv_eqfind_small(); + dd::test_bdd::test_bddv_eqfind(); + dd::test_bdd::test_bddv_addsub(); + dd::test_bdd::test_bddv_mul(); + dd::test_bdd::test_bddv_ule(); + dd::test_bdd::test_fdd3(); + dd::test_bdd::test_fdd4(); + dd::test_bdd::test_fdd_reorder(); + dd::test_bdd::test_fdd_twovars(); + dd::test_bdd::test_fdd_find_hint(); + dd::test_bdd::test_cofactor(); + dd::test_bdd::test_inf(); + dd::test_bdd::test_sup(); }