diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 394ecafa4..35af6091a 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1441,8 +1441,7 @@ void core::patch_monomial_with_real_var(lpvar j) { erase_from_to_refine(j); break; } - } - + } } void core::patch_monomials_with_real_vars() { @@ -1465,7 +1464,8 @@ lbool core::check(vector& l_vec) { TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";); m_lar_solver.get_rid_of_inf_eps(); m_lemma_vec = &l_vec; - if (!(m_lar_solver.get_status() == lp::lp_status::OPTIMAL || m_lar_solver.get_status() == lp::lp_status::FEASIBLE )) { + if (!(m_lar_solver.get_status() == lp::lp_status::OPTIMAL || + m_lar_solver.get_status() == lp::lp_status::FEASIBLE)) { TRACE("nla_solver", tout << "unknown because of the m_lar_solver.m_status = " << m_lar_solver.get_status() << "\n";); return l_undef; } @@ -1478,13 +1478,10 @@ lbool core::check(vector& l_vec) { init_search(); - bool enable_grobner = false; + if (need_to_call_algebraic_methods() && m_horner.horner_lemmas()) + goto finish_up; - if (need_to_call_algebraic_methods()) { - enable_grobner = !m_horner.horner_lemmas(); - } - - if (enable_grobner && !done()) { + 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()) { find_nl_cluster(); @@ -1512,6 +1509,8 @@ lbool core::check(vector& l_vec) { m_tangents.tangent_lemma(); } + finish_up: + lbool ret = !l_vec.empty() && !lp_settings().get_cancel_flag() ? l_false : l_undef; 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());}); diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index f75718bb1..98df516cb 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -34,7 +34,7 @@ lbool solver::run_nra(lp::explanation & expl) { lbool solver::check(vector& l, lp::explanation& expl) { set_use_nra_model(false); lbool ret = m_core->check(l); - if (false && ret == l_undef) { // disable the call to nlsat + 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); @@ -54,6 +54,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; } bool solver::influences_nl_var(lpvar j) const { diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 8aa4fbf26..ab1f6e18a 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -9,6 +9,7 @@ #include "math/polynomial/polynomial.h" #include "math/polynomial/algebraic_numbers.h" #include "util/map.h" +#include "util/uint_set.h" #include "math/lp/nla_core.h" @@ -18,10 +19,12 @@ typedef nla::mon_eq mon_eq; typedef nla::variable_map_type variable_map_type; struct solver::imp { - lp::lar_solver& s; - reslimit& m_limit; - params_ref m_params; - u_map m_lp2nl; // map from lar_solver variables to nlsat::solver variables + lp::lar_solver& s; + reslimit& m_limit; + params_ref m_params; + u_map m_lp2nl; // map from lar_solver variables to nlsat::solver variables + svector m_terms; + uint_set m_term_set; scoped_ptr m_nlsat; scoped_ptr m_zero; mutable variable_map_type m_variable_values; // current model @@ -37,28 +40,6 @@ struct solver::imp { } - /* - \brief Check if polynomials are well defined. - multiply values for vs and check if they are equal to value for v. - epsilon has been computed. - */ - /* bool check_assignment(mon_eq const& m) const { - rational r1 = m_variable_values[m.m_v]; - rational r2(1); - for (auto w : m.vars()) { - r2 *= m_variable_values[w]; - } - return r1 == r2; - } - - bool check_assignments() const { - s.get_model(m_variable_values); - for (auto const& m : m_monics) { - if (!check_assignment(m)) return false; - } - return true; - } - */ /** \brief one-shot nlsat check. A one shot checker is the least functionality that can @@ -74,6 +55,8 @@ struct solver::imp { SASSERT(need_check() && ex.size() == 0); m_nlsat = alloc(nlsat::solver, m_limit, m_params, false); m_zero = alloc(scoped_anum, am()); + m_terms.reset(); + m_term_set.reset(); m_lp2nl.reset(); vector core; @@ -86,6 +69,9 @@ struct solver::imp { for (auto const& m : m_nla_core.emons()) { add_monic_eq(m); } + for (unsigned i = 0; i < m_terms.size(); ++i) { + add_term(m_terms[i]); + } // TBD: add variable bounds? lbool r = l_undef; @@ -195,10 +181,23 @@ struct solver::imp { r = m_nlsat->mk_var(is_int(v)); m_lp2nl.insert(v, r); TRACE("arith", tout << "j" << v << " := x" << r << "\n";); +#if 0 + // TBD: + if (m_nla_core.is_from_a_term(v) && !m_term_set.contains(v)) { + m_terms.push_back(m_nla_core.column2tv(v)); + } +#endif } return r; } + void add_term(lp::tv const& t) { +#if 0 + // TBD: code that creates a polynomial equality between the linear coefficients and + // variable representing the term. +#endif + } + nlsat::anum const& value(lp::var_index v) const { polynomial::var pv; if (m_lp2nl.find(v, pv)) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 328a5e952..e2c56f7e5 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -286,8 +286,15 @@ class theory_lra::imp { } }; - bool use_nra_model() const { - return m_nla && m_nla->use_nra_model(); + bool use_nra_model() { + if (m_nla && m_nla->use_nra_model()) { + if (!m_a1) { + m_a1 = alloc(scoped_anum, m_nla->am()); + m_a2 = alloc(scoped_anum, m_nla->am()); + } + return true; + } + return false; } struct var_value_hash { @@ -1619,6 +1626,11 @@ public: unsigned old_sz = m_assume_eq_candidates.size(); unsigned num_candidates = 0; int start = ctx().get_random_value(); + auto has_value = [&](theory_var v) { + if (use_nra_model()) + return true; + return can_get_ivalue(v); + }; for (theory_var i = 0; i < sz; ++i) { theory_var v = (i + start) % sz; enode* n1 = get_enode(v); @@ -1626,9 +1638,8 @@ public: continue; } ensure_column(v); - if (!can_get_ivalue(v)) { + if (!can_get_ivalue(v)) continue; - } theory_var other = m_model_eqs.insert_if_not_there(v); TRACE("arith", tout << "insert: v" << v << " := " << get_value(v) << " found: v" << other << "\n";); if (other == v) { @@ -2152,7 +2163,6 @@ public: } lbool check_nla_continue() { - m_a1 = nullptr; m_a2 = nullptr; auto & lv = m_nla_lemma_vector; m_explanation.clear(); lbool r = m_nla->check(lv, m_explanation); @@ -2176,10 +2186,6 @@ public: break; } case l_true: - if (use_nra_model()) { - m_a1 = alloc(scoped_anum, m_nla->am()); - m_a2 = alloc(scoped_anum, m_nla->am()); - } if (assume_eqs()) { return l_false; } @@ -3358,7 +3364,7 @@ public: m_todo_terms.push_back(std::make_pair(t, rational::one())); - TRACE("arith", tout << "v" << v << " := w" << t.to_string() << "\n"; + TRACE("nl_value", tout << "v" << v << " := w" << t.to_string() << "\n"; lp().print_term(lp().get_term(t), tout) << "\n";); m_nla->am().set(r, 0); @@ -3367,7 +3373,7 @@ public: t = m_todo_terms.back().first; m_todo_terms.pop_back(); lp::lar_term const& term = lp().get_term(t); - TRACE("arith", lp().print_term(term, tout) << "\n";); + TRACE("nl_value", lp().print_term(term, tout) << "\n";); scoped_anum r1(m_nla->am()); rational c1(0); m_nla->am().set(r1, c1.to_mpq()); @@ -3789,7 +3795,8 @@ public: if (!ctx().is_relevant(get_enode(v))) out << "irr: "; out << "v" << v << " "; if (t.is_null()) out << "null"; else out << (t.is_term() ? "t":"j") << t.id(); - if (can_get_value(v)) out << " = " << get_value(v); + if (use_nra_model() && can_get_ivalue(v)) m_nla->am().display(out << " = ", nl_value(v, *m_a1)); + else if (can_get_value(v)) out << " = " << get_value(v); if (is_int(v)) out << ", int"; if (ctx().is_shared(get_enode(v))) out << ", shared"; out << " := "; th.display_var_flat_def(out, v) << "\n";