From 2513deb8172f3519192282ef71f6da297f927bf4 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 10 Apr 2019 16:01:07 -0700
Subject: [PATCH] Add forgotten file

---
 src/util/lp/nla_solver.h | 31 ++-----------------------------
 1 file changed, 2 insertions(+), 29 deletions(-)

diff --git a/src/util/lp/nla_solver.h b/src/util/lp/nla_solver.h
index f80ad16c4..dfd84e7d3 100644
--- a/src/util/lp/nla_solver.h
+++ b/src/util/lp/nla_solver.h
@@ -25,39 +25,12 @@ Revision History:
 #include "nlsat/nlsat_solver.h"
 #include "util/lp/lar_solver.h"
 #include "util/lp/monomial.h"
-
+#include "util/lp/nla_core.h"
 namespace nla {
-struct ineq {
-    lp::lconstraint_kind m_cmp;
-    lp::lar_term         m_term;
-    rational             m_rs;
-    ineq(lp::lconstraint_kind cmp, const lp::lar_term& term, const rational& rs) : m_cmp(cmp), m_term(term), m_rs(rs) {}
-    bool operator==(const ineq& a) const {
-        return m_cmp == a.m_cmp && m_term == a.m_term && m_rs == a.m_rs;
-    }
-    const lp::lar_term& term() const { return m_term; };
-    lp::lconstraint_kind cmp() const { return m_cmp;  };
-    const rational& rs() const { return m_rs; };
-};
 
-class lemma {
-    vector<ineq>     m_ineqs;
-    lp::explanation  m_expl;
-public:
-    void push_back(const ineq& i) { m_ineqs.push_back(i);}
-    size_t size() const { return m_ineqs.size() + m_expl.size(); }
-    const vector<ineq>& ineqs() const { return m_ineqs; }
-    vector<ineq>& ineqs() { return m_ineqs; }
-    lp::explanation& expl() { return m_expl; }
-    const lp::explanation& expl() const { return m_expl; }
-    bool is_conflict() const { return m_ineqs.empty() && !m_expl.empty(); }
-};
-
-typedef vector<monomial> polynomial;
 // nonlinear integer incremental linear solver
 class solver {
-    struct imp;
-    imp* m_imp;
+    core* m_core;
 public:
     // returns the monomial index
     unsigned add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs);