From bdac86501d6e27b8032925d6f9be02c5501bff0e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Oct 2023 20:33:48 -0700 Subject: [PATCH] add facility to check for missing propagations --- src/math/lp/nla_grobner.cpp | 42 +++++++++++++++++++---- src/math/lp/nla_grobner.h | 3 ++ src/math/lp/nra_solver.cpp | 66 +++++++++++++++++++++++++++++++++++-- src/math/lp/nra_solver.h | 7 +++- src/smt/theory_lra.cpp | 2 +- 5 files changed, 109 insertions(+), 11 deletions(-) diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index f2fe8d9b2..c6d29ac05 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -61,6 +61,9 @@ namespace nla { } + // DEBUG_CODE(for (auto e : m_solver.equations()) check_missing_propagation(*e);); + + if (m_quota > 0) --m_quota; @@ -125,11 +128,11 @@ namespace nla { typedef lp::lar_term term; bool grobner::propagate_fixed(const dd::solver::equation& eq) { dd::pdd const& p = eq.poly(); - //IF_VERBOSE(0, verbose_stream() << p << "\n"); if (p.is_unary()) { unsigned v = p.var(); if (c().var_is_fixed(v)) return false; + ineq new_eq(v, llc::EQ, rational::zero()); if (c().ineq_holds(new_eq)) return false; @@ -147,12 +150,19 @@ namespace nla { rational d = lcm(denominator(a), denominator(b)); a *= d; b *= d; +#if 0 + c().lra.update_column_type_and_bound(v, lp::lconstraint_kind::EQ, b/a, eq.dep()); + lp::explanation exp; + explain(eq, exp); + c().add_fixed_equality(c().lra.column_to_reported_index(v), b/a, exp); +#else ineq new_eq(term(a, v), llc::EQ, b); if (c().ineq_holds(new_eq)) return false; new_lemma lemma(c(), "pdd-eq"); add_dependencies(lemma, eq); lemma |= new_eq; +#endif return true; } @@ -193,15 +203,19 @@ namespace nla { return true; } - - void grobner::add_dependencies(new_lemma& lemma, const dd::solver::equation& eq) { - lp::explanation ex; + void grobner::explain(const dd::solver::equation& eq, lp::explanation& exp) { u_dependency_manager dm; vector lv; dm.linearize(eq.dep(), lv); for (unsigned ci : lv) - ex.push_back(ci); - lemma &= ex; + exp.push_back(ci); + } + + + void grobner::add_dependencies(new_lemma& lemma, const dd::solver::equation& eq) { + lp::explanation exp; + explain(eq, exp); + lemma &= exp; } void grobner::configure() { @@ -280,6 +294,10 @@ namespace nla { } bool grobner::is_conflicting(const dd::solver::equation& e) { + for (auto j : e.poly().free_vars()) + if (lra.column_is_free(j)) + return false; + auto& di = c().m_intervals.get_dep_intervals(); dd::pdd_interval eval(di); eval.var2interval() = [this](lpvar j, bool deps, scoped_dep_interval& a) { @@ -549,4 +567,16 @@ namespace nla { tout << "\n"); } + void grobner::check_missing_propagation(const dd::solver::equation& e) { + vector eqs; + eqs.push_back(e.poly()); + lbool r = c().m_nra.check(eqs); + CTRACE("grobner", r == l_false, m_solver.display(tout << "missed conflict ", e);); + if (r != l_true) + return; + r = c().m_nra.check_tight(e.poly()); + CTRACE("grobner", r == l_false, m_solver.display(tout << "tight equality ", e);); + } + + } diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h index c7d41413c..1c04c82e0 100644 --- a/src/math/lp/nla_grobner.h +++ b/src/math/lp/nla_grobner.h @@ -41,6 +41,9 @@ namespace nla { bool propagate_factorization(const dd::solver::equation& eq); void add_dependencies(new_lemma& lemma, const dd::solver::equation& eq); + void explain(const dd::solver::equation& eq, lp::explanation& exp); + + void check_missing_propagation(const dd::solver::equation& eq); // setup void configure(); diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index dc4681559..182845d58 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -206,14 +206,62 @@ struct solver::imp { } } + if (r == l_true) + return r; + IF_VERBOSE(0, verbose_stream() << "check-nra " << r << "\n"; m_nlsat->display(verbose_stream()); for (auto const& [v, w] : m_lp2nl) { auto& ls = m_nla_core.lra; if (ls.column_has_lower_bound(v)) - verbose_stream() << w << " >= " << ls.get_lower_bound(v) << "\n"; + verbose_stream() << "x" << w << " >= " << ls.get_lower_bound(v) << "\n"; if (ls.column_has_upper_bound(v)) - verbose_stream() << w << " <= " << ls.get_upper_bound(v) << "\n"; + verbose_stream() << "x" << w << " <= " << ls.get_upper_bound(v) << "\n"; + }); + + + return r; + } + + lbool check_tight(dd::pdd const& eq) { + m_zero = nullptr; + m_nlsat = alloc(nlsat::solver, m_limit, m_params, false); + m_zero = alloc(scoped_anum, am()); + m_lp2nl.reset(); + m_term_set.reset(); + add_eq(eq); + for (auto const& [v, w] : m_lp2nl) { + auto& ls = m_nla_core.lra; + if (ls.column_has_lower_bound(v)) + add_strict_lb(ls.get_lower_bound(v), w); + if (ls.column_has_upper_bound(v)) + add_strict_ub(ls.get_upper_bound(v), w); + } + + lbool r = l_undef; + try { + r = m_nlsat->check(); + } + catch (z3_exception&) { + if (m_limit.is_canceled()) { + r = l_undef; + } + else { + throw; + } + } + + if (r == l_true) + return r; + + IF_VERBOSE(0, verbose_stream() << "check-nra tight " << r << "\n"; + m_nlsat->display(verbose_stream()); + for (auto const& [v, w] : m_lp2nl) { + auto& ls = m_nla_core.lra; + if (ls.column_has_lower_bound(v)) + verbose_stream() << "x" << w << " >= " << ls.get_lower_bound(v) << "\n"; + if (ls.column_has_upper_bound(v)) + verbose_stream() << "x" << w << " <= " << ls.get_upper_bound(v) << "\n"; }); @@ -235,6 +283,13 @@ struct solver::imp { m_nlsat->mk_clause(1, &lit, nullptr); } + void add_strict_lb(lp::impq const& b, unsigned w) { + add_bound(b.x, w, false, nlsat::atom::kind::GT); + } + void add_strict_ub(lp::impq const& b, unsigned w) { + add_bound(b.x, w, false, nlsat::atom::kind::LT); + } + void add_lb(lp::impq const& b, unsigned w) { add_bound(b.x, w, b.y <= 0, b.y > 0 ? nlsat::atom::kind::GT : nlsat::atom::kind::LT); } @@ -269,7 +324,8 @@ struct solver::imp { m_lp2nl.insert(v, w); } polynomial::polynomial_ref vp(pm.mk_polynomial(w, 1), pm); - return pm.add(lo, pm.mul(vp, hi)); + polynomial::polynomial_ref mp(pm.mul(vp, hi), pm); + return pm.add(lo, mp); } bool is_int(lp::var_index v) { @@ -361,6 +417,10 @@ lbool solver::check(vector const& eqs) { return m_imp->check(eqs); } +lbool solver::check_tight(dd::pdd const& eq) { + return m_imp->check_tight(eq); +} + bool solver::need_check() { return m_imp->need_check(); } diff --git a/src/math/lp/nra_solver.h b/src/math/lp/nra_solver.h index b8863e44b..3f6335013 100644 --- a/src/math/lp/nra_solver.h +++ b/src/math/lp/nra_solver.h @@ -38,10 +38,15 @@ namespace nra { lbool check(); /** - \breif Check feasibility of equalities modulo bounds constraints on their variables. + \brief Check feasibility of equalities modulo bounds constraints on their variables. */ lbool check(vector const& eqs); + /** + \brief Check if equality is tight. + */ + lbool check_tight(const dd::pdd& eq); + /* \brief determine whether nra check is needed. */ diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 9e8f57e2c..b98cc002f 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2158,7 +2158,6 @@ public: if (m_nla) { m_nla->propagate(); add_lemmas(); - add_equalities(); lp().collect_more_rows_for_lp_propagation(); } } @@ -2193,6 +2192,7 @@ public: assume_literal(i); for (const nla::lemma & l : m_nla->lemmas()) false_case_of_check_nla(l); + add_equalities(); } bool should_propagate() const {