From a744a465e6fb8a5ef211e722b322f730a174e8ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Dec 2019 21:25:18 -0800 Subject: [PATCH] pdd fixes Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.cpp | 112 ++++++++++++++++++++++++++++------------- src/math/dd/dd_pdd.h | 11 ++++ src/test/pdd.cpp | 31 +++++++++++- 3 files changed, 117 insertions(+), 37 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 427d5a445..ad3205286 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -64,6 +64,8 @@ namespace dd { pdd pdd_manager::mul(rational const& r, pdd const& b) { pdd c(mk_val(r)); return pdd(apply(c.root, b.root, pdd_mul_op), this); } 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::minus(pdd const& b) { return pdd(apply(zero_pdd, b.root, pdd_sub_op), this); } + pdd pdd_manager::zero() { return pdd(zero_pdd, this); } + pdd pdd_manager::one() { return pdd(one_pdd, this); } pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) { bool first = true; @@ -144,12 +146,18 @@ namespace dd { if (is_val(a)) { SASSERT(!is_val(b)); push(apply_rec(a, lo(b), op)); - r = make_node(level_b, read(1), hi(b)); - npop = 1; + if (op == pdd_sub_op) { + push(apply_rec(zero_pdd, hi(b), op)); + r = make_node(level_b, read(2), read(1)); + } + else { + r = make_node(level_b, read(1), hi(b)); + npop = 1; + } } else if (is_val(b)) { SASSERT(!is_val(a)); - push(apply_rec(b, lo(a), op)); + push(apply_rec(lo(a), b, op)); r = make_node(level_a, read(1), hi(a)); npop = 1; } @@ -164,9 +172,10 @@ namespace dd { npop = 1; } else { - push(apply_rec(lo(b), a, op)); - r = make_node(level_b, read(1), hi(b)); - npop = 1; + SASSERT(op == pdd_sub_op); + push(apply_rec(a, lo(b), op)); + push(apply_rec(zero_pdd, hi(b), op)); + r = make_node(level_b, read(2), read(1)); } break; case pdd_mul_op: @@ -217,6 +226,7 @@ namespace dd { } pop(npop); e1->m_result = r; + // SASSERT(well_formed()); SASSERT(!m_free_nodes.contains(r)); return r; @@ -227,6 +237,7 @@ namespace dd { SASSERT(level(a) == level(b) && !is_val(a) && !is_val(b)); if (lm_divides(b, a)) { PDD q = lt_quotient(b, a); + std::cout << pdd(b, this) << " divides " << pdd(a, this) << " q: " << pdd(q, this) << "\n"; PDD r = apply(q, b, pdd_mul_op); return apply(a, r, pdd_sub_op); } @@ -254,16 +265,16 @@ namespace dd { // assume lm_divides(p, q) pdd_manager::PDD pdd_manager::lt_quotient(PDD p, PDD q) { SASSERT(lm_divides(p, q)); + SASSERT(is_val(p) || !is_val(q)); if (is_val(p)) { if (is_val(q)) { return imk_val(val(q)/val(p)); } } else if (level(p) == level(q)) { - p = hi(p); + return lt_quotient(hi(p), hi(q)); } - SASSERT(!is_val(q)); - return lt_quotient(p, hi(q)); + return apply(m_var2pdd[var(p)], lt_quotient(p, hi(q)), pdd_mul_op); } // @@ -277,9 +288,9 @@ 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); - for (unsigned i = p.size(); i-- > 0; ) r1 = mul(mk_var(p[i]), r1); - pdd r2 = mul(qc, b); - for (unsigned i = q.size(); i-- > 0; ) r2 = mul(mk_var(q[i]), r2); + for (unsigned i = q.size(); i-- > 0; ) r1 = mul(mk_var(q[i]), r1); + pdd r2 = mul(pc, b); + for (unsigned i = p.size(); i-- > 0; ) r2 = mul(mk_var(p[i]), r2); return sub(r1, r2); } @@ -290,8 +301,8 @@ namespace dd { while (true) { if (is_val(x) || is_val(y)) { if (!has_common) return false; - while (!is_val(y)) y = hi(y); - while (!is_val(x)) x = hi(x); + while (!is_val(y)) q.push_back(var(y)), y = hi(y); + while (!is_val(x)) p.push_back(var(x)), x = hi(x); pc = val(x); qc = val(y); return true; @@ -532,29 +543,50 @@ namespace dd { } } + pdd_manager::monomials_t pdd_manager::to_monomials(pdd const& p) { + + if (p.is_val()) { + std::pair m; + m.first = p.val(); + monomials_t mons; + if (!m.first.is_zero()) { + mons.push_back(m); + } + return mons; + } + else { + monomials_t mons = to_monomials(p.hi()); + for (auto & m : mons) { + m.second.push_back(p.var()); + } + mons.append(to_monomials(p.lo())); + return mons; + } + } + std::ostream& pdd_manager::display(std::ostream& out, pdd const& b) { - init_mark(); - m_todo.push_back(b.root); - while (!m_todo.empty()) { - PDD r = m_todo.back(); - if (is_marked(r)) { - m_todo.pop_back(); - } - else if (is_val(r)) { - set_mark(r); - out << r << " : " << val(r) << "\n"; - m_todo.pop_back(); - } - else if (!is_marked(lo(r))) { - m_todo.push_back(lo(r)); - } - else if (!is_marked(hi(r))) { - m_todo.push_back(hi(r)); + auto mons = to_monomials(b); + bool first = true; + for (auto& m : mons) { + if (!first) { + if (m.first.is_neg()) out << " - "; + else out << " + "; } else { - out << r << " : " << var(r) << " @ " << level(r) << " " << lo(r) << " " << hi(r) << "\n"; - set_mark(r); - m_todo.pop_back(); + if (m.first.is_neg()) out << "- "; + } + first = false; + rational c = abs(m.first); + m.second.reverse(); + if (!c.is_one()) { + out << c; + if (!m.second.empty()) out << "*"; + } + bool f = true; + for (unsigned v : m.second) { + if (!f) out << "*"; + f = false; + out << "v" << v; } } return out; @@ -577,6 +609,7 @@ namespace dd { unsigned lvl = n.m_level; PDD lo = n.m_lo; PDD hi = n.m_hi; + if (hi == 0) continue; // it is a value ok &= is_val(lo) || level(lo) <= lvl; ok &= is_val(hi) || level(hi) <= lvl; ok &= is_val(lo) || !m_nodes[lo].is_internal(); @@ -593,8 +626,15 @@ namespace dd { std::ostream& pdd_manager::display(std::ostream& out) { for (unsigned i = 0; i < m_nodes.size(); ++i) { pdd_node const& n = m_nodes[i]; - if (n.is_internal()) continue; - out << i << " : v" << m_level2var[n.m_level] << " " << n.m_lo << " " << n.m_hi << "\n"; + if (i != 0 && n.is_internal()) { + continue; + } + else if (is_val(i)) { + out << i << " : " << val(i) << "\n"; + } + else { + out << i << " : v" << m_level2var[n.m_level] << " " << n.m_lo << " " << n.m_hi << "\n"; + } } return out; } diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index 3dddb7401..c130a4349 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -36,6 +36,7 @@ namespace dd { friend pdd; typedef unsigned PDD; + typedef vector> monomials_t; const PDD null_pdd = UINT_MAX; const PDD zero_pdd = 0; @@ -192,6 +193,9 @@ namespace dd { pdd spoly(pdd const& a, pdd const& b, unsigned_vector const& p, unsigned_vector const& q, rational const& pc, rational const& qc); bool common_factors(pdd const& a, pdd const& b, unsigned_vector& p, unsigned_vector& q, rational& pc, rational& qc); + monomials_t to_monomials(pdd const& p); + + struct scoped_push { pdd_manager& m; unsigned m_size; @@ -211,6 +215,8 @@ namespace dd { pdd mk_var(unsigned i); pdd mk_val(rational const& r); + pdd zero(); + pdd one(); pdd minus(pdd const& a); pdd add(pdd const& a, pdd const& b); pdd add(rational const& a, pdd const& b); @@ -256,7 +262,12 @@ namespace dd { }; inline pdd operator*(rational const& r, pdd& b) { return b * r; } + inline pdd operator*(int x, pdd& b) { return b * rational(x); } + inline pdd operator*(pdd& b, int x) { return b * rational(x); } + inline pdd operator+(rational const& r, pdd& b) { return b + r; } + inline pdd operator+(int x, pdd& b) { return b + rational(x); } + inline pdd operator+(pdd& b, int x) { return b + rational(x); } std::ostream& operator<<(std::ostream& out, pdd const& b); diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp index 03acabcc4..e38ad2901 100644 --- a/src/test/pdd.cpp +++ b/src/test/pdd.cpp @@ -2,7 +2,7 @@ namespace dd { static void test1() { - pdd_manager m(20); + pdd_manager m(3); pdd v0 = m.mk_var(0); pdd v1 = m.mk_var(1); pdd v2 = m.mk_var(2); @@ -18,6 +18,35 @@ namespace dd { c2 = v2 + v1 + v0; std::cout << c1 << "\n"; SASSERT(c1 == c2); + + c1 = (v0+v1) * v2; + c2 = (v0*v2) + (v1*v2); + std::cout << c1 << "\n"; + SASSERT(c1 == c2); + c1 = (c1 + 3) + 1; + c2 = (c2 + 1) + 3; + std::cout << c1 << "\n"; + SASSERT(c1 == c2); + c1 = v0 - v1; + c2 = v1 - v0; + std::cout << c1 << " " << c2 << "\n"; + + c1 = v1*v2; + c2 = (v0*v2) + (v2*v2); + pdd c3 = m.zero(); + VERIFY(m.try_spoly(c1, c2, c3)); + std::cout << c1 << " " << c2 << " spoly: " << c3 << "\n"; + + c1 = v1*v2; + c2 = (v0*v2) + (v1*v1); + VERIFY(m.try_spoly(c1, c2, c3)); + std::cout << c1 << " " << c2 << " spoly: " << c3 << "\n"; + + c1 = (v0*v1) - (v0*v0); + c2 = (v0*v1*(v2 + v0)) + v2; + c3 = c2.reduce(c1); + std::cout << c1 << " " << c2 << " reduce: " << c3 << "\n"; + } }