working on multiple intervals

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

src/math/dd/pdd_interval.h

@@ -21,6 +21,7 @@ Revision History:
 
 #include "math/dd/dd_pdd.h"
 #include "math/interval/dep_intervals.h"
+#include "util/scoped_ptr_vector.h"
 
 namespace dd {
 typedef dep_intervals::interval interval;
@@ -29,7 +30,7 @@ typedef dep_intervals::with_deps_t w_dep;
 class pdd_interval {
     dep_intervals& m_dep_intervals;
     std::function<void (unsigned, bool, scoped_dep_interval&)> m_var2interval;
-    std::function<void (unsigned, bool, vector<scoped_dep_interval>&)> m_var2intervals;
+    std::function<void (unsigned, bool, scoped_ptr_vector<scoped_dep_interval>&)> m_var2intervals;
 
     // retrieve intervals after distributing multiplication over addition.
     template <w_dep wd>
@@ -66,8 +67,8 @@ public:
     std::function<void (unsigned, bool, scoped_dep_interval&)>& var2interval() { return m_var2interval; } // setter
     const std::function<void (unsigned, bool, scoped_dep_interval&)>& var2interval() const { return m_var2interval; } // getter
 
-    std::function<void (unsigned, bool, vector<scoped_dep_interval>&)>& var2intervals() { return m_var2intervals; } // setter
+    std::function<void (unsigned, bool, scoped_ptr_vector<scoped_dep_interval>&)>& var2intervals() { return m_var2intervals; } // setter
-    const std::function<void (unsigned, bool, vector<scoped_dep_interval>&)>& var2intervals() const { return m_var2intervals; } // getter
+    const std::function<void (unsigned, bool, scoped_ptr_vector<scoped_dep_interval>&)>& var2intervals() const { return m_var2intervals; } // getter
 
     template <w_dep wd>
     void get_interval(pdd const& p, scoped_dep_interval& ret) {
@@ -96,7 +97,6 @@ public:
         get_interval_distributed<wd>(p, i, ret);
     }
 
-
     //
     // produce an explanation for a range using weaker bounds.
     //
@@ -121,17 +121,37 @@ public:
             m_dep_intervals.mul<dep_intervals::with_deps>(hi, a, hi_interval);
             m_dep_intervals.sub(bound, hi_interval, lo_bound);
             explain(p.lo(), lo_bound, lo_interval);
-            m_dep_intervals.add<dep_intervals::with_deps>(lo_interval, hi_interval, ret);
         }
         else { 
+            // lo_B + coeff*v : bounds
+            // v in (bounds - l_B) / coeff
+            
             get_interval<w_dep::without_deps>(p.lo(), lo_interval);
             m_dep_intervals.sub(bound, lo_interval, hi_bound);
             m_dep_intervals.div(hi_bound, p.hi().val().to_mpq(), hi_bound);
-            vector<scoped_dep_interval> as;
+            scoped_ptr_vector<scoped_dep_interval> var_intervals;
-            m_var2intervals(p.var(), true, as);
+            scoped_dep_interval var_interval(m());
-            // use hi_bound to adjust for variable bound.
+            m_var2intervals(p.var(), true, var_intervals);
+            for (auto* vip : var_intervals) {
+                auto & vi = *vip;
+                if (!m_dep_intervals.lower_is_inf(vi) && !m_dep_intervals.lower_is_inf(hi_bound) && rational(m_dep_intervals.lower(vi)) > m_dep_intervals.lower(hi_bound)) {
+                    if (m_dep_intervals.lower_is_inf(var_interval) || m_dep_intervals.lower(vi) > m_dep_intervals.lower(var_interval)) {
+                        m_dep_intervals.set_lower(var_interval, m_dep_intervals.lower(vi));
+                        m_dep_intervals.set_lower_dep(var_interval, m_dep_intervals.lower_dep(vi));                        
                     }
-        
+                }
+                if (!m_dep_intervals.upper_is_inf(vi) && !m_dep_intervals.upper_is_inf(hi_bound) && m_dep_intervals.upper(hi_bound) > m_dep_intervals.upper(vi)) {
+                    if (m_dep_intervals.upper_is_inf(var_interval) || m_dep_intervals.upper(var_interval) > m_dep_intervals.upper(vi)) {
+                        m_dep_intervals.set_upper(var_interval, m_dep_intervals.upper(vi));
+                        m_dep_intervals.set_upper_dep(var_interval, m_dep_intervals.upper_dep(vi));                        
+                    }
+                }
+            }
+            m_dep_intervals.mul(var_interval, p.hi().val().to_mpq(), hi_interval);
+            m_dep_intervals.sub(bound, hi_interval, lo_bound);            
+            explain(p.lo(), lo_bound, lo_interval);
+        }
+        m_dep_intervals.add<dep_intervals::with_deps>(lo_interval, hi_interval, ret);
     }
 };
 }

