From c1032c34038116d05a6b134c3d6b62c8c98abef3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Jan 2020 00:39:50 -0800 Subject: [PATCH] remove watch, hoist orbit to track used variables Signed-off-by: Nikolaj Bjorner --- src/math/dd/dd_pdd.cpp | 7 ++- src/math/grobner/pdd_simplifier.cpp | 51 +++++++++------- src/math/grobner/pdd_simplifier.h | 6 +- src/math/grobner/pdd_solver.cpp | 95 ++--------------------------- src/math/grobner/pdd_solver.h | 3 - src/math/simplex/bit_matrix.cpp | 1 + 6 files changed, 46 insertions(+), 117 deletions(-) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index f3488f0b1..1a3717a3e 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -285,7 +285,12 @@ namespace dd { if (level_p > level_q) { push(apply_rec(lo(p), q, op)); push(apply_rec(hi(p), q, op)); - r = make_node(level_p, read(2), read(1)); + if (read(2) == lo(p) && read(1) == hi(p)) { + r = p; + } + else { + r = make_node(level_p, read(2), read(1)); + } } else { SASSERT(level_p == level_q); diff --git a/src/math/grobner/pdd_simplifier.cpp b/src/math/grobner/pdd_simplifier.cpp index 285e9c668..09dd9ae96 100644 --- a/src/math/grobner/pdd_simplifier.cpp +++ b/src/math/grobner/pdd_simplifier.cpp @@ -56,7 +56,6 @@ #include "math/grobner/pdd_simplifier.h" #include "math/simplex/bit_matrix.h" -#include "util/uint_set.h" namespace dd { @@ -395,34 +394,42 @@ namespace dd { vector eqs, simp_eqs; for (auto* e : s.m_to_simplify) if (!e->dep()) eqs.push_back(e->poly()); for (auto* e : s.m_processed) if (!e->dep()) eqs.push_back(e->poly()); - exlin_augment(eqs); - simplify_exlin(eqs, simp_eqs); + vector orbits(s.m.num_vars()); + init_orbits(eqs, orbits); + exlin_augment(orbits, eqs); + simplify_exlin(orbits, eqs, simp_eqs); for (pdd const& p : simp_eqs) { s.add(p); } return !simp_eqs.empty() && simplify_linear_step(false); } - /** - augment set of equations by multiplying with selected variables. - Uses orbits to prune which variables are multiplied. - TBD: could also prune added polynomials based on a maximal degree. - */ - void simplifier::exlin_augment(vector& eqs) { - unsigned nv = s.m.num_vars(); - vector orbits(nv); - random_gen rand(s.m_config.m_random_seed); - unsigned modest_num_eqs = std::min(eqs.size(), 500u); - unsigned max_xlin_eqs = modest_num_eqs*modest_num_eqs + eqs.size(); - for (pdd p : eqs) { + void simplifier::init_orbits(vector const& eqs, vector& orbits) { + for (pdd const& p : eqs) { auto const& fv = p.free_vars(); for (unsigned i = fv.size(); i-- > 0; ) { + orbits[fv[i]].insert(fv[i]); // if v is used, it is in its own orbit. for (unsigned j = i; j-- > 0; ) { orbits[fv[i]].insert(fv[j]); orbits[fv[j]].insert(fv[i]); } } } + } + + + /** + augment set of equations by multiplying with selected variables. + Uses orbits to prune which variables are multiplied. + TBD: could also prune added polynomials based on a maximal degree. + TBD: for large systems, extract cluster of polynomials based on sampling orbits + */ + + void simplifier::exlin_augment(vector const& orbits, vector& eqs) { + unsigned nv = s.m.num_vars(); + random_gen rand(s.m_config.m_random_seed); + unsigned modest_num_eqs = std::min(eqs.size(), 500u); + unsigned max_xlin_eqs = modest_num_eqs*modest_num_eqs + eqs.size(); TRACE("dd.solver", tout << "augment " << nv << "\n"; for (auto const& o : orbits) tout << o.num_elems() << "\n"; ); @@ -435,7 +442,7 @@ namespace dd { pdd pv = s.m.mk_var(v); for (pdd p : eqs) { for (unsigned w : p.free_vars()) { - if (orbitv.contains(w)) { + if (v != w && orbitv.contains(w)) { n_eqs.push_back(pv * p); break; } @@ -453,7 +460,7 @@ namespace dd { if (orbitv.empty()) continue; pdd pv = s.m.mk_var(v); for (unsigned w : orbitv) { - if (v > w) continue; + if (v >= w) continue; pdd pw = s.m.mk_var(w); for (pdd p : eqs) { if (n_eqs.size() > max_xlin_eqs) { @@ -474,7 +481,7 @@ namespace dd { TRACE("dd.solver", for (pdd const& p : eqs) tout << p << "\n";); } - void simplifier::simplify_exlin(vector const& eqs, vector& simp_eqs) { + void simplifier::simplify_exlin(vector const& orbits, vector const& eqs, vector& simp_eqs) { // create variables for each non-constant monomial. u_map mon2idx; @@ -497,9 +504,11 @@ namespace dd { // insert variables last. unsigned nv = s.m.num_vars(); for (unsigned v = 0; v < nv; ++v) { - pdd r = s.m.mk_var(v); - mon2idx.insert(r.index(), idx2mon.size()); - idx2mon.push_back(r); + if (!orbits[v].empty()) { // not all variables are used. + pdd r = s.m.mk_var(v); + mon2idx.insert(r.index(), idx2mon.size()); + idx2mon.push_back(r); + } } bit_matrix bm; diff --git a/src/math/grobner/pdd_simplifier.h b/src/math/grobner/pdd_simplifier.h index 08c4b4756..c3fdbe036 100644 --- a/src/math/grobner/pdd_simplifier.h +++ b/src/math/grobner/pdd_simplifier.h @@ -13,6 +13,7 @@ --*/ #pragma once +#include "util/uint_set.h" #include "math/grobner/pdd_solver.h" namespace dd { @@ -46,8 +47,9 @@ private: bool simplify_elim_dual_step(); bool simplify_leaf_step(); bool simplify_exlin(); - void exlin_augment(vector& eqs); - void simplify_exlin(vector const& eqs, vector& simp_eqs); + void init_orbits(vector const& eqs, vector& orbits); + void exlin_augment(vector const& orbits, vector& eqs); + void simplify_exlin(vector const& orbits, vector const& eqs, vector& simp_eqs); }; diff --git a/src/math/grobner/pdd_solver.cpp b/src/math/grobner/pdd_solver.cpp index b1bfa281e..cceced193 100644 --- a/src/math/grobner/pdd_solver.cpp +++ b/src/math/grobner/pdd_solver.cpp @@ -47,18 +47,6 @@ namespace dd { - 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: - do not occur in watch list - - 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). @@ -67,12 +55,6 @@ namespace dd { 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 no variables watched - - elements in A are always reduced modulo all variables above the current x_i. */ @@ -99,7 +81,6 @@ namespace dd { DEBUG_CODE(invariant();); } catch (pdd_manager::mem_out) { - m_watch.reset(); IF_VERBOSE(2, verbose_stream() << "mem-out\n"); // don't reduce further } @@ -161,8 +142,7 @@ namespace dd { /* Use the given equation to simplify equations in set */ - void solver::simplify_using(equation_vector& set, equation const& eq) { - + void solver::simplify_using(equation_vector& set, equation const& eq) { struct scoped_update { equation_vector& set; unsigned i, j, sz; @@ -195,9 +175,8 @@ namespace dd { else if (simplified && changed_leading_term) { SASSERT(target.state() == processed); push_equation(to_simplify, target); - if (!m_watch.empty()) { + if (!m_var2level.empty()) { m_levelp1 = std::max(m_var2level[target.poly().var()]+1, m_levelp1); - add_to_watch(target); } } else { @@ -276,7 +255,6 @@ namespace dd { if (!e) return false; scoped_process sd(*this, e); equation& eq = *e; - SASSERT(!m_watch[eq.poly().var()].contains(e)); SASSERT(eq.state() == to_simplify); simplify_using(eq, m_processed); if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; } @@ -286,7 +264,7 @@ namespace dd { if (done()) return false; TRACE("dd.solver", display(tout << "eq = ", eq);); superpose(eq); - simplify_watch(eq); + simplify_using(m_to_simplify, eq); if (done()) return false; if (!m_too_complex) sd.done(); return true; @@ -300,58 +278,14 @@ namespace dd { m_level2var[i] = l2v[i]; m_var2level[l2v[i]] = i; } - m_watch.reset(); - m_watch.reserve(m_level2var.size()); m_levelp1 = m_level2var.size(); - for (equation* eq : m_to_simplify) add_to_watch(*eq); - } - - void solver::add_to_watch(equation& eq) { - SASSERT(eq.state() == to_simplify); - pdd const& p = eq.poly(); - if (!p.is_val()) { - m_watch[p.var()].push_back(&eq); - } - } - - void solver::simplify_watch(equation const& eq) { - unsigned v = eq.poly().var(); - auto& watch = m_watch[v]; - unsigned j = 0; - for (equation* _target : watch) { - equation& target = *_target; - SASSERT(target.state() == to_simplify); - SASSERT(target.poly().var() == v); - bool changed_leading_term = false; - if (!done()) { - try_simplify_using(target, eq, changed_leading_term); - } - if (is_trivial(target)) { - pop_equation(target); - retire(&target); - } - else if (is_conflict(target)) { - pop_equation(target); - set_conflict(target); - } - else if (target.poly().var() != v) { - // move to other watch list - m_watch[target.poly().var()].push_back(_target); - } - else { - // keep watching same variable - watch[j++] = _target; - } - } - watch.shrink(j); } solver::equation* solver::pick_next() { 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) { + for (equation* curr : m_to_simplify) { pdd const& p = curr->poly(); if (curr->state() == to_simplify && p.var() == v) { if (!eq || is_simpler(*curr, *eq)) @@ -360,7 +294,6 @@ namespace dd { } if (eq) { pop_equation(eq); - m_watch[eq->poly().var()].erase(eq); return eq; } --m_levelp1; @@ -384,7 +317,6 @@ namespace dd { m_processed.reset(); m_to_simplify.reset(); m_stats.reset(); - m_watch.reset(); m_level2var.reset(); m_var2level.reset(); m_conflict = nullptr; @@ -398,9 +330,8 @@ namespace dd { } push_equation(to_simplify, eq); - if (!m_watch.empty()) { + if (!m_var2level.empty()) { m_levelp1 = std::max(m_var2level[p.var()]+1, m_levelp1); - add_to_watch(*eq); } update_stats_max_degree_and_size(*eq); } @@ -524,28 +455,12 @@ namespace dd { // 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->idx() == i); VERIFY(e->state() == to_simplify); pdd const& p = e->poly(); VERIFY(!p.is_val()); - CTRACE("dd.solver", !m_watch.empty() && !m_watch[p.var()].contains(e), - display(tout << "not watched: ", *e) << "\n";); - VERIFY(m_watch.empty() || m_watch[p.var()].contains(e)); - ++i; - } - // the watch list consists of equations in to_simplify - // they watch the top most variable in poly - i = 0; - for (auto const& w : m_watch) { - for (equation* e : w) { - VERIFY(!e->poly().is_val()); - VERIFY(e->poly().var() == i); - VERIFY(e->state() == to_simplify); - VERIFY(m_to_simplify.contains(e)); - } ++i; } } diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h index 8ff6486ed..b0f2a6a30 100644 --- a/src/math/grobner/pdd_solver.h +++ b/src/math/grobner/pdd_solver.h @@ -147,14 +147,11 @@ 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; } - vector m_watch; // watch list mapping variables to vector of equations where they occur (generally a subset) unsigned m_levelp1; // index into level+1 unsigned_vector m_level2var; // level -> var unsigned_vector m_var2level; // var -> level void init_saturate(); - void simplify_watch(equation const& eq); - void add_to_watch(equation& eq); void del_equation(equation& eq) { del_equation(&eq); } void del_equation(equation* eq); diff --git a/src/math/simplex/bit_matrix.cpp b/src/math/simplex/bit_matrix.cpp index 42d3d1a84..b45f5eb8e 100644 --- a/src/math/simplex/bit_matrix.cpp +++ b/src/math/simplex/bit_matrix.cpp @@ -49,6 +49,7 @@ std::ostream& bit_matrix::row::display(std::ostream& out) const { void bit_matrix::reset(unsigned num_columns) { m_region.reset(); + m_rows.reset(); m_num_columns = num_columns; m_num_chunks = (num_columns + 63)/64; }