From 65d818437ae394be4c70539410e6adaf1361540d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Dec 2019 19:31:18 -0800 Subject: [PATCH] add simplification routines Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.cpp | 21 +-- src/math/dd/dd_pdd.h | 3 + src/math/grobner/pdd_grobner.cpp | 297 +++++++++++++++++++++++++------ src/math/grobner/pdd_grobner.h | 50 ++++-- src/test/pdd_grobner.cpp | 22 ++- 5 files changed, 297 insertions(+), 96 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 01cca363c..aac440485 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -87,7 +87,7 @@ namespace dd { } } SASSERT(well_formed()); - return 0; + return null_pdd; } bool pdd_manager::check_result(op_entry*& e1, op_entry const* e2, PDD a, PDD b, PDD c) { @@ -112,21 +112,21 @@ namespace dd { if (is_zero(p)) return q; if (is_zero(q)) return p; if (is_val(p) && is_val(q)) return imk_val(val(p) + val(q)); - if (!is_val(p) && level(p) < level(q)) std::swap(p, q); if (is_val(p)) std::swap(p, q); + else if (!is_val(q) && level(p) < level(q)) std::swap(p, q); break; case pdd_mul_op: if (is_zero(p) || is_zero(q)) return zero_pdd; if (is_one(p)) return q; if (is_one(q)) return p; if (is_val(p) && is_val(q)) return imk_val(val(p) * val(q)); - if (!is_val(p) && level(p) < level(q)) std::swap(p, q); if (is_val(p)) std::swap(p, q); + else if (!is_val(q) && level(p) < level(q)) std::swap(p, q); break; case pdd_reduce_op: if (is_zero(q)) return p; if (is_val(p)) return p; - if (level(p) < level(q)) return p; + if (!is_val(q) && level(p) < level(q)) return p; break; default: UNREACHABLE(); @@ -156,14 +156,12 @@ namespace dd { push(apply_rec(hi(p), hi(q), op)); r = make_node(level_p, read(2), read(1)); } - else if (level_p > level_q) { + else { + SASSERT(level_p > level_q); push(apply_rec(lo(p), q, op)); r = make_node(level_p, read(1), hi(p)); npop = 1; } - else { - UNREACHABLE(); - } break; case pdd_mul_op: SASSERT(!is_val(p)); @@ -179,7 +177,7 @@ namespace dd { // == x((a+b)(c+d)+bd) + bd // push(apply_rec(lo(p), lo(q), pdd_mul_op)); - unsigned bd = read(3); + unsigned bd = read(1); push(apply_rec(hi(p), lo(p), pdd_add_op)); push(apply_rec(hi(q), lo(q), pdd_add_op)); push(apply_rec(read(1), read(2), pdd_mul_op)); @@ -239,9 +237,7 @@ namespace dd { UNREACHABLE(); } pop(npop); - e1->m_result = r; - - // SASSERT(well_formed()); + e1->m_result = r; SASSERT(!m_free_nodes.contains(r)); return r; } @@ -852,6 +848,7 @@ namespace dd { out << "v" << v; } } + if (first) out << "0"; return out; } diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index c9d41bfb4..0665cfd6f 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -281,6 +281,7 @@ namespace dd { ~pdd() { m.dec_ref(root); } 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); } bool is_val() const { return m.is_val(root); } @@ -317,6 +318,8 @@ namespace dd { inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); } inline pdd& operator*=(pdd & p, pdd const& q) { p = p * q; return p; } inline pdd& operator|=(pdd & p, pdd const& q) { p = p | q; return p; } + inline pdd& operator-=(pdd & p, pdd const& q) { p = p - q; return p; } + inline pdd& operator+=(pdd & p, pdd const& q) { p = p + q; return p; } std::ostream& operator<<(std::ostream& out, pdd const& b); diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp index 1c3d165ba..35e60a884 100644 --- a/src/math/grobner/pdd_grobner.cpp +++ b/src/math/grobner/pdd_grobner.cpp @@ -151,10 +151,10 @@ namespace dd { scoped_detach sd(*this, e); equation& eq = *e; TRACE("grobner", display(tout << "eq = ", eq); display(tout);); - SASSERT(!eq.is_processed()); + SASSERT(eq.state() == to_simplify); if (!simplify_using(eq, m_processed)) return false; if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; } - if (check_conflict(eq)) return false; + if (check_conflict(eq)) { sd.e = nullptr; return false; } if (!simplify_using(m_processed, eq)) return false; superpose(eq); return simplify_using(m_to_simplify, eq); @@ -167,7 +167,7 @@ namespace dd { eq = curr; } } - if (eq) pop_equation(eq, m_to_simplify); + if (eq) pop_equation(eq); return eq; } @@ -178,13 +178,13 @@ namespace dd { eq = curr; } } - if (eq) pop_equation(eq, m_to_simplify); + if (eq) pop_equation(eq); return eq; } - void grobner::simplify_linear() { + void grobner::simplify() { try { - while (simplify_linear_step()) { + while (simplify_linear_step() /*|| simplify_cc_step() */ || simplify_elim_step()) { DEBUG_CODE(invariant();); } } @@ -207,38 +207,149 @@ namespace dd { } } if (linear.empty()) return false; - vector use_list; - for (equation * e : m_to_simplify) { - add_to_use(e, use_list); - } - for (equation * e : m_processed) { - add_to_use(e, use_list); - } + use_list_t use_list = get_use_list(); compare_top_var ctv; std::stable_sort(linear.begin(), linear.end(), ctv); for (equation* src : linear) { equation_vector const& uses = use_list[src->poly().var()]; bool changed_leading_term; for (equation* dst : uses) { - if (src == dst || !simplify_source_target(*src, *dst, changed_leading_term)) { + if (src == dst) { continue; } - if (dst->is_processed() && changed_leading_term) { - dst->set_processed(false); - pop_equation(dst, m_processed); - push_equation(dst, m_to_simplify); + simplify_using(*dst, *src, changed_leading_term); + if (check_conflict(*dst)) { + return false; + } + if (is_trivial(*dst)) { + SASSERT(false); + } + if (changed_leading_term) { + pop_equation(dst); + push_equation(to_simplify, dst); } } } for (equation* src : linear) { - pop_equation(src, m_to_simplify); - push_equation(src, m_processed); - src->set_processed(true); + pop_equation(src); + push_equation(solved, src); } return true; } - void grobner::add_to_use(equation* e, vector& use_list) { + /** + \brief simplify using congruences + replace pair px + q and ry + q by + px + q, px - ry + since px = ry + */ + bool grobner::simplify_cc_step() { + u_map los; + bool reduced = false; + unsigned j = 0; + for (equation* eq1 : m_to_simplify) { + SASSERT(eq1->state() == to_simplify); + pdd p = eq1->poly(); + auto* e = los.insert_if_not_there2(p.lo().index(), eq1); + equation* eq2 = e->get_data().m_value; + if (eq2 != eq1 && !p.lo().is_val()) { + *eq1 = p - eq2->poly(); + *eq1 = m_dep_manager.mk_join(eq1->dep(), eq2->dep()); + reduced = true; + if (is_trivial(*eq1)) { + retire(eq1); + continue; + } + else if (check_conflict(*eq1)) { + continue; + } + } + m_to_simplify[j] = eq1; + eq1->set_index(j++); + } + m_to_simplify.shrink(j); + return reduced; + } + + /** + \brief treat equations as processed if top variable occurs only once. + reduce equations where top variable occurs only twice and linear in one of the occurrences. + */ + bool grobner::simplify_elim_step() { + use_list_t use_list = get_use_list(); + unsigned j = 0; + for (equation* e : m_to_simplify) { + pdd p = e->poly(); + if (!p.is_val() && p.hi().is_val() && use_list[p.var()].size() == 1) { + push_equation(solved, e); + } + else { + m_to_simplify[j] = e; + e->set_index(j++); + } + } + if (j != m_to_simplify.size()) { + m_to_simplify.shrink(j); + return true; + } + j = 0; + for (unsigned i = 0; i < m_to_simplify.size(); ++i) { + equation* e = m_to_simplify[i]; + pdd p = e->poly(); + // check that e is linear in top variable. + if (e->state() != to_simplify) { + // this was moved before this pass + } + else if (!done() && !is_trivial(*e) && p.hi().is_val() && use_list[p.var()].size() == 2) { + for (equation* e2 : use_list[p.var()]) { + if (e2 == e) continue; + bool changed_leading_term; + + remove_from_use(e2, use_list); + simplify_using(*e2, *e, changed_leading_term); + if (check_conflict(*e2)) { + break; + } + if (is_trivial(*e2)) { + break; + } + if (changed_leading_term) { + pop_equation(e2); + push_equation(to_simplify, e2); + } + add_to_use(e2, use_list); + break; + } + push_equation(solved, e); + } + else { + m_to_simplify[j] = e; + e->set_index(j++); + } + } + if (j != m_to_simplify.size()) { + // clean up elements in m_to_simplify + // they may have moved. + m_to_simplify.shrink(j); + j = 0; + for (equation* e : m_to_simplify) { + if (is_trivial(*e)) { + retire(e); + } + else if (e->state() == to_simplify) { + m_to_simplify[j] = e; + e->set_index(j++); + } + } + m_to_simplify.shrink(j); + return true; + } + else { + return false; + } + } + + void grobner::add_to_use(equation* e, use_list_t& use_list) { unsigned_vector const& fv = m.free_vars(e->poly()); for (unsigned v : fv) { use_list.reserve(v + 1); @@ -246,6 +357,25 @@ namespace dd { } } + void grobner::remove_from_use(equation* e, use_list_t& use_list) { + unsigned_vector const& fv = m.free_vars(e->poly()); + for (unsigned v : fv) { + use_list.reserve(v + 1); + use_list[v].erase(e); + } + } + + grobner::use_list_t grobner::get_use_list() { + use_list_t use_list; + for (equation * e : m_to_simplify) { + add_to_use(e, use_list); + } + for (equation * e : m_processed) { + add_to_use(e, use_list); + } + return use_list; + } + void grobner::superpose(equation const & eq) { for (equation* target : m_processed) { superpose(eq, *target); @@ -257,7 +387,6 @@ namespace dd { */ bool grobner::simplify_using(equation& eq, equation_vector const& eqs) { bool simplified, changed_leading_term; - TRACE("grobner", display(tout << "simplifying: ", eq); tout << "using equalities of size " << eqs.size() << "\n";); do { simplified = false; for (equation* p : eqs) { @@ -273,7 +402,6 @@ namespace dd { TRACE("grobner", display(tout << "simplification result: ", eq);); - check_conflict(eq); return !done(); } @@ -281,7 +409,6 @@ namespace dd { Use the given equation to simplify equations in set */ bool grobner::simplify_using(equation_vector& set, equation const& eq) { - TRACE("grobner", tout << "poly " << eq.poly() << "\n";); unsigned j = 0, sz = set.size(); for (unsigned i = 0; i < sz; ++i) { equation& target = *set[i]; @@ -290,13 +417,15 @@ namespace dd { if (simplified && is_trivial(target)) { retire(&target); } - else if (simplified && !check_conflict(target) && changed_leading_term) { - SASSERT(target.is_processed()); - target.set_processed(false); + else if (simplified && check_conflict(target)) { + // pushed to solved + } + else if (simplified && changed_leading_term) { + SASSERT(target.state() == processed); if (is_tuned()) { m_levelp1 = std::max(m_var2level[target.poly().var()]+1, m_levelp1); } - push_equation(target, m_to_simplify); + push_equation(to_simplify, target); } else { set[j] = set[i]; @@ -312,22 +441,44 @@ namespace dd { return true if the target was simplified. set changed_leading_term if the target is in the m_processed set and the leading term changed. */ - bool grobner::simplify_source_target(equation const& source, equation& target, bool& changed_leading_term) { - TRACE("grobner", tout << "simplifying: " << target.poly() << "\nusing: " << source.poly() << "\n";); - m_stats.m_simplified++; - pdd t = source.poly(); - pdd r = target.poly().reduce(t); - if (r == target.poly() || is_too_complex(r)) { + bool grobner::simplify_source_target(equation const& src, equation& dst, bool& changed_leading_term) { + if (&src == &dst) { return false; } - changed_leading_term = target.is_processed() && m.different_leading_term(r, target.poly()); - target = r; - target = m_dep_manager.mk_join(target.dep(), source.dep()); - update_stats_max_degree_and_size(target); - TRACE("grobner", tout << "simplified " << target.poly() << "\n";); + m_stats.m_simplified++; + pdd t = src.poly(); + pdd r = dst.poly().reduce(t); + if (r == dst.poly() || is_too_complex(r)) { + return false; + } + TRACE("grobner", + tout << "reduce: " << dst.poly() << "\n"; + tout << "using: " << t << "\n"; + tout << "to: " << r << "\n";); + changed_leading_term = dst.state() == processed && m.different_leading_term(r, dst.poly()); + dst = r; + dst = m_dep_manager.mk_join(dst.dep(), src.dep()); + update_stats_max_degree_and_size(dst); return true; } + void grobner::simplify_using(equation & dst, equation const& src, bool& changed_leading_term) { + if (&src == &dst) return; + m_stats.m_simplified++; + pdd t = src.poly(); + pdd r = dst.poly().reduce(t); + changed_leading_term = dst.state() == processed && m.different_leading_term(r, dst.poly()); + TRACE("grobner", + tout << "reduce: " << dst.poly() << "\n"; + tout << "using: " << t << "\n"; + tout << "to: " << r << "\n";); + + if (r == dst.poly()) return; + dst = r; + dst = m_dep_manager.mk_join(dst.dep(), src.dep()); + update_stats_max_degree_and_size(dst); + } + /* let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0 */ @@ -347,10 +498,10 @@ namespace dd { scoped_detach sd(*this, e); equation& eq = *e; SASSERT(!m_watch[eq.poly().var()].contains(e)); - SASSERT(!eq.is_processed()); + SASSERT(eq.state() == to_simplify); if (!simplify_using(eq, m_processed)) return false; if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; } - if (check_conflict(eq)) return false; + if (check_conflict(eq)) { sd.e = nullptr; return false; } if (!simplify_using(m_processed, eq)) return false; TRACE("grobner", display(tout << "eq = ", eq);); superpose(eq); @@ -372,7 +523,7 @@ namespace dd { } void grobner::add_to_watch(equation& eq) { - SASSERT(!eq.is_processed()); + SASSERT(eq.state() == to_simplify); SASSERT(is_tuned()); pdd const& p = eq.poly(); if (!p.is_val()) { @@ -386,7 +537,7 @@ namespace dd { unsigned j = 0; for (equation* _target : watch) { equation& target = *_target; - SASSERT(!target.is_processed()); + SASSERT(target.state() == to_simplify); SASSERT(target.poly().var() == v); bool changed_leading_term = false; if (!done()) simplify_source_target(eq, target, changed_leading_term); @@ -394,8 +545,9 @@ namespace dd { retire(&target); } else if (check_conflict(target)) { - // remove from watch - } else if (target.poly().var() != v) { + // pushed to solved + } + else if (target.poly().var() != v) { // move to other watch list m_watch[target.poly().var()].push_back(_target); } @@ -415,13 +567,13 @@ namespace dd { equation* eq = nullptr; for (equation* curr : watch) { pdd const& p = curr->poly(); - if (!curr->is_processed() && !p.is_val() && p.var() == v) { + if (curr->state() == to_simplify && !p.is_val() && p.var() == v) { if (!eq || is_simpler(*curr, *eq)) eq = curr; } } if (eq) { - pop_equation(eq, m_to_simplify); + pop_equation(eq); m_watch[eq->poly().var()].erase(eq); return eq; } @@ -432,14 +584,17 @@ namespace dd { grobner::equation_vector const& grobner::equations() { m_all_eqs.reset(); + for (equation* eq : m_solved) m_all_eqs.push_back(eq); for (equation* eq : m_to_simplify) m_all_eqs.push_back(eq); for (equation* eq : m_processed) m_all_eqs.push_back(eq); return m_all_eqs; } void grobner::reset() { + for (equation* e : m_solved) dealloc(e); for (equation* e : m_to_simplify) dealloc(e); for (equation* e : m_processed) dealloc(e); + m_solved.reset(); m_processed.reset(); m_to_simplify.reset(); m_stats.reset(); @@ -448,9 +603,13 @@ namespace dd { void grobner::add(pdd const& p, u_dependency * dep) { if (p.is_zero()) return; - equation * eq = alloc(equation, p, dep, m_to_simplify.size()); - m_to_simplify.push_back(eq); - if (!check_conflict(*eq) && is_tuned()) { + equation * eq = alloc(equation, p, dep); + if (check_conflict(*eq)) { + return; + } + push_equation(to_simplify, eq); + + if (is_tuned()) { m_levelp1 = std::max(m_var2level[p.var()]+1, m_levelp1); } update_stats_max_degree_and_size(*eq); @@ -467,12 +626,23 @@ namespace dd { m_conflict != nullptr; } + grobner::equation_vector& grobner::get_queue(equation const& eq) { + switch (eq.state()) { + case processed: return m_processed; + case to_simplify: return m_to_simplify; + case solved: return m_solved; + } + UNREACHABLE(); + return m_to_simplify; + } + void grobner::del_equation(equation& eq) { - pop_equation(eq, eq.is_processed() ? m_processed : m_to_simplify); + pop_equation(eq); retire(&eq); } - void grobner::pop_equation(equation& eq, equation_vector& v) { + void grobner::pop_equation(equation& eq) { + equation_vector& v = get_queue(eq); unsigned idx = eq.idx(); if (idx != v.size() - 1) { equation* eq2 = v.back(); @@ -482,7 +652,9 @@ namespace dd { v.pop_back(); } - void grobner::push_equation(equation& eq, equation_vector& v) { + void grobner::push_equation(eq_state st, equation& eq) { + eq.set_state(st); + equation_vector& v = get_queue(eq); eq.set_index(v.size()); v.push_back(&eq); } @@ -507,6 +679,7 @@ namespace dd { } std::ostream& grobner::display(std::ostream& out) const { + out << "solved\n"; for (auto e : m_solved) display(out, *e); out << "processed\n"; for (auto e : m_processed) display(out, *e); out << "to_simplify\n"; for (auto e : m_to_simplify) display(out, *e); statistics st; @@ -520,17 +693,27 @@ namespace dd { // they are labled as processed unsigned i = 0; for (auto* e : m_processed) { - VERIFY(e->is_processed()); + VERIFY(e->state() == processed); + VERIFY(e->idx() == i); + VERIFY(!e->poly().is_val()); + ++i; + } + + i = 0; + for (auto* e : m_solved) { + VERIFY(e->state() == solved); VERIFY(e->idx() == i); ++i; } + // equations in to_simplify have correct indices // they are labeled as non-processed // their top-most variable is watched i = 0; for (auto* e : m_to_simplify) { - VERIFY(!e->is_processed()); VERIFY(e->idx() == i); + VERIFY(e->state() == to_simplify); + VERIFY(!e->poly().is_val()); if (is_tuned()) { pdd const& p = e->poly(); VERIFY(p.is_val() || m_watch[p.var()].contains(e)); @@ -544,7 +727,7 @@ namespace dd { for (equation* e : w) { VERIFY(!e->poly().is_val()); VERIFY(e->poly().var() == i); - VERIFY(!e->is_processed()); + VERIFY(e->state() == to_simplify); VERIFY(m_to_simplify.contains(e)); } ++i; diff --git a/src/math/grobner/pdd_grobner.h b/src/math/grobner/pdd_grobner.h index 8fd0dc37f..8c8b10b39 100644 --- a/src/math/grobner/pdd_grobner.h +++ b/src/math/grobner/pdd_grobner.h @@ -51,15 +51,21 @@ public: {} }; + enum eq_state { + solved, + processed, + to_simplify + }; + class equation { - bool m_processed; //!< state + eq_state m_state; unsigned m_idx; //!< unique index pdd m_poly; //!< polynomial in pdd form u_dependency * m_dep; //!< justification for the equality public: - equation(pdd const& p, u_dependency* d, unsigned idx): - m_processed(false), - m_idx(idx), + equation(pdd const& p, u_dependency* d): + m_state(to_simplify), + m_idx(0), m_poly(p), m_dep(d) {} @@ -69,8 +75,8 @@ public: unsigned idx() const { return m_idx; } void operator=(pdd& p) { m_poly = p; } void operator=(u_dependency* d) { m_dep = d; } - bool is_processed() const { return m_processed; } - void set_processed(bool p) { m_processed = p; } + eq_state state() const { return m_state; } + void set_state(eq_state st) { m_state = st; } void set_index(unsigned idx) { m_idx = idx; } }; private: @@ -83,11 +89,12 @@ private: stats m_stats; config m_config; print_dep_t m_print_dep; + equation_vector m_solved; // equations with solved variables, triangular equation_vector m_processed; equation_vector m_to_simplify; mutable u_dependency_manager m_dep_manager; equation_vector m_all_eqs; - equation const* m_conflict; + equation* m_conflict; public: grobner(reslimit& lim, pdd_manager& m); ~grobner(); @@ -99,7 +106,7 @@ public: void add(pdd const& p) { add(p, nullptr); } void add(pdd const& p, u_dependency * dep); - void simplify_linear(); + void simplify(); void saturate(); equation_vector const& equations(); @@ -120,14 +127,15 @@ private: void superpose(equation const& eq1, equation const& eq2); void superpose(equation const& eq); bool simplify_source_target(equation const& source, equation& target, bool& changed_leading_term); - bool simplify_using(equation_vector& set, equation const& eq); bool simplify_using(equation& eq, equation_vector const& eqs); + bool simplify_using(equation_vector& set, equation const& eq); + void simplify_using(equation & dst, equation const& src, bool& changed_leading_term); bool eliminate(equation& eq) { return is_trivial(eq) && (del_equation(eq), true); } bool is_trivial(equation const& eq) const { return eq.poly().is_zero(); } bool is_simpler(equation const& eq1, equation const& eq2) { return eq1.poly() < eq2.poly(); } - bool check_conflict(equation const& eq) { return eq.poly().is_val() && !is_trivial(eq) && (set_conflict(eq), true); } - void set_conflict(equation const& eq) { m_conflict = &eq; } + bool check_conflict(equation& eq) { return eq.poly().is_val() && !is_trivial(eq) && (set_conflict(eq), true); } + void set_conflict(equation& eq) { m_conflict = &eq; push_equation(solved, eq); } bool is_too_complex(const equation& eq) const { return is_too_complex(eq.poly()); } bool is_too_complex(const pdd& p) const { return p.tree_size() > m_config.m_expr_size_limit; } @@ -144,16 +152,22 @@ private: void add_to_watch(equation& eq); void del_equation(equation& eq); + equation_vector& get_queue(equation const& eq); void retire(equation* eq) { dealloc(eq); } - void pop_equation(equation& eq, equation_vector& v); - void pop_equation(equation* eq, equation_vector& v) { pop_equation(*eq, v); } - void push_equation(equation& eq, equation_vector& v); - void push_equation(equation* eq, equation_vector& v) { push_equation(*eq, v); } + void pop_equation(equation& eq); + void pop_equation(equation* eq) { pop_equation(*eq); } + void push_equation(eq_state st, equation& eq); + void push_equation(eq_state st, equation* eq) { push_equation(st, *eq); } struct compare_top_var; bool simplify_linear_step(); - void add_to_use(equation* e, vector& use_list); + typedef vector use_list_t; + use_list_t get_use_list(); + void add_to_use(equation* e, use_list_t& use_list); + void remove_from_use(equation* e, use_list_t& use_list); + bool simplify_cc_step(); + bool simplify_elim_step(); void invariant() const; struct scoped_detach { @@ -162,9 +176,7 @@ private: scoped_detach(grobner& g, equation* e): g(g), e(e) {} ~scoped_detach() { if (e) { - e->set_processed(true); - e->set_index(g.m_processed.size()); - g.m_processed.push_back(e); + g.push_equation(processed, *e); } } }; diff --git a/src/test/pdd_grobner.cpp b/src/test/pdd_grobner.cpp index 783821efc..4073a55ab 100644 --- a/src/test/pdd_grobner.cpp +++ b/src/test/pdd_grobner.cpp @@ -3,6 +3,7 @@ #include "ast/bv_decl_plugin.h" #include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" #include "ast/reg_decl_plugins.h" #include "tactic/goal.h" #include "tactic/tactic.h" @@ -76,31 +77,33 @@ namespace dd { void add_def(unsigned_vector const& id2var, app* e, ast_manager& m, pdd_manager& p, grobner& g) { expr* a, *b; pdd v1 = p.mk_var(id2var[e->get_id()]); + pdd q(p); if (m.is_and(e)) { pdd r = p.one(); for (expr* arg : *e) r *= p.mk_var(id2var[arg->get_id()]); - g.add(v1 + r + 1); + q = v1 + r; } else if (m.is_or(e)) { pdd r = p.zero(); for (expr* arg : *e) r |= p.mk_var(id2var[arg->get_id()]); - g.add(v1 + r + 1); + q = v1 + r; } else if (m.is_not(e, a)) { pdd v2 = p.mk_var(id2var[a->get_id()]); - g.add(v1 + v2 + 1); + q = v1 + v2 + 1; } else if (m.is_eq(e, a, b)) { pdd v2 = p.mk_var(id2var[a->get_id()]); pdd v3 = p.mk_var(id2var[b->get_id()]); - g.add(v1 + v2 + v3 + 1); + q = v1 + v2 + v3 + 1; } else if (is_uninterp_const(e)) { - // pass + return; } else { UNREACHABLE(); } + g.add(q); } void collect_id2var(unsigned_vector& id2var, expr_ref_vector const& fmls) { @@ -133,7 +136,10 @@ namespace dd { for (expr* e : fmls) { g.add(p.mk_var(id2var[e->get_id()]) + 1); } - g.simplify_linear(); + g.display(std::cout); + g.simplify(); + g.display(std::cout); + g.saturate(); g.display(std::cout); } @@ -141,8 +147,8 @@ namespace dd { ast_manager m; reg_decl_plugins(m); bv_util bv(m); - expr_ref x(m.mk_const("x", bv.mk_sort(4)), m); - expr_ref y(m.mk_const("y", bv.mk_sort(4)), m); + expr_ref x(m.mk_const("x", bv.mk_sort(3)), m); + expr_ref y(m.mk_const("y", bv.mk_sort(3)), m); expr_ref xy(bv.mk_bv_mul(x, y), m); expr_ref yx(bv.mk_bv_mul(y, x), m); expr_ref eq(m.mk_not(m.mk_eq(xy,yx)), m);