mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-12 00:53:25 +00:00
Code Activity

merge changes from no_deps_gb branch

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-02 10:53:17 -08:00
parent a67f0bbb46
commit 8ed22c77aa
3 changed files with 28 additions and 78 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -138,8 +138,8 @@ namespace dd {
DEBUG_CODE(invariant();); DEBUG_CODE(invariant(););
} }
catch (pdd_manager::mem_out) { catch (pdd_manager::mem_out) {
m_watch.reset();
IF_VERBOSE(2, verbose_stream() << "mem-out\n"); IF_VERBOSE(2, verbose_stream() << "mem-out\n");
DEBUG_CODE(invariant(););
// don't reduce further // don't reduce further
} }
} }
@ -197,6 +197,7 @@ namespace dd {
} }
catch (pdd_manager::mem_out) { catch (pdd_manager::mem_out) {
// done reduce // done reduce
IF_VERBOSE(2, verbose_stream() << "mem-out simplify\n");
DEBUG_CODE(invariant();); DEBUG_CODE(invariant(););
} }
} }
@ -564,9 +565,8 @@ namespace dd {
else if (simplified && changed_leading_term) { else if (simplified && changed_leading_term) {
SASSERT(target.state() == processed); SASSERT(target.state() == processed);
push_equation(to_simplify, target); 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); m_levelp1 = std::max(m_var2level[target.poly().var()]+1, m_levelp1);
add_to_watch(target);
} }
} }
else { else {
@ -594,13 +594,13 @@ namespace dd {
m_too_complex = true; m_too_complex = true;
return false; return false;
} }
SASSERT(!t.hi().is_val() || !m.free_vars(r).contains(t.var()));
TRACE("grobner", TRACE("grobner",
tout << "reduce: " << dst.poly() << "\n"; tout << "reduce: " << dst.poly() << "\n";
tout << "using: " << t << "\n"; tout << "using: " << t << "\n";
tout << "to: " << r << "\n";); tout << "to: " << r << "\n";);
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());
dst = r; dst = r;
dst = m_dep_manager.mk_join(dst.dep(), src.dep());
update_stats_max_degree_and_size(dst); update_stats_max_degree_and_size(dst);
return true; return true;
} }
@ -644,7 +644,6 @@ namespace dd {
if (!e) return false; if (!e) return false;
scoped_process sd(*this, e); scoped_process sd(*this, e);
equation& eq = *e; equation& eq = *e;
SASSERT(!m_watch[eq.poly().var()].contains(e));
SASSERT(eq.state() == to_simplify); SASSERT(eq.state() == to_simplify);
simplify_using(eq, m_processed); simplify_using(eq, m_processed);
if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; } if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; }
@ -654,7 +653,7 @@ namespace dd {
if (done()) return false; if (done()) return false;
TRACE("grobner", display(tout << "eq = ", eq);); TRACE("grobner", display(tout << "eq = ", eq););
superpose(eq); superpose(eq);
simplify_watch(eq); simplify_using(m_to_simplify, eq);
if (done()) return false; if (done()) return false;
if (!m_too_complex) sd.done(); if (!m_too_complex) sd.done();
return true; return true;
@ -668,58 +667,15 @@ namespace dd {
m_level2var[i] = l2v[i]; m_level2var[i] = l2v[i];
m_var2level[l2v[i]] = i; m_var2level[l2v[i]] = i;
} }
m_watch.reset();
m_watch.reserve(m_level2var.size());
m_levelp1 = m_level2var.size(); m_levelp1 = m_level2var.size();
for (equation* eq : m_to_simplify) add_to_watch(*eq);
} }
void grobner::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 grobner::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);
}
grobner::equation* grobner::tuned_pick_next() { grobner::equation* grobner::tuned_pick_next() {
while (m_levelp1 > 0) { while (m_levelp1 > 0) {
unsigned v = m_level2var[m_levelp1-1]; unsigned v = m_level2var[m_levelp1-1];
equation_vector const& watch = m_watch[v];
equation* eq = nullptr; equation* eq = nullptr;
for (equation* curr : watch) { for (equation* curr : m_to_simplify) {
pdd const& p = curr->poly(); pdd const& p = curr->poly();
if (curr->state() == to_simplify && p.var() == v) { if (curr->state() == to_simplify && p.var() == v) {
if (!eq || is_simpler(*curr, *eq)) if (!eq || is_simpler(*curr, *eq))
@ -728,7 +684,6 @@ namespace dd {
} }
if (eq) { if (eq) {
pop_equation(eq); pop_equation(eq);
m_watch[eq->poly().var()].erase(eq);
return eq; return eq;
} }
--m_levelp1; --m_levelp1;
@ -752,7 +707,6 @@ namespace dd {
m_processed.reset(); m_processed.reset();
m_to_simplify.reset(); m_to_simplify.reset();
m_stats.reset(); m_stats.reset();
m_watch.reset();
m_level2var.reset(); m_level2var.reset();
m_var2level.reset(); m_var2level.reset();
m_conflict = nullptr; m_conflict = nullptr;
@ -766,18 +720,17 @@ namespace dd {
} }
push_equation(to_simplify, eq); push_equation(to_simplify, eq);
if (!m_watch.empty()) { if (!m_var2level.empty()) {
m_levelp1 = std::max(m_var2level[p.var()]+1, m_levelp1); m_levelp1 = std::max(m_var2level[p.var()]+1, m_levelp1);
add_to_watch(*eq);
} }
update_stats_max_degree_and_size(*eq); update_stats_max_degree_and_size(*eq);
} }
bool grobner::canceled() { bool grobner::canceled() const {
return m_limit.get_cancel_flag(); return m_limit.get_cancel_flag();
} }
bool grobner::done() { bool grobner::done() const {
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 ||
canceled() || canceled() ||
@ -857,6 +810,7 @@ namespace dd {
} }
void grobner::invariant() const { void grobner::invariant() const {
if (done()) return;
// equations in processed have correct indices // equations in processed have correct indices
// they are labled as processed // they are labled as processed
unsigned i = 0; unsigned i = 0;
@ -876,14 +830,19 @@ namespace dd {
pdd p = e->poly(); pdd p = e->poly();
if (!p.is_val() && p.hi().is_val()) { if (!p.is_val() && p.hi().is_val()) {
unsigned v = p.var(); unsigned v = p.var();
SASSERT(!head_vars.contains(v)); VERIFY(!head_vars.contains(v));
head_vars.insert(v); head_vars.insert(v);
} }
} }
if (!head_vars.empty()) { if (!head_vars.empty()) {
for (auto * e : m_to_simplify) { for (auto * e : m_to_simplify) {
for (auto v : m.free_vars(e->poly())) VERIFY(!head_vars.contains(v)); 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 * e : m_processed) {
for (auto v : m.free_vars(e->poly())) VERIFY(!head_vars.contains(v)); for (auto v : m.free_vars(e->poly())) VERIFY(!head_vars.contains(v));
@ -899,21 +858,6 @@ namespace dd {
VERIFY(e->state() == to_simplify); VERIFY(e->state() == to_simplify);
pdd const& p = e->poly(); pdd const& p = e->poly();
VERIFY(!p.is_val()); VERIFY(!p.is_val());
CTRACE("grobner", !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; ++i;
} }
} }

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

@ -130,8 +130,8 @@ public:
private: private:
bool step(); bool step();
equation* pick_next(); equation* pick_next();
bool canceled(); bool canceled() const;
bool done(); bool done() const;
void superpose(equation const& eq1, equation const& eq2); void superpose(equation const& eq1, equation const& eq2);
void superpose(equation const& eq); void superpose(equation const& eq);
void simplify_using(equation& eq, equation_vector const& eqs); void simplify_using(equation& eq, equation_vector const& eqs);

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

@ -1399,9 +1399,15 @@ std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const
void core::run_pdd_grobner() { void core::run_pdd_grobner() {
lp_settings().stats().m_grobner_calls++; lp_settings().stats().m_grobner_calls++;
m_pdd_grobner.reset(); m_pdd_grobner.reset();
set_level2var_for_pdd_grobner(); try {
for (unsigned i : m_rows) { set_level2var_for_pdd_grobner();
add_row_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]); for (unsigned i : m_rows) {
add_row_to_pdd_grobner(m_lar_solver.A_r().m_rows[i]);
}
}
catch (...) {
IF_VERBOSE(2, verbose_stream() << "pdd throw\n");
return;
} }
#if 0 #if 0
IF_VERBOSE(2, m_pdd_grobner.display(verbose_stream())); IF_VERBOSE(2, m_pdd_grobner.display(verbose_stream()));