From 72b47ba519193d0b67e31ccc93a01fa31dce586c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 21 Dec 2019 17:57:01 -0800 Subject: [PATCH] use while loop for reduce Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.cpp | 43 ++++++++++++++++++++++++------------------ src/test/pdd.cpp | 21 ++++++++++++++++++++- 2 files changed, 45 insertions(+), 19 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 8c3269435..a5137e097 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -177,27 +177,36 @@ namespace dd { r = make_node(level_a, read(2), read(1)); } 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)); if (m_mod2_semantics) { - push(apply_rec(read(1), ac, pdd_add_op)); + // + // (xa+b)*(xc+d) mod2 == x(ac+bc+ad) + bd + // == x((a+b)(c+d)+bd) + bd + // + push(apply_rec(lo(a), lo(b), pdd_mul_op)); + unsigned bd = read(3); + push(apply_rec(hi(a), lo(a), pdd_add_op)); + push(apply_rec(hi(b), lo(b), pdd_add_op)); + push(apply_rec(read(1), read(2), pdd_mul_op)); + push(apply_rec(read(1), bd, pdd_add_op)); r = make_node(level_a, bd, read(1)); - npop = 6; } else { + // + // (xa+b)*(xc+d) = x(x*ac + (ad+bc)) + 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; } + npop = 5; } else { - // (xa+b)*c = x(ac) + bc + // (x*hi(a)+lo(a))*b = x*hi(a)*b + lo(a)*b SASSERT(level_a > level_b); push(apply_rec(lo(a), b, op)); push(apply_rec(hi(a), b, op)); @@ -267,14 +276,12 @@ namespace dd { // q = lt(a)/lt(b), return a - b*q pdd_manager::PDD pdd_manager::reduce_on_match(PDD a, PDD b) { SASSERT(level(a) == level(b) && !is_val(a) && !is_val(b)); - if (lm_divides(b, a)) { + while (lm_divides(b, a)) { PDD q = lt_quotient(b, a); PDD r = apply(q, b, pdd_mul_op); - return apply(a, r, pdd_add_op); - } - else { - return a; + a = apply(a, r, pdd_add_op); } + return a; } // true if leading monomial of p divides leading monomial of q @@ -306,7 +313,7 @@ namespace dd { else if (level(p) == level(q)) { return lt_quotient(hi(p), hi(q)); } - return apply(m_var2pdd[var(p)], lt_quotient(p, hi(q)), pdd_mul_op); + return apply(m_var2pdd[var(q)], lt_quotient(p, hi(q)), pdd_mul_op); } // diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp index e38ad2901..fb71b01af 100644 --- a/src/test/pdd.cpp +++ b/src/test/pdd.cpp @@ -46,10 +46,29 @@ namespace dd { c2 = (v0*v1*(v2 + v0)) + v2; c3 = c2.reduce(c1); std::cout << c1 << " " << c2 << " reduce: " << c3 << "\n"; - } + + static void test2() { + std::cout << "\ntest2\n"; + // a(b^2)cd + abc + bcd + bc + cd + 3 reduce by bc + pdd_manager m(4); + pdd a = m.mk_var(0); + pdd b = m.mk_var(1); + pdd c = m.mk_var(2); + pdd d = m.mk_var(3); + pdd e = (a * b * b * c * d) + (2*a*b*c) + (b*c*d) + (b*c) + (c*d) + 3; + std::cout << e << "\n"; + pdd f = b * c; + pdd r_ef = m.reduce(e, f); + m.display(std::cout); + std::cout << "result of reduce " << e << " by " << f << " is " << r_ef << "\n"; + pdd r_fe = m.reduce(f, e); + std::cout << "result of reduce " << f << " by " << e << " is " << r_fe << "\n" ; + } + } void tst_pdd() { dd::test1(); + dd::test2(); }