From 58003f9f97b07de7af4b25c7e80abff704873725 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 5 Jun 2019 15:56:44 -0700
Subject: [PATCH] hook up nla_solver it lp bound propagation

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/interval/interval.h        |  7 ++-----
 src/math/interval/interval_def.h    | 21 +++++++++++----------
 src/math/lp/CMakeLists.txt          |  1 +
 src/math/lp/lp_bound_propagator.cpp |  1 +
 4 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/src/math/interval/interval.h b/src/math/interval/interval.h
index 695c1c78e..273d9a626 100644
--- a/src/math/interval/interval.h
+++ b/src/math/interval/interval.h
@@ -197,6 +197,8 @@ public:
 
     void set(interval & t, interval const & s);
 
+    void set(interval & t, numeral const& n);
+
     bool eq(interval const & a, interval const & b) const;
 
     /**
@@ -234,11 +236,6 @@ public:
 
     bool check_invariant(interval const & n) const;
 
-    /**
-       \brief b <- k
-    */
-    void set(numeral const& k, interval & b);
-
     /**
        \brief b <- -a
     */
diff --git a/src/math/interval/interval_def.h b/src/math/interval/interval_def.h
index 293a85eac..1b9bb473e 100644
--- a/src/math/interval/interval_def.h
+++ b/src/math/interval/interval_def.h
@@ -662,16 +662,6 @@ bool interval_manager<C>::check_invariant(interval const & n) const {
     return true;
 }
 
-template<typename C>
-void interval_manager<C>::set(numeral const& k, interval & b) {
-    set_lower_is_inf(b, false);
-    set_upper_is_inf(b, false);
-    m().set(lower(b), k);
-    m().set(upper(b), k);
-    set_lower_is_open(b, false);
-    set_upper_is_open(b, false);
-}
-
 template<typename C>
 void interval_manager<C>::set(interval & t, interval const & s) {
     if (&t == &const_cast<interval&>(s))
@@ -695,6 +685,17 @@ void interval_manager<C>::set(interval & t, interval const & s) {
     SASSERT(check_invariant(t));
 }
 
+template<typename C>
+void interval_manager<C>::set(interval & t, numeral const& n) {
+    m().set(lower(t), n);
+    set_lower_is_inf(t, false);
+    m().set(upper(t), n);
+    set_upper_is_inf(t, false);    
+    set_lower_is_open(t, false);
+    set_upper_is_open(t, false);
+    SASSERT(check_invariant(t));
+}
+
 template<typename C>
 bool interval_manager<C>::eq(interval const & a, interval const & b) const {
     return
diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt
index 647687b04..77c7422e5 100644
--- a/src/math/lp/CMakeLists.txt
+++ b/src/math/lp/CMakeLists.txt
@@ -28,6 +28,7 @@ z3_add_component(lp
     nla_basics_lemmas.cpp
     nla_common.cpp
     nla_core.cpp
+    nla_intervals.cpp
     nla_monotone_lemmas.cpp
     nla_order_lemmas.cpp
     nla_solver.cpp
diff --git a/src/math/lp/lp_bound_propagator.cpp b/src/math/lp/lp_bound_propagator.cpp
index afe9d4371..d8b02e45d 100644
--- a/src/math/lp/lp_bound_propagator.cpp
+++ b/src/math/lp/lp_bound_propagator.cpp
@@ -4,6 +4,7 @@
 */
 #include "math/lp/lar_solver.h"
 #include "math/lp/nla_solver.h"
+#include "math/lp/nla_intervals.h"
 namespace lp {
 
 lp_bound_propagator::lp_bound_propagator(lar_solver & ls, nla::solver* nla):