From 151397a067740baad3394e65c4cbef1061d36823 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 7 May 2020 17:12:38 -0700
Subject: [PATCH] nra to nla

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/smt/theory_lra.cpp | 26 +++++---------------------
 1 file changed, 5 insertions(+), 21 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ca2afce59..89906549d 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -270,20 +270,6 @@ class theory_lra::imp {
     scoped_ptr<nla::solver>  m_nla;
     scoped_ptr<scoped_anum>  m_a1, m_a2;
 
-    struct switcher {
-        theory_lra::imp& m_th_imp;
-        scoped_ptr<nla::solver>*  m_nla;
-        switcher(theory_lra::imp& i): m_th_imp(i), m_nla(nullptr) {
-        }
-        
-        bool need_check() {
-            if (m_nla != nullptr)
-                return (*m_nla)->need_check();
-            return false;
-        }
-                
-    };
-
     // integer arithmetic
     scoped_ptr<lp::int_solver> m_lia;
 
@@ -314,7 +300,6 @@ class theory_lra::imp {
     scoped_ptr<lp::lar_solver> m_solver;
     resource_limit         m_resource_limit;
     lp_bounds              m_new_bounds;
-    switcher               m_switcher;
     symbol                 m_farkas;
 
     context& ctx() const { return th.get_context(); }
@@ -957,7 +942,6 @@ public:
         m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
         m_solver(nullptr),
         m_resource_limit(*this),
-        m_switcher(*this),
         m_farkas("farkas") {
     }
         
@@ -1710,7 +1694,7 @@ public:
                 break;
             }
             
-            switch (check_nra()) {
+            switch (check_nla()) {
             case l_true:
                 break;
             case l_false:
@@ -2151,7 +2135,7 @@ public:
         set_conflict_or_lemma(core, false);
     }
     
-    lbool check_nra_continue() {
+    lbool check_nla_continue() {
         m_a1 = nullptr; m_a2 = nullptr;
         auto & lv = m_nla_lemma_vector;
         lbool r = m_nla->check(lv);
@@ -2174,14 +2158,14 @@ public:
         return r;
     }
 
-    lbool check_nra() {
+    lbool check_nla() {
         if (!m.inc()) {
             TRACE("arith", tout << "canceled\n";);
             return l_undef;
         }
         if (!m_nla) return l_true;
-        if (!m_switcher.need_check()) return l_true;
-        return check_nra_continue();
+        if (!m_nla->need_check()) return l_true;
+        return check_nla_continue();
     }
 
     /**