work on horner's heuristic

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

src/math/lp/horner.cpp

@@ -22,19 +22,25 @@
 #include "math/lp/nla_core.h"
 
 namespace nla {
-
+typedef nla_expr<rational> nex;
 horner::horner(core * c) : common(c) {}
 
 template <typename T>
-bool horner::row_is_interesting(const T&) const {
+bool horner::row_is_interesting(const T& row) const {
-    return true;
+    for (const auto& p : row) {
+        if (c().m_to_refine.contains(p.var()))
+            return true;
+    }
+    return false;
 }
 
 template <typename T> 
 void horner::lemma_on_row(const T& row) {
     if (!row_is_interesting(row))
         return;
-    SASSERT(false);
+    nex e = create_expr_from_row(row);
+    intervals::interval inter = interval_of_expr(e);
+    check_interval_for_conflict(inter);
 }
 
 void horner::horner_lemmas() {
@@ -53,4 +59,105 @@ void horner::horner_lemmas() {
     SASSERT(false);
 }
 
+nex horner::nexvar(lpvar j) const {
+    if (!c().is_monomial_var(j))
+        return nex::var(j);
+    const monomial& m = c().emons()[j];
+    nex e(expr_type::MUL);
+    for (lpvar k : m.vars()) {
+        e.add_child(nex::var(k));
+    }
+    return e;
+}
+
+void process_var_occurences(lpvar j, std::unordered_set<lpvar>& seen, std::unordered_map<lpvar, unsigned>& occurences) {
+    if (seen.find(j) != seen.end()) return;
+    seen.insert(j);
+    auto it = occurences.find(j);
+    if (it == occurences.end())
+        occurences[j] = 1;
+    else
+        it->second ++;
+}
+
+void process_mul_occurences(const nex& e, std::unordered_set<lpvar>& seen, std::unordered_map<lpvar, unsigned>& occurences) {
+    SASSERT(e.type() == expr_type::MUL);
+    for (const auto & ce : e.children()) {
+        if (ce.type() == expr_type::SCALAR) {
+        }  else  if (ce.type() ==  expr_type::VAR) {
+            process_var_occurences(ce.var(), seen, occurences);
+        } else if (ce.type() ==  expr_type::MUL){
+            process_mul_occurences(ce, seen, occurences);
+        } else {        
+            SASSERT(false); // unexpected type
+        }
+    }
+}
+
+
+
+// j -> the number of expressions j appears in
+void horner::get_occurences_map(const nla_expr<rational>& e, std::unordered_map<lpvar, unsigned>& occurences) const {
+    SASSERT(e.type() == expr_type::SUM);
+    for (const auto & ce : e.children()) {
+        std::unordered_set<lpvar> seen;
+        if (ce.type() == expr_type::MUL) {
+            for (const auto & cce : ce.children()) {
+                if (cce.type() == expr_type::SCALAR) {
+                }  else  if (cce.type() ==  expr_type::VAR) {
+                    process_var_occurences(cce.var(), seen, occurences);
+                } else if (cce.type() == expr_type::MUL) {
+                    process_mul_occurences(cce, seen, occurences);
+                } else {
+                    TRACE("nla_cn", tout << "e = " << e << "\nce = " << ce << std::endl <<
+                          "ce type = " << ce.type() << std::endl;);
+                    
+                    SASSERT(false); // unexpected type
+                }
+            }
+        } else if (ce.type() ==  expr_type::VAR) {
+            process_var_occurences(ce.var(), seen, occurences);
+        } else {
+            SASSERT(false);
+        }
+    }
+}
+
+
+nex horner::cross_nested_of_sum(const nla_expr<rational>& e) const {
+    SASSERT(e.type() == expr_type::SUM);
+    std::unordered_map<lpvar, unsigned>  occurences;
+    get_occurences_map(e, occurences);
+    TRACE("nla_cn",
+          tout << "e = "  << e << "\noccurences ";
+          for (auto p : occurences){
+              tout << "(v"<<p.first << ", "<< p.second<<")";
+          }
+          tout << std::endl;);
+    SASSERT(false);    
+}
+
+template <typename T> nex horner::create_expr_from_row(const T& row) {
+    nex e;
+    if (row.size() > 1) {
+        e.type() = expr_type::SUM;
+        for (const auto &p : row) {
+            e.add_child(nex::mul(p.coeff(), nexvar(p.var())));
+        }
+        return cross_nested_of_sum(e);
+    }
+    if (row.size() == 1) {
+        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);
+}
+void horner::check_interval_for_conflict(const intervals::interval&) {
+    SASSERT(false);
+}
 }

src/math/lp/horner.h

@@ -20,6 +20,8 @@
 #pragma once
 
 #include "math/lp/nla_common.h"
+#include "math/lp/nla_intervals.h"
+#include "math/lp/nla_expr.h"
 
 namespace nla {
 class core;
@@ -33,6 +35,12 @@ public:
     void lemma_on_row(const T&);
     template <typename T>
     bool row_is_interesting(const T&) const;
-private:    
+    template <typename T> nla_expr<rational> create_expr_from_row(const T&);
+    intervals::interval interval_of_expr(const nla_expr<rational>& e);
+    void check_interval_for_conflict(const intervals::interval&);
+    nla_expr<rational> nexvar(lpvar j) const;
+    nla_expr<rational> cross_nested_of_sum(const nla_expr<rational>&) const;    
+    void get_occurences_map(const nla_expr<rational>& e, std::unordered_map<unsigned, lpvar>& ) const;
+
 }; // end of horner
 }

src/math/lp/int_set.h

@@ -54,6 +54,8 @@ public:
         m_data[j] = -1;
     }
 
