From bc695a5a97ce4532c1c8c0b1578d75c5ca43a42b Mon Sep 17 00:00:00 2001 From: alexandernutz <14171425+alexandernutz@users.noreply.github.com> Date: Tue, 20 Apr 2021 18:09:17 +0200 Subject: [PATCH 1/2] monotonicity unit tests (#5202) * monotonicity unit tests * indentation --- src/test/polysat.cpp | 102 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 102 insertions(+) diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index a9047d154..0cf3d57a4 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -141,6 +141,108 @@ namespace polysat { s.check(); } + + /** + * Monotonicity example from certora (1) + * expected: unsat + */ + static void test_monot1() { + scoped_solver s; + auto bw = 5; + + auto tb1 = s.var(s.add_var(bw)); + auto tb2 = s.var(s.add_var(bw)); + auto a = s.var(s.add_var(bw)); + auto v = s.var(s.add_var(bw)); + auto base1 = s.var(s.add_var(bw)); + auto base2 = s.var(s.add_var(bw)); + auto elastic1 = s.var(s.add_var(bw)); + auto elastic2 = s.var(s.add_var(bw)); + auto err = s.var(s.add_var(bw)); + + auto rem1 = s.var(s.add_var(bw)); + auto quot2 = s.var(s.add_var(bw)); + auto rem2 = s.var(s.add_var(bw)); + auto rem3 = s.var(s.add_var(bw)); + auto quot4 = s.var(s.add_var(bw)); + auto rem4 = s.var(s.add_var(bw)); + + s.add_diseq(elastic1); + + // tb1 = (v * base1) / elastic1; + s.add_eq((tb1 * elastic1) + rem1 - (v * base1)); + + // quot2 = (a * base1) / elastic1 + s.add_eq((quot2 * elastic1) + rem2 - (a * base1)); + + s.add_eq(base1 + quot2 - base2); + + s.add_eq(elastic1 + a - elastic2); + + // tb2 = ((v * base2) / elastic2); + s.add_eq((tb2 * elastic2) + rem3 - (v * base2)); + + // quot4 = v / (elastic1 + a); + s.add_eq((quot4 * (elastic1 + a)) + rem4 - v); + + s.add_eq(quot4 + 1 - err); + + s.add_ult(tb1, tb2); + s.check(); + } + + /** + * Monotonicity example from certora (2) + * expected: unsat + * + * only difference to (1) is the inequality right before the check + */ + static void test_monot2() { + scoped_solver s; + auto bw = 5; + + auto tb1 = s.var(s.add_var(bw)); + auto tb2 = s.var(s.add_var(bw)); + auto a = s.var(s.add_var(bw)); + auto v = s.var(s.add_var(bw)); + auto base1 = s.var(s.add_var(bw)); + auto base2 = s.var(s.add_var(bw)); + auto elastic1 = s.var(s.add_var(bw)); + auto elastic2 = s.var(s.add_var(bw)); + auto err = s.var(s.add_var(bw)); + + auto rem1 = s.var(s.add_var(bw)); + auto quot2 = s.var(s.add_var(bw)); + auto rem2 = s.var(s.add_var(bw)); + auto rem3 = s.var(s.add_var(bw)); + auto quot4 = s.var(s.add_var(bw)); + auto rem4 = s.var(s.add_var(bw)); + + s.add_diseq(elastic1); + + // tb1 = (v * base1) / elastic1; + s.add_eq((tb1 * elastic1) + rem1 - (v * base1)); + + // quot2 = (a * base1) / elastic1 + s.add_eq((quot2 * elastic1) + rem2 - (a * base1)); + + s.add_eq(base1 + quot2 - base2); + + s.add_eq(elastic1 + a - elastic2); + + // tb2 = ((v * base2) / elastic2); + s.add_eq((tb2 * elastic2) + rem3 - (v * base2)); + + // quot4 = v / (elastic1 + a); + s.add_eq((quot4 * (elastic1 + a)) + rem4 - v); + + s.add_eq(quot4 + 1 - err); + + s.add_ult(tb1 + err, tb2); + 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() { From 77350d97da6656972afe1c6f16a875ca1d387835 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Tue, 20 Apr 2021 18:09:32 +0200 Subject: [PATCH 2/2] BDD vectors: add subtract and quot_rem, move finite domain abstraction out of bdd_manager (#5201) * Coding style * Simplify bddv class * mk_eq: run loop from below * Add unit test for bddv unsigned comparison * Add test that shows contains_num/find_num fail after reordering * Add BDD vector subtraction * Call apply_rec in mk_ite_rec instead of apply * Question about mk_quant * Implement quot_rem over BDD vectors * Move shl/shr to bddv * Make unit test smaller * Add class dd::fdd to manage association between BDDs and numbers * Remove contains_num/find_num from bdd_manager --- src/math/dd/CMakeLists.txt | 1 + src/math/dd/dd_bdd.cpp | 168 ++++++++--------- src/math/dd/dd_bdd.h | 143 ++++++-------- src/math/dd/dd_fdd.cpp | 88 +++++++++ src/math/dd/dd_fdd.h | 69 +++++++ src/math/polysat/eq_constraint.cpp | 8 +- src/math/polysat/solver.cpp | 20 +- src/math/polysat/solver.h | 6 +- src/math/polysat/types.h | 1 + src/test/bdd.cpp | 291 +++++++++++++++++++---------- 10 files changed, 494 insertions(+), 301 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 aeb38d764..41706266d 100644 --- a/src/math/dd/dd_bdd.cpp +++ b/src/math/dd/dd_bdd.cpp @@ -23,19 +23,6 @@ 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; @@ -606,10 +593,10 @@ namespace dd { 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); @@ -659,6 +646,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); } @@ -911,65 +899,18 @@ namespace dd { std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); } - 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)) { - 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_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_result::empty; - bool is_unique = true; - unsigned var_idx = bits.size(); - while (!is_true(b)) { - 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))) { - SASSERT(var(b) == bits[var_idx]); - val += rational::power_of_two(var_idx); - b = hi(b); - } - else - b = lo(b); - } - if (var_idx > 0) - is_unique = false; - - return is_unique ? find_result::singleton : find_result::multiple; - } - - 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; ) { + 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 = a.size(); i-- > 0; ) + for (unsigned i = 0; i < a.size(); ++i) b &= n.get_bit(i) ? a[i] : !a[i]; return b; } @@ -977,7 +918,7 @@ namespace dd { 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 = vars.size(); i-- > 0; ) + for (unsigned i = 0; i < vars.size(); ++i) b &= n.get_bit(i) ? mk_var(vars[i]) : mk_nvar(vars[i]); return b; } @@ -1006,9 +947,8 @@ namespace dd { carry = (carry && a[i]) || (carry && b[i]) || (a[i] && b[i]); } #else - if (a.size() > 0) { + 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]); @@ -1017,11 +957,18 @@ namespace dd { return result; } - void bdd_manager::bddv_shl(bddv &a) { - for (unsigned j = a.size(); j-- > 1; ) { - a[j] = a[j - 1]; + 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]); } - a[0] = mk_false(); + return result; } bddv bdd_manager::mk_mul(bddv const& a, bddv const& b) { @@ -1031,18 +978,16 @@ namespace dd { for (unsigned i = 0; i < b.size(); ++i) { #if 1 bddv s = a_shifted; - for (unsigned j = i; j < b.size(); ++j) { + 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) { + for (unsigned j = 0; j < result.size(); ++j) result[j] = mk_ite(b[i], added[j], result[j]); - } #endif - bddv_shl(a_shifted); + a_shifted.shl(); } return result; } @@ -1052,10 +997,9 @@ namespace dd { bddv a_shifted = a; bddv result = mk_zero(a.size()); for (unsigned i = 0; i < a.size(); ++i) { - if (get_bit(i)) { + if (get_bit(i)) result = mk_add(result, a_shifted); - } - bddv_shl(a_shifted); + a_shifted.shl(); } return result; } @@ -1070,36 +1014,63 @@ namespace dd { return mk_mul(a, [b](unsigned i) { return b[i]; }); } + 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()); + // We work with double-size vectors + unsigned worksize = a.size() + b.size(); + // Extend dividend to worksize + rem = a; + for (unsigned i = b.size(); i-- > 0; ) + rem.push_back(mk_false()); + // Shift divisor to the left + bddv div(this); + for (unsigned i = a.size(); i-- > 0; ) + div.push_back(mk_false()); + div.m_bits.append(b.m_bits); + // Keep shifting divisor to the right and subtract whenever it is + // smaller than the remaining value + for (int i = 0; i <= b.size(); ++i) { + bdd divLteRem = div <= rem; + bddv remSubDiv = rem - div; + + for (int 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) { + 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) { + 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) { + 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) { + for (unsigned i = 0; i < num_bits; ++i) result.push_back(mk_var(vars[i])); - } return result; } @@ -1108,7 +1079,7 @@ namespace dd { } bool bdd_manager::is_constv(bddv const& a) { - for (bdd const& bit : a.bits) + for (bdd const& bit : a.bits()) if (!is_const(bit.root)) return false; return true; @@ -1119,9 +1090,8 @@ namespace dd { for (unsigned i = 0; i < a.size(); ++i) { bdd const &bit = a[i]; SASSERT(is_const(bit.root)); - if (bit.is_true()) { + if (bit.is_true()) result += rational::power_of_two(i); - } } return result; } @@ -1131,8 +1101,18 @@ 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_sub(bddv const& a, bddv const& b); - void bdd_manager::mk_quot_rem(bddv const& a, bddv const& b, bddv& quot, bddv& rem); #endif + 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(); + } + } diff --git a/src/math/dd/dd_bdd.h b/src/math/dd/dd_bdd.h index f2f2778c4..b86b2ebab 100644 --- a/src/math/dd/dd_bdd.h +++ b/src/math/dd/dd_bdd.h @@ -27,16 +27,14 @@ namespace dd { class bdd; class bddv; - - enum class find_result { empty, singleton, multiple }; - std::ostream& operator<<(std::ostream& out, find_result x); + class test_bdd; class bdd_manager { friend bdd; friend bddv; + friend test_bdd; typedef unsigned BDD; - typedef svector BDDV; const BDD null_bdd = UINT_MAX; @@ -206,10 +204,6 @@ 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 bddv mk_mul(bddv const& a, GetBitFn get_bit); public: @@ -284,7 +278,8 @@ 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!() const { return m->mk_not(*this); } bdd operator&&(bdd const& other) const { return m->mk_and(*this, other); } @@ -298,22 +293,6 @@ 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. - * - * 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. - * - * 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); @@ -321,79 +300,69 @@ namespace dd { 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 bits; - bdd_manager& m; + vector m_bits; + bdd_manager* m; - bddv(vector bits, bdd_manager* m): bits(bits), m(*m) { inc_bits_ref(); } - bddv(vector&& 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); } - } + bddv(vector 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(); - // 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 m_bits.size(); } + vector const& bits() const { return m_bits; } - unsigned size() const { return bits.size(); } - vector const& get_bits() const { return 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 - 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); } + /* 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 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); } + 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); } - // void mk_quot_rem(bddv const& a, bddv const& b, bddv& quot, bddv& rem); + 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); } - bool is_const() const { return m.is_constv(*this); } - rational to_val() const { return m.to_val(*this); } + 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); } } diff --git a/src/math/dd/dd_fdd.cpp b/src/math/dd/dd_fdd.cpp new file mode 100644 index 000000000..e981f496f --- /dev/null +++ b/src/math/dd/dd_fdd.cpp @@ -0,0 +1,88 @@ +/*++ +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; + } + } + + 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 { + out_val = 0; + if (b.is_false()) + return find_t::empty; + bool is_unique = true; + unsigned num_vars = 0; + while (!b.is_true()) { + ++num_vars; + unsigned const pos = var2pos(b.var()); + SASSERT(pos != UINT_MAX && "Unexpected BDD variable"); + if (b.lo().is_false()) { + out_val += rational::power_of_two(pos); + b = b.hi(); + } + else { + if (!b.hi().is_false()) + is_unique = false; + b = b.lo(); + } + } + if (num_vars != num_bits()) + is_unique = false; + 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; + } + +} diff --git a/src/math/dd/dd_fdd.h b/src/math/dd/dd_fdd.h new file mode 100644 index 000000000..be8841488 --- /dev/null +++ b/src/math/dd/dd_fdd.h @@ -0,0 +1,69 @@ +/*++ +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 + +--*/ +#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; // NOTE: currently unused + bddv m_var; + + static unsigned_vector seq(unsigned count) { + unsigned_vector result; + for (unsigned i = 0; i < count; ++i) + result.push_back(i); + return result; + } + + unsigned var2pos(unsigned var) const; + + public: + /** Initialize FDD using BDD variables from 0 to num_bits-1. */ + fdd(bdd_manager& manager, unsigned num_bits) : fdd(manager, seq(num_bits)) { } + 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; } + + /** 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; + }; + +} diff --git a/src/math/polysat/eq_constraint.cpp b/src/math/polysat/eq_constraint.cpp index 96ed83bc5..a27682084 100644 --- a/src/math/polysat/eq_constraint.cpp +++ b/src/math/polysat/eq_constraint.cpp @@ -57,13 +57,13 @@ namespace polysat { if (try_narrow_with(q, s)) { rational val; switch (s.find_viable(other_var, val)) { - case dd::find_result::empty: + case dd::find_t::empty: s.set_conflict(*this); return false; - case dd::find_result::singleton: + case dd::find_t::singleton: s.propagate(other_var, val, *this); return false; - case dd::find_result::multiple: + case dd::find_t::multiple: /* do nothing */ break; } @@ -95,7 +95,7 @@ namespace polysat { pvar v = q.var(); rational a = q.hi().val(); rational b = q.lo().val(); - bddv const& x = s.m_bdd.mk_var(s.sz2bits(s.size(v))); + bddv const& x = s.sz2bits(s.size(v)).var(); bdd xs = (a * x + b == rational(0)); s.intersect_viable(v, xs); s.push_cjust(v, this); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 931e05f8b..c120f6f10 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -29,20 +29,18 @@ namespace polysat { return *m_pdd[sz]; } - unsigned_vector const& solver::sz2bits(unsigned sz) { + dd::fdd const& solver::sz2bits(unsigned sz) { m_bits.reserve(sz + 1); auto* bits = m_bits[sz]; if (!bits) { - m_bits.set(sz, alloc(unsigned_vector)); + m_bits.set(sz, alloc(dd::fdd, m_bdd, sz)); bits = m_bits[sz]; - for (unsigned i = 0; i < sz; ++i) - bits->push_back(i); } return *bits; } bool solver::is_viable(pvar v, rational const& val) { - return m_viable[v].contains_num(val, sz2bits(size(v))); + return sz2bits(size(v)).contains(m_viable[v], val); } void solver::add_non_viable(pvar v, rational const& val) { @@ -50,7 +48,7 @@ namespace polysat { TRACE("polysat", tout << "v" << v << " /= " << val << "\n";); SASSERT(is_viable(v, val)); auto& bits = sz2bits(size(v)); - intersect_viable(v, !m_bdd.mk_eq(bits, val)); + intersect_viable(v, bits.var() != val); } void solver::intersect_viable(pvar v, bdd vals) { @@ -60,8 +58,8 @@ namespace polysat { set_conflict(v); } - dd::find_result solver::find_viable(pvar v, rational & val) { - return m_viable[v].find_num(sz2bits(size(v)), val); + dd::find_t solver::find_viable(pvar v, rational & val) { + return sz2bits(size(v)).find(m_viable[v], val); } solver::solver(reslimit& lim): @@ -323,15 +321,15 @@ namespace polysat { IF_LOGGING(log_viable(v)); rational val; switch (find_viable(v, val)) { - case dd::find_result::empty: + case dd::find_t::empty: LOG("Conflict: no value for pvar " << v); set_conflict(v); break; - case dd::find_result::singleton: + case dd::find_t::singleton: LOG("Propagation: pvar " << v << " := " << val << " (due to unique value)"); assign_core(v, val, justification::propagation(m_level)); break; - case dd::find_result::multiple: + case dd::find_t::multiple: LOG("Decision: pvar " << v << " := " << val); push_level(); assign_core(v, val, justification::decision(m_level)); diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 6f2263f8f..5b237bea3 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -45,7 +45,7 @@ namespace polysat { reslimit& m_lim; scoped_ptr_vector m_pdd; - scoped_ptr_vector m_bits; + scoped_ptr_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_result find_viable(pvar v, rational & val); + dd::find_t 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); - unsigned_vector const& sz2bits(unsigned sz); + dd::fdd const& sz2bits(unsigned sz); void push_level(); void pop_levels(unsigned num_levels); diff --git a/src/math/polysat/types.h b/src/math/polysat/types.h index ea6d8fb37..f799ff70c 100644 --- a/src/math/polysat/types.h +++ b/src/math/polysat/types.h @@ -20,6 +20,7 @@ Author: #include "util/ref_vector.h" #include "math/dd/dd_pdd.h" #include "math/dd/dd_bdd.h" +#include "math/dd/dd_fdd.h" namespace polysat { diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp index 1e598e3ba..5fcacb0e8 100644 --- a/src/test/bdd.cpp +++ b/src/test/bdd.cpp @@ -1,6 +1,11 @@ #include "math/dd/dd_bdd.h" +#include "math/dd/dd_fdd.h" namespace dd { + +class test_bdd { +public: + static void test1() { bdd_manager m(20); bdd v0 = m.mk_var(0); @@ -86,52 +91,65 @@ namespace dd { } static void test_bddv_ops_on_constants() { - unsigned const num_bits = 4; + 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); 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) { + for (unsigned n = 0; n < 8; ++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) { + 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); SASSERT_EQ((nv + kv).to_val(), (nr + kr) % modulus); + SASSERT_EQ((nv - kv).to_val(), (nr - kr + modulus) % 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))); + SASSERT(eq.is_const() && (eq.is_true() == (n == k))); eq = m.mk_eq(nv, kr); - SASSERT((eq.is_true() || eq.is_false()) && (eq.is_true() == (n == k))); + SASSERT(eq.is_const() && (eq.is_true() == (n == k))); + + bddv quotv = m.mk_zero(num_bits); + bddv remv = m.mk_zero(num_bits); + nv.quot_rem(kv, quotv, remv); + if (k != 0) { + SASSERT_EQ(quotv.to_val(), rational(n / k)); + SASSERT_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); - 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); + 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_is_one.find_num(bits, r); - SASSERT_EQ(res, find_result::singleton); + auto res = x_dom.find(x_is_one, r); + SASSERT_EQ(res, find_t::singleton); SASSERT_EQ(r, rational(1)); } static void test_bddv_eqfind() { - unsigned const num_bits = 4; - bdd_manager m(num_bits); + std::cout << "test_bddv_eqfind\n"; + bdd_manager m(4); unsigned_vector bits; bits.push_back(0); @@ -139,43 +157,60 @@ namespace dd { 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); + 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()); - 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()); + SASSERT((one == rational(1)).is_true()); + SASSERT((five == rational(5)).is_true()); + SASSERT((five == rational(4)).is_false()); + SASSERT((five == five).is_true()); + SASSERT((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_is_five.find_num(bits, r); - SASSERT_EQ(res, find_result::singleton); - SASSERT_EQ(r, rational(5)); + auto res = x_dom.find(x_is_five, r); + SASSERT_EQ(res, find_t::singleton); + SASSERT_EQ(r, 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)); + auto res = x_dom.find(x_is_five, r); + SASSERT_EQ(res, find_t::singleton); + SASSERT_EQ(r, 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)); + auto res = x_dom.find(x_is_five, r); + SASSERT_EQ(res, find_t::singleton); + SASSERT_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); + SASSERT_EQ(x - rational(3) == rational(2), x == rational(5)); + SASSERT_EQ(x + rational(3) == rational(5), x == rational(2)); + SASSERT_EQ(x - rational(3) == rational(6), x == rational(1)); + SASSERT_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); @@ -191,112 +226,164 @@ namespace dd { 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)); - } + // 5*x == 1 (mod 16) => x == 13 (mod 16) + bdd const five_inv = x * five == one; + SASSERT_EQ(five_inv, x == 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 == 1 (mod 16) => no solution for x + bdd const six_inv = x * six == one; + 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))); - } + // 6*x == 0 (mod 16) => x is either 0 or 8 (mod 16) + bdd const b = six * x == zero; + SASSERT_EQ(b, x == rational(0) || x == rational(8)); + SASSERT((b && (x != rational(0)) && (x != rational(8))).is_false()); + SASSERT_EQ(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()); + SASSERT_EQ((x * zero).bits(), (x * rational(0)).bits()); + SASSERT_EQ((x * one).bits(), (x * rational(1)).bits()); + SASSERT_EQ((x * five).bits(), (x * rational(5)).bits()); + SASSERT_EQ((x * six).bits(), (x * rational(6)).bits()); } - static void test_int() { - unsigned const w = 3; // bit width + 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); - bdd_manager m(w); + 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); + + SASSERT_EQ(x >= four && x < five, x == four); + SASSERT_EQ(four <= x && x < five, x == four); + SASSERT_EQ(three < x && x < five, x == four); + SASSERT_EQ(three < x && x <= four, x == four); + SASSERT_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 = [] (rational const& a, bddv const& x, rational const& b) { - return (a*x + b == rational(0)); + 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 < (1 << x_dom.num_bits()); ++n) { + num.push_back(x == rational(n)); + SASSERT(x_dom.contains(num[n], rational(n))); + rational r; + SASSERT_EQ(x_dom.find(num[n], r), find_t::singleton); + SASSERT_EQ(r, n); + } + + // need something extra to skew costs and trigger a reorder + bdd atleast3 = (x >= rational(3)); + SASSERT(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"; + SASSERT(old_levels != m.m_var2level); // ensure that reorder actually did something. + + // Should still give the correct answer after reordering + for (unsigned n = 0; n < (1 << x_dom.num_bits()); ++n) { + SASSERT(x_dom.contains(num[n], rational(n))); + rational r; + SASSERT_EQ(x_dom.find(num[n], r), find_t::singleton); + SASSERT_EQ(r, n); + } + } + +}; + } void tst_bdd() { - dd::test1(); - 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(); + 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(); }