From b2dc21b1072508abb9d9391d9f7043b2312bc36b Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 12 May 2020 19:34:03 -0700 Subject: [PATCH] simplify the nla_solver interface (#4312) * simplify the nla_solver interface Signed-off-by: Lev Nachmanson * more simplifications Signed-off-by: Lev Nachmanson * init m_use_nra_model Signed-off-by: Lev Nachmanson Co-authored-by: Nikolaj Bjorner --- src/math/lp/nla_core.cpp | 34 +++++++++++++++++++++++++++------- src/math/lp/nla_core.h | 5 ++++- src/math/lp/nla_solver.cpp | 32 ++++++++++++++------------------ src/math/lp/nla_solver.h | 20 ++++++-------------- src/smt/theory_lra.cpp | 19 ++++--------------- 5 files changed, 55 insertions(+), 55 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 35af6091a..84e1b507a 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -32,7 +32,9 @@ core::core(lp::lar_solver& s, reslimit & lim) : m_pdd_manager(s.number_of_vars()), m_pdd_grobner(lim, m_pdd_manager), m_emons(m_evars), - m_reslim(lim) + m_reslim(lim), + m_use_nra_model(false), + m_nra(s, lim, *this) {} bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const { @@ -1472,15 +1474,15 @@ lbool core::check(vector& l_vec) { init_to_refine(); patch_monomials_with_real_vars(); - if (m_to_refine.is_empty()) { - return l_true; - } - + if (m_to_refine.is_empty()) { return l_true; } init_search(); + + set_use_nra_model(false); if (need_to_call_algebraic_methods() && m_horner.horner_lemmas()) goto finish_up; + if (!done()) { clear_and_resize_active_var_set(); // NSB code review: why is this independent of whether Grobner is run? if (m_nla_settings.run_grobner()) { @@ -1509,9 +1511,27 @@ lbool core::check(vector& l_vec) { m_tangents.tangent_lemma(); } - finish_up: + if (lp_settings().get_cancel_flag()) + return l_undef; - lbool ret = !l_vec.empty() && !lp_settings().get_cancel_flag() ? l_false : l_undef; + + finish_up: + lbool ret = l_vec.empty() ? l_undef : l_false; +#if 0 + if (l_vec.empty()) { + lp::explanation expl; + ret = m_nra.check(expl); + + if (ret == l_false) { + new_lemma lemma(*this, __FUNCTION__); + lemma &= expl; + set_use_nra_model(true); + } else if (ret == l_true) { + set_use_nra_model(true); + } + } +#endif + TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << l_vec.size() << "\n";); IF_VERBOSE(2, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monics(verbose_stream());}); CTRACE("nla_solver", ret == l_undef, tout << "Monomials\n"; print_monics(tout);); diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index fb8697d00..9598f3374 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -161,6 +161,8 @@ private: lp::u_set m_rows; public: reslimit& m_reslim; + bool m_use_nra_model; + nra::solver m_nra; void insert_to_refine(lpvar j); void erase_from_to_refine(lpvar j); @@ -454,7 +456,8 @@ public: bool var_is_big(lpvar) const; bool has_real(const factorization&) const; bool has_real(const monic& m) const; - + void set_use_nra_model(bool m) { m_use_nra_model = m; } + bool use_nra_model() const { return m_use_nra_model; } }; // end of core struct pp_mon { diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 98df516cb..3f34fbdf1 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -12,6 +12,8 @@ #include "math/lp/var_eqs.h" #include "math/lp/factorization.h" #include "math/lp/nla_solver.h" +#include "math/lp/nla_core.h" + namespace nla { nla_settings& solver::settings() { return m_core->m_nla_settings; } @@ -26,21 +28,9 @@ bool solver::is_monic_var(lpvar v) const { bool solver::need_check() { return true; } -lbool solver::run_nra(lp::explanation & expl) { - return m_nra.check(expl); -} - -lbool solver::check(vector& l, lp::explanation& expl) { - set_use_nra_model(false); - lbool ret = m_core->check(l); - if (ret == l_undef) { // disable the call to nlsat - ret = run_nra(expl); - if (ret == l_true || expl.size() > 0) { - set_use_nra_model(true); - } - } - return ret; +lbool solver::check(vector& l) { + return m_core->check(l); } void solver::push(){ @@ -52,9 +42,7 @@ void solver::pop(unsigned n) { } solver::solver(lp::lar_solver& s, reslimit& limit): - m_core(alloc(core, s, limit)), - m_nra(s, limit, *m_core) { - m_use_nra_model = false; + m_core(alloc(core, s, limit)) { } bool solver::influences_nl_var(lpvar j) const { @@ -68,9 +56,17 @@ solver::~solver() { std::ostream& solver::display(std::ostream& out) const { m_core->print_monics(out); if( use_nra_model()) { - return m_nra.display(out); + m_core->m_nra.display(out); } return out; } +bool solver::use_nra_model() const { return m_core->use_nra_model(); } +core& solver::get_core() { return *m_core; } +nlsat::anum_manager& solver::am() { return m_core->m_nra.am(); } +nlsat::anum const& solver::am_value(lp::var_index v) const { + SASSERT(use_nra_model()); + return m_core->m_nra.value(v); +} + } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index b61e8a26e..42231a4ee 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -23,29 +23,21 @@ class core; // nonlinear integer incremental linear solver class solver { core* m_core; - nra::solver m_nra; - bool m_use_nra_model; - lbool run_nra(lp::explanation&); - void set_use_nra_model(bool m) { m_use_nra_model = m; } public: - void add_monic(lpvar v, unsigned sz, lpvar const* vs); - + void add_monic(lpvar v, unsigned sz, lpvar const* vs); solver(lp::lar_solver& s, reslimit& limit); ~solver(); nla_settings& settings(); void push(); void pop(unsigned scopes); bool need_check(); - lbool check(vector&, lp::explanation& lp); + lbool check(vector&); bool is_monic_var(lpvar) const; bool influences_nl_var(lpvar) const; std::ostream& display(std::ostream& out) const; - bool use_nra_model() const { return m_use_nra_model; } - core& get_core() { return *m_core; } - nlsat::anum_manager& am() { return m_nra.am(); } - nlsat::anum const& am_value(lp::var_index v) const { - SASSERT(use_nra_model()); - return m_nra.value(v); - } + bool use_nra_model() const; + core& get_core(); + nlsat::anum_manager& am(); + nlsat::anum const& am_value(lp::var_index v) const; }; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 64eae7105..b8a36fd28 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2158,24 +2158,13 @@ public: } lbool check_nla_continue() { - auto & lv = m_nla_lemma_vector; - m_explanation.clear(); - lbool r = m_nla->check(lv, m_explanation); - if (use_nra_model()) - m_stats.m_nra_calls ++; - - if (m_explanation.size()) { - SASSERT(use_nra_model()); - SASSERT(r == l_false); - set_conflict(); - return l_false; - } + lbool r = m_nla->check(m_nla_lemma_vector); + if (use_nra_model()) m_stats.m_nra_calls ++; switch (r) { case l_false: { - SASSERT(m_explanation.size() == 0); - m_stats.m_nla_lemmas += lv.size(); - for (const nla::lemma & l : lv) { + m_stats.m_nla_lemmas += m_nla_lemma_vector.size(); + for (const nla::lemma & l : m_nla_lemma_vector) { false_case_of_check_nla(l); } break;