save

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/horner.cpp

@@ -23,7 +23,8 @@
 
 namespace nla {
 typedef nla_expr<rational> nex;
-horner::horner(core * c) : common(c) {}
+typedef intervals::interval interv;
+horner::horner(core * c) : common(c), m_intervals(c->reslim()) {}
 
 template <typename T>
 bool horner::row_is_interesting(const T& row) const {
@@ -39,7 +40,7 @@ void horner::lemma_on_row(const T& row) {
     if (!row_is_interesting(row))
         return;
     nex e = create_expr_from_row(row);
-    TRACE("nla_cn", tout << "cn e = " << e << std::endl;);
+    TRACE("nla_cn", tout << "cross nested e = " << e << std::endl;);
     intervals::interval inter = interval_of_expr(e);
     check_interval_for_conflict(inter);
 }
@@ -95,6 +96,7 @@ void process_mul_occurences(const nex& e, std::unordered_set<lpvar>& seen, std::
     }
 }
 
+// return a valid j if some variable appears more than once
 unsigned horner::random_most_occured_var(std::unordered_map<lpvar, unsigned>& occurences)  {
     unsigned max = 0;
     unsigned ret = -1;
@@ -111,6 +113,8 @@ unsigned horner::random_most_occured_var(std::unordered_map<lpvar, unsigned>& oc
             }
         } 
     }
+    if (max <= 1)
+        return -1;
     SASSERT(ret + 1);
     return ret;
 }
@@ -166,12 +170,13 @@ nex horner::split_with_var(const nex& e, lpvar j) {
     }
 
     if (b.is_undef()) {
+        SASSERT(b.children().size() == 0);
         nex r(expr_type::MUL);        
         r.add_child(nex::var(j));
-        r.add_child(a);
+        r.add_child(cross_nested_of_sum(a));
         return r;
     }
