From e32a6714a5ff310237d0d2b76912cd1e97799389 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 8 May 2020 15:34:43 -0700 Subject: [PATCH] call nlsat Signed-off-by: Lev Nachmanson --- src/math/lp/monic.h | 3 ++ src/math/lp/nla_basics_lemmas.cpp | 5 +--- src/math/lp/nla_core.cpp | 19 ++++++++++++ src/math/lp/nla_core.h | 7 ++--- src/math/lp/nla_monotone_lemmas.cpp | 17 ++++++++++- src/math/lp/nla_monotone_lemmas.h | 1 + src/math/lp/nla_order_lemmas.cpp | 1 - src/math/lp/nla_solver.cpp | 17 +++++++++-- src/math/lp/nla_solver.h | 7 +++-- src/math/lp/nra_solver.cpp | 42 +++++---------------------- src/math/lp/nra_solver.h | 12 -------- src/smt/theory_lra.cpp | 9 ++++-- src/tactic/smtlogics/qfnra_tactic.cpp | 14 +++++---- 13 files changed, 86 insertions(+), 68 deletions(-) diff --git a/src/math/lp/monic.h b/src/math/lp/monic.h index d399909e6..6add1719b 100644 --- a/src/math/lp/monic.h +++ b/src/math/lp/monic.h @@ -74,6 +74,9 @@ public: void reset_rfields() { m_rsign = false; m_rvars.reset(); SASSERT(m_rvars.size() == 0); } void push_rvar(signed_var sv) { m_rsign ^= sv.sign(); m_rvars.push_back(sv.var()); } void sort_rvars() { std::sort(m_rvars.begin(), m_rvars.end()); } + + svector::const_iterator begin() const { return vars().begin(); } + svector::const_iterator end() const { return vars().end(); } }; inline std::ostream& operator<<(std::ostream& out, monic const& m) { diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp index ea6bf2539..b4baac7a8 100644 --- a/src/math/lp/nla_basics_lemmas.cpp +++ b/src/math/lp/nla_basics_lemmas.cpp @@ -359,8 +359,7 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factoriz // x != 0 or y = 0 => |xy| >= |y| void basics::proportion_lemma_model_based(const monic& rm, const factorization& factorization) { - if (c().has_real(factorization)) // todo: handle the situaiton when all factors are greater than 1, - return; // or smaller than 1 + if (c().factorization_has_real(factorization)) // todo: handle the situaiton when all factors are greater than 1, return; // or smaller than 1 rational rmv = abs(var_val(rm)); if (rmv.is_zero()) { SASSERT(c().has_zero_factor(factorization)); @@ -486,8 +485,6 @@ bool basics::is_separated_from_zero(const factorization& f) const { return true; } - - // here we use the fact xy = 0 -> x = 0 or y = 0 void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) { TRACE("nla_solver", c().trace_print_monic_and_factorization(rm, f, tout);); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 394ecafa4..9f0d91db7 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1895,4 +1895,23 @@ bool core::influences_nl_var(lpvar j) const { return false; } +bool core::factorization_has_real(const factorization& f) const { + for (const factor& fc: f) { + lpvar j = var(fc); + if (!var_is_int(j)) + return true; + } + return false; +} + +bool core::monic_has_real(const monic& m) const { + if (!var_is_int(m.var())) + return true; + for (lpvar j : m) { + if (!var_is_int(j)) + return true; + } + return false; +} + } // end of nla diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 03850941d..e49535b4f 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -153,7 +153,7 @@ public: void insert_to_refine(lpvar j); void erase_from_to_refine(lpvar j); - + const lp::u_set& to_refine() const { return m_to_refine; } const lp::u_set& active_var_set () const { return m_active_var_set;} bool active_var_set_contains(unsigned j) const { return m_active_var_set.contains(j); } @@ -441,9 +441,8 @@ public: bool patch_blocker(lpvar u, const monic& m) const; bool has_big_num(const monic&) const; bool var_is_big(lpvar) const; - bool has_real(const factorization&) const; - bool has_real(const monic& m) const; - + bool factorization_has_real(const factorization&) const; + bool monic_has_real(const monic&) const; }; // end of core struct pp_mon { diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp index d4d4a19b3..20b2ff8c3 100644 --- a/src/math/lp/nla_monotone_lemmas.cpp +++ b/src/math/lp/nla_monotone_lemmas.cpp @@ -11,13 +11,25 @@ namespace nla { monotone::monotone(core * c) : common(c) {} +// return false if at least one variable, including the monic var, is real, +// or one of the variable from m.vars() is zero +bool monotone::monotonicity_lemma_candidate(const monic & m) const { + if (!c().var_is_int(m.var())) + return false; + for (lpvar j : m) { + if (!c().var_is_int(j) || val(j).is_zero()) + return false; + } + return true; +} void monotone::monotonicity_lemma() { unsigned shift = random(); unsigned size = c().m_to_refine.size(); for (unsigned i = 0; i < size && !done(); i++) { lpvar v = c().m_to_refine[(i + shift) % size]; - monotonicity_lemma(c().emons()[v]); + if (monotonicity_lemma_candidate(c().emons()[v])) + monotonicity_lemma(c().emons()[v]); } } @@ -33,6 +45,9 @@ void monotone::monotonicity_lemma(monic const& m) { monotonicity_lemma_lt(m, prod_val); else if (m_val > prod_val) monotonicity_lemma_gt(m, prod_val); + else { + TRACE("nla_solver", tout << "equal\n";); + } } void monotone::monotonicity_lemma_gt(const monic& m, const rational& prod_val) { diff --git a/src/math/lp/nla_monotone_lemmas.h b/src/math/lp/nla_monotone_lemmas.h index fa8a64e75..a2c1d1dee 100644 --- a/src/math/lp/nla_monotone_lemmas.h +++ b/src/math/lp/nla_monotone_lemmas.h @@ -18,5 +18,6 @@ private: void monotonicity_lemma_lt(const monic& m, const rational& prod_val); std::vector get_sorted_key(const monic& rm) const; vector> get_sorted_key_with_rvars(const monic& a) const; + bool monotonicity_lemma_candidate(const monic& m) const; }; } diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 91612e4a9..09d62c456 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -40,7 +40,6 @@ void order::order_lemma() { void order::order_lemma_on_monic(const monic& m) { TRACE("nla_solver_details", tout << "m = " << pp_mon(c(), m);); - if (c().has_real(m)) return; for (auto ac : factorization_factory_imp(m, _())) { diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 19f27734f..0c9175e27 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -28,10 +28,23 @@ bool solver::is_monic_var(lpvar v) const { bool solver::need_check() { return true; } -lbool solver::check(vector& l) { - return m_core->check(l); +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) { + ret = run_nra(expl); + if (ret == l_true) { + set_use_nra_model(true); + } + } + return ret; +} + void solver::push(){ m_core->push(); } diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h index 63182731b..9e74873fa 100644 --- a/src/math/lp/nla_solver.h +++ b/src/math/lp/nla_solver.h @@ -26,6 +26,9 @@ class solver { reslimit m_res_limit; 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); @@ -35,11 +38,11 @@ public: void push(); void pop(unsigned scopes); bool need_check(); - lbool check(vector&); + lbool check(vector&, lp::explanation& lp); 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; } }; } diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 732d21776..1d49ae744 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -24,8 +24,6 @@ struct solver::imp { u_map m_lp2nl; // map from lar_solver variables to nlsat::solver variables scoped_ptr m_nlsat; scoped_ptr m_zero; - vector m_monics; - unsigned_vector m_monics_lim; mutable variable_map_type m_variable_values; // current model nla::core& m_nla_core; imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, nla::core& nla_core): @@ -35,22 +33,9 @@ struct solver::imp { m_nla_core(nla_core) {} bool need_check() { - return !m_monics.empty() && !check_assignments(m_monics, s, m_variable_values); + return m_nla_core.to_refine().size() != 0; } - void add(lp::var_index v, unsigned sz, lp::var_index const* vs) { - m_monics.push_back(mon_eq(v, sz, vs)); - } - - void push() { - m_monics_lim.push_back(m_monics.size()); - } - - void pop(unsigned n) { - if (n == 0) return; - m_monics.shrink(m_monics_lim[m_monics_lim.size() - n]); - m_monics_lim.shrink(m_monics_lim.size() - n); - } /* \brief Check if polynomials are well defined. @@ -85,8 +70,8 @@ struct solver::imp { TBD: use partial model from lra_solver to prime the state of nlsat_solver. TBD: explore more incremental ways of applying nlsat (using assumptions) */ - lbool check(lp::explanation& ex) { - SASSERT(need_check()); + lbool check(lp::explanation& ex) { + SASSERT(need_check() && ex.size() == 0); m_nlsat = alloc(nlsat::solver, m_limit, m_params, false); m_zero = alloc(scoped_anum, am()); m_lp2nl.reset(); @@ -97,10 +82,10 @@ struct solver::imp { add_constraint(ci); } - // add polynomial definitions. - for (auto const& m : m_monics) { - add_monic_eq(m); - } + // // add polynomial definitions. + // for (auto const& m : m_monics) { + // add_monic_eq(m); + // } // TBD: add variable bounds? lbool r = l_undef; @@ -227,7 +212,7 @@ struct solver::imp { } std::ostream& display(std::ostream& out) const { - for (auto m : m_monics) { + for (auto m : m_nla_core.emons()) { out << "j" << m.var() << " = "; for (auto v : m.vars()) { out << "j" << v << " "; @@ -246,9 +231,6 @@ solver::~solver() { dealloc(m_imp); } -void solver::add_monic(lp::var_index v, unsigned sz, lp::var_index const* vs) { - m_imp->add(v, sz, vs); -} lbool solver::check(lp::explanation& ex) { return m_imp->check(ex); @@ -258,14 +240,6 @@ bool solver::need_check() { return m_imp->need_check(); } -void solver::push() { - m_imp->push(); -} - -void solver::pop(unsigned n) { - m_imp->pop(n); -} - std::ostream& solver::display(std::ostream& out) const { return m_imp->display(out); } diff --git a/src/math/lp/nra_solver.h b/src/math/lp/nra_solver.h index 0303b76be..f86720350 100644 --- a/src/math/lp/nra_solver.h +++ b/src/math/lp/nra_solver.h @@ -29,11 +29,6 @@ namespace nra { ~solver(); - /* - \brief Add a definition v = vs[0]*vs[1]*...*vs[sz-1] - The variable v is equal to the product of variables vs. - */ - void add_monic(lp::var_index v, unsigned sz, lp::var_index const* vs); /* \brief Check feasiblity of linear constraints augmented by polynomial definitions @@ -53,13 +48,6 @@ namespace nra { nlsat::anum_manager& am(); - /* - \brief push and pop scope. - Monomial definitions are retraced when popping scope. - */ - void push(); - - void pop(unsigned n); /* \brief display state diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 89906549d..a13141f39 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -632,7 +632,8 @@ class theory_lra::imp { vars.push_back(register_theory_var_in_lar_solver(v)); } TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << "\n" << vars << "\n";); - m_solver->register_existing_terms(); + m_solver->register_existing_terms(); + ensure_nla(); m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr()); } return v; @@ -2138,7 +2139,11 @@ public: lbool check_nla_continue() { m_a1 = nullptr; m_a2 = nullptr; auto & lv = m_nla_lemma_vector; - lbool r = m_nla->check(lv); + lbool r = m_nla->check(lv, m_explanation); + if (m_explanation.size()) { + NOT_IMPLEMENTED_YET(); // the nra_solver worked + } + switch (r) { case l_false: { m_stats.m_nla_lemmas += lv.size(); diff --git a/src/tactic/smtlogics/qfnra_tactic.cpp b/src/tactic/smtlogics/qfnra_tactic.cpp index 7d93abe25..4d7c2b28f 100644 --- a/src/tactic/smtlogics/qfnra_tactic.cpp +++ b/src/tactic/smtlogics/qfnra_tactic.cpp @@ -44,12 +44,14 @@ tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) { return and_then(mk_simplify_tactic(m, p), mk_propagate_values_tactic(m, p), - or_else(try_for(mk_qfnra_nlsat_tactic(m, p0), 5000), - try_for(mk_qfnra_nlsat_tactic(m, p1), 10000), - mk_qfnra_sat_solver(m, p, 4), - and_then(try_for(mk_smt_tactic(m), 5000), mk_fail_if_undecided_tactic()), - mk_qfnra_sat_solver(m, p, 6), - mk_qfnra_nlsat_tactic(m, p2))); + //or_else(//try_for(mk_qfnra_nlsat_tactic(m, p0), 5000), + //try_for(mk_qfnra_nlsat_tactic(m, p1), 10000), + //mk_qfnra_sat_solver(m, p, 4), + //and_then(try_for(mk_smt_tactic(m), 5000), mk_fail_if_undecided_tactic()), + mk_qfnra_sat_solver(m, p, 6) + //mk_qfnra_nlsat_tactic(m, p2) + //) + ); }