From 86a086b698bac936b68ca728665a77ead58b5305 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sat, 29 Jun 2019 14:57:59 -0700
Subject: [PATCH] toward horner lemma

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/horner.cpp | 60 +++++++++++++++++++++++++++++++++++++++---
 src/math/lp/horner.h   |  8 +++---
 src/math/lp/nla_expr.h | 42 +++++++++++++++++++++++++++--
 3 files changed, 101 insertions(+), 9 deletions(-)

diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 1085b5a2a..2320aaf5d 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -39,6 +39,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;);
     intervals::interval inter = interval_of_expr(e);
     check_interval_for_conflict(inter);
 }
@@ -94,6 +95,25 @@ void process_mul_occurences(const nex& e, std::unordered_set<lpvar>& seen, std::
     }
 }
 
+unsigned horner::random_most_occured_var(std::unordered_map<lpvar, unsigned>& occurences)  {
+    unsigned max = 0;
+    unsigned ret = -1;
+    unsigned n = 0;
+    for (const auto & p : occurences) {
+        if (p.second > max) {
+            n = 0;
+            max = p.second;
+            ret = p.first;
+        } else if (p.second == max) {
+            n++;
+            if (random() % n == 0) {
+                ret = p.first;
+            }
+        } 
+    }
+    SASSERT(ret + 1);
+    return ret;
+}
 
 
 // j -> the number of expressions j appears in
@@ -123,18 +143,50 @@ void horner::get_occurences_map(const nla_expr<rational>& e, std::unordered_map<
     }
 }
 
+nex horner::split_with_var(const nex& e, lpvar j) {
+    if (!e.is_sum())
+        return e;
+    nex a, b;
+    for (const nex & ce: e.children()) {
+        if (ce.is_mul() && ce.contains(j)) {
+            a.add_child(ce / j);
+        } else {
+            b.add_child(ce);
+        }        
+    }
+    if (a.children().size() == 1)
+        return e;
+    SASSERT(a.children().size());
+    a.type() = expr_type::SUM;
+    
+    if (b.children().size() == 1) {
+        b = b.children()[0];      
+    } else if (b.children().size() > 1) {
+        b.type() = expr_type::SUM;
+    }
 
-nex horner::cross_nested_of_sum(const nla_expr<rational>& e) const {
-    SASSERT(e.type() == expr_type::SUM);
+    if (b.is_undef()) {
+        nex r(expr_type::MUL);        
+        r.add_child(nex::var(j));
+        r.add_child(a);
+        return r;
+    }
+    return nex::sum(nex::mul(a, nex::var(j)), b);    
+}
+
+nex horner::cross_nested_of_sum(const nex& e) {
+    if (!e.is_sum())
+        return e;
     std::unordered_map<lpvar, unsigned>  occurences;
     get_occurences_map(e, occurences);
+    lpvar j = random_most_occured_var(occurences);
     TRACE("nla_cn",
           tout << "e = "  << e << "\noccurences ";
           for (auto p : occurences){
               tout << "(v"<<p.first << ", "<< p.second<<")";
           }
-          tout << std::endl;);
-    SASSERT(false);    
+          tout << std::endl << "most occured = v" << j << std::endl;);
+    return split_with_var(e, j);
 }
 
 template <typename T> nex horner::create_expr_from_row(const T& row) {
diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h
index 4a6c53730..f02bd5326 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -39,8 +39,10 @@ public:
     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;
-
+    nla_expr<rational> cross_nested_of_sum(const nla_expr<rational>&);    
+    void get_occurences_map(const nla_expr<rational>& e,
+                            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);
 }; // end of horner
 }
diff --git a/src/math/lp/nla_expr.h b/src/math/lp/nla_expr.h
index ca6848943..80b623666 100644
--- a/src/math/lp/nla_expr.h
+++ b/src/math/lp/nla_expr.h
@@ -52,6 +52,10 @@ class nla_expr {
     T             m_v; // for the scalar
     vector<nla_expr> m_children;
 public:
+    bool is_sum() const { return m_type == expr_type::SUM; }
+    bool is_var() const { return m_type == expr_type::VAR; }
+    bool is_mul() const { return m_type == expr_type::MUL; }
+    bool is_undef() const { return m_type == expr_type::UNDEF; }
     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; }
@@ -136,6 +140,16 @@ public:
         }
     }
 
+    unsigned size() {
+        switch(m_type) {
+        case expr_type::SUM:
+        case expr_type::MUL:
+            return m_children.size();
+        
+        default:
+            return 1;
+        }
+    }
     nla_expr(expr_type t): m_type(t) {}
     nla_expr() {
 #if Z3DEBUG
@@ -144,7 +158,6 @@ public:
     }
     
     void add_child(const nla_expr& e) {
-        SASSERT(m_type == expr_type::SUM || m_type == expr_type::MUL);
         m_children.push_back(e);
     }
 
@@ -188,9 +201,34 @@ public:
         r.m_j = j;
         return r;
     }
-    
+
+    bool contains(lpvar j) const {
+        if (is_var())
+            return m_j == j;
+        if (is_mul()) {
+            for (const nla_expr<T>& c : children()) {
+                if (c.is_var() && c.var() == j) return true;
+            }
+        }
+        return false;
+    }
     
 };
+template <typename T> 
+nla_expr<T> operator/(const nla_expr<T>& a, lpvar j) {
+    SASSERT(a.is_mul());
+    nla_expr<T> b;
+    for (const nla_expr<T>& c : a.children()) {
+        if (c.is_var() && c.var() == j) continue;
+        b.add_child(c);
+    }
+    if (b.children().size() > 1) {
+        b.type() = expr_type::MUL;
+    } else {
+        b = b.children()[0];
+    }
+    return b;
+}
 template <typename T>
 std::ostream& operator<<(std::ostream& out, const nla_expr<T>& e ) {
     return e.print(out);