outline for monomial bound propagation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/interval/dep_intervals.cpp

@@ -122,4 +122,25 @@ bool dep_intervals::is_empty(interval const& a) const {
     return false;
 }
 
+bool dep_intervals::is_above(const interval& i, const rational& r) const {
+    if (lower_is_inf(i))
+        return false;
+    if (m_num_manager.lt(lower(i), r.to_mpq()))
+        return false;
+    if (m_num_manager.eq(lower(i), r.to_mpq()) && !m_config.lower_is_open(i))
+        return false;
+    return true;
+}
+
+bool dep_intervals::is_below(const interval& i, const rational& r) const {
+    if (upper_is_inf(i))
+        return false;
+    if (m_num_manager.lt(upper(i), r.to_mpq()))
+        return false;
+    if (m_num_manager.eq(upper(i), r.to_mpq()) && !m_config.upper_is_open(i))
+        return false;
+    return true;
+}
+
+
 template class interval_manager<dep_intervals::im_config>;

src/math/interval/dep_intervals.h

@@ -97,6 +97,8 @@ private:
         void set_upper_is_open(interval& a, bool v) const { a.m_upper_open = v; }
         void set_lower_is_inf(interval& a, bool v) const { a.m_lower_inf = v; }
         void set_upper_is_inf(interval& a, bool v) const { a.m_upper_inf = v; }
+        void set_lower_dep(interval& a, u_dependency* d) const { a.m_lower_dep = d; }
+        void set_upper_dep(interval& a, u_dependency* d) const { a.m_upper_dep = d; }
 
         // Reference to numeral manager
         numeral_manager& m() const { return m_manager; }
@@ -190,11 +192,19 @@ public:
     void set_lower_is_inf(interval& a, bool inf) { m_config.set_lower_is_inf(a, inf); }
     void set_upper_is_open(interval& a, bool strict) { m_config.set_upper_is_open(a, strict); }
     void set_upper_is_inf(interval& a, bool inf) { m_config.set_upper_is_inf(a, inf); }
+    void set_lower_dep(interval& a, u_dependency* d) const { m_config.set_lower_dep(a, d); }
+    void set_upper_dep(interval& a, u_dependency* d) const { m_config.set_upper_dep(a, d); }
     bool is_zero(const interval& a) const { return m_config.is_zero(a); }
     bool upper_is_inf(const interval& a) const { return m_config.upper_is_inf(a); }
     bool lower_is_inf(const interval& a) const { return m_config.lower_is_inf(a); }
     bool lower_is_open(const interval& a) const { return m_config.lower_is_open(a); }
     bool upper_is_open(const interval& a) const { return m_config.upper_is_open(a); }
+    template <typename T>
+    void get_upper_dep(const interval& a, T& expl) { linearize(a.m_upper_dep, expl); }
+    template <typename T>
+    void get_lower_dep(const interval& a, T& expl) { linearize(a.m_lower_dep, expl); }
+    bool is_above(const interval& a, const rational& r) const;
+    bool is_below(const interval& a, const rational& r) const;    
     void add(const rational& r, interval& a) const;
     void mul(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); }
     void add(const interval& a, const interval& b, interval& c) { m_imanager.add(a, b, c); }

src/math/lp/CMakeLists.txt

