From 8b546867f07234a08abe80e5743db004453de7b3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 12 May 2020 19:47:29 -0700
Subject: [PATCH] move lemma creation into nra_solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/nla_core.cpp   | 18 ++++--------------
 src/math/lp/nra_solver.cpp | 15 ++++++++++-----
 src/math/lp/nra_solver.h   |  2 +-
 3 files changed, 15 insertions(+), 20 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 84e1b507a..6df7af584 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1511,25 +1511,15 @@ lbool core::check(vector<lemma>& l_vec) {
             m_tangents.tangent_lemma();
     }
 
-    if (lp_settings().get_cancel_flag())
+    if (!m_reslim.inc())
         return 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);
-        }        
-    }
+    if (l_vec.empty()) 
+        ret = m_nra.check();
+    }        
 #endif
     
     TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << l_vec.size() << "\n";);
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index ab1f6e18a..962271566 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -51,7 +51,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) {        
+    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());
@@ -89,8 +90,9 @@ struct solver::imp {
         TRACE("arith", display(tout); m_nlsat->display(tout << r << "\n"););
         switch (r) {
         case l_true: 
+            m_nla_core.set_use_nra_model(true);
             break;
-        case l_false: 
+        case l_false: {
             ex.clear();
             m_nlsat->get_core(core);
             for (auto c : core) {
@@ -98,8 +100,11 @@ struct solver::imp {
                 ex.push_justification(idx, rational(1));
                 TRACE("arith", tout << "ex: " << idx << "\n";);
             }
+            nla::new_lemma lemma(m_nla_core, __FUNCTION__);
+            lemma &= ex;
+            m_nla_core.set_use_nra_model(true);
             break;
-
+        }
         case l_undef:
             break;
         }            
@@ -231,8 +236,8 @@ solver::~solver() {
 }
 
 
-lbool solver::check(lp::explanation& ex) {
-    return m_imp->check(ex);
+lbool solver::check() {
+    return m_imp->check();
 }
 
 bool solver::need_check() {
diff --git a/src/math/lp/nra_solver.h b/src/math/lp/nra_solver.h
index f86720350..eaac27655 100644
--- a/src/math/lp/nra_solver.h
+++ b/src/math/lp/nra_solver.h
@@ -34,7 +34,7 @@ namespace nra {
           \brief Check feasiblity of linear constraints augmented by polynomial definitions
           that are added.
          */
-        lbool check(lp::explanation& ex);
+        lbool check();
 
         /*
           \brief determine whether nra check is needed.