src/math/interval/dep_intervals.h

@@ -80,6 +80,8 @@ private:
         mpq const& upper(interval const& a) const { return a.m_upper; }
         mpq& lower(interval& a) { return a.m_lower; }
         mpq& upper(interval& a) { return a.m_upper; }
+        u_dependency* upper_dep(interval const & a) { return a.m_upper_dep; }
+        u_dependency* lower_dep(interval const & a) { return a.m_lower_dep; }
         bool lower_is_open(interval const& a) const { return a.m_lower_open; }
         bool upper_is_open(interval const& a) const { return a.m_upper_open; }
         bool lower_is_inf(interval const& a) const { return a.m_lower_inf; }
@@ -196,6 +198,7 @@ public:
     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); }
     void sub(const interval& a, const interval& b, interval& c) { m_imanager.sub(a, b, c); }
+    void mul(const interval& a, const mpq& b, interval& c) { m_imanager.mul(b, a, c); }
     void div(const interval& a, const mpq& b, interval& c) { m_imanager.div(a, b, c); }
 
     template <enum with_deps_t wd>
@@ -297,6 +300,18 @@ public:
         }
     }
     
+    template <enum with_deps_t wd>
+    void mul(const interval& a, const mpq& b, interval& c) {
+        if (wd == with_deps) {
+            interval_deps_combine_rule comb_rule;
+            mul(b, a, c, comb_rule);
+            combine_deps(a, comb_rule, c);
+        }
+        else {
+            mul(b, a, c);
+        }
+    }
+
     template <enum with_deps_t wd>
     void copy_upper_bound(const interval& a, interval& i) const {
         SASSERT(a.m_upper_inf == false);
@@ -359,6 +374,10 @@ public:
     mpq const& lower(interval const& a) const { return m_config.lower(a); }
     mpq const& upper(interval const& a) const { return m_config.upper(a); }
 
+    u_dependency* upper_dep(interval const & a) { return m_config.upper_dep(a); }
+    u_dependency* lower_dep(interval const & a) { return m_config.lower_dep(a); }
+
+
     bool is_empty(interval const& a) const;
     void set_interval_for_scalar(interval&, const rational&);
     template <typename T> 
@@ -441,6 +460,7 @@ private:
     void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); }
     void sub(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.sub(a, b, c, deps); }
     void div(const interval& a, const mpq& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.div(a, b, c, deps); }
+    void mul(const interval& a, const mpq& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(b, a, c, deps); }
    
     void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const {
         m_config.add_deps(a, b, deps, i);

src/math/lp/nla_core.cpp

@@ -1535,7 +1535,7 @@ void core::add_bounds() {
             //m_lar_solver.print_column_info(j, verbose_stream() << "check variable " << j << " ") << "\n";
             if (var_is_free(j)) 
                 m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));
-#if 0
+#if 1
             else if (has_lower_bound(j) && can_add_bound(j, m_lower_bounds_added)) 
                 m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::LE, get_lower_bound(j)));
             else if (has_upper_bound(j) && can_add_bound(j, m_upper_bounds_added))
@@ -1574,13 +1574,10 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
     bool run_bounded_nlsat = should_run_bounded_nlsat();
     bool run_bounds = params().arith_nl_branching();    
 
-    
-    if (l_vec.empty() && !done()) 
-        m_monomial_bounds();
-
-
     auto no_effect = [&]() { return !done() && l_vec.empty() && lits.empty(); };
     
+    if (no_effect())
+        m_monomial_bounds();
     
     {
         std::function<void(void)> check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); };
@@ -1596,14 +1593,13 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
             return l_false;
     }
                 
-    
+    if (no_effect()) 
-    if (l_vec.empty() && !done()) 
         m_basics.basic_lemma(true); 
 
-    if (l_vec.empty() && !done()) 
+    if (no_effect()) 
         m_basics.basic_lemma(false);
 
-    if (l_vec.empty() && !done())
+    if (no_effect()) 
         m_divisions.check();
     
     if (!conflict_found() && !done() && run_bounded_nlsat)

src/math/lp/nla_grobner.cpp