@@ -30,6 +30,7 @@ z3_add_component(lp
     lp_utils.cpp
     matrix.cpp
     mon_eq.cpp
+    monomial_bounds.cpp
     nex_creator.cpp
     nla_basics_lemmas.cpp
     nla_common.cpp

src/math/lp/monomial_bounds.cpp

@@ -0,0 +1,82 @@
+/*++
+  Copyright (c) 2020 Microsoft Corporation
+
+  Author:
+  Nikolaj Bjorner (nbjorner)
+  Lev Nachmanson (levnach)
+
+  --*/
+#pragma once
+
+#include "math/lp/monomial_bounds.h"
+#include "math/lp/nla_core.h"
+#include "math/lp/nla_intervals.h"
+
+namespace nla {
+
+    monomial_bounds::monomial_bounds(core* c):common(c) {}
+
+    bool monomial_bounds::operator()() {
+        bool propagated = false;
+        for (lpvar v : c().m_to_refine) {
+            monic const& m = c().emons()[v];
+            if (propagate_up(m))
+                propagated = true;
+        }
+        return propagated;
+    }
+
+    bool monomial_bounds::propagate_up(monic const& m) {
+        auto & intervals = c().m_intervals;
+        auto & dep_intervals = intervals.get_dep_intervals();
+        scoped_dep_interval product(dep_intervals), di(dep_intervals);
+        lpvar v = m.vars()[0];
+        var2interval(v, product);
+        for (unsigned i = 1; i < m.size(); ++i) {
+            var2interval(m.vars()[i], di);
+            dep_intervals.mul(product, di, product);
+        }
+        if (dep_intervals.is_below(product, c().val(m.var()))) {
+            lp::explanation ex;
+            dep_intervals.get_upper_dep(product, ex);
+            new_lemma lemma(c(), "propagate up - upper bound of product is below value");
+            lemma &= ex;
+            auto const& upper = dep_intervals.upper(product);
+            auto cmp = dep_intervals.upper_is_open(product) ? llc::LT : llc::LE;
+            lemma |= ineq(m.var(), cmp, upper); 
+            return true;
+        }
+        else if (dep_intervals.is_above(product, c().val(m.var()))) {
+            lp::explanation ex;
+            dep_intervals.get_lower_dep(product, ex);
+            new_lemma lemma(c(), "propagate up - lower bound of product is above value");
+            lemma &= ex;
+            auto const& lower = dep_intervals.upper(product);
+            auto cmp = dep_intervals.lower_is_open(product) ? llc::GT : llc::GE;
+            lemma |= ineq(m.var(), cmp, lower); 
+            return true;
+        }
+        else {
+            return false;
+        }
+    }
+
+    void monomial_bounds::var2interval(lpvar v, scoped_dep_interval& i) {
+        auto & intervals = c().m_intervals;
+        auto & dep_intervals = intervals.get_dep_intervals();
+        lp::constraint_index ci;
+        rational bound;
+        bool is_strict;
+        if (c().has_lower_bound(v, ci, bound, is_strict)) {
+            dep_intervals.set_lower_is_open(i, is_strict);
+            dep_intervals.set_lower(i, bound);
+            dep_intervals.set_lower_dep(i, dep_intervals.mk_leaf(ci));
+        }
+        if (c().has_upper_bound(v, ci, bound, is_strict)) {
+            dep_intervals.set_upper_is_open(i, is_strict);
+            dep_intervals.set_upper(i, bound);
+            dep_intervals.set_upper_dep(i, dep_intervals.mk_leaf(ci));            
+        }
+    }
+}
+

src/math/lp/monomial_bounds.h

@@ -0,0 +1,27 @@
+/*++
+  Copyright (c) 2020 Microsoft Corporation
+
+  Author:
+  Nikolaj Bjorner (nbjorner)
+  Lev Nachmanson (levnach)
+
+  --*/
+#pragma once
+
+#include "math/lp/nla_common.h"
+#include "math/lp/nla_intervals.h"
+#include "math/lp/nex.h"
+#include "math/lp/cross_nested.h"
+#include "math/lp/u_set.h"
+
+namespace nla {
+    class core;
+
+    class monomial_bounds : common {
+        void var2interval(lpvar v, scoped_dep_interval& i);
+        bool propagate_up(monic const& m);
+    public:
+        monomial_bounds(core* core);
+        bool operator()();
+    }; 
+}

src/math/lp/nla_core.h

@@ -321,6 +321,13 @@ public:
     }
     const rational& get_upper_bound(unsigned j) const;
     const rational& get_lower_bound(unsigned j) const;    
+    bool has_lower_bound(lp::var_index var, lp::constraint_index& ci, lp::mpq& value, bool& is_strict) const { 
+        return m_lar_solver.has_lower_bound(var, ci, value, is_strict); 
+    }
+    bool has_upper_bound(lp::var_index var, lp::constraint_index& ci, lp::mpq& value, bool& is_strict) const {
+        return m_lar_solver.has_upper_bound(var, ci, value, is_strict);
+    }
+
     
     bool zero_is_an_inner_point_of_bounds(lpvar j) const;    
     bool var_is_int(lpvar j) const { return m_lar_solver.column_is_int(j); }