From 6ad55cc8f6826bb1c297c848121228334175dbde Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Dec 2019 15:26:55 -0800 Subject: [PATCH] add tuned implementation Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.cpp | 39 +++++++ src/math/dd/dd_pdd.h | 12 ++- src/math/grobner/pdd_grobner.cpp | 169 +++++++++++++++++++++++++++---- src/math/grobner/pdd_grobner.h | 33 +++++- 4 files changed, 230 insertions(+), 23 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 4f59f21e4..7d9b3efa2 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -362,6 +362,13 @@ namespace dd { } } + // a = s*x + t, where s is a constant, b = u*x + v, where u is a constant. + // since x is the maximal variable, it does not occur in t or v. + // thus, both a and b are linear in x + bool pdd_manager::spoly_is_invertible(pdd const& a, pdd const& b) { + return a.is_var() && b.is_var() && a.hi().is_val() && b.hi().is_val() && a.var() == b.var(); + } + /* * Compare leading monomials. * The pdd format makes lexicographic comparison easy: compare based on @@ -609,6 +616,38 @@ namespace dd { return m_tree_size[p.root]; } + unsigned_vector const& pdd_manager::free_vars(pdd const& p) { + return free_vars_except(p, zero()); + } + + unsigned_vector const& pdd_manager::free_vars_except(pdd const& p, pdd const& q) { + init_mark(); + m_free_vars.reset(); + m_todo.push_back(q.root); + while (!m_todo.empty()) { + PDD r = m_todo.back(); + m_todo.pop_back(); + if (is_val(r) || is_marked(r)) continue; + set_mark(r); + set_mark(m_var2pdd[var(r)]); + if (!is_marked(lo(r))) m_todo.push_back(lo(r)); + if (!is_marked(hi(r))) m_todo.push_back(hi(r)); + } + m_todo.push_back(p.root); + while (!m_todo.empty()) { + PDD r = m_todo.back(); + m_todo.pop_back(); + if (is_val(r) || is_marked(r)) continue; + PDD v = m_var2pdd[var(r)]; + if (!is_marked(v)) m_free_vars.push_back(var(r)); + set_mark(r); + set_mark(v); + if (!is_marked(lo(r))) m_todo.push_back(lo(r)); + if (!is_marked(hi(r))) m_todo.push_back(hi(r)); + } + return m_free_vars; + } + void pdd_manager::alloc_free_nodes(unsigned n) { for (unsigned i = 0; i < n; ++i) { diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index 19bf4db8a..5de035c11 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -148,6 +148,7 @@ namespace dd { bool m_is_new_node; unsigned m_max_num_pdd_nodes; bool m_mod2_semantics; + unsigned_vector m_free_vars; PDD make_node(unsigned level, PDD l, PDD r); PDD insert_node(pdd_node const& n); @@ -221,7 +222,7 @@ namespace dd { void set_mod2_semantics() { m_mod2_semantics = true; } void set_max_num_nodes(unsigned n) { m_max_num_pdd_nodes = n; } - void set_var_order(unsigned_vector const& levels); // TBD: set variable order (m_var2level, m_level2var) before doing anything else. + void set_var_order(unsigned_vector const& levels); // TBD: set variable order (m_var2level, m_level2var) before doing anything else. pdd mk_var(unsigned i); pdd mk_val(rational const& r); @@ -234,11 +235,19 @@ namespace dd { pdd mul(pdd const& a, pdd const& b); pdd mul(rational const& c, pdd const& b); pdd reduce(pdd const& a, pdd const& b); + + // create an spoly r if leading monomials of a and b overlap bool try_spoly(pdd const& a, pdd const& b, pdd& r); + + // true if b can be computed using a and the result of spoly + bool spoly_is_invertible(pdd const& a, pdd const& b); bool lt(pdd const& a, pdd const& b); bool different_leading_term(pdd const& a, pdd const& b); double tree_size(pdd const& p); + unsigned_vector const& free_vars(pdd const& p); + unsigned_vector const& free_vars_except(pdd const& p, pdd const& q); + std::ostream& display(std::ostream& out); std::ostream& display(std::ostream& out, pdd const& b); @@ -260,6 +269,7 @@ namespace dd { pdd hi() const { return pdd(m->hi(root), m); } unsigned var() const { return m->var(root); } rational const& val() const { SASSERT(is_val()); return m->val(root); } + bool is_var() const { return !m->is_val(root); } bool is_val() const { return m->is_val(root); } bool is_zero() const { return m->is_zero(root); } diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp index 07eac76c5..970fa14e8 100644 --- a/src/math/grobner/pdd_grobner.cpp +++ b/src/math/grobner/pdd_grobner.cpp @@ -92,6 +92,7 @@ namespace dd { } void grobner::saturate() { + if (is_tuned()) tuned_init(); try { while (!done() && step()) { TRACE("grobner", display(tout);); @@ -105,6 +106,15 @@ namespace dd { bool grobner::step() { m_stats.m_compute_steps++; + if (is_tuned()) { + return tuned_step(); + } + else { + return basic_step(); + } + } + + bool grobner::basic_step() { equation* e = pick_next(); if (!e) return false; equation& eq = *e; @@ -132,9 +142,18 @@ namespace dd { } void grobner::superpose(equation const & eq) { - for (equation * target : m_processed) { - superpose(eq, *target); + unsigned j = 0; + for (equation* target : m_processed) { + if (superpose(eq, *target)) { + // remove from watch lists + retire(target); + } + else { + target->set_index(j); + m_processed[j++] = target; + } } + m_processed.shrink(j); } /* @@ -172,18 +191,15 @@ namespace dd { equation& target = *set[i]; bool changed_leading_term = false; bool simplified = !done() && simplify_source_target(eq, target, changed_leading_term); - if (simplified && (is_trivial(target) || is_too_complex(target))) { + if (simplified && is_trivial(target)) { retire(&target); } - else if (simplified && !check_conflict(target) && changed_leading_term && target.is_processed()) { - target.set_index(m_to_simplify.size()); - target.set_processed(false); - m_to_simplify.push_back(&target); + else if (simplified && !check_conflict(target) && changed_leading_term) { + push_equation(target, m_to_simplify); } else { - set[j] = ⌖ - target.set_index(j); - ++j; + set[j] = set[i]; + target.set_index(j++); } } set.shrink(j); @@ -198,14 +214,32 @@ 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 r = source.poly().reduce(target.poly()); - if (r == source.poly()) { + pdd t = target.poly(); + pdd r = source.poly().reduce(t); + if (r == source.poly() || is_too_complex(r)) { return false; } changed_leading_term = target.is_processed() && m.different_leading_term(r, source.poly()); target = r; target = m_dep_manager.mk_join(target.dep(), source.dep()); update_stats_max_degree_and_size(target); + if (changed_leading_term) { + target.set_processed(false); + } + if (is_tuned()) { + if (r == t) { + // noop + } + else if (changed_leading_term) { + add_to_watch(target); + } + else if (target.is_processed()) { + add_diff_to_watch(target, t); + } + else { + add_to_watch(target); + } + } TRACE("grobner", tout << "simplified " << target.poly() << "\n";); return true; @@ -214,14 +248,104 @@ namespace dd { /* let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0 */ - void grobner::superpose(equation const& eq1, equation const& eq2) { + bool grobner::superpose(equation const& eq1, equation const& eq2) { TRACE("grobner_d", tout << "eq1="; display_equation(tout, eq1) << "eq2="; display_equation(tout, eq2);); pdd r(m); - if (!m.try_spoly(eq1.poly(), eq2.poly(), r)) return; + if (!m.try_spoly(eq1.poly(), eq2.poly(), r)) return false; m_stats.m_superposed++; - if (r.is_zero()) return; - if (is_too_complex(r)) return; + if (r.is_zero() || is_too_complex(r)) return false; add(r, m_dep_manager.mk_join(eq1.dep(), eq2.dep())); + return is_tuned() && m.spoly_is_invertible(eq1.poly(), eq2.poly()); + } + + bool grobner::tuned_step() { + equation* e = tuned_pick_next(); + if (!e) return false; + equation& eq = *e; + SASSERT(!eq.is_processed()); + if (!simplify_watch(eq, true)) return false; + if (eliminate(eq)) 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); + add_diff_to_watch(eq, m.zero()); + return simplify_watch(eq, false); + } + + void grobner::tuned_init() { + // TBD: extract free variables, order them, set pointer into variable list. + NOT_IMPLEMENTED_YET(); + m_watch.reserve(m_vars.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(); + if (is_tuned() && !p.is_val()) { + m_watch[p.var()].push_back(&eq); + } + } + + // add all variables in q but not p into watch. + void grobner::add_diff_to_watch(equation& eq, pdd const& p) { + SASSERT(eq.is_processed()); + pdd const& q = eq.poly(); + if (is_tuned() && !q.is_val()) { + for (unsigned v : m.free_vars_except(q, p)) { + m_watch[v].push_back(&eq); + } + } + } + + bool grobner::simplify_watch(equation const& eq, bool is_processed) { + unsigned v = m_vars[m_var]; + auto& watch = m_watch[v]; + unsigned j = 0; + for (equation* _target : watch) { + equation& target = *_target; + bool changed_leading_term = false; + bool simplified = !done() && simplify_source_target(eq, target, changed_leading_term); + if (simplified && is_trivial(target)) { + retire(&target); + } + else if (simplified && !check_conflict(target) && changed_leading_term) { + SASSERT(!target.is_processed()); + pop_equation(target.idx(), m_processed); + push_equation(target, m_to_simplify); + } + else { + watch[++j] = _target; + } + } + watch.shrink(j); + return false; + } + + grobner::equation* grobner::tuned_pick_next() { + while (m_var < m_vars.size()) { + unsigned v = m_vars[m_var]; + equation_vector const& watch = m_watch[v]; + equation* eq = nullptr; + for (equation* curr : watch) { + pdd const& p = curr->poly(); + if (!curr->is_processed() && !p.is_val() && p.var() == v) { + if (!eq || is_simpler(*curr, *eq)) + eq = curr; + } + } + if (eq) { + pop_equation(eq->idx(), m_to_simplify); + return eq; + } + ++m_var; + } + return nullptr; } grobner::equation_vector const& grobner::equations() { @@ -262,11 +386,18 @@ namespace dd { } void grobner::pop_equation(unsigned idx, equation_vector& v) { - equation* eq2 = v.back(); - eq2->set_index(idx); - v[idx] = eq2; + if (idx != v.size() - 1) { + equation* eq2 = v.back(); + eq2->set_index(idx); + v[idx] = eq2; + } v.pop_back(); } + + void grobner::push_equation(equation& eq, equation_vector& v) { + eq.set_index(v.size()); + v.push_back(&eq); + } void grobner::update_stats_max_degree_and_size(const equation& e) { m_stats.m_max_expr_size = std::max(m_stats.m_max_expr_size, e.poly().tree_size()); diff --git a/src/math/grobner/pdd_grobner.h b/src/math/grobner/pdd_grobner.h index eb9a9d410..f2690c38f 100644 --- a/src/math/grobner/pdd_grobner.h +++ b/src/math/grobner/pdd_grobner.h @@ -42,6 +42,12 @@ public: struct config { unsigned m_eqs_threshold; unsigned m_expr_size_limit; + enum { basic, tuned } m_algorithm; + config() : + m_eqs_threshold(UINT_MAX), + m_expr_size_limit(UINT_MAX), + m_algorithm(basic) + {} }; private: @@ -80,7 +86,7 @@ private: equation_vector m_to_simplify; mutable u_dependency_manager m_dep_manager; equation_vector m_all_eqs; - equation const* m_conflict; + equation const* m_conflict; public: grobner(reslimit& lim, pdd_manager& m); ~grobner(); @@ -102,10 +108,11 @@ public: private: bool step(); + bool basic_step(); equation* pick_next(); bool canceled(); bool done(); - void superpose(equation const& eq1, equation const& eq2); + bool 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); @@ -119,13 +126,33 @@ private: 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; } + + // 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. + + bool tuned_step(); + void tuned_init(); + equation* tuned_pick_next(); + bool simplify_watch(equation const& eq, bool is_processed); + void add_to_watch(equation& eq); + void add_diff_to_watch(equation& eq, pdd const& p); + void del_equation(equation& eq); - void retire(equation* eq) { dealloc(eq); } + void retire(equation* eq) { + if (is_tuned()) + for (auto v : m.free_vars(eq->poly())) m_watch[v].erase(eq); + dealloc(eq); + } void pop_equation(unsigned idx, equation_vector& v); + void push_equation(equation& eq, equation_vector& v); void invariant() const; void update_stats_max_degree_and_size(const equation& e); + bool is_tuned() const { return m_config.m_algorithm == config::tuned; } + bool is_basic() const { return m_config.m_algorithm == config::basic; } }; }