diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 88a91e764..ef0ec4a77 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -30,12 +30,14 @@ namespace dd { alloc_free_nodes(1024 + num_vars); m_disable_gc = false; m_is_new_node = false; + m_mod2_semantics = false; // add dummy nodes for operations, and 0, 1 pdds. - imk_val(rational::zero()); // becomes pdd_zero - imk_val(rational::one()); // becomes pdd_one + const_info info; + init_value(info, rational::zero()); // becomes pdd_zero + init_value(info, rational::one()); // becomes pdd_one for (unsigned i = 2; i <= pdd_no_op + 2; ++i) { - m_nodes.push_back(pdd_node(0,0,0,0)); + m_nodes.push_back(pdd_node(0,0,0)); m_nodes.back().m_refcount = max_rc; m_nodes.back().m_index = m_nodes.size()-1; } @@ -105,7 +107,7 @@ namespace dd { case pdd_add_op: if (is_zero(a)) return b; if (is_zero(b)) return a; - if (is_val(a) && is_val(b)) return imk_val(val(a) + val(b)); + if (is_val(a) && is_val(b)) return imk_val(m_mod2_semantics ? ((val(a) + val(b)) % rational(2)) : val(a) + val(b)); if (level(a) < level(b)) std::swap(a, b); break; case pdd_mul_op: @@ -176,15 +178,23 @@ namespace dd { } else if (level_a == level_b) { // (xa+b)*(xc+d) = x(x*ac + (ad+bc)) + bd + // (xa+b)*(xc+d) mod2 == x(ac+bc+ad) + bd push(apply_rec(hi(a), hi(b), op)); push(apply_rec(hi(a), lo(b), op)); push(apply_rec(lo(a), hi(b), op)); push(apply_rec(lo(a), lo(b), op)); unsigned ac = read(4), ad = read(3), bc = read(2), bd = read(1); push(apply_rec(ad, bc, pdd_add_op)); - r = make_node(level_a, read(1), ac); - r = make_node(level_a, bd, r); - npop = 5; + if (m_mod2_semantics) { + push(apply_rec(read(1), ac, pdd_add_op)); + r = make_node(level_a, bd, read(1)); + npop = 6; + } + else { + r = make_node(level_a, read(1), ac); + r = make_node(level_a, bd, r); + npop = 5; + } } else { // (xa+b)*c = x(ac) + bc @@ -218,6 +228,9 @@ namespace dd { } pdd pdd_manager::minus(pdd const& a) { + if (m_mod2_semantics) { + return a; + } bool first = true; SASSERT(well_formed()); scoped_push _sp(*this); @@ -285,7 +298,8 @@ namespace dd { SASSERT(is_val(p) || !is_val(q)); if (is_val(p)) { if (is_val(q)) { - return imk_val(-val(q)/val(p)); + SASSERT(!val(p).is_zero()); + return m_mod2_semantics ? imk_val(val(q)) : imk_val(-val(q)/val(p)); } } else if (level(p) == level(q)) { @@ -304,10 +318,12 @@ namespace dd { } pdd pdd_manager::spoly(pdd const& a, pdd const& b, unsigned_vector const& p, unsigned_vector const& q, rational const& pc, rational const& qc) { - pdd r1 = mul(qc, a); + pdd r1 = mk_val(qc); for (unsigned i = q.size(); i-- > 0; ) r1 = mul(mk_var(q[i]), r1); - pdd r2 = mul(-pc, b); + r1 = mul(a, r1); + pdd r2 = mk_val(m_mod2_semantics ? pc : -pc); for (unsigned i = p.size(); i-- > 0; ) r2 = mul(mk_var(p[i]), r2); + r2 = mul(b, r2); return add(r1, r2); } @@ -385,14 +401,11 @@ namespace dd { y = hi(y); } else { - return false; + return true; } } } - double pdd_manager::tree_size(pdd const& p) const { return tree_size(p.root); } - - void pdd_manager::push(PDD b) { m_pdd_stack.push_back(b); } @@ -428,24 +441,30 @@ namespace dd { } pdd_manager::PDD pdd_manager::imk_val(rational const& r) { + if (r.is_zero()) return zero_pdd; + if (r.is_one()) return one_pdd; const_info info; if (!m_mpq_table.find(r, info)) { - pdd_node n(m_values.size()); - info.m_value_index = m_values.size(); - info.m_node_index = insert_node(n); - m_mpq_table.insert(r, info); - m_values.push_back(r); - m_nodes[info.m_node_index].m_refcount = max_rc; + init_value(info, r); } return info.m_node_index; } + void pdd_manager::init_value(const_info& info, rational const& r) { + pdd_node n(m_values.size()); + info.m_value_index = m_values.size(); + info.m_node_index = insert_node(n); + m_mpq_table.insert(r, info); + m_values.push_back(r); + m_nodes[info.m_node_index].m_refcount = max_rc; + } + pdd_manager::PDD pdd_manager::make_node(unsigned lvl, PDD l, PDD h) { m_is_new_node = false; if (is_zero(h)) return l; SASSERT(is_val(l) || level(l) < lvl); SASSERT(is_val(h) || level(h) <= lvl); - pdd_node n(lvl, l, h, tree_size(l) + tree_size(h) + 1); + pdd_node n(lvl, l, h); return insert_node(n); } @@ -557,6 +576,33 @@ namespace dd { return m_degree[b.root]; } + + double pdd_manager::tree_size(pdd const& p) { + init_mark(); + m_tree_size.reserve(m_nodes.size()); + m_todo.push_back(p.root); + while (!m_todo.empty()) { + PDD r = m_todo.back(); + if (is_marked(r)) { + m_todo.pop_back(); + } + else if (is_val(r)) { + m_tree_size[r] = 1; + set_mark(r); + } + else if (!is_marked(lo(r)) || !is_marked(hi(r))) { + m_todo.push_back(lo(r)); + m_todo.push_back(hi(r)); + } + else { + m_tree_size[r] = 1 + m_tree_size[lo(r)] + m_tree_size[hi(r)]; + set_mark(r); + } + } + return m_tree_size[p.root]; + } + + void pdd_manager::alloc_free_nodes(unsigned n) { for (unsigned i = 0; i < n; ++i) { m_free_nodes.push_back(m_nodes.size()); diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index e70c8aed2..19bf4db8a 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -56,30 +56,27 @@ namespace dd { }; struct pdd_node { - pdd_node(unsigned level, PDD lo, PDD hi, double tree_size): + pdd_node(unsigned level, PDD lo, PDD hi): m_refcount(0), m_level(level), m_lo(lo), m_hi(hi), - m_index(0), - m_tree_size(tree_size) + m_index(0) {} pdd_node(unsigned value): m_refcount(0), m_level(0), m_lo(value), m_hi(0), - m_index(0), - m_tree_size(1) + m_index(0) {} - pdd_node(): m_refcount(0), m_level(0), m_lo(0), m_hi(0), m_index(0), m_tree_size(0) {} + pdd_node(): m_refcount(0), m_level(0), m_lo(0), m_hi(0), m_index(0) {} unsigned m_refcount : 10; unsigned m_level : 22; PDD m_lo; PDD m_hi; unsigned m_index; - double m_tree_size; unsigned hash() const { return mk_mix(m_level, m_lo, m_hi); } bool is_internal() const { return m_lo == 0 && m_hi == 0; } void set_internal() { m_lo = 0; m_hi = 0; } @@ -146,9 +143,11 @@ namespace dd { mutable unsigned m_mark_level; mutable svector m_todo; mutable unsigned_vector m_degree; + mutable svector m_tree_size; bool m_disable_gc; bool m_is_new_node; unsigned m_max_num_pdd_nodes; + bool m_mod2_semantics; PDD make_node(unsigned level, PDD l, PDD r); PDD insert_node(pdd_node const& n); @@ -162,7 +161,8 @@ namespace dd { bool lm_divides(PDD p, PDD q) const; PDD lt_quotient(PDD p, PDD q); - PDD imk_val(rational const& r); + PDD imk_val(rational const& r); + void init_value(const_info& info, rational const& r); void push(PDD b); void pop(unsigned num_scopes); @@ -190,7 +190,6 @@ namespace dd { inline void inc_ref(PDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount++; SASSERT(!m_free_nodes.contains(b)); } inline void dec_ref(PDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount--; SASSERT(!m_free_nodes.contains(b)); } inline PDD level2pdd(unsigned l) const { return m_var2pdd[m_level2var[l]]; } - inline double tree_size(PDD p) const { return m_nodes[p].m_tree_size; } unsigned dag_size(pdd const& b); unsigned degree(pdd const& p); @@ -220,6 +219,7 @@ namespace dd { pdd_manager(unsigned nodes); ~pdd_manager(); + void set_mod2_semantics() { m_mod2_semantics = true; } void set_max_num_nodes(unsigned n) { m_max_num_pdd_nodes = n; } void set_var_order(unsigned_vector const& levels); // TBD: set variable order (m_var2level, m_level2var) before doing anything else. @@ -237,7 +237,7 @@ namespace dd { bool try_spoly(pdd const& a, pdd const& b, pdd& r); bool lt(pdd const& a, pdd const& b); bool different_leading_term(pdd const& a, pdd const& b); - double tree_size(pdd const& p) const; + double tree_size(pdd const& p); std::ostream& display(std::ostream& out); std::ostream& display(std::ostream& out, pdd const& b);