From 97058b0d5d8e9f3138479b5f77250f7477c29222 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 19 Oct 2023 16:08:35 -0700 Subject: [PATCH] allow for propagations the trigger make-feasible check --- src/math/lp/nla_core.cpp | 12 +++++------- src/math/lp/nla_core.h | 2 ++ src/math/lp/nla_grobner.cpp | 6 ++---- src/math/lp/nla_solver.h | 1 + src/smt/theory_lra.cpp | 23 +++++++++++++---------- 5 files changed, 23 insertions(+), 21 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 50cd31661..978348816 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -819,6 +819,7 @@ void core::clear() { m_fixed_equalities.clear(); m_equalities.clear(); m_conflicts = 0; + m_check_feasible = false; } void core::init_search() { @@ -1192,11 +1193,7 @@ void core::negate_relation(new_lemma& lemma, unsigned j, const rational& a) { } bool core::conflict_found() const { - for (const auto & l : m_lemmas) { - if (l.is_conflict()) - return true; - } - return false; + return any_of(m_lemmas, [&](const auto& l) { return l.is_conflict(); }); } bool core::done() const { @@ -1555,7 +1552,7 @@ lbool core::check() { bool run_bounded_nlsat = should_run_bounded_nlsat(); bool run_bounds = params().arith_nl_branching(); - auto no_effect = [&]() { return !done() && m_lemmas.empty() && m_literals.empty(); }; + auto no_effect = [&]() { return !done() && m_lemmas.empty() && m_literals.empty() && !m_check_feasible; }; if (no_effect()) m_monomial_bounds.propagate(); @@ -1573,6 +1570,7 @@ lbool core::check() { {1, check2}, {1, check3} }; check_weighted(3, checks); + if (!m_lemmas.empty() || !m_literals.empty()) return l_false; } @@ -1610,7 +1608,7 @@ lbool core::check() { lp_settings().stats().m_nra_calls++; } - if (ret == l_undef && !m_lemmas.empty() && m_reslim.inc()) + if (ret == l_undef && !no_effect() && m_reslim.inc()) ret = l_false; lp_settings().stats().m_nla_lemmas += m_lemmas.size(); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index f99f640bf..bd2b19a9a 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -87,6 +87,7 @@ class core { intervals m_intervals; monomial_bounds m_monomial_bounds; unsigned m_conflicts; + bool m_check_feasible = false; horner m_horner; grobner m_grobner; emonics m_emons; @@ -424,6 +425,7 @@ public: vector const& literals() const { return m_literals; } vector const& equalities() const { return m_equalities; } vector const& fixed_equalities() const { return m_fixed_equalities; } + bool check_feasible() const { return m_check_feasible; } void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); } void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); } diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index b3ad6173e..be7c4d519 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -401,9 +401,7 @@ namespace nla { auto q = e.poly(); -#if 0 - // TODO: instead add a row to lra solver, make sure that make_feasible - // gets invoked (for example, bail out of final check). +#if 1 vector> coeffs; while (!q.is_val()) { coeffs.push_back({lc*q.hi().val(), q.var()}); @@ -413,7 +411,7 @@ namespace nla { lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX); term_index = c().lra.map_term_index_to_column_index(term_index); c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, -lc*q.val(), e.dep()); - + c().m_check_feasible = true; #else new_lemma lemma(m_core,"nla-linear"); diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index c508e68d0..10cc8e006 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -51,5 +51,6 @@ namespace nla { vector const& literals() const; vector const& fixed_equalities() const; vector const& equalities() const; + bool check_feasible() const { return m_core->check_feasible(); } }; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b98cc002f..0fabe7ecd 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2162,15 +2162,6 @@ public: } } - void add_equalities() { - if (!propagate_eqs()) - return; - for (auto const& [v,k,e] : m_nla->fixed_equalities()) - add_equality(v, k, e); - for (auto const& [i,j,e] : m_nla->equalities()) - add_eq(i,j,e,false); - } - void add_equality(lpvar j, rational const& k, lp::explanation const& exp) { TRACE("arith", tout << "equality " << j << " " << k << "\n"); theory_var v; @@ -2188,11 +2179,23 @@ public: } void add_lemmas() { + if (m_nla->check_feasible()) { + auto is_sat = make_feasible(); + if (l_false == is_sat) { + get_infeasibility_explanation_and_set_conflict(); + return; + } + } for (const nla::ineq& i : m_nla->literals()) assume_literal(i); for (const nla::lemma & l : m_nla->lemmas()) false_case_of_check_nla(l); - add_equalities(); + if (!propagate_eqs()) + return; + for (auto const& [v, k, e] : m_nla->fixed_equalities()) + add_equality(v, k, e); + for (auto const& [i, j, e] : m_nla->equalities()) + add_eq(i, j, e, false); } bool should_propagate() const {