From 78b022491d950df569695096732486756a0ff6d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Dec 2019 09:26:02 -0800 Subject: [PATCH] comments Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.cpp | 13 +- src/math/grobner/pdd_grobner.cpp | 196 +++++++++++++++++-------------- src/math/grobner/pdd_grobner.h | 37 +++--- 3 files changed, 138 insertions(+), 108 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index ef0ec4a77..4f59f21e4 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -107,7 +107,7 @@ namespace dd { case pdd_add_op: if (is_zero(a)) return b; if (is_zero(b)) return a; - if (is_val(a) && is_val(b)) return imk_val(m_mod2_semantics ? ((val(a) + val(b)) % rational(2)) : val(a) + val(b)); + if (is_val(a) && is_val(b)) return imk_val(val(a) + val(b)); if (level(a) < level(b)) std::swap(a, b); break; case pdd_mul_op: @@ -249,6 +249,7 @@ namespace dd { } pdd_manager::PDD pdd_manager::minus_rec(PDD a) { + SASSERT(!m_mod2_semantics); if (is_zero(a)) return zero_pdd; if (is_val(a)) return imk_val(-val(a)); op_entry* e1 = pop_entry(a, a, pdd_minus_op); @@ -299,7 +300,7 @@ namespace dd { if (is_val(p)) { if (is_val(q)) { SASSERT(!val(p).is_zero()); - return m_mod2_semantics ? imk_val(val(q)) : imk_val(-val(q)/val(p)); + return imk_val(-val(q)/val(p)); } } else if (level(p) == level(q)) { @@ -321,7 +322,7 @@ namespace dd { pdd r1 = mk_val(qc); for (unsigned i = q.size(); i-- > 0; ) r1 = mul(mk_var(q[i]), r1); r1 = mul(a, r1); - pdd r2 = mk_val(m_mod2_semantics ? pc : -pc); + pdd r2 = mk_val(-pc); for (unsigned i = p.size(); i-- > 0; ) r2 = mul(mk_var(p[i]), r2); r2 = mul(b, r2); return add(r1, r2); @@ -338,6 +339,11 @@ namespace dd { while (!is_val(x)) p.push_back(var(x)), x = hi(x); pc = val(x); qc = val(y); + if (!m_mod2_semantics && pc.is_int() && qc.is_int()) { + rational g = gcd(pc, qc); + pc /= g; + qc /= g; + } return true; } if (level(x) == level(y)) { @@ -443,6 +449,7 @@ namespace dd { pdd_manager::PDD pdd_manager::imk_val(rational const& r) { if (r.is_zero()) return zero_pdd; if (r.is_one()) return one_pdd; + if (m_mod2_semantics) return imk_val(mod(r, rational(2))); const_info info; if (!m_mpq_table.find(r, info)) { init_value(info, r); diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp index aee5e8535..07eac76c5 100644 --- a/src/math/grobner/pdd_grobner.cpp +++ b/src/math/grobner/pdd_grobner.cpp @@ -16,7 +16,7 @@ namespace dd { /*** - The main algorithm maintains two sets (S, A), + A simple algorithm maintains two sets (S, A), where S is m_processed, and A is m_to_simplify. Initially S is empty and A contains the initial equations. @@ -29,22 +29,71 @@ namespace dd { add b to A - add a to S - simplify A using a + + Alternate: + + - Fix a variable ordering x1 > x2 > x3 > .... + In each step: + - pick a in A with *highest* variable x_i in leading term of *lowest* degree. + - simplify a using S + - simplify S using a + - if a does not contains x_i, put it back into A and pick again (determine whether possible) + - for s in S: + b = superpose(a, s) + if superposition is invertible, then remove s + add b to A + - add a to S + - simplify A using a + + + Apply a watch list to filter out relevant elements of S + Index leading_term_watch: Var -> Equation* + Only need to simplify equations that contain eliminated variable. + The watch list can be used to index into equations that are useful to simplify. + A Bloom filter on leading term could further speed up test whether reduction applies. + + For p in A: + populate watch list by maxvar(p) |-> p + For p in S: + populate watch list by vars(p) |-> p + + - the variable ordering should be chosen from a candidate model M, + in a way that is compatible with weights that draw on the number of occurrences + in polynomials with violated evaluations and with the maximal slack (degree of freedom). + + weight(x) := < count { p in P | x in p, M(p) != 0 }, min_{p in P | x in p} slack(p,x) > + + slack is computed from interval assignments to variables, and is an interval in which x can possibly move + (an over-approximation). + + The alternative version maintains the following invariant: + - polynomials not in the watch list cannot be simplified using a + Justification: + - elements in S have all variables watched + - elements in A are always reduced modulo all variables above the current x_i. + + Invertible rules: + when p, q are linear in x, e.g., is of the form p = k*x + a, q = l*x + b + where k, l are constant and x is maximal, then + from l*a - k*b and k*x + a we have the equality lkx+al+kb-al, which is lx+b + So we can throw away q after superposition without losing solutions. + - this corresponds to triangulating a matrix during Gauss. + */ grobner::grobner(reslimit& lim, pdd_manager& m) : m(m), m_limit(lim), - m_conflict(false) + m_conflict(nullptr) {} - grobner::~grobner() { - del_equations(0); + reset(); } - void grobner::compute_basis() { + void grobner::saturate() { try { - while (!done() && compute_basis_step()) { + while (!done() && step()) { TRACE("grobner", display(tout);); DEBUG_CODE(invariant();); } @@ -54,7 +103,7 @@ namespace dd { } } - bool grobner::compute_basis_step() { + bool grobner::step() { m_stats.m_compute_steps++; equation* e = pick_next(); if (!e) return false; @@ -66,7 +115,8 @@ namespace dd { if (!simplify_using(m_processed, eq)) return false; TRACE("grobner", tout << "eq = "; display_equation(tout, eq);); superpose(eq); - toggle_processed(eq); + eq.set_processed(true); + m_processed.push_back(e); return simplify_using(m_to_simplify, eq); } @@ -77,7 +127,7 @@ namespace dd { eq = curr; } } - if (eq) m_to_simplify.erase(eq); + if (eq) pop_equation(eq->idx(), m_to_simplify); return eq; } @@ -90,7 +140,7 @@ namespace dd { /* Use a set of equations to simplify eq */ - bool grobner::simplify_using(equation& eq, equation_set const& eqs) { + 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";); do { @@ -115,31 +165,29 @@ namespace dd { /* Use the given equation to simplify equations in set */ - bool grobner::simplify_using(equation_set& set, equation const& eq) { + bool grobner::simplify_using(equation_vector& set, equation const& eq) { TRACE("grobner", tout << "poly " << eq.poly() << "\n";); - ptr_buffer to_delete; - ptr_buffer to_move; - bool changed_leading_term = false; - for (equation* target : set) { - if (canceled()) - return false; - if (simplify_source_target(eq, *target, changed_leading_term)) { - if (is_trivial(*target)) - to_delete.push_back(target); - else if (is_too_complex(*target)) - to_delete.push_back(target); - else if (check_conflict(*target)) - return false; - else if (changed_leading_term && target->is_processed()) { - to_move.push_back(target); - } - } + unsigned j = 0, sz = set.size(); + for (unsigned i = 0; i < sz; ++i) { + 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))) { + 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 { + set[j] = ⌖ + target.set_index(j); + ++j; + } } - for (equation* eq : to_delete) - del_equation(eq); - for (equation* eq : to_move) - toggle_processed(*eq); - return true; + set.shrink(j); + return !done(); } /* @@ -173,70 +221,51 @@ namespace dd { m_stats.m_superposed++; if (r.is_zero()) return; if (is_too_complex(r)) return; - equation* eq = alloc(equation, r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()), m_equations.size()); - m_equations.push_back(eq); - update_stats_max_degree_and_size(*eq); - check_conflict(*eq); - m_to_simplify.insert(eq); + add(r, m_dep_manager.mk_join(eq1.dep(), eq2.dep())); } - void grobner::toggle_processed(equation& eq) { - if (eq.is_processed()) { - m_to_simplify.insert(&eq); - m_processed.erase(&eq); - } - else { - m_processed.insert(&eq); - m_to_simplify.erase(&eq); - } - eq.set_processed(!eq.is_processed()); - } - - grobner::equation_set const& grobner::equations() { + grobner::equation_vector const& grobner::equations() { m_all_eqs.reset(); - for (equation* eq : m_equations) if (eq) m_all_eqs.insert(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() { - del_equations(0); - SASSERT(m_equations.empty()); + for (equation* e : m_to_simplify) dealloc(e); + for (equation* e : m_processed) dealloc(e); m_processed.reset(); m_to_simplify.reset(); m_stats.reset(); - m_conflict = false; + m_conflict = nullptr; } void grobner::add(pdd const& p, u_dependency * dep) { if (p.is_zero()) return; - if (p.is_val()) set_conflict(); - equation * eq = alloc(equation, p, dep, m_equations.size()); - m_equations.push_back(eq); - m_to_simplify.insert(eq); + equation * eq = alloc(equation, p, dep, m_to_simplify.size()); + m_to_simplify.push_back(eq); + check_conflict(*eq); + update_stats_max_degree_and_size(*eq); } - - void grobner::del_equations(unsigned old_size) { - for (unsigned i = m_equations.size(); i-- > old_size; ) { - del_equation(m_equations[i]); - } - m_equations.shrink(old_size); - } - - void grobner::del_equation(equation* eq) { - if (!eq) return; - unsigned idx = eq->idx(); - m_processed.erase(eq); - m_to_simplify.erase(eq); - dealloc(m_equations[idx]); - m_equations[idx] = nullptr; - } bool grobner::canceled() { return m_limit.get_cancel_flag(); } bool grobner::done() { - return m_to_simplify.size() + m_processed.size() >= m_config.m_eqs_threshold || canceled() || m_conflict; + return m_to_simplify.size() + m_processed.size() >= m_config.m_eqs_threshold || canceled() || m_conflict != nullptr; + } + + void grobner::del_equation(equation& eq) { + pop_equation(eq.idx(), eq.is_processed() ? m_processed : m_to_simplify); + retire(&eq); + } + + void grobner::pop_equation(unsigned idx, equation_vector& v) { + equation* eq2 = v.back(); + eq2->set_index(idx); + v[idx] = eq2; + v.pop_back(); } void grobner::update_stats_max_degree_and_size(const equation& e) { @@ -268,21 +297,18 @@ namespace dd { } void grobner::invariant() const { + unsigned i = 0; for (auto* e : m_processed) { SASSERT(e->is_processed()); + SASSERT(e->idx() == i); + ++i; } + i = 0; for (auto* e : m_to_simplify) { SASSERT(!e->is_processed()); - } - for (auto* e : m_equations) { - if (e) { - SASSERT(!e->is_processed() || m_processed.contains(e)); - SASSERT(e->is_processed() || m_to_simplify.contains(e)); - SASSERT(!is_trivial(*e)); - } + SASSERT(e->idx() == i); + ++i; } } - - } diff --git a/src/math/grobner/pdd_grobner.h b/src/math/grobner/pdd_grobner.h index f89f54e83..eb9a9d410 100644 --- a/src/math/grobner/pdd_grobner.h +++ b/src/math/grobner/pdd_grobner.h @@ -47,7 +47,7 @@ public: private: class equation { bool m_processed; //!< state - unsigned m_idx; //!< position at m_equations + unsigned m_idx; //!< unique index pdd m_poly; //!< polynomial in pdd form u_dependency * m_dep; //!< justification for the equality public: @@ -60,15 +60,14 @@ private: const pdd& poly() const { return m_poly; } u_dependency * dep() const { return m_dep; } - unsigned hash() const { return m_idx; } 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; } + void set_index(unsigned idx) { m_idx = idx; } }; - typedef obj_hashtable equation_set; typedef ptr_vector equation_vector; typedef std::function print_dep_t; @@ -77,12 +76,11 @@ private: stats m_stats; config m_config; print_dep_t m_print_dep; - equation_vector m_equations; - equation_set m_processed; - equation_set m_to_simplify; + equation_vector m_processed; + equation_vector m_to_simplify; mutable u_dependency_manager m_dep_manager; - equation_set m_all_eqs; - bool m_conflict; + equation_vector m_all_eqs; + equation const* m_conflict; public: grobner(reslimit& lim, pdd_manager& m); ~grobner(); @@ -93,9 +91,9 @@ public: void reset(); void add(pdd const&, u_dependency * dep); - void compute_basis(); + void saturate(); - equation_set const& equations(); + equation_vector const& equations(); u_dependency_manager& dep() const { return m_dep_manager; } void collect_statistics(statistics & st) const; @@ -103,28 +101,27 @@ public: std::ostream& display(std::ostream& out) const; private: - bool compute_basis_step(); + bool step(); equation* pick_next(); bool canceled(); bool done(); 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_set& set, equation const& eq); - bool simplify_using(equation& eq, equation_set const& eqs); - void toggle_processed(equation& eq); + bool simplify_using(equation_vector& set, equation const& eq); + bool simplify_using(equation& eq, equation_vector const& eqs); - bool eliminate(equation& eq) { return is_trivial(eq) && (del_equation(&eq), true); } + 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(), true); } - void set_conflict() { m_conflict = true; } + 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 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; } - - void del_equations(unsigned old_size); - void del_equation(equation* eq); + void del_equation(equation& eq); + void retire(equation* eq) { dealloc(eq); } + void pop_equation(unsigned idx, equation_vector& v); void invariant() const;