mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 17:08:45 +00:00
Code Activity

apply hardcoded thresholds

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-07 17:51:43 -08:00
parent 976f10c613
commit 2b7393778e
4 changed files with 50 additions and 875 deletions
Download patch file Download diff file Expand all files Collapse all files

865
src/math/grobner/pdd_grobner.cpp
View file

@ -1,865 +0,0 @@
/*++
Copyright (c) 2019 Microsoft Corporation
Abstract:
Grobner core based on pdd representation of polynomials
Author:
Nikolaj Bjorner (nbjorner)
Lev Nachmanson (levnach)
--*/
#include "math/grobner/pdd_grobner.h"
#include "util/uint_set.h"
namespace dd {
/***
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.
Each step proceeds as follows:
- pick a in A, and remove a from A
- simplify a using S
- simplify S using a
- for s in S:
b = superpose(a, s)
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)
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:
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).
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 no variables watched
- elements in A are always reduced modulo all variables above the current x_i.
TBD:
Linear Elimination:
- comprises of a simplification pass that puts linear equations in to_processed
- so before simplifying with respect to the variable ordering, eliminate linear equalities.
Extended Linear Simplification (as exploited in Bosphorus AAAI 2019):
- multiply each polynomial by one variable from their orbits.
- The orbit of a varible are the variables that occur in the same monomial as it in some polynomial.
- The extended set of polynomials is fed to a linear Gauss Jordan Eliminator that extracts
additional linear equalities.
- Bosphorus uses M4RI to perform efficient GJE to scale on large bit-matrices.
Long distance vanishing polynomials (used by PolyCleaner ICCAD 2019):
- identify polynomials p, q, such that p*q = 0
- main case is half-adders and full adders (p := x + y, q := x * y) over GF2
because (x+y)*x*y = 0 over GF2
To work beyond GF2 we would need to rely on simplification with respect to asserted equalities.
The method seems rather specific to hardware multipliers so not clear it is useful to
generalize.
- find monomials that contain pairs of vanishing polynomials, transitively
withtout actually inlining.
Then color polynomial variables w by p, resp, q if they occur in polynomial equalities
w - r = 0, such that all paths in r contain a node colored by p, resp q.
polynomial variables that get colored by both p and q can be set to 0.
When some variable gets colored, other variables can be colored.
- We can walk pdd nodes by level to perform coloring in a linear sweep.
PDD nodes that are equal to 0 using some equality are marked as definitions.
First walk definitions to search for vanishing polynomial pairs.
Given two definition polynomials d1, d2, it must be the case that
level(lo(d1)) = level(lo(d1)) for the polynomial lo(d1)*lo(d2) to be vanishing.
Then starting from the lowest level examine pdd nodes.
Let the current node be called p, check if the pdd node p is used in an equation
w - r = 0. In which case, w inherits the labels from r.
Otherwise, label the node by the intersection of vanishing polynomials from lo(p) and hi(p).
Eliminating multiplier variables, but not adders [Kaufmann et al FMCAD 2019 for GF2];
- Only apply GB saturation with respect to variables that are part of multipliers.
- Perhaps this amounts to figuring out whether a variable is used in an xor or more
*/
grobner::grobner(reslimit& lim, pdd_manager& m) :
m(m),
m_limit(lim),
m_conflict(nullptr)
{}
grobner::~grobner() {
reset();
}
void grobner::saturate() {
simplify();
tuned_init();
TRACE("grobner", display(tout););
try {
while (!done() && step()) {
TRACE("grobner", display(tout););
DEBUG_CODE(invariant(););
IF_VERBOSE(3, display_statistics(verbose_stream()));
}
DEBUG_CODE(invariant(););
}
catch (pdd_manager::mem_out) {
IF_VERBOSE(2, verbose_stream() << "mem-out\n");
DEBUG_CODE(invariant(););
// don't reduce further
}
}
bool grobner::step() {
m_stats.m_compute_steps++;
return tuned_step();
}
void grobner::scoped_process::done() {
pdd p = e->poly();
SASSERT(!p.is_val());
if (p.hi().is_val()) {
g.push_equation(solved, e);
}
else {
g.push_equation(processed, e);
}
e = nullptr;
}
grobner::scoped_process::~scoped_process() {
if (e) {
pdd p = e->poly();
SASSERT(!p.is_val());
g.push_equation(processed, e);
}
}
grobner::equation* grobner::pick_next() {
equation* eq = nullptr;
for (auto* curr : m_to_simplify) {
if (!eq || is_simpler(*curr, *eq)) {
eq = curr;
}
}
if (eq) pop_equation(eq);
return eq;
}
void grobner::simplify() {
try {
while (!done() &&
(simplify_linear_step(true) ||
simplify_elim_pure_step() ||
simplify_cc_step() ||
simplify_leaf_step() ||
simplify_linear_step(false) ||
/*simplify_elim_dual_step() ||*/
false)) {
DEBUG_CODE(invariant(););
TRACE("grobner", display(tout););
}
}
catch (pdd_manager::mem_out) {
// done reduce
IF_VERBOSE(2, verbose_stream() << "mem-out simplify\n");
DEBUG_CODE(invariant(););
}
}
struct grobner::compare_top_var {
bool operator()(equation* a, equation* b) const {
return a->poly().var() < b->poly().var();
}
};
bool grobner::simplify_linear_step(bool binary) {
TRACE("grobner", tout << "binary " << binary << "\n";);
IF_VERBOSE(2, verbose_stream() << "binary " << binary << "\n");
equation_vector linear;
for (equation* e : m_to_simplify) {
pdd p = e->poly();
if (binary) {
if (p.is_binary()) linear.push_back(e);
}
else if (p.is_linear()) {
linear.push_back(e);
}
}
return simplify_linear_step(linear);
}
/**
\brief simplify linear equations by using top variable as solution.
The linear equation is moved to set of solved equations.
*/
bool grobner::simplify_linear_step(equation_vector& linear) {
if (linear.empty()) return false;
use_list_t use_list = get_use_list();
compare_top_var ctv;
std::stable_sort(linear.begin(), linear.end(), ctv);
equation_vector trivial;
unsigned j = 0;
bool has_conflict = false;
for (equation* src : linear) {
if (has_conflict) {
break;
}
unsigned v = src->poly().var();
equation_vector const& uses = use_list[v];
TRACE("grobner",
display(tout << "uses of: ", *src) << "\n";
for (equation* e : uses) {
display(tout, *e) << "\n";
});
bool changed_leading_term;
bool all_reduced = true;
for (equation* dst : uses) {
if (src == dst || is_trivial(*dst)) {
continue;
}
pdd q = dst->poly();
if (!src->poly().is_binary() && !q.is_linear()) {
all_reduced = false;
continue;
}
remove_from_use(dst, use_list, v);
simplify_using(*dst, *src, changed_leading_term);
if (is_trivial(*dst)) {
trivial.push_back(dst);
}
else if (is_conflict(dst)) {
pop_equation(dst);
set_conflict(dst);
has_conflict = true;
}
else if (changed_leading_term) {
pop_equation(dst);
push_equation(to_simplify, dst);
}
// v has been eliminated.
SASSERT(!m.free_vars(dst->poly()).contains(v));
add_to_use(dst, use_list);
}
if (all_reduced) {
linear[j++] = src;
}
}
if (!has_conflict) {
linear.shrink(j);
for (equation* src : linear) {
pop_equation(src);
push_equation(solved, src);
}
}
for (equation* e : trivial) {
del_equation(e);
}
DEBUG_CODE(invariant(););
return j > 0 || has_conflict;
}
/**
\brief simplify using congruences
replace pair px + q and ry + q by
px + q, px - ry
since px = ry
*/
bool grobner::simplify_cc_step() {
TRACE("grobner", tout << "cc\n";);
IF_VERBOSE(2, verbose_stream() << "cc\n");
u_map<equation*> los;
bool reduced = false;
unsigned j = 0;
for (equation* eq1 : m_to_simplify) {
SASSERT(eq1->state() == to_simplify);
pdd p = eq1->poly();
auto* e = los.insert_if_not_there2(p.lo().index(), eq1);
equation* eq2 = e->get_data().m_value;
pdd q = eq2->poly();
if (eq2 != eq1 && (p.hi().is_val() || q.hi().is_val()) && !p.lo().is_val()) {
*eq1 = p - eq2->poly();
*eq1 = m_dep_manager.mk_join(eq1->dep(), eq2->dep());
reduced = true;
if (is_trivial(*eq1)) {
retire(eq1);
continue;
}
else if (check_conflict(*eq1)) {
continue;
}
}
m_to_simplify[j] = eq1;
eq1->set_index(j++);
}
m_to_simplify.shrink(j);
return reduced;
}
/**
\brief remove ax+b from p if x occurs as a leaf in p and a is a constant.
*/
bool grobner::simplify_leaf_step() {
TRACE("grobner", tout << "leaf\n";);
IF_VERBOSE(2, verbose_stream() << "leaf\n");
use_list_t use_list = get_use_list();
equation_vector leaves;
for (unsigned i = 0; i < m_to_simplify.size(); ++i) {
equation* e = m_to_simplify[i];
pdd p = e->poly();
if (!p.hi().is_val()) {
continue;
}
leaves.reset();
for (equation* e2 : use_list[p.var()]) {
if (e != e2 && e2->poly().var_is_leaf(p.var())) {
leaves.push_back(e2);
}
}
for (equation* e2 : leaves) {
bool changed_leading_term;
remove_from_use(e2, use_list);
simplify_using(*e2, *e, changed_leading_term);
add_to_use(e2, use_list);
if (is_trivial(*e2)) {
pop_equation(e2);
retire(e2);
}
else if (e2->poly().is_val()) {
pop_equation(e2);
set_conflict(*e2);
return true;
}
else if (changed_leading_term) {
pop_equation(e2);
push_equation(to_simplify, e2);
}
}
}
return false;
}
/**
\brief treat equations as processed if top variable occurs only once.
*/
bool grobner::simplify_elim_pure_step() {
TRACE("grobner", tout << "pure\n";);
IF_VERBOSE(2, verbose_stream() << "pure\n");
use_list_t use_list = get_use_list();
unsigned j = 0;
for (equation* e : m_to_simplify) {
pdd p = e->poly();
if (!p.is_val() && p.hi().is_val() && use_list[p.var()].size() == 1) {
push_equation(solved, e);
}
else {
m_to_simplify[j] = e;
e->set_index(j++);
}
}
if (j != m_to_simplify.size()) {
m_to_simplify.shrink(j);
return true;
}
return false;
}
/**
\brief
reduce equations where top variable occurs only twice and linear in one of the occurrences.
*/
bool grobner::simplify_elim_dual_step() {
use_list_t use_list = get_use_list();
unsigned j = 0;
bool reduced = false;
for (unsigned i = 0; i < m_to_simplify.size(); ++i) {
equation* e = m_to_simplify[i];
pdd p = e->poly();
// check that e is linear in top variable.
if (e->state() != to_simplify) {
reduced = true;
}
else if (!done() && !is_trivial(*e) && p.hi().is_val() && use_list[p.var()].size() == 2) {
for (equation* e2 : use_list[p.var()]) {
if (e2 == e) continue;
bool changed_leading_term;
remove_from_use(e2, use_list);
simplify_using(*e2, *e, changed_leading_term);
if (is_conflict(e2)) {
pop_equation(e2);
set_conflict(e2);
}
// when e2 is trivial, leading term is changed
SASSERT(!is_trivial(*e2) || changed_leading_term);
if (changed_leading_term) {
pop_equation(e2);
push_equation(to_simplify, e2);
}
add_to_use(e2, use_list);
break;
}
reduced = true;
push_equation(solved, e);
}
else {
m_to_simplify[j] = e;
e->set_index(j++);
}
}
if (reduced) {
// clean up elements in m_to_simplify
// they may have moved.
m_to_simplify.shrink(j);
j = 0;
for (equation* e : m_to_simplify) {
if (is_trivial(*e)) {
retire(e);
}
else if (e->state() == to_simplify) {
m_to_simplify[j] = e;
e->set_index(j++);
}
}
m_to_simplify.shrink(j);
return true;
}
else {
return false;
}
}
void grobner::add_to_use(equation* e, use_list_t& use_list) {
unsigned_vector const& fv = m.free_vars(e->poly());
for (unsigned v : fv) {
use_list.reserve(v + 1);
use_list[v].push_back(e);
}
}
void grobner::remove_from_use(equation* e, use_list_t& use_list) {
unsigned_vector const& fv = m.free_vars(e->poly());
for (unsigned v : fv) {
use_list.reserve(v + 1);
use_list[v].erase(e);
}
}
void grobner::remove_from_use(equation* e, use_list_t& use_list, unsigned except_v) {
unsigned_vector const& fv = m.free_vars(e->poly());
for (unsigned v : fv) {
if (v != except_v) {
use_list.reserve(v + 1);
use_list[v].erase(e);
}
}
}
grobner::use_list_t grobner::get_use_list() {
use_list_t use_list;
for (equation * e : m_to_simplify) {
add_to_use(e, use_list);
}
for (equation * e : m_processed) {
add_to_use(e, use_list);
}
return use_list;
}
void grobner::superpose(equation const & eq) {
for (equation* target : m_processed) {
superpose(eq, *target);
}
}
/*
Use a set of equations to simplify eq
*/
void grobner::simplify_using(equation& eq, equation_vector const& eqs) {
bool simplified, changed_leading_term;
do {
simplified = false;
for (equation* p : eqs) {
if (try_simplify_using(eq, *p, changed_leading_term)) {
simplified = true;
}
if (canceled() || eq.poly().is_val()) {
break;
}
}
}
while (simplified && !eq.poly().is_val());
TRACE("grobner", display(tout << "simplification result: ", eq););
}
/*
Use the given equation to simplify equations in set
*/
void grobner::simplify_using(equation_vector& set, equation const& eq) {
struct scoped_update {
equation_vector& set;
unsigned i, j, sz;
scoped_update(equation_vector& set): set(set), i(0), j(0), sz(set.size()) {}
void nextj() {
set[j] = set[i];
set[i]->set_index(j++);
}
~scoped_update() {
for (; i < sz; ++i) {
nextj();
}
set.shrink(j);
}
};
scoped_update sr(set);
for (; sr.i < sr.sz; ++sr.i) {
equation& target = *set[sr.i];
bool changed_leading_term = false;
bool simplified = true;
simplified = !done() && try_simplify_using(target, eq, changed_leading_term);
if (simplified && is_trivial(target)) {
retire(&target);
}
else if (simplified && check_conflict(target)) {
// pushed to solved
}
else if (simplified && changed_leading_term) {
SASSERT(target.state() == processed);
push_equation(to_simplify, target);
if (!m_var2level.empty()) {
m_levelp1 = std::max(m_var2level[target.poly().var()]+1, m_levelp1);
}
}
else {
sr.nextj();
}
}
}
/*
simplify target using source.
return true if the target was simplified.
set changed_leading_term if the target is in the m_processed set and the leading term changed.
*/
bool grobner::try_simplify_using(equation& dst, equation const& src, bool& changed_leading_term) {
if (&src == &dst) {
return false;
}
m_stats.m_simplified++;
pdd t = src.poly();
pdd r = dst.poly().reduce(t);
if (r == dst.poly()){
return false;
}
if (is_too_complex(r)) {
m_too_complex = true;
return false;
}
SASSERT(!t.hi().is_val() || !m.free_vars(r).contains(t.var()));
TRACE("grobner",
tout << "reduce: " << dst.poly() << "\n";
tout << "using: " << t << "\n";
tout << "to: " << r << "\n";);
changed_leading_term = dst.state() == processed && m.different_leading_term(r, dst.poly());
dst = r;
update_stats_max_degree_and_size(dst);
return true;
}
void grobner::simplify_using(equation & dst, equation const& src, bool& changed_leading_term) {
if (&src == &dst) return;
m_stats.m_simplified++;
pdd t = src.poly();
pdd r = dst.poly().reduce(t);
changed_leading_term = dst.state() == processed && m.different_leading_term(r, dst.poly());
TRACE("grobner",
tout << "reduce: " << dst.poly() << "\n";
tout << "using: " << t << "\n";
tout << "to: " << r << "\n";);
if (r == dst.poly()) return;
dst = r;
dst = m_dep_manager.mk_join(dst.dep(), src.dep());
update_stats_max_degree_and_size(dst);
}
/*
let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0
*/
void grobner::superpose(equation const& eq1, equation const& eq2) {
TRACE("grobner_d", display(tout << "eq1=", eq1); display(tout << "eq2=", eq2););
pdd r(m);
if (m.try_spoly(eq1.poly(), eq2.poly(), r) && !r.is_zero()) {
if (is_too_complex(r)) {
m_too_complex = true;
}
else {
m_stats.m_superposed++;
add(r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()));
}
}
}
bool grobner::tuned_step() {
equation* e = tuned_pick_next();
if (!e) return false;
scoped_process sd(*this, e);
equation& eq = *e;
SASSERT(eq.state() == to_simplify);
simplify_using(eq, m_processed);
if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; }
if (check_conflict(eq)) { sd.e = nullptr; return false; }
m_too_complex = false;
simplify_using(m_processed, eq);
if (done()) return false;
TRACE("grobner", display(tout << "eq = ", eq););
superpose(eq);
simplify_using(m_to_simplify, eq);
if (done()) return false;
if (!m_too_complex) sd.done();
return true;
}
void grobner::tuned_init() {
unsigned_vector const& l2v = m.get_level2var();
m_level2var.resize(l2v.size());
m_var2level.resize(l2v.size());
for (unsigned i = 0; i < l2v.size(); ++i) {
m_level2var[i] = l2v[i];
m_var2level[l2v[i]] = i;
}
m_levelp1 = m_level2var.size();
}
grobner::equation* grobner::tuned_pick_next() {
while (m_levelp1 > 0) {
unsigned v = m_level2var[m_levelp1-1];
equation* eq = nullptr;
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))
eq = curr;
}
}
if (eq) {
pop_equation(eq);
return eq;
}
--m_levelp1;
}
return nullptr;
}
grobner::equation_vector const& grobner::equations() {
m_all_eqs.reset();
for (equation* eq : m_solved) m_all_eqs.push_back(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() {
for (equation* e : m_solved) dealloc(e);
for (equation* e : m_to_simplify) dealloc(e);
for (equation* e : m_processed) dealloc(e);
m_solved.reset();
m_processed.reset();
m_to_simplify.reset();
m_stats.reset();
m_level2var.reset();
m_var2level.reset();
m_conflict = nullptr;
}
void grobner::add(pdd const& p, u_dependency * dep) {
if (p.is_zero()) return;
equation * eq = alloc(equation, p, dep);
if (check_conflict(*eq)) {
return;
}
push_equation(to_simplify, eq);
if (!m_var2level.empty()) {
m_levelp1 = std::max(m_var2level[p.var()]+1, m_levelp1);
}
update_stats_max_degree_and_size(*eq);
}
bool grobner::canceled() const {
return m_limit.get_cancel_flag();
}
bool grobner::done() const {
return
m_to_simplify.size() + m_processed.size() >= m_config.m_eqs_threshold ||
canceled() ||
m_stats.m_compute_steps > m_config.m_max_steps ||
m_conflict != nullptr;
}
grobner::equation_vector& grobner::get_queue(equation const& eq) {
switch (eq.state()) {
case processed: return m_processed;
case to_simplify: return m_to_simplify;
case solved: return m_solved;
}
UNREACHABLE();
return m_to_simplify;
}
void grobner::del_equation(equation* eq) {
pop_equation(eq);
retire(eq);
}
void grobner::pop_equation(equation& eq) {
equation_vector& v = get_queue(eq);
unsigned idx = eq.idx();
if (idx != v.size() - 1) {
equation* eq2 = v.back();
eq2->set_index(idx);
v[idx] = eq2;
}
v.pop_back();
}
void grobner::push_equation(eq_state st, equation& eq) {
SASSERT(st != to_simplify || !eq.poly().is_val());
SASSERT(st != processed || !eq.poly().is_val());
eq.set_state(st);
equation_vector& v = get_queue(eq);
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());
m_stats.m_max_expr_degree = std::max(m_stats.m_max_expr_degree, e.poly().degree());
}
void grobner::collect_statistics(statistics& st) const {
st.update("dd.solver.steps", m_stats.m_compute_steps);
st.update("dd.solver.simplified", m_stats.m_simplified);
st.update("dd.solver.superposed", m_stats.m_superposed);
st.update("dd.solver.processed", m_processed.size());
st.update("dd.solver.solved", m_solved.size());
st.update("dd.solver.to_simplify", m_to_simplify.size());
st.update("dd.solver.degree", m_stats.m_max_expr_degree);
st.update("dd.solver.size", m_stats.m_max_expr_size);
}
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 << "solved\n"; for (auto e : m_solved) display(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);
return display_statistics(out);
}
std::ostream& grobner::display_statistics(std::ostream& out) const {
statistics st;
collect_statistics(st);
st.display(out);
return out;
}
void grobner::invariant() const {
if (done()) return;
// equations in processed have correct indices
// they are labled as processed
unsigned i = 0;
for (auto* e : m_processed) {
VERIFY(e->state() == processed);
VERIFY(e->idx() == i);
VERIFY(!e->poly().is_val());
++i;
}
i = 0;
uint_set head_vars;
for (auto* e : m_solved) {
VERIFY(e->state() == solved);
VERIFY(e->idx() == i);
++i;
pdd p = e->poly();
if (!p.is_val() && p.hi().is_val()) {
unsigned v = p.var();
VERIFY(!head_vars.contains(v));
head_vars.insert(v);
}
}
if (!head_vars.empty()) {
for (auto * e : m_to_simplify) {
for (auto v : m.free_vars(e->poly())) {
if (head_vars.contains(v)) {
display(verbose_stream() << "free var in to_simplify: v" << v << "\n");
}
VERIFY(!head_vars.contains(v));
}
}
for (auto * e : m_processed) {
for (auto v : m.free_vars(e->poly())) VERIFY(!head_vars.contains(v));
}
}
// 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());
++i;
}
}
}