+    int operator[](unsigned j) const { return m_index[j]; }
+    
     void resize(unsigned size) {
         m_data.resize(size, -1);
     }
@@ -61,7 +63,7 @@ public:
     void increase_size_by_one() {
         resize(m_data.size() + 1);
     }
-
+   
     unsigned data_size() const {  return m_data.size(); }
     unsigned size() const { return m_index.size();}
     bool is_empty() const { return size() == 0; }
@@ -76,6 +78,7 @@ public:
         }
         out << std::endl;
     }
-    
+    const int * begin() const { return m_index.begin(); }
+    const int * end() const { return m_index.end(); }
 };
 }

src/math/lp/nla_basics_lemmas.cpp

@@ -149,8 +149,8 @@ bool basics::basic_sign_lemma(bool derived) {
         return basic_sign_lemma_model_based();
 
     std::unordered_set<unsigned> explored;
-    for (lpvar i : c().m_to_refine){
+    for (lpvar j : c().m_to_refine){
-        if (basic_sign_lemma_on_mon(i, explored))
+        if (basic_sign_lemma_on_mon(j, explored))
             return true;
     }
     return false;

src/math/lp/nla_core.cpp

@@ -831,37 +831,6 @@ void core::collect_equivs() {
     }
 }
 
-void core::collect_equivs_of_fixed_vars() {
-    std::unordered_map<rational, svector<lpvar> > abs_map;
-    for (lpvar j = 0; j < m_lar_solver.number_of_vars(); j++) {
-        if (!var_is_fixed(j))
-            continue;
-        rational v = abs(val(j));
-        auto it = abs_map.find(v);
-        if (it == abs_map.end()) {
-            abs_map[v] = svector<lpvar>();
-            abs_map[v].push_back(j);
-        } else {
-            it->second.push_back(j);
-        }
-    }
-    for (auto p : abs_map) {
-        svector<lpvar>& v = p.second;
-        lpvar head = v[0];
-        auto c0 = m_lar_solver.get_column_upper_bound_witness(head);
-        auto c1 = m_lar_solver.get_column_lower_bound_witness(head);
-        for (unsigned k = 1; k < v.size(); k++) {
-            auto c2 = m_lar_solver.get_column_upper_bound_witness(v[k]);
-            auto c3 = m_lar_solver.get_column_lower_bound_witness(v[k]);
-            if (val(head) == val(v[k])) {
-                m_evars.merge_plus(head, v[k], eq_justification({c0, c1, c2, c3}));
-            } else {
-                SASSERT(val(head) == -val(v[k]));
-                m_evars.merge_minus(head, v[k], eq_justification({c0, c1, c2, c3}));
-            }
-        }
-    }
-}
 
 // returns true iff the term is in a form +-x-+y.
 // the sign is true iff the term is x+y, -x-y.
@@ -975,11 +944,12 @@ void core::init_search() {
 void core::init_to_refine() {
     TRACE("nla_solver", tout << "emons:" << pp_emons(*this, m_emons););
     m_to_refine.clear();
+    m_to_refine.resize(m_lar_solver.number_of_vars());
     unsigned r = random(), sz = m_emons.number_of_monomials();
     for (unsigned k = 0; k < sz; k++) {
         auto const & m = *(m_emons.begin() + (k + r)% sz);
         if (!check_monomial(m)) 
-            m_to_refine.push_back(m.var());
+            m_to_refine.insert(m.var());
     }
     
     TRACE("nla_solver", 
@@ -1333,7 +1303,7 @@ lbool core::check(vector<lemma>& l_vec) {
     }
 
     init_to_refine();
-    if (m_to_refine.empty()) {
+    if (m_to_refine.is_empty()) {
         return l_true;
     }
     init_search();

src/math/lp/nla_core.h

@@ -82,7 +82,7 @@ public:
     var_eqs<emonomials>      m_evars;
     lp::lar_solver&          m_lar_solver;
     vector<lemma> *          m_lemma_vec;
-    svector<lpvar>           m_to_refine;
+    lp::int_set               m_to_refine;
     tangents                 m_tangents;
     basics                   m_basics;
     order                    m_order;
@@ -291,8 +291,6 @@ public:
     // we look for octagon constraints here, with a left part  +-x +- y 
     void collect_equivs();
 
-    void collect_equivs_of_fixed_vars();
-
     bool is_octagon_term(const lp::lar_term& t, bool & sign, lpvar& i, lpvar &j) const;
     
     void add_equivalence_maybe(const lp::lar_term *t, lpci c0, lpci c1);

src/math/lp/nla_expr.h

@@ -19,15 +19,45 @@ Revision History:
 #pragma once
 #include "math/lp/nla_defs.h"
 namespace nla {
-enum class expr_type { SUM, MUL, VAR, SCALAR };
+enum class expr_type { SUM, MUL, VAR, SCALAR, UNDEF };
+inline std::ostream & operator<<(std::ostream& out, expr_type t) {
+    switch (t) {
+    case expr_type::SUM:
+        out << "SUM";
+        break;
+    case expr_type::MUL:
+        out << "MUL";
+        break;
+    case expr_type::VAR:
+        out << "VAR";
+        break;
+    case expr_type::SCALAR:
+        out << "SCALAR";
+        break;
+    case expr_type::UNDEF:
+        out << "UNDEF";
+        break;
+    default:
+        out << "NN";
+        break;
+    }
+    return out;
+}
 // This class is needed in horner calculation with intervals
 template <typename T>
 class nla_expr {
+    // todo: use union
     expr_type       m_type;
     lpvar           m_j;
     T             m_v; // for the scalar
     vector<nla_expr> m_children;
 public:
+    lpvar var() const { SASSERT(m_type == expr_type::VAR); return m_j; }
+    expr_type type() const { return m_type; }
+    expr_type& type() { return m_type; }
+    const vector<nla_expr>& children() const { return m_children; }
+    vector<nla_expr>& children() { return m_children; }
+    
     std::string str() const { std::stringstream ss; ss << *this; return ss.str(); }
     std::ostream & print_sum(std::ostream& out) const {
         bool first = true;
@@ -90,6 +120,7 @@ public:
             out << m_v;
             return out;
         default:
+            out << "undef";
             return out;
         }
     }
@@ -106,6 +137,11 @@ public:
     }
 
     nla_expr(expr_type t): m_type(t) {}
+    nla_expr() {
+#if Z3DEBUG
+        m_type = expr_type::UNDEF;
+#endif
+    }
     
     void add_child(const nla_expr& e) {
         SASSERT(m_type == expr_type::SUM || m_type == expr_type::MUL);
@@ -126,6 +162,21 @@ public:
         return r;
     }
 
+    static nla_expr mul(const T& v, const nla_expr & w) {
+        if (v == 1)
+            return w;
+        nla_expr r(expr_type::MUL);
+        r.add_child(scalar(v));
+        r.add_child(w);
+        return r;
+    }
+
+    static nla_expr mul(const T& v, lpvar j) {
+        if (v == 1)
+            return var(j);
+        return mul(scalar(v), var(j));
+    }
+
     static nla_expr scalar(const T& v)  {
         nla_expr r(expr_type::SCALAR);
         r.m_v = v;