simplify the nla_solver interface (#4312)

* simplify the nla_solver interface

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* more simplifications

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* init m_use_nra_model

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<lemma>& 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<lemma>& 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););

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 {

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<lemma>& 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<lemma>& 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);
+}
+
 }

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<lemma>&, lp::explanation& lp);
+    lbool check(vector<lemma>&);
     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;
 };
 }

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;