@@ -274,8 +274,14 @@ namespace nla {
         if (di.upper(i) >= mx)
             return false;
 
+        eval.var2intervals() = [this](lpvar j, bool deps, scoped_ptr_vector<scoped_dep_interval>& intervals) {
+            verbose_stream() << "get-intervals\n";
+            // var2intervals(j, deps, intervals);
+        };
         // TODO - relax bound dependencies to weakest that admit within interval -mx, mx.
-        eval.get_interval<dd::w_dep::with_deps>(lo, i_wd);
+        eval.explain(lo, i, i_wd);
+
+        // eval.get_interval<dd::w_dep::with_deps>(lo, i_wd);
 
         lp::lar_term lo_t;
         rational k(0);
@@ -311,6 +317,7 @@ namespace nla {
         return true;
     }
 
+
     void grobner::add_dependencies(new_lemma& lemma, const dd::solver::equation& eq) {
         lp::explanation ex;
         u_dependency_manager dm;

src/math/lp/nla_grobner.h

@@ -48,6 +48,8 @@ namespace nla {
         
         void add_dependencies(new_lemma& lemma, const dd::solver::equation& eq);
 
+        void var2intervals(lpvar j, bool deps, vector<scoped_dep_interval>& intervals);
+
         // setup
         void configure();
         void set_level2var();

src/math/lp/nla_intervals.cpp

@@ -62,7 +62,8 @@ std::ostream & intervals::print_dependencies(u_dependency* deps , std::ostream&
         if (!expl.empty()) {
             m_core->print_explanation(e, out);
             expl.clear();
-        } else {
+        }
+        else {
             out << "\nno constraints\n";
         }
     }
@@ -135,7 +136,8 @@ lp::lar_term intervals::expression_to_normalized_term(const nex_sum* e, rational
     for (const nex* c : *e) {
         if (c->is_scalar()) {
             b += c->to_scalar().value();
-        } else {
+        }
+        else {
             add_linear_to_vector(c, v);
             if (v.empty())
                 continue;
@@ -153,7 +155,8 @@ lp::lar_term intervals::expression_to_normalized_term(const nex_sum* e, rational
         for (auto& p : v) {
             t.add_monomial(p.first, p.second);
         }
-    } else {
+    }
+    else {
         for (unsigned k = 0; k < v.size(); k++) {
             auto& p = v[k];
             if (k != a_index) 
@@ -212,26 +215,23 @@ u_dependency *intervals::mk_dep(lp::constraint_index ci) {
 
 u_dependency *intervals::mk_dep(const lp::explanation& expl) {
     u_dependency * r = nullptr;
-    for (auto p : expl) {
+    for (auto p : expl) 
-        if (r == nullptr) {
-            r = m_dep_intervals.mk_leaf(p.ci());
-        } else {
         r = m_dep_intervals.mk_join(r, m_dep_intervals.mk_leaf(p.ci()));
-        }
-    }
     return r;
 }
 
 std::ostream& intervals::display(std::ostream& out, const interval& i) const {
     if (m_dep_intervals.lower_is_inf(i)) {
         out << "(-oo";
-    } else {
+    }
+    else {
         out << (m_dep_intervals.lower_is_open(i)? "(":"[") << rational(m_dep_intervals.lower(i));        
     }
     out << ",";
     if (m_dep_intervals.upper_is_inf(i)) {
         out << "oo)";
-    } else {
+    }
+    else {
         out << rational(m_dep_intervals.upper(i)) << (m_dep_intervals.upper_is_open(i)? ")":"]");         
     }
     svector<lp::constraint_index> expl;
@@ -247,7 +247,7 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const {
 }
 
 template <e_with_deps wd>
-void intervals::set_var_interval(lpvar v, interval& b) {
+void intervals::set_var_interval1(lpvar v, interval& b) {
     TRACE("nla_intervals_details", m_core->print_var(v, tout) << "\n";);
     lp::constraint_index ci;
     rational val;
@@ -274,17 +274,29 @@ void intervals::set_var_interval(lpvar v, interval& b) {
         m_dep_intervals.set_upper_is_inf(b, true);
         if (wd == e_with_deps::with_deps) b.m_upper_dep = nullptr;
     }
+}
 
+template <e_with_deps wd>
+bool intervals::set_var_interval2(lpvar v, scoped_dep_interval& b) {
     if (ls().column_corresponds_to_term(v)) {
         auto const& lt = ls().column_index_to_term(v);
+        return interval_from_lar_term<wd>(lt, b);
+    }
+    return false;
+}
+    
+template <e_with_deps wd>
+void intervals::set_var_interval(lpvar v, interval& b) {
+    set_var_interval1<wd>(v, b);
     scoped_dep_interval ti(m_dep_intervals), r(m_dep_intervals);
-        if (interval_from_lar_term<wd>(lt, ti)) {
+    if (set_var_interval2<wd>(v, ti)) {
         m_dep_intervals.intersect<wd>(b, ti, r);
         m_dep_intervals.set<wd>(b, r);
     }
-    }
 }
 
+
+    
 template <dep_intervals::with_deps_t wd>
 bool intervals::interval_from_lar_term(lp::lar_term const& t, scoped_dep_interval& i) {
     m_dep_intervals.set_value(i, rational::zero());
@@ -363,21 +375,14 @@ bool intervals::interval_of_sum_no_term(const nex_sum& e, scoped_dep_interval &
 
 // return true iff a.upper < b.lower, or a.upper == b.lower and one of these bounds is open
 bool intervals::conflict_u_l(const interval& a, const interval& b) const {
-     if (a.m_upper_inf) {
+     if (a.m_upper_inf) 
          return false;
-     }
+     if (b.m_lower_inf) 
-     if (b.m_lower_inf) {
          return false;
-     }
+     if (m_dep_intervals.num_manager().lt(a.m_upper, b.m_lower)) 
-
-     if (m_dep_intervals.num_manager().lt(a.m_upper, b.m_lower)) {
          return true;
-     }
+     if (m_dep_intervals.num_manager().gt(a.m_upper, b.m_lower)) 
-
-     if (m_dep_intervals.num_manager().gt(a.m_upper, b.m_lower)) {
          return false;
-     }
-
      return a.m_upper_open || b.m_upper_open;
 }
 
@@ -468,31 +473,24 @@ template <e_with_deps wd, typename T>
 bool intervals::interval_of_expr(const nex* e, unsigned p, scoped_dep_interval& a, const std::function<void (const T&)>& f) {
     switch (e->type()) {
     case expr_type::SCALAR:
-        {
         m_dep_intervals.set_interval_for_scalar(a, power(to_scalar(e)->value(), p));        
-        }
         break;
-    case expr_type::SUM: {
+    case expr_type::SUM: 
         if (!interval_of_sum<wd>(e->to_sum(), a, f))
             return false;
-        if (p != 1) {
+        if (p != 1) 
             to_power<wd>(a, p);
-        }
         break;
-    }
+    case expr_type::MUL: 
-    case expr_type::MUL: {
         if (!interval_of_mul<wd>(e->to_mul(), a, f))
             return false;
-        if (p != 1) {
+        if (p != 1) 
             to_power<wd>(a, p);
-        }
         break;
-    }
     case expr_type::VAR:
         set_var_interval<wd>(e->to_var().var(), a);
-        if (p != 1) {
+        if (p != 1) 
             to_power<wd>(a, p);
-        }
         break;
     default:
         TRACE("nla_intervals_details", tout << e->type() << "\n";);
@@ -507,5 +505,7 @@ lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; }
 const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; }
 
 
+
 } // end of nla namespace
 
+

src/math/lp/nla_intervals.h

@@ -52,6 +52,12 @@ public:
     template <dep_intervals::with_deps_t wd>
     void set_var_interval(lpvar v, interval& b);
 
+    template <dep_intervals::with_deps_t wd>
+    void set_var_interval1(lpvar v, interval& b);
+
+    template <dep_intervals::with_deps_t wd>
+    bool set_var_interval2(lpvar v, scoped_dep_interval& b);
+        
     template <dep_intervals::with_deps_t wd>
     bool interval_from_term(const nex& e, scoped_dep_interval& i); 
 

src/sat/smt/arith_solver.cpp

@@ -1420,8 +1420,11 @@ namespace arith {
     }
 
     void solver::assume_literals() {
-        for (auto const& ineq : m_nla_literals)
+        for (auto const& ineq : m_nla_literals) {
-            s().set_phase(mk_ineq_literal(ineq));        
+            auto lit = mk_ineq_literal(ineq);
+            ctx.mark_relevant(lit);
+            s().set_phase(lit);
+        }
     }
     
     sat::literal solver::mk_ineq_literal(nla::ineq const& ineq) {

src/smt/theory_lra.cpp

@@ -2575,17 +2575,18 @@ public:
 
     void assume_literal(nla::ineq const& i) {
         auto lit = mk_literal(i);
+        ctx().mark_as_relevant(lit);
         ctx().set_true_first_flag(lit.var());
     }
     
     final_check_status check_nla_continue() {
         m_a1 = nullptr; m_a2 = nullptr;
         lbool r = m_nla->check(m_nla_literals, m_nla_lemma_vector);
-        for (const nla::ineq& i : m_nla_literals)
-            return (assume_literal(i), FC_CONTINUE); 
 
         switch (r) {
         case l_false:
+            for (const nla::ineq& i : m_nla_literals)
+                assume_literal(i); 
             for (const nla::lemma & l : m_nla_lemma_vector) 
                 false_case_of_check_nla(l);
             return FC_CONTINUE;