35
src/math/grobner/pdd_solver.cpp
View file

@ -14,6 +14,7 @@
#include "math/grobner/pdd_solver.h" #include "math/grobner/pdd_solver.h"
#include "math/grobner/pdd_simplifier.h" #include "math/grobner/pdd_simplifier.h"
#include "util/uint_set.h" #include "util/uint_set.h"
#include <math.h>
namespace dd { namespace dd {
@ -68,6 +69,29 @@ namespace dd {
reset(); reset();
} }
void solver::set_thresholds() {
IF_VERBOSE(3, verbose_stream() << "start saturate\n"; display_statistics(verbose_stream()));
if (m_to_simplify.size() == 0)
return;
m_config.m_eqs_threshold = 10 * ceil(log(m_to_simplify.size()))*m_to_simplify.size();
m_config.m_expr_size_limit = 0;
m_config.m_expr_degree_limit = 0;
for (equation* e: m_to_simplify) {
m_config.m_expr_size_limit = std::max(m_config.m_expr_size_limit, (unsigned)e->poly().tree_size());
m_config.m_expr_degree_limit = std::max(m_config.m_expr_degree_limit, e->poly().degree());
}
m_config.m_expr_size_limit *= 2;
m_config.m_expr_degree_limit *= 2;
IF_VERBOSE(3, verbose_stream() << "set m_config.m_eqs_threshold to 10 * " << 10 * ceil(log(m_to_simplify.size())) << "* " << m_to_simplify.size() << " = " << m_config.m_eqs_threshold << "\n";
verbose_stream() << "set m_config.m_expr_size_limit to " << m_config.m_expr_size_limit << "\n";
verbose_stream() << "set m_config.m_expr_degree_limit to " << m_config.m_expr_degree_limit << "\n";
);
m_config.m_max_steps = 700;
m_config.m_max_simplified = 7000;
}
void solver::saturate() { void solver::saturate() {
simplify(); simplify();
init_saturate(); init_saturate();
@ -194,7 +218,7 @@ namespace dd {
if (&src == &dst) { if (&src == &dst) {
return false; return false;
} }
m_stats.m_simplified++; m_stats.incr_simplified();
pdd t = src.poly(); pdd t = src.poly();
pdd r = dst.poly().reduce(t); pdd r = dst.poly().reduce(t);
if (r == dst.poly()){ if (r == dst.poly()){
@ -217,7 +241,7 @@ namespace dd {
void solver::simplify_using(equation & dst, equation const& src, bool& changed_leading_term) { void solver::simplify_using(equation & dst, equation const& src, bool& changed_leading_term) {
if (&src == &dst) return; if (&src == &dst) return;
m_stats.m_simplified++; m_stats.incr_simplified();
pdd t = src.poly(); pdd t = src.poly();
pdd r = dst.poly().reduce(t); pdd r = dst.poly().reduce(t);
changed_leading_term = dst.state() == processed && m.different_leading_term(r, dst.poly()); changed_leading_term = dst.state() == processed && m.different_leading_term(r, dst.poly());
@ -251,6 +275,7 @@ namespace dd {
bool solver::step() { bool solver::step() {
m_stats.m_compute_steps++; m_stats.m_compute_steps++;
IF_VERBOSE(3, if (m_stats.m_compute_steps % 100 == 0) verbose_stream() << "compute steps = " << m_stats.m_compute_steps << "\n";);
equation* e = pick_next(); equation* e = pick_next();
if (!e) return false; if (!e) return false;
scoped_process sd(*this, e); scoped_process sd(*this, e);
@ -342,7 +367,8 @@ namespace dd {
bool solver::done() { bool solver::done() {
return return
m_to_simplify.size() + m_processed.size() >= m_config.m_eqs_threshold || m_to_simplify.size() + m_processed.size() >= m_config.m_eqs_threshold ||
m_stats.simplified() >= m_config.m_max_simplified ||
canceled() || canceled() ||
m_stats.m_compute_steps > m_config.m_max_steps || m_stats.m_compute_steps > m_config.m_max_steps ||
m_conflict != nullptr; m_conflict != nullptr;
@ -390,7 +416,7 @@ namespace dd {
void solver::collect_statistics(statistics& st) const { void solver::collect_statistics(statistics& st) const {
st.update("dd.solver.steps", m_stats.m_compute_steps); st.update("dd.solver.steps", m_stats.m_compute_steps);
st.update("dd.solver.simplified", m_stats.m_simplified); st.update("dd.solver.simplified", m_stats.simplified());
st.update("dd.solver.superposed", m_stats.m_superposed); st.update("dd.solver.superposed", m_stats.m_superposed);
st.update("dd.solver.processed", m_processed.size()); st.update("dd.solver.processed", m_processed.size());
st.update("dd.solver.solved", m_solved.size()); st.update("dd.solver.solved", m_solved.size());
@ -416,6 +442,7 @@ namespace dd {
statistics st; statistics st;
collect_statistics(st); collect_statistics(st);
st.display(out); st.display(out);
out << "\n----\n";
return out; return out;
} }

23
src/math/grobner/pdd_solver.h
View file

@ -31,26 +31,36 @@ namespace dd {
class solver { class solver {
friend class simplifier; friend class simplifier;
public: public:
struct stats { class stats {
unsigned m_simplified; unsigned m_simplified;
public:
double m_max_expr_size; double m_max_expr_size;
unsigned m_max_expr_degree; unsigned m_max_expr_degree;
unsigned m_superposed; unsigned m_superposed;
unsigned m_compute_steps; unsigned m_compute_steps;
void reset() { memset(this, 0, sizeof(*this)); } void reset() { memset(this, 0, sizeof(*this)); }
stats() { reset(); } stats() { reset(); }
unsigned simplified() const { return m_simplified; }
void incr_simplified() {
m_simplified++;
}
}; };
struct config { struct config {
unsigned m_eqs_threshold; unsigned m_eqs_threshold;
unsigned m_expr_size_limit; unsigned m_expr_size_limit;
unsigned m_expr_degree_limit;
unsigned m_max_steps; unsigned m_max_steps;
unsigned m_max_simplified;
unsigned m_random_seed; unsigned m_random_seed;
bool m_enable_exlin; bool m_enable_exlin;
config() : config() :
m_eqs_threshold(UINT_MAX), m_eqs_threshold(UINT_MAX),
m_expr_size_limit(UINT_MAX), m_expr_size_limit(UINT_MAX),
m_expr_degree_limit(UINT_MAX),
m_max_steps(UINT_MAX), m_max_steps(UINT_MAX),
m_max_simplified(UINT_MAX),
m_random_seed(0), m_random_seed(0),
m_enable_exlin(false) m_enable_exlin(false)
{} {}
@ -73,7 +83,9 @@ public:
m_idx(0), m_idx(0),
m_poly(p), m_poly(p),
m_dep(d) m_dep(d)
{} {
}
const pdd& poly() const { return m_poly; } const pdd& poly() const { return m_poly; }
u_dependency * dep() const { return m_dep; } u_dependency * dep() const { return m_dep; }
@ -100,7 +112,7 @@ private:
mutable u_dependency_manager m_dep_manager; mutable u_dependency_manager m_dep_manager;
equation_vector m_all_eqs; equation_vector m_all_eqs;
equation* m_conflict; equation* m_conflict;
bool m_too_complex; bool m_too_complex;
public: public:
solver(reslimit& lim, pdd_manager& m); solver(reslimit& lim, pdd_manager& m);
~solver(); ~solver();
@ -126,6 +138,7 @@ public:
std::ostream& display_statistics(std::ostream& out) const; std::ostream& display_statistics(std::ostream& out) const;
const stats& get_stats() const { return m_stats; } const stats& get_stats() const { return m_stats; }
stats& get_stats() { return m_stats; } stats& get_stats() { return m_stats; }
void set_thresholds();
private: private:
bool step(); bool step();
@ -147,12 +160,12 @@ private:
void set_conflict(equation& eq) { m_conflict = &eq; push_equation(solved, eq); } void set_conflict(equation& eq) { m_conflict = &eq; push_equation(solved, eq); }
void set_conflict(equation* eq) { m_conflict = eq; push_equation(solved, eq); } void set_conflict(equation* eq) { m_conflict = eq; push_equation(solved, eq); }
bool is_too_complex(const equation& eq) const { return is_too_complex(eq.poly()); } 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; } bool is_too_complex(const pdd& p) const { return p.tree_size() > m_config.m_expr_size_limit
|| p.degree() > m_config.m_expr_degree_limit; }
unsigned m_levelp1; // index into level+1 unsigned m_levelp1; // index into level+1
unsigned_vector m_level2var; // level -> var unsigned_vector m_level2var; // level -> var
unsigned_vector m_var2level; // var -> level unsigned_vector m_var2level; // var -> level
void init_saturate(); void init_saturate();
void del_equation(equation& eq) { del_equation(&eq); } void del_equation(equation& eq) { del_equation(&eq); }

2
src/math/lp/nla_core.cpp
View file

@ -1436,7 +1436,7 @@ void core::run_pdd_grobner() {
m_pdd_grobner.set(cfg); m_pdd_grobner.set(cfg);
m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes. m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes.
m_pdd_grobner.set_thresholds();
m_pdd_grobner.saturate(); m_pdd_grobner.saturate();
bool conflict = false; bool conflict = false;
for (auto eq : m_pdd_grobner.equations()) { for (auto eq : m_pdd_grobner.equations()) {