From 0520558fc0e18979d79935c3630ad5bde09a1dae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Dec 2023 08:53:58 -0800 Subject: [PATCH] port updated pdd from polysat Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.cpp | 160 +++++++++++++++++++++++++----------- src/math/dd/dd_pdd.h | 180 +++++++++++++++++++++++++---------------- 2 files changed, 222 insertions(+), 118 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 970eb991f..55156c53a 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -113,11 +113,34 @@ namespace dd { pdd pdd_manager::add(rational const& r, pdd const& b) { pdd c(mk_val(r)); return pdd(apply(c.root, b.root, pdd_add_op), this); } pdd pdd_manager::zero() { return pdd(zero_pdd, this); } pdd pdd_manager::one() { return pdd(one_pdd, this); } - - pdd pdd_manager::mk_or(pdd const& p, pdd const& q) { return p + q - (p*q); } - pdd pdd_manager::mk_xor(pdd const& p, pdd const& q) { if (m_semantics == mod2_e) return p + q; return (p*q*2) - p - q; } - pdd pdd_manager::mk_xor(pdd const& p, unsigned x) { pdd q(mk_val(x)); if (m_semantics == mod2_e) return p + q; return (p*q*2) - p - q; } - pdd pdd_manager::mk_not(pdd const& p) { return 1 - p; } + + // NOTE: bit-wise AND cannot be expressed in mod2N_e semantics with the existing operations. + pdd pdd_manager::mk_and(pdd const& p, pdd const& q) { + VERIFY(m_semantics == mod2_e || m_semantics == zero_one_vars_e); + return p * q; + } + + pdd pdd_manager::mk_or(pdd const& p, pdd const& q) { + return p + q - mk_and(p, q); + } + + pdd pdd_manager::mk_xor(pdd const& p, pdd const& q) { + if (m_semantics == mod2_e) + return p + q; + return p + q - 2*mk_and(p, q); + } + + pdd pdd_manager::mk_xor(pdd const& p, unsigned x) { + pdd q(mk_val(x)); + return mk_xor(p, q); + } + + pdd pdd_manager::mk_not(pdd const& p) { + if (m_semantics == mod2N_e) + return -p - 1; + VERIFY(m_semantics == mod2_e || m_semantics == zero_one_vars_e); + return 1 - p; + } pdd pdd_manager::subst_val(pdd const& p, unsigned v, rational const& val) { pdd r = mk_var(v) + val; @@ -173,15 +196,8 @@ namespace dd { if (m_semantics != mod2N_e) return 0; - if (is_val(p)) { - rational v = val(p); - if (v.is_zero()) - return m_power_of_2 + 1; - unsigned r = 0; - while (v.is_even() && v > 0) - r++, v /= 2; - return r; - } + if (is_val(p)) + return val(p).parity(m_power_of_2); init_mark(); PDD q = p; m_todo.push_back(hi(q)); @@ -189,9 +205,9 @@ namespace dd { q = lo(q); m_todo.push_back(hi(q)); } - unsigned p2 = val(q).trailing_zeros(); + unsigned parity = val(q).parity(m_power_of_2); init_mark(); - while (p2 != 0 && !m_todo.empty()) { + while (parity != 0 && !m_todo.empty()) { PDD r = m_todo.back(); m_todo.pop_back(); if (is_marked(r)) @@ -203,11 +219,11 @@ namespace dd { } else if (val(r).is_zero()) continue; - else if (val(r).trailing_zeros() < p2) - p2 = val(r).trailing_zeros(); + else + parity = std::min(parity, val(r).trailing_zeros()); } m_todo.reset(); - return p2; + return parity; } pdd pdd_manager::subst_val(pdd const& p, pdd const& s) { @@ -246,7 +262,7 @@ namespace dd { } pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) { - bool first = true; + unsigned count = 0; SASSERT(well_formed()); scoped_push _sp(*this); while (true) { @@ -255,8 +271,9 @@ namespace dd { } catch (const mem_out &) { try_gc(); - if (!first) throw; - first = false; + if (count > 0) + m_max_num_nodes *= 2; + count++; } } SASSERT(well_formed()); @@ -507,7 +524,7 @@ namespace dd { if (m_semantics == mod2_e) { return a; } - bool first = true; + unsigned count = 0; SASSERT(well_formed()); scoped_push _sp(*this); while (true) { @@ -516,8 +533,9 @@ namespace dd { } catch (const mem_out &) { try_gc(); - if (!first) throw; - first = false; + if (count > 0) + m_max_num_nodes *= 2; + ++count; } } SASSERT(well_formed()); @@ -565,7 +583,7 @@ namespace dd { return true; } SASSERT(c.is_int()); - bool first = true; + unsigned count = 0; SASSERT(well_formed()); scoped_push _sp(*this); while (true) { @@ -578,8 +596,9 @@ namespace dd { } catch (const mem_out &) { try_gc(); - if (!first) throw; - first = false; + if (count > 0) + m_max_num_nodes *= 2; + ++count; } } } @@ -1138,6 +1157,7 @@ namespace dd { unsigned pdd_manager::max_pow2_divisor(PDD p) { init_mark(); unsigned min_j = UINT_MAX; + SASSERT(m_todo.empty()); m_todo.push_back(p); while (!m_todo.empty()) { PDD r = m_todo.back(); @@ -1785,27 +1805,42 @@ namespace dd { } pdd& pdd::operator=(pdd const& other) { + if (m != other.m) { + verbose_stream() << "pdd manager confusion: " << *this << " (mod 2^" << power_of_2() << ") := " << other << " (mod 2^" << other.power_of_2() << ")\n"; + // TODO: in the end, this operator should probably be changed to also update the manager. But for now I want to detect such confusions. + } + SASSERT_EQ(power_of_2(), other.power_of_2()); + VERIFY_EQ(power_of_2(), other.power_of_2()); + VERIFY_EQ(m, other.m); unsigned r1 = root; root = other.root; - m.inc_ref(root); - m.dec_ref(r1); + m->inc_ref(root); + m->dec_ref(r1); return *this; } pdd& pdd::operator=(unsigned k) { - m.dec_ref(root); - root = m.mk_val(k).root; - m.inc_ref(root); + m->dec_ref(root); + root = m->mk_val(k).root; + m->inc_ref(root); return *this; } pdd& pdd::operator=(rational const& k) { - m.dec_ref(root); - root = m.mk_val(k).root; - m.inc_ref(root); + m->dec_ref(root); + root = m->mk_val(k).root; + m->inc_ref(root); return *this; } + /* Reset pdd to 0. Allows re-assigning the pdd manager. */ + void pdd::reset(pdd_manager& new_m) { + m->dec_ref(root); + root = 0; + m = &new_m; + SASSERT(is_zero()); + } + rational const& pdd::leading_coefficient() const { pdd p = *this; while (!p.is_val()) @@ -1813,11 +1848,10 @@ namespace dd { return p.val(); } - rational const& pdd::offset() const { - pdd p = *this; - while (!p.is_val()) - p = p.lo(); - return p.val(); + rational const& pdd_manager::offset(PDD p) const { + while (!is_val(p)) + p = lo(p); + return val(p); } pdd pdd::shl(unsigned n) const { @@ -1831,7 +1865,7 @@ namespace dd { pdd pdd::subst_pdd(unsigned v, pdd const& r) const { if (is_val()) return *this; - if (m.m_var2level[var()] < m.m_var2level[v]) + if (m->m_var2level[var()] < m->m_var2level[v]) return *this; pdd l = lo().subst_pdd(v, r); pdd h = hi().subst_pdd(v, r); @@ -1840,7 +1874,7 @@ namespace dd { else if (l == lo() && h == hi()) return *this; else - return m.mk_var(var())*h + l; + return m->mk_var(var())*h + l; } std::pair pdd::var_factors() const { @@ -1871,7 +1905,7 @@ namespace dd { ++i; ++j; } - else if (m.m_var2level[lo_vars[i]] > m.m_var2level[hi_vars[j]]) + else if (m->m_var2level[lo_vars[i]] > m->m_var2level[hi_vars[j]]) hi_vars[jr++] = hi_vars[j++]; else lo_vars[ir++] = lo_vars[i++]; @@ -1882,7 +1916,7 @@ namespace dd { auto mul = [&](unsigned_vector const& vars, pdd p) { for (auto v : vars) - p *= m.mk_var(v); + p *= m->mk_var(v); return p; }; @@ -1908,7 +1942,7 @@ namespace dd { std::ostream& operator<<(std::ostream& out, pdd const& b) { return b.display(out); } void pdd_iterator::next() { - auto& m = m_pdd.m; + auto& m = m_pdd.manager(); while (!m_nodes.empty()) { auto& p = m_nodes.back(); if (p.first && !m.is_val(p.second)) { @@ -1935,13 +1969,16 @@ namespace dd { void pdd_iterator::first() { unsigned n = m_pdd.root; - auto& m = m_pdd.m; + auto& m = m_pdd.manager(); while (!m.is_val(n)) { m_nodes.push_back(std::make_pair(true, n)); m_mono.vars.push_back(m.var(n)); n = m.hi(n); } m_mono.coeff = m.val(n); + // if m_pdd is constant and non-zero, the iterator should return a single monomial + if (m_nodes.empty() && !m_mono.coeff.is_zero()) + m_nodes.push_back(std::make_pair(false, n)); } pdd_iterator pdd::begin() const { return pdd_iterator(*this, true); } @@ -1960,5 +1997,32 @@ namespace dd { return out; } + void pdd_linear_iterator::first() { + m_next = m_pdd.root; + next(); + } -} + void pdd_linear_iterator::next() { + SASSERT(m_next != pdd_manager::null_pdd); + auto& m = m_pdd.manager(); + while (!m.is_val(m_next)) { + unsigned const var = m.var(m_next); + rational const val = m.offset(m.hi(m_next)); + m_next = m.lo(m_next); + if (!val.is_zero()) { + m_mono = {val, var}; + return; + } + } + m_next = pdd_manager::null_pdd; + } + + pdd_linear_iterator pdd::pdd_linear_monomials::begin() const { + return pdd_linear_iterator(m_pdd, true); + } + + pdd_linear_iterator pdd::pdd_linear_monomials::end() const { + return pdd_linear_iterator(m_pdd, false); + } + +} // namespace dd diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index f2547e962..2dc9a9480 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -45,6 +45,7 @@ namespace dd { class pdd; class pdd_manager; class pdd_iterator; + class pdd_linear_iterator; class pdd_manager { public: @@ -53,13 +54,14 @@ namespace dd { friend test; friend pdd; friend pdd_iterator; + friend pdd_linear_iterator; typedef unsigned PDD; typedef vector> monomials_t; - const PDD null_pdd = UINT_MAX; - const PDD zero_pdd = 0; - const PDD one_pdd = 1; + static constexpr PDD null_pdd = UINT_MAX; + static constexpr PDD zero_pdd = 0; + static constexpr PDD one_pdd = 1; enum pdd_op { pdd_add_op = 2, @@ -261,6 +263,7 @@ namespace dd { inline PDD lo(PDD p) const { return m_nodes[p].m_lo; } inline PDD hi(PDD p) const { return m_nodes[p].m_hi; } inline rational const& val(PDD p) const { SASSERT(is_val(p)); return m_values[lo(p)]; } + inline rational get_signed_val(PDD p) const { SASSERT(m_semantics == mod2_e || m_semantics == mod2N_e); rational const& a = val(p); return a.get_bit(power_of_2() - 1) ? a - two_to_N() : a; } inline void inc_ref(PDD p) { if (m_nodes[p].m_refcount != max_rc) m_nodes[p].m_refcount++; SASSERT(!m_free_nodes.contains(p)); } inline void dec_ref(PDD p) { if (m_nodes[p].m_refcount != max_rc) m_nodes[p].m_refcount--; SASSERT(!m_free_nodes.contains(p)); } inline PDD level2pdd(unsigned l) const { return m_var2pdd[m_level2var[l]]; } @@ -341,9 +344,10 @@ namespace dd { pdd mul(rational const& c, pdd const& b); pdd div(pdd const& a, rational const& c); bool try_div(pdd const& a, rational const& c, pdd& out_result); + pdd mk_and(pdd const& p, pdd const& q); pdd mk_or(pdd const& p, pdd const& q); pdd mk_xor(pdd const& p, pdd const& q); - pdd mk_xor(pdd const& p, unsigned q); + pdd mk_xor(pdd const& p, unsigned x); pdd mk_not(pdd const& p); pdd reduce(pdd const& a, pdd const& b); pdd subst_val0(pdd const& a, vector> const& s); @@ -368,6 +372,8 @@ namespace dd { bool is_univariate_in(PDD p, unsigned v); void get_univariate_coefficients(PDD p, vector& coeff); + rational const& offset(PDD p) const; + // create an spoly r if leading monomials of a and b overlap bool try_spoly(pdd const& a, pdd const& b, pdd& r); @@ -399,106 +405,120 @@ namespace dd { friend test; friend class pdd_manager; friend class pdd_iterator; + friend class pdd_linear_iterator; unsigned root; - pdd_manager& m; - pdd(unsigned root, pdd_manager& m): root(root), m(m) { m.inc_ref(root); } - pdd(unsigned root, pdd_manager* _m): root(root), m(*_m) { m.inc_ref(root); } + pdd_manager* m; + pdd(unsigned root, pdd_manager& pm): root(root), m(&pm) { m->inc_ref(root); } + pdd(unsigned root, pdd_manager* pm): root(root), m(pm) { m->inc_ref(root); } public: - pdd(pdd_manager& pm): root(0), m(pm) { SASSERT(is_zero()); } - pdd(pdd const& other): root(other.root), m(other.m) { m.inc_ref(root); } - pdd(pdd && other) noexcept : root(0), m(other.m) { std::swap(root, other.root); } + pdd(pdd_manager& m): pdd(0, m) { SASSERT(is_zero()); } + pdd(pdd const& other): pdd(other.root, other.m) { m->inc_ref(root); } + pdd(pdd && other) noexcept : pdd(0, other.m) { std::swap(root, other.root); } pdd& operator=(pdd const& other); pdd& operator=(unsigned k); pdd& operator=(rational const& k); - ~pdd() { m.dec_ref(root); } - pdd lo() const { return pdd(m.lo(root), m); } - pdd hi() const { return pdd(m.hi(root), m); } + // TODO: pdd& operator=(pdd&& other); (just swap like move constructor?) + ~pdd() { m->dec_ref(root); } + void reset(pdd_manager& new_m); + pdd lo() const { return pdd(m->lo(root), m); } + pdd hi() const { return pdd(m->hi(root), m); } unsigned index() const { return root; } - unsigned var() const { return m.var(root); } - rational const& val() const { SASSERT(is_val()); return m.val(root); } + unsigned var() const { return m->var(root); } + rational const& val() const { return m->val(root); } + rational get_signed_val() const { return m->get_signed_val(root); } rational const& leading_coefficient() const; - rational const& offset() const; - bool is_val() const { return m.is_val(root); } - bool is_one() const { return m.is_one(root); } - bool is_zero() const { return m.is_zero(root); } - bool is_linear() const { return m.is_linear(root); } - bool is_var() const { return m.is_var(root); } - bool is_max() const { return m.is_max(root); } + rational const& offset() const { return m->offset(root); } + bool is_val() const { return m->is_val(root); } + bool is_one() const { return m->is_one(root); } + bool is_zero() const { return m->is_zero(root); } + bool is_linear() const { return m->is_linear(root); } + bool is_var() const { return m->is_var(root); } + bool is_max() const { return m->is_max(root); } /** Polynomial is of the form a * x + b for some numerals a, b. */ bool is_unilinear() const { return !is_val() && lo().is_val() && hi().is_val(); } /** Polynomial is of the form a * x for some numeral a. */ bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); } bool is_offset() const { return !is_val() && lo().is_val() && hi().is_one(); } - bool is_binary() const { return m.is_binary(root); } - bool is_monomial() const { return m.is_monomial(root); } - bool is_univariate() const { return m.is_univariate(root); } - bool is_univariate_in(unsigned v) const { return m.is_univariate_in(root, v); } - void get_univariate_coefficients(vector& coeff) const { m.get_univariate_coefficients(root, coeff); } - vector get_univariate_coefficients() const { vector coeff; m.get_univariate_coefficients(root, coeff); return coeff; } - bool is_never_zero() const { return m.is_never_zero(root); } - unsigned min_parity() const { return m.min_parity(root); } - bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); } + bool is_binary() const { return m->is_binary(root); } + bool is_monomial() const { return m->is_monomial(root); } + bool is_univariate() const { return m->is_univariate(root); } + bool is_univariate_in(unsigned v) const { return m->is_univariate_in(root, v); } + void get_univariate_coefficients(vector& coeff) const { m->get_univariate_coefficients(root, coeff); } + vector get_univariate_coefficients() const { vector coeff; m->get_univariate_coefficients(root, coeff); return coeff; } + bool is_never_zero() const { return m->is_never_zero(root); } + unsigned min_parity() const { return m->min_parity(root); } + bool var_is_leaf(unsigned v) const { return m->var_is_leaf(root, v); } - pdd operator-() const { return m.minus(*this); } - pdd operator+(pdd const& other) const { return m.add(*this, other); } - pdd operator-(pdd const& other) const { return m.sub(*this, other); } - pdd operator*(pdd const& other) const { return m.mul(*this, other); } - pdd operator&(pdd const& other) const { return m.mul(*this, other); } - pdd operator|(pdd const& other) const { return m.mk_or(*this, other); } - pdd operator^(pdd const& other) const { return m.mk_xor(*this, other); } - pdd operator^(unsigned other) const { return m.mk_xor(*this, other); } + pdd operator-() const { return m->minus(*this); } + pdd operator+(pdd const& other) const { VERIFY_EQ(m, other.m); return m->add(*this, other); } + pdd operator-(pdd const& other) const { VERIFY_EQ(m, other.m); return m->sub(*this, other); } + pdd operator*(pdd const& other) const { VERIFY_EQ(m, other.m); return m->mul(*this, other); } + pdd operator&(pdd const& other) const { VERIFY_EQ(m, other.m); return m->mk_and(*this, other); } + pdd operator|(pdd const& other) const { VERIFY_EQ(m, other.m); return m->mk_or(*this, other); } + pdd operator^(pdd const& other) const { VERIFY_EQ(m, other.m); return m->mk_xor(*this, other); } + pdd operator^(unsigned other) const { return m->mk_xor(*this, m->mk_val(other)); } - pdd operator*(rational const& other) const { return m.mul(other, *this); } - pdd operator+(rational const& other) const { return m.add(other, *this); } - pdd operator~() const { return m.mk_not(*this); } + pdd operator*(rational const& other) const { return m->mul(other, *this); } + pdd operator+(rational const& other) const { return m->add(other, *this); } + pdd operator~() const { return m->mk_not(*this); } pdd shl(unsigned n) const; - pdd rev_sub(rational const& r) const { return m.sub(m.mk_val(r), *this); } - pdd div(rational const& other) const { return m.div(*this, other); } - bool try_div(rational const& other, pdd& out_result) const { return m.try_div(*this, other, out_result); } - pdd pow(unsigned j) const { return m.pow(*this, j); } - pdd reduce(pdd const& other) const { return m.reduce(*this, other); } - bool different_leading_term(pdd const& other) const { return m.different_leading_term(*this, other); } - void factor(unsigned v, unsigned degree, pdd& lc, pdd& rest) const { m.factor(*this, v, degree, lc, rest); } - bool factor(unsigned v, unsigned degree, pdd& lc) const { return m.factor(*this, v, degree, lc); } - bool resolve(unsigned v, pdd const& other, pdd& result) { return m.resolve(v, *this, other, result); } - pdd reduce(unsigned v, pdd const& other) const { return m.reduce(v, *this, other); } + pdd rev_sub(rational const& r) const { return m->sub(m->mk_val(r), *this); } + pdd div(rational const& other) const { return m->div(*this, other); } + bool try_div(rational const& other, pdd& out_result) const { VERIFY_EQ(m, out_result.m); return m->try_div(*this, other, out_result); } + pdd pow(unsigned j) const { return m->pow(*this, j); } + pdd reduce(pdd const& other) const { VERIFY_EQ(m, other.m); return m->reduce(*this, other); } + bool different_leading_term(pdd const& other) const { VERIFY_EQ(m, other.m); return m->different_leading_term(*this, other); } + void factor(unsigned v, unsigned degree, pdd& lc, pdd& rest) const { VERIFY_EQ(m, lc.m); VERIFY_EQ(m, rest.m); m->factor(*this, v, degree, lc, rest); } + bool factor(unsigned v, unsigned degree, pdd& lc) const { VERIFY_EQ(m, lc.m); return m->factor(*this, v, degree, lc); } + bool resolve(unsigned v, pdd const& other, pdd& result) { VERIFY_EQ(m, other.m); VERIFY_EQ(m, result.m); return m->resolve(v, *this, other, result); } + pdd reduce(unsigned v, pdd const& other) const { VERIFY_EQ(m, other.m); return m->reduce(v, *this, other); } /** * \brief factor out variables */ std::pair var_factors() const; - pdd subst_val0(vector> const& s) const { return m.subst_val0(*this, s); } - pdd subst_val(pdd const& s) const { return m.subst_val(*this, s); } - pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); } - pdd subst_add(unsigned var, rational const& val) const { return m.subst_add(*this, var, val); } - bool subst_get(unsigned var, rational& out_val) const { return m.subst_get(*this, var, out_val); } + pdd subst_val0(vector> const& s) const { return m->subst_val0(*this, s); } + pdd subst_val(pdd const& s) const { VERIFY_EQ(m, s.m); return m->subst_val(*this, s); } + pdd subst_val(unsigned v, rational const& val) const { return m->subst_val(*this, v, val); } + pdd subst_add(unsigned var, rational const& val) const { return m->subst_add(*this, var, val); } + bool subst_get(unsigned var, rational& out_val) const { return m->subst_get(*this, var, out_val); } /** * \brief substitute variable v by r. */ pdd subst_pdd(unsigned v, pdd const& r) const; - std::ostream& display(std::ostream& out) const { return m.display(out, *this); } - bool operator==(pdd const& other) const { return root == other.root; } - bool operator!=(pdd const& other) const { return root != other.root; } + std::ostream& display(std::ostream& out) const { return m->display(out, *this); } + bool operator==(pdd const& other) const { return root == other.root && m == other.m; } + bool operator!=(pdd const& other) const { return !operator==(other); } unsigned hash() const { return root; } - unsigned power_of_2() const { return m.power_of_2(); } + unsigned power_of_2() const { return m->power_of_2(); } - unsigned dag_size() const { return m.dag_size(*this); } - double tree_size() const { return m.tree_size(*this); } - unsigned degree() const { return m.degree(*this); } - unsigned degree(unsigned v) const { return m.degree(root, v); } - unsigned max_pow2_divisor() const { return m.max_pow2_divisor(root); } - unsigned_vector const& free_vars() const { return m.free_vars(*this); } + unsigned dag_size() const { return m->dag_size(*this); } + double tree_size() const { return m->tree_size(*this); } + unsigned degree() const { return m->degree(*this); } + unsigned degree(unsigned v) const { return m->degree(root, v); } + unsigned max_pow2_divisor() const { return m->max_pow2_divisor(root); } + unsigned_vector const& free_vars() const { return m->free_vars(*this); } - void swap(pdd& other) { std::swap(root, other.root); } + void swap(pdd& other) { VERIFY_EQ(m, other.m); std::swap(root, other.root); } pdd_iterator begin() const; pdd_iterator end() const; - pdd_manager& manager() const { return m; } + class pdd_linear_monomials { + friend class pdd; + pdd const& m_pdd; + pdd_linear_monomials(pdd const& p): m_pdd(p) {} + public: + pdd_linear_iterator begin() const; + pdd_linear_iterator end() const; + }; + pdd_linear_monomials linear_monomials() const { return pdd_linear_monomials(*this); } + + pdd_manager& manager() const { return *m; } }; inline pdd operator*(rational const& r, pdd const& b) { return b * r; } @@ -552,7 +572,27 @@ namespace dd { pdd_iterator& operator++() { next(); return *this; } pdd_iterator operator++(int) { auto tmp = *this; next(); return tmp; } bool operator==(pdd_iterator const& other) const { return m_nodes == other.m_nodes; } - bool operator!=(pdd_iterator const& other) const { return m_nodes != other.m_nodes; } + bool operator!=(pdd_iterator const& other) const { return !operator==(other); } + }; + + class pdd_linear_iterator { + friend class pdd::pdd_linear_monomials; + pdd m_pdd; + std::pair m_mono; + pdd_manager::PDD m_next = pdd_manager::null_pdd; + pdd_linear_iterator(pdd const& p, bool at_start): m_pdd(p) { if (at_start) first(); } + void first(); + void next(); + public: + using value_type = std::pair; // coefficient and variable + using reference = value_type const&; + using pointer = value_type const*; + reference operator*() const { return m_mono; } + pointer operator->() const { return &m_mono; } + pdd_linear_iterator& operator++() { next(); return *this; } + pdd_linear_iterator operator++(int) { auto tmp = *this; next(); return tmp; } + bool operator==(pdd_linear_iterator const& other) const { return m_next == other.m_next; } + bool operator!=(pdd_linear_iterator const& other) const { return m_next != other.m_next; } }; class val_pp {