From 58be42d2a95be9a4864e771cae9280067f79ffdf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 22 Dec 2019 10:59:12 -0800 Subject: [PATCH] initial unit test for pdd_grobner Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.cpp | 2 +- src/math/grobner/pdd_grobner.cpp | 56 ++++++++++++++++---------------- src/math/grobner/pdd_grobner.h | 25 +++++++++++--- src/test/CMakeLists.txt | 1 + src/test/main.cpp | 1 + src/test/pdd_grobner.cpp | 53 ++++++++++++++++++++++++++++++ 6 files changed, 104 insertions(+), 34 deletions(-) create mode 100644 src/test/pdd_grobner.cpp diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index d9ff062ca..ac6709630 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -761,7 +761,7 @@ namespace dd { first = false; rational c = abs(m.first); m.second.reverse(); - if (!c.is_one()) { + if (!c.is_one() || m.second.empty()) { out << c; if (!m.second.empty()) out << "*"; } diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp index 9edc4aac9..90e2a9d13 100644 --- a/src/math/grobner/pdd_grobner.cpp +++ b/src/math/grobner/pdd_grobner.cpp @@ -112,16 +112,15 @@ namespace dd { bool grobner::basic_step() { equation* e = pick_next(); if (!e) return false; + scoped_detach sd(*this, e); equation& eq = *e; + TRACE("grobner", display(tout << "eq = ", eq); display(tout);); SASSERT(!eq.is_processed()); if (!simplify_using(eq, m_processed)) return false; - if (eliminate(eq)) return true; + if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; } if (check_conflict(eq)) return false; if (!simplify_using(m_processed, eq)) return false; - TRACE("grobner", tout << "eq = "; display_equation(tout, eq);); superpose(eq); - eq.set_processed(true); - m_processed.push_back(e); return simplify_using(m_to_simplify, eq); } @@ -156,7 +155,7 @@ namespace dd { */ bool grobner::simplify_using(equation& eq, equation_vector const& eqs) { bool simplified, changed_leading_term; - TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of size " << eqs.size() << "\n";); + TRACE("grobner", display(tout << "simplifying: ", eq); tout << "using equalities of size " << eqs.size() << "\n";); do { simplified = false; for (equation* p : eqs) { @@ -170,7 +169,7 @@ namespace dd { } while (simplified && !eq.poly().is_val()); - TRACE("grobner", tout << "simplification result: "; display_equation(tout, eq);); + TRACE("grobner", display(tout << "simplification result: ", eq);); check_conflict(eq); return !done(); @@ -209,12 +208,12 @@ namespace dd { 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 = target.poly(); - pdd r = source.poly().reduce(t); - if (r == source.poly() || is_too_complex(r)) { + pdd t = source.poly(); + pdd r = target.poly().reduce(t); + if (r == target.poly() || is_too_complex(r)) { return false; } - changed_leading_term = target.is_processed() && m.different_leading_term(r, source.poly()); + 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); @@ -230,7 +229,7 @@ namespace dd { let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0 */ bool grobner::superpose(equation const& eq1, equation const& eq2) { - TRACE("grobner_d", tout << "eq1="; display_equation(tout, eq1) << "eq2="; display_equation(tout, eq2);); + TRACE("grobner_d", tout << "eq1="; display(tout, eq1) << "eq2="; display(tout, eq2);); pdd r(m); if (!m.try_spoly(eq1.poly(), eq2.poly(), r)) return false; m_stats.m_superposed++; @@ -242,29 +241,28 @@ namespace dd { bool grobner::tuned_step() { equation* e = tuned_pick_next(); if (!e) return false; + scoped_detach sd(*this, e); equation& eq = *e; SASSERT(!m_watch[eq.poly().var()].contains(e)); SASSERT(!eq.is_processed()); if (!simplify_using(eq, m_processed)) return false; - if (eliminate(eq)) return true; + if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; } if (check_conflict(eq)) return false; if (!simplify_using(m_processed, eq)) return false; - TRACE("grobner", tout << "eq = "; display_equation(tout, eq);); + TRACE("grobner", tout << "eq = "; display(tout, eq);); superpose(eq); - eq.set_processed(true); - m_processed.push_back(e); return simplify_to_simplify(eq); } void grobner::tuned_init() { // TBD: extract free variables, order them, set pointer into variable list. NOT_IMPLEMENTED_YET(); - m_watch.reserve(m_vars.size()); + m_watch.reserve(m_level2var.size()); + m_levelp1 = m_level2var.size(); for (equation* eq : m_to_simplify) add_to_watch(*eq); SASSERT(m_processed.empty()); } - // watch top variable void grobner::add_to_watch(equation& eq) { SASSERT(!eq.is_processed()); pdd const& p = eq.poly(); @@ -274,12 +272,12 @@ namespace dd { } bool grobner::simplify_to_simplify(equation const& eq) { - unsigned v = m_vars[m_var]; + unsigned v = eq.poly().var(); auto& watch = m_watch[v]; unsigned j = 0; for (equation* _target : watch) { equation& target = *_target; - if (target.is_processed()) continue; + SASSERT(!target.is_processed()); bool changed_leading_term = false; bool simplified = !done() && simplify_source_target(eq, target, changed_leading_term); if (simplified && is_trivial(target)) { @@ -299,8 +297,8 @@ namespace dd { } grobner::equation* grobner::tuned_pick_next() { - while (m_var < m_vars.size()) { - unsigned v = m_vars[m_var]; + while (m_levelp1 > 0) { + unsigned v = m_level2var[m_levelp1-1]; equation_vector const& watch = m_watch[v]; equation* eq = nullptr; for (equation* curr : watch) { @@ -315,7 +313,7 @@ namespace dd { m_watch[eq->poly().var()].erase(eq); return eq; } - ++m_var; + --m_levelp1; } return nullptr; } @@ -340,7 +338,9 @@ namespace dd { if (p.is_zero()) return; equation * eq = alloc(equation, p, dep, m_to_simplify.size()); m_to_simplify.push_back(eq); - check_conflict(*eq); + if (!check_conflict(*eq) && is_tuned()) { + m_levelp1 = std::max(m_var2level[p.var()]+1, m_levelp1); + } update_stats_max_degree_and_size(*eq); } @@ -384,15 +384,15 @@ namespace dd { st.update("size", m_stats.m_max_expr_size); } - std::ostream& grobner::display_equation(std::ostream & out, const equation & eq) const { - out << "expr = " << eq.poly() << "\n"; - m_print_dep(eq.dep(), out); + std::ostream& grobner::display(std::ostream & out, const equation & eq) const { + out << eq.poly() << "\n"; + if (m_print_dep) m_print_dep(eq.dep(), out); return out; } std::ostream& grobner::display(std::ostream& out) const { - out << "processed\n"; for (auto e : m_processed) display_equation(out, *e); - out << "to_simplify\n"; for (auto e : m_to_simplify) display_equation(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; collect_statistics(st); st.display(out); diff --git a/src/math/grobner/pdd_grobner.h b/src/math/grobner/pdd_grobner.h index 5ece8560e..f0a78413f 100644 --- a/src/math/grobner/pdd_grobner.h +++ b/src/math/grobner/pdd_grobner.h @@ -37,6 +37,7 @@ public: unsigned m_superposed; unsigned m_compute_steps; void reset() { memset(this, 0, sizeof(*this)); } + stats() { reset(); } }; struct config { @@ -50,7 +51,6 @@ public: {} }; -private: class equation { bool m_processed; //!< state unsigned m_idx; //!< unique index @@ -73,6 +73,7 @@ private: void set_processed(bool p) { m_processed = p; } void set_index(unsigned idx) { m_idx = idx; } }; +private: typedef ptr_vector equation_vector; typedef std::function print_dep_t; @@ -95,7 +96,8 @@ public: void operator=(config const& c) { m_config = c; } void reset(); - void add(pdd const&, u_dependency * dep); + void add(pdd const& p) { add(p, nullptr); } + void add(pdd const& p, u_dependency * dep); void saturate(); @@ -103,7 +105,7 @@ public: u_dependency_manager& dep() const { return m_dep_manager; } void collect_statistics(statistics & st) const; - std::ostream& display_equation(std::ostream& out, const equation& eq) const; + std::ostream& display(std::ostream& out, const equation& eq) const; std::ostream& display(std::ostream& out) const; private: @@ -129,8 +131,9 @@ private: // tuned implementation vector m_watch; // watch list mapping variables to vector of equations where they occur (generally a subset) - unsigned m_var; // index into vars with current variable - unsigned_vector m_vars; // variables sorted by priority, higher priority first. + unsigned m_levelp1; // index into level+1 + unsigned_vector m_level2var; // level -> var + unsigned_vector m_var2level; // var -> level bool tuned_step(); void tuned_init(); @@ -146,6 +149,18 @@ private: void push_equation(equation& eq, equation_vector& v); void invariant() const; + struct scoped_detach { + grobner& g; + equation* e; + 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); + } + } + }; void update_stats_max_degree_and_size(const equation& e); bool is_tuned() const { return m_config.m_algorithm == config::tuned; } diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index b6d783dd3..6d1e3ea32 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -83,6 +83,7 @@ add_executable(test-z3 parray.cpp pb2bv.cpp pdd.cpp + pdd_grobner.cpp permutation.cpp polynomial.cpp polynorm.cpp diff --git a/src/test/main.cpp b/src/test/main.cpp index 177f4e742..fa5c351dd 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -254,6 +254,7 @@ int main(int argc, char ** argv) { TST_ARGV(cnf_backbones); TST(bdd); TST(pdd); + TST(pdd_grobner); TST(solver_pool); //TST_ARGV(hs); } diff --git a/src/test/pdd_grobner.cpp b/src/test/pdd_grobner.cpp new file mode 100644 index 000000000..f2dd444c1 --- /dev/null +++ b/src/test/pdd_grobner.cpp @@ -0,0 +1,53 @@ +#include "util/rlimit.h" +#include "math/grobner/pdd_grobner.h" + +namespace dd { + void print_eqs(ptr_vector const& eqs) { + std::cout << "eqs\n"; + for (grobner::equation* e : eqs) { + std::cout << e->poly() << "\n"; + } + } + void test1() { + pdd_manager m(4); + reslimit lim; + pdd v0 = m.mk_var(0); + pdd v1 = m.mk_var(1); + pdd v2 = m.mk_var(2); + pdd v3 = m.mk_var(3); + + grobner gb(lim, m); + gb.add(v1*v2 + v1*v3); + gb.add(v1 - 1); + print_eqs(gb.equations()); + gb.saturate(); + print_eqs(gb.equations()); + gb.reset(); + + gb.add(v1*v1*v2 + v2*v3); + gb.add(v1*v1*v2 + v2*v1); + gb.saturate(); + print_eqs(gb.equations()); + gb.reset(); + + gb.add(v1*v1*v2 + v2*v1); + gb.add(v1*v1*v2 + v2*v1); + gb.saturate(); + print_eqs(gb.equations()); + gb.reset(); + + gb.add(v1*v3*v3 + v3*v1 + 2); + gb.add(v1*v3*v3 + v3*v1); + gb.add(v3*v1 + v1*v2 + v2*v3); + gb.add(v3*v1 + v1*v2 + v2*v3 + v1); + gb.add(v3*v1 + v1*v2 + v2*v3 + v2); + gb.saturate(); + print_eqs(gb.equations()); + gb.reset(); + + } +} + +void tst_pdd_grobner() { + dd::test1(); +}