mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

prepare for equality propagation from Grobner basis

Browse source 
Attempt to remedy performance regressions from the new solver core for NLA. It misses easy lemmas, presumably due to weaker bounds information.
This commit is contained in:
Nikolaj Bjorner 2022-06-14 09:50:53 -07:00
parent 8e2027107d
commit 3d00d1d56b
3 changed files with 2009 additions and 1978 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/math/dd/dd_pdd.h
View file

@ -341,6 +341,7 @@ namespace dd {
bool is_zero() const { return m.is_zero(root); } bool is_zero() const { return m.is_zero(root); }
bool is_linear() const { return m.is_linear(root); } bool is_linear() const { return m.is_linear(root); }
bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); } bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); }
bool is_offset() const { return !is_val() && lo().is_val() && hi().is_one(); }
bool is_binary() const { return m.is_binary(root); } bool is_binary() const { return m.is_binary(root); }
bool is_monomial() const { return m.is_monomial(root); } bool is_monomial() const { return m.is_monomial(root); }
bool is_non_zero() const { return m.is_non_zero(root); } bool is_non_zero() const { return m.is_non_zero(root); }

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

@ -160,6 +160,9 @@ namespace dd {
} }
while (simplified && !eq.poly().is_val()); while (simplified && !eq.poly().is_val());
if (eq.poly().is_unary() && eq.poly().hi().val() < 0)
eq = -eq.poly();
TRACE("dd.solver", display(tout << "simplification result: ", eq);); TRACE("dd.solver", display(tout << "simplification result: ", eq););
} }

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

@ -1654,13 +1654,40 @@ void core::run_grobner() {
} }
if (conflict) { if (conflict) {
IF_VERBOSE(2, verbose_stream() << "grobner conflict\n"); IF_VERBOSE(2, verbose_stream() << "grobner conflict\n");
return;
} }
else {
if (quota > 1) #if 0
quota--; bool propagated = false;
IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << quota << "\n"); for (auto eq : m_pdd_grobner.equations()) {
IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream())); auto const& p = eq->poly();
if (p.is_offset()) {
lpvar v = p.var();
if (m_lar_solver.column_has_lower_bound(v) &&
m_lar_solver.column_has_upper_bound(v))
continue;
rational fixed_val = -p.lo().val();
lp::explanation ex;
u_dependency_manager dm;
vector<unsigned, false> lv;
dm.linearize(eq->dep(), lv);
for (unsigned ci : lv)
ex.push_back(ci);
new_lemma lemma(*this, "pdd-eq");
lemma &= ex;
lemma |= ineq(v, llc::EQ, fixed_val);
propagated = true;
}
} }
if (propagated)
return;
#endif
if (quota > 1)
quota--;
IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << quota << "\n");
IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
} }
void core::configure_grobner() { void core::configure_grobner() {