-    return nex::sum(nex::mul(a, nex::var(j)), b);    
+    return nex::sum(nex::mul(cross_nested_of_sum(a), nex::var(j)), b);    
 }
 
 nex horner::cross_nested_of_sum(const nex& e) {
@@ -180,6 +185,7 @@ nex horner::cross_nested_of_sum(const nex& e) {
     std::unordered_map<lpvar, unsigned>  occurences;
     get_occurences_map(e, occurences);
     lpvar j = random_most_occured_var(occurences);
+    if (j + 1 == 0) return e;
     TRACE("nla_cn",
           tout << "e = "  << e << "\noccurences ";
           for (auto p : occurences){
@@ -202,13 +208,53 @@ template <typename T> nex horner::create_expr_from_row(const T& row) {
         const auto &p  = *row.begin();
         return nex::mul(p.coeff(), nexvar(p.var()));
     }
-    
     SASSERT(false);
 }
 intervals::interval horner::interval_of_expr(const nex& e) {
-    
-    SASSERT(false);
+    interv a;
+    switch (e.type()) {
+    case expr_type::SCALAR:
+        m_intervals.set_lower(a, e.value());
+        m_intervals.set_upper(a, e.value());
+        return a;
+    case expr_type::SUM:
+        return interval_of_sum(e.children());
+    case expr_type::MUL:
+        return interval_of_mul(e.children());
+    case expr_type::VAR:
+        return interval_of_var(e.var());                               
+    default:
+        TRACE("nla_cn", tout << e.type() << "\n";);
+        SASSERT(false);
+        return e;
+    }
 }
+
+void horner::set_var_interval(lpvar v, interv& b) {
+    const auto& ls = c().m_lar_solver;
+    lp::constraint_index ci;
+    rational val;
+    bool is_strict;
+    if (ls.has_lower_bound(v, ci, val, is_strict)) {            
+        m_intervals.set_lower(b, val);
+        m_intervals.set_lower_is_open(b, is_strict);
+        m_intervals.set_lower_is_inf(b, false);
+    }
+    else {
+        m_intervals.set_lower_is_open(b, true);
+        m_intervals.set_lower_is_inf(b, true);
+    }
+    if (ls.has_upper_bound(v, ci, val, is_strict)) {
+        m_intervals.set_upper(b, val);
+        m_intervals.set_upper_is_open(b, is_strict);
+        m_intervals.set_upper_is_inf(b, false);
+    }
+    else {
+        m_intervals.set_upper_is_open(b, true);
+        m_intervals.set_upper_is_inf(b, true);
+    }
+}
+
 void horner::check_interval_for_conflict(const intervals::interval&) {
     SASSERT(false);
 }

src/math/lp/horner.h

@@ -28,7 +28,9 @@ class core;
 
 
 class horner : common {   
+    intervals m_intervals;
 public:
+    
     horner(core *core);
     void horner_lemmas();
     template <typename T> // T has an iterator of (coeff(), var())
@@ -44,5 +46,6 @@ public:
                             std::unordered_map<unsigned, lpvar>& ) const;
     unsigned random_most_occured_var(std::unordered_map<lpvar, unsigned>& occurences);
     nla_expr<rational> split_with_var(const nla_expr<rational> &, lpvar);
+    void set_var_interval(lpvar j, intervals::interval&);
 }; // end of horner
 }

src/math/lp/nla_core.cpp

@@ -30,7 +30,9 @@ core::core(lp::lar_solver& s, reslimit & lim) :
     m_order(this),
     m_monotone(this),
     m_horner(this),
-    m_emons(m_evars) {}
+    m_emons(m_evars),
+    m_reslim(lim)
+{}
     
 bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const {
     switch(cmp) {

src/math/lp/nla_core.h

@@ -93,6 +93,8 @@ private:
     emonomials               m_emons;
     svector<lpvar>           m_add_buffer;
 public:
+    reslimit                   m_reslim;
+    reslimit &               reslim() { return m_reslim; }  
     emonomials& emons() { return m_emons; }
     const emonomials& emons() const { return m_emons; }
     // constructor

src/math/lp/nla_expr.h

@@ -61,7 +61,7 @@ public:
     expr_type& type() { return m_type; }
     const vector<nla_expr>& children() const { return m_children; }
     vector<nla_expr>& children() { return m_children; }
-    
+    const T& value() const { SASSERT(m_type == expr_type::SCALAR); return m_v; }
     std::string str() const { std::stringstream ss; ss << *this; return ss.str(); }
     std::ostream & print_sum(std::ostream& out) const {
         bool first = true;

src/math/lp/nla_intervals.cpp

@@ -3,19 +3,7 @@
 #include "math/lp/nla_intervals.h"
 
 namespace nla {
-
-bool intervals::get_lemmas() {
-    m_region.reset();
-    bool ret = false;
-    for (auto const& k : c().m_to_refine) {
-        if (get_lemma(c().emons()[k])) {
-            ret = true;
-        }
-        if (c().done())
-            break;
-    }
-    return ret;
-}
+/*
 // create a product of interval signs together with the depencies
 intervals::interval intervals::mul_signs_with_deps(const svector<lpvar>& vars) const {
     interval a, b, c;
@@ -32,102 +20,6 @@ intervals::interval intervals::mul_signs_with_deps(const svector<lpvar>& vars) c
     return a;    
 }
 
-void intervals::get_lemma_for_zero_interval(monomial const& m) {
-    if (val(m).is_zero()) return;
-    interval signs_a = mul_signs_with_deps(m.vars());
-    add_empty_lemma();
-    svector<lp::constraint_index> expl;
-    m_dep_manager.linearize(signs_a.m_lower_dep, expl);
-    TRACE("nla_solver", print_vector(expl, tout) << "\n";);
-    _().current_expl().add_expl(expl);
-    mk_ineq(m.var(), llc::EQ);
-    TRACE("nla_solver", _().print_lemma(tout); );
-}
-
-bool intervals::get_lemma_for_lower(const monomial& m, const interval& a) {
-    if (m_vars_pushed_up[m.var()] > 10)
-        return false;
-    lp::impq lb(rational(a.m_lower));
-    if (m_config.lower_is_open(a))
-        lb.y = 1;
-
-    lp::impq v(val(m.var()));        
-    if (v < lb) {
-        m_vars_pushed_up[m.var()] = m_vars_pushed_up[m.var()] + 1;
-        interval signs_a = mul_signs_with_deps(m.vars());
-        add_empty_lemma();
-        svector<lp::constraint_index> expl;
-        m_dep_manager.linearize(signs_a.m_lower_dep, expl); 
-        _().current_expl().add_expl(expl);
-        llc cmp = m_config.lower_is_open(a)? llc::GT: llc::GE;
-        mk_ineq(m.var(), cmp,  lb.x);
-        TRACE("nla_solver", _().print_lemma(tout); );
-        return true;
-    }
-    return false;
-}
-
-bool intervals::get_lemma_for_upper(const monomial& m, const interval& a) {
-    if (m_vars_pushed_down[m.var()] > 10)
-        return false;
-    lp::impq ub(rational(a.m_upper));
-    if (m_config.upper_is_open(a))
-        ub.y = 1;
-    lp::impq v(val(m.var()));
-    if (v > ub) {
-        m_vars_pushed_down[m.var()] = m_vars_pushed_down[m.var()] + 1;
-        interval signs_a = mul_signs_with_deps(m.vars());
-        add_empty_lemma();
-        svector<lp::constraint_index> expl;
-        m_dep_manager.linearize(signs_a.m_upper_dep, expl); 
-        _().current_expl().add_expl(expl);
-        llc cmp = m_config.upper_is_open(a)? llc::LT: llc::LE;
-        mk_ineq(m.var(), cmp,  ub.x);
-        TRACE("nla_solver", _().print_lemma(tout); );
-        return true;
-    }
-    return false;
-}
-bool intervals::get_lemma(monomial const& m) {
-    interval  b, c, d;
-    interval a = mul(m.vars());
-    if (m_imanager.is_zero(a)) {
-        get_lemma_for_zero_interval(m);
-        return true;
-    }
-    if (!m_imanager.lower_is_inf(a)) {
-        return get_lemma_for_lower(m, a);
-    }
-
-    if (!m_imanager.upper_is_inf(a)) {
-        return get_lemma_for_upper(m, a);
-    }
-    return false;
-} 
-void intervals::set_var_interval(lpvar v, interval& b) const {
-    lp::constraint_index ci;
-    rational val;
-    bool is_strict;
-    if (ls().has_lower_bound(v, ci, val, is_strict)) {            
-        m_config.set_lower(b, val);
-        m_config.set_lower_is_open(b, is_strict);
-        m_config.set_lower_is_inf(b, false);
-    }
-    else {
-        m_config.set_lower_is_open(b, true);
-        m_config.set_lower_is_inf(b, true);
-    }
-    if (ls().has_upper_bound(v, ci, val, is_strict)) {
-        m_config.set_upper(b, val);
-        m_config.set_upper_is_open(b, is_strict);
-        m_config.set_upper_is_inf(b, false);
-    }
-    else {
-        m_config.set_upper_is_open(b, true);
-        m_config.set_upper_is_inf(b, true);
-    }
-}
-
 rational sign(const rational& v) { return v.is_zero()? v : (rational(v.is_pos()? 1 : -1)); }
 
 void intervals::set_var_interval_signs(lpvar v, interval& b) const {
@@ -186,27 +78,7 @@ intervals::ci_dependency *intervals::mk_dep(lp::constraint_index ci) const {
     return m_dep_manager.mk_leaf(ci);
 }
     
-lp::impq intervals::get_upper_bound_of_monomial(lpvar j) const {
-    const monomial& m = m_core->emons()[j];
-    interval a = mul(m.vars());
-    SASSERT(!m_imanager.upper_is_inf(a));
-    auto r = lp::impq(a.m_upper);
-    if (a.m_upper_open)
-        r.y = -1;
-    TRACE("nla_intervals_detail", m_core->print_monomial_with_vars(m, tout) << "upper = " << r << "\n";);
-    return r;
-}
-lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const {
-    const monomial& m = m_core->emons()[j];
-    interval a = mul(m.vars());
-    SASSERT(!a.m_lower_inf);    
-    auto r = lp::impq(a.m_lower);
-    if (a.m_lower_open)
-        r.y = 1;
-    TRACE("nla_intervals_detail", m_core->print_monomial_with_vars(m, tout) << "lower = " << r << "\n";);
-    return r;
-}
-
+*/
 std::ostream& intervals::display(std::ostream& out, const interval& i) const {
     if (m_imanager.lower_is_inf(i)) {
         out << "(-oo";
@@ -222,7 +94,7 @@ std::ostream& intervals::display(std::ostream& out, const interval& i) const {
     return out;
 }
 
-
+/*
 intervals::interval intervals::mul(const svector<lpvar>& vars) const {
     interval a;
     m_imanager.set(a, mpq(1));
@@ -260,55 +132,7 @@ bool intervals::product_has_upper_bound(int sign, const svector<lpvar>& vars) co
     SASSERT(sign == 1 || sign == -1);
     return sign == 1 ? !m_imanager.upper_is_inf(a) : !m_imanager.lower_is_inf(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());
-}
-lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; }
-
-const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; }
-
-std::ostream& intervals::print_explanations(const svector<lp::constraint_index> &expl , std::ostream& out) const {
-    out << "interv expl:\n ";
-    for (auto ci : expl)
-        m_core->m_lar_solver.print_constraint_indices_only(ci, out);
-    return out;
-}
-
-void intervals::get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const {
-    interval a = mul_signs_with_deps(m_core->emons()[j].vars());
-    m_dep_manager.linearize(a.m_upper_dep, expl);
-    TRACE("nla_intervals", print_explanations(expl, tout););
-}
-void intervals::get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const{
-    interval a = mul_signs_with_deps(m_core->emons()[j].vars());
-    m_dep_manager.linearize(a.m_lower_dep, expl);    
-    TRACE("nla_intervals", print_explanations(expl, tout););
-    //    return m_intervals.get_explanation_of_lower_bound_for_monomial(j, expl ) 
-}
-void intervals::push() {
-    m_vars_pushed_up.push();
-    m_vars_pushed_down.push();
-}
-void intervals::pop(unsigned k) {
-    m_vars_pushed_up.pop(k);
-    m_vars_pushed_down.pop(k);
-}
-
-void intervals::init() {
-    SASSERT(m_vars_pushed_down.size() == m_vars_pushed_up.size());
-    unsigned n = c().m_lar_solver.number_of_vars();
-    while (m_vars_pushed_up.size() < n) {
-        m_vars_pushed_up.push_back(0);
-        m_vars_pushed_down.push_back(0);
-    }
-}
+*/
 }
 
 // instantiate the template

src/math/lp/nla_intervals.h

@@ -20,19 +20,12 @@
 #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"
 
 
 namespace nla {
-class core;
-
-class intervals : common {
-    // fields to throttle the propagation on intervals
-    lp::stacked_vector<unsigned> m_vars_pushed_up;
-    lp::stacked_vector<unsigned> m_vars_pushed_down;
 
+class intervals {
     class ci_value_manager {
     public:
         void inc_ref(lp::constraint_index const & v) {
@@ -93,8 +86,8 @@ class intervals : common {
             
         // Getters
         mpq const & lower(interval const & a) const { return a.m_lower; }
-        mpq const & upper(interval const & a) const { return a.m_upper; }
         mpq & lower(interval & a) { return a.m_lower; }
+        mpq const & upper(interval const & a) const { return a.m_upper; }
         mpq & upper(interval & a) { return a.m_upper; }
         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; }
@@ -156,36 +149,32 @@ private:
 
     ci_dependency* mk_dep(lp::constraint_index ci) const;
 
-    lp::lar_solver& ls();
-    const lp::lar_solver& ls() const;
 public:
-    intervals(core* c, reslimit& lim) :
-        common(c),
+    intervals(reslimit& lim) :
         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))
     {}
-    bool get_lemmas();
-    bool get_lemma(monomial const& m);
-    void get_lemma_for_zero_interval(monomial const& m);
-    bool get_lemma_for_lower(monomial const& m, const interval& );
-    bool get_lemma_for_upper(monomial const& m, const interval &);
     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;
     interval mul(const svector<lpvar>&) const;
+    
     interval mul_signs(const svector<lpvar>&) const;
     interval mul_signs_with_deps(const svector<lpvar>&) const;
     void get_explanation_of_upper_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
     void get_explanation_of_lower_bound_for_monomial(lpvar j, svector<lp::constraint_index>& expl) const;
     std::ostream& print_explanations(const svector<lp::constraint_index> &, std::ostream&) const;
-    void push();
-    void pop(unsigned k);
-    void init();
     std::ostream& display(std::ostream& out, const intervals::interval& i) const;
+    void set_lower(interval & a, rational const & n) const { m_config.set_lower(a, n.to_mpq()); }
+    void set_upper(interval & a, rational const & n) const { m_config.set_upper(a, n.to_mpq()); }
+    void set_lower_is_open(interval & a, bool strict) { m_config.set_lower_is_open(a, strict); }
+    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); }
 };
 
 } // end of namespace nla