From a4ad71bf3338c91fbf9df1ce180e5dc064e4a27c Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 5 Jun 2019 20:40:51 -0700
Subject: [PATCH] hook up nla_intervals
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/lp/nla_core.cpp | 15 ------------
src/math/lp/nla_core.h | 4 ----
src/math/lp/nla_intervals.cpp | 45 ++++++++++++++++++++++++++---------
src/math/lp/nla_intervals.h | 14 +++++++----
src/math/lp/nla_solver.cpp | 16 ++++++-------
src/math/lp/nla_solver.h | 3 +++
6 files changed, 54 insertions(+), 43 deletions(-)
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 3a3fb8b6e..16afe48ad 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1331,21 +1331,6 @@ lbool core::test_check(
return check(l);
}
-lp::impq core::get_upper_bound_of_monomial(lpvar j) const {
- SASSERT(false);
-}
-
-lp::impq core::get_lower_bound_of_monomial(lpvar j) const {
- SASSERT(false);
-}
-
-bool core::monomial_has_lower_bound(lpvar j) const {
- SASSERT(false);
-}
-
-bool core::monomial_has_upper_bound(lpvar j) const {
- SASSERT(false);
-}
} // end of nla
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 06f4871b7..2c9f346c3 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -338,10 +338,6 @@ public:
lbool test_check(vector<lemma>& l);
lpvar map_to_root(lpvar) const;
- lp::impq get_upper_bound_of_monomial(lpvar j) const;
- lp::impq get_lower_bound_of_monomial(lpvar j) const;
- bool monomial_has_lower_bound(lpvar j) const;
- bool monomial_has_upper_bound(lpvar j) const;
}; // end of core
struct pp_mon {
diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp
index 14d683fb5..be3674c66 100644
--- a/src/math/lp/nla_intervals.cpp
+++ b/src/math/lp/nla_intervals.cpp
@@ -6,17 +6,17 @@
namespace nla {
bool intervals::check() {
- m_region.reset();
- for (auto const& m : c().emons()) {
- if (!check(m)) {
- return false;
- }
- }
- for (auto const& t : m_solver.terms()) {
- if (!check(*t)) {
- return false;
- }
- }
+ // m_region.reset();
+ // for (auto const& m : m_core->emons()) {
+ // if (!check(m)) {
+ // return false;
+ // }
+ // }
+ // for (auto const& t : m_solver.terms()) {
+ // if (!check(*t)) {
+ // return false;
+ // }
+ // }
return true;
}
@@ -104,4 +104,27 @@ namespace nla {
// convert term into factors for improved precision
return true;
}
+
+lp::impq intervals::get_upper_bound_of_monomial(lpvar j) const {
+ SASSERT(false);
+}
+
+lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const {
+ SASSERT(false);
+}
+
+bool intervals::product_has_upper_bound(int sign, const svector<lpvar>&) const {
+ interval a;
+
+}
+
+bool intervals::monomial_has_lower_bound(lpvar j) const {
+ const monomial& m = m_core->emons()[j];
+ return product_has_upper_bound(1, m.vars());
+}
+
+bool intervals::monomial_has_upper_bound(lpvar j) const {
+ const monomial& m = m_core->emons()[j];
+ return product_has_upper_bound(-1, m.vars());
+}
}
diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h
index 7213adba8..8602a2bfe 100644
--- a/src/math/lp/nla_intervals.h
+++ b/src/math/lp/nla_intervals.h
@@ -27,8 +27,8 @@
namespace nla {
class core;
- class intervals : common {
-
+ class intervals {
+ core * m_core;
class ci_value_manager {
public:
void inc_ref(lp::constraint_index const & v) {
@@ -138,7 +138,7 @@ namespace nla {
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,8 +151,12 @@ namespace nla {
bool check(lp::lar_term const& t);
public:
- intervals(core* c);
+ intervals(core* c) : m_core(c) {}
bool check();
+ bool monomial_has_lower_bound(lpvar j) const;
+ bool monomial_has_upper_bound(lpvar j) const;
+ bool product_has_upper_bound(int sign, const svector<lpvar>&) const;
+ lp::impq get_upper_bound_of_monomial(lpvar j) const;
+ lp::impq get_lower_bound_of_monomial(lpvar j) const;
};
-
} // end of namespace nla
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index 8665d1612..cde83ea8a 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -24,6 +24,7 @@
#include "math/lp/var_eqs.h"
#include "math/lp/factorization.h"
#include "math/lp/nla_solver.h"
+#include "math/lp/nla_intervals.h"
namespace nla {
// returns the monomial index
@@ -54,28 +55,27 @@ void solver::pop(unsigned n) {
}
-solver::solver(lp::lar_solver& s) {
- m_core = alloc(core, s);
+solver::solver(lp::lar_solver& s): m_core(alloc(core, s)), m_intervals(m_core) {
}
solver::~solver() {
dealloc(m_core);
}
lp::impq solver::get_upper_bound(lpvar j) const {
- SASSERT(is_monomial_var(j) && m_core->monomial_has_upper_bound(j));
- return m_core->get_upper_bound_of_monomial(j);
+ SASSERT(is_monomial_var(j) && m_intervals.monomial_has_upper_bound(j));
+ return m_intervals.get_upper_bound_of_monomial(j);
}
lp::impq solver::get_lower_bound(lpvar j) const {
- SASSERT(is_monomial_var(j) && m_core->monomial_has_lower_bound(j));
- return m_core->get_lower_bound_of_monomial(j);
+ SASSERT(is_monomial_var(j) && m_intervals.monomial_has_lower_bound(j));
+ return m_intervals.get_lower_bound_of_monomial(j);
}
bool solver::monomial_has_lower_bound(lpvar j) const {
- return m_core->monomial_has_lower_bound(j);
+ return m_intervals.monomial_has_lower_bound(j);
}
bool solver::monomial_has_upper_bound(lpvar j) const {
- return m_core->monomial_has_upper_bound(j);
+ return m_intervals.monomial_has_upper_bound(j);
}
}
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index 292298742..3672ca158 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -26,11 +26,14 @@ Revision History:
#include "math/lp/lar_solver.h"
#include "math/lp/monomial.h"
#include "math/lp/nla_core.h"
+#include "math/lp/nla_intervals.h"
+
namespace nla {
// nonlinear integer incremental linear solver
class solver {
core* m_core;
+ intervals m_intervals;
public:
void add_monomial(lpvar v, unsigned sz, lpvar const* vs);