From 9ce2733105b5754365973f1e970f68d46b4687f2 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 6 Jun 2019 09:21:45 -0700
Subject: [PATCH] unresolved in nla_intervals

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_intervals.cpp |  4 +++-
 src/math/lp/nla_intervals.h   | 17 ++++++++++++++---
 src/math/lp/nla_solver.cpp    |  2 +-
 src/math/lp/nla_solver.h      |  1 +
 4 files changed, 19 insertions(+), 5 deletions(-)
 mode change 100644 => 100755 src/math/lp/nla_intervals.cpp
 mode change 100644 => 100755 src/math/lp/nla_intervals.h

diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
old mode 100644
new mode 100755
index be3674c66..7c78999b3
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -107,15 +107,17 @@ namespace nla {
 
 lp::impq intervals::get_upper_bound_of_monomial(lpvar j) const {
     SASSERT(false);
+    throw;
 }
 
 lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const {
     SASSERT(false);
+    throw;
 }
 
 bool intervals::product_has_upper_bound(int sign, const svector<lpvar>&) const {
     interval a;
-    
+    throw;
 }
 
 bool intervals::monomial_has_lower_bound(lpvar j) const {
diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h
old mode 100644
new mode 100755
index 8602a2bfe..b86140754
--- a/src/math/lp/nla_intervals.h
+++ b/src/math/lp/nla_intervals.h
@@ -19,6 +19,7 @@
   --*/
 #pragma once
 #include "util/dependency.h"
+#include "util/small_object_allocator.h"
 #include "math/lp/nla_common.h"
 #include "math/lp/lar_solver.h"
 #include "math/interval/interval.h"
@@ -134,11 +135,14 @@ namespace nla {
             }
         };
 
-        ci_dependency_manager        m_dep_manager;
+        small_object_allocator      m_alloc;
+        ci_value_manager            m_val_manager;
+        unsynch_mpq_manager         m_num_manager;
+        ci_dependency_manager       m_dep_manager;
         im_config                   m_config;
         interval_manager<im_config> m_imanager;
         region                      m_region;
-        //   lp::lar_solver&             m_solver;
+        lp::lar_solver&             m_solver;
 
         typedef interval_manager<im_config>::interval interval;
 
@@ -151,7 +155,14 @@ namespace nla {
         bool check(lp::lar_term const& t);
 
     public:
-        intervals(core* c) : m_core(c) {}
+        intervals(core* c, reslimit& lim, lp::lar_solver& s) : 
+            m_core(c), 
+            m_alloc("intervals"),
+            m_dep_manager(m_val_manager, m_alloc),
+            m_config(m_num_manager, m_dep_manager),
+            m_imanager(lim, im_config(m_num_manager, m_dep_manager)),
+            m_solver(s)
+        {}
         bool check();
         bool monomial_has_lower_bound(lpvar j) const;
         bool monomial_has_upper_bound(lpvar j) const;
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index cde83ea8a..60becfa3f 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -55,7 +55,7 @@ void solver::pop(unsigned n) {
     }
 
         
-solver::solver(lp::lar_solver& s): m_core(alloc(core, s)), m_intervals(m_core)  {
+solver::solver(lp::lar_solver& s): m_core(alloc(core, s)), m_intervals(m_core, m_res_limit, s)  {
 }
 
 solver::~solver() {
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index 3672ca158..8f1fd7622 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -33,6 +33,7 @@ namespace nla {
 // nonlinear integer incremental linear solver
 class solver {
     core* m_core;
+    reslimit m_res_limit;
     intervals m_intervals;
 public:
     void add_monomial(lpvar v, unsigned sz, lpvar const* vs);