add stubs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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());});

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 {    

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))