mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
remove watch, hoist orbit to track used variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
1d0572354b
commit
c1032c3403
|
@ -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);
|
||||
|
|
|
@ -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<pdd> 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<uint_set> 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<pdd>& eqs) {
|
||||
unsigned nv = s.m.num_vars();
|
||||
vector<uint_set> 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<pdd> const& eqs, vector<uint_set>& 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<uint_set> const& orbits, vector<pdd>& 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<pdd> const& eqs, vector<pdd>& simp_eqs) {
|
||||
void simplifier::simplify_exlin(vector<uint_set> const& orbits, vector<pdd> const& eqs, vector<pdd>& simp_eqs) {
|
||||
|
||||
// create variables for each non-constant monomial.
|
||||
u_map<unsigned> 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;
|
||||
|
|
|
@ -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<pdd>& eqs);
|
||||
void simplify_exlin(vector<pdd> const& eqs, vector<pdd>& simp_eqs);
|
||||
void init_orbits(vector<pdd> const& eqs, vector<uint_set>& orbits);
|
||||
void exlin_augment(vector<uint_set> const& orbits, vector<pdd>& eqs);
|
||||
void simplify_exlin(vector<uint_set> const& orbits, vector<pdd> const& eqs, vector<pdd>& simp_eqs);
|
||||
|
||||
|
||||
};
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
}
|
||||
|
|
|
@ -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<equation_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);
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue