From be1a1dd7c2e369c38af33b8587400c644f779ed6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 12 May 2020 17:36:46 -0700
Subject: [PATCH] add stubs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/math/lp/nla_core.cpp | 17 ++++++-------
src/math/lp/nla_solver.cpp | 3 ++-
src/math/lp/nra_solver.cpp | 51 +++++++++++++++++++-------------------
src/smt/theory_lra.cpp | 31 ++++++++++++++---------
4 files changed, 54 insertions(+), 48 deletions(-)
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<lemma>& 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<lemma>& 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<lemma>& 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<lemma>& 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<polynomial::var> m_lp2nl; // map from lar_solver variables to nlsat::solver variables
+ lp::lar_solver& s;
+ reslimit& m_limit;
+ params_ref m_params;
+ u_map<polynomial::var> m_lp2nl; // map from lar_solver variables to nlsat::solver variables
+ svector<lp::tv> m_terms;
+ uint_set m_term_set;
scoped_ptr<nlsat::solver> m_nlsat;
scoped_ptr<scoped_anum> 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<nlsat::assumption, false> 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";