From 81a9edae7ec30dc16755505b6a54be382ef04fcd Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 21 Aug 2019 10:31:13 -0700
Subject: [PATCH] simplify more aggressively in horner scheme, imlement
 is_linear

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/cross_nested.h | 11 +++++------
 src/math/lp/horner.cpp     | 19 +++++++++++++++++--
 src/math/lp/horner.h       |  1 +
 src/math/lp/nex.h          | 18 +++++++++++++++++-
 4 files changed, 40 insertions(+), 9 deletions(-)

diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index 339bdc860..79c80b283 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -59,6 +59,8 @@ public:
 
     
     void run(nex *e) {
+        TRACE("nla_cn", tout << *e << "\n";);
+        SASSERT(e->is_simplified());
         m_e = e;
 #ifdef Z3DEBUG
         //        m_e_clone = clone(m_e);
@@ -503,13 +505,10 @@ public:
         }
     }
 
-    void update_front_with_split_with_non_empty_b(nex* &e, lpvar j, vector<nex**> & front, nex* a, nex* b) {
-
-        SASSERT(a->is_sum());
-        
+    void update_front_with_split_with_non_empty_b(nex* &e, lpvar j, vector<nex**> & front, nex_sum* a, nex* b) {
         TRACE("nla_cn_details", tout << "b = " << *b << "\n";);
         e = mk_sum(mk_mul(mk_var(j), a), b); // e = j*a + b
-        if (!to_sum(a)->is_linear()) {
+        if (!a->is_linear()) {
             nex **ptr_to_a = &(to_mul(to_sum(e)->children()[0]))->children()[1];
             push_to_front(front, ptr_to_a);
         }
@@ -520,7 +519,7 @@ public:
         }
     }
     
-   void update_front_with_split(nex* & e, lpvar j, vector<nex**> & front, nex* a, nex* b) {
+   void update_front_with_split(nex* & e, lpvar j, vector<nex**> & front, nex_sum* a, nex* b) {
         if (b == nullptr) {
             e = mk_mul(mk_var(j), a);
             if (!to_sum(a)->is_linear())
diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 5c842dd78..133642cdc 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -133,6 +133,20 @@ nex * horner::nexvar(lpvar j, cross_nested& cn) const {
     return e;
 }
 
+nex * horner::nexvar(const rational & coeff, lpvar j, cross_nested& cn) const {
+    // todo: consider deepen the recursion
+    if (!c().is_monomial_var(j))
+        return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j));
+    const monomial& m = c().emons()[j];
+    nex_mul * e = cn.mk_mul(cn.mk_scalar(coeff));
+    for (lpvar k : m.vars()) {
+        e->add_child(cn.mk_var(k));
+        CTRACE("nla_horner", c().is_monomial_var(k), c().print_var(k, tout) << "\n";);
+    }
+    return e;
+}
+
+
 template <typename T> nex_sum* horner::create_sum_from_row(const T& row, cross_nested& cn) {
     TRACE("nla_horner", tout << "row="; m_core->print_term(row, tout) << "\n";);
     SASSERT(row.size() > 1);
@@ -140,8 +154,9 @@ template <typename T> nex_sum* horner::create_sum_from_row(const T& row, cross_n
     for (const auto &p : row) {
         if (p.coeff().is_one())
             e->add_child(nexvar(p.var(), cn));
-        else
-            e->add_child(cn.mk_mul(cn.mk_scalar(p.coeff()), nexvar(p.var(), cn)));
+        else {           
+            e->add_child(nexvar(p.coeff(), p.var(), cn));
+        }
     }
     return e;
 }
diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h
index 86cd14acd..2d8732e69 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -42,6 +42,7 @@ public:
     intervals::interval interval_of_expr(const nex* e);
     
     nex* nexvar(lpvar j, cross_nested& cn) const;
+    nex* nexvar(const rational& coeff, lpvar j, cross_nested& cn) const;
     intervals::interval interval_of_sum(const nex_sum*);
     intervals::interval interval_of_sum_no_terms(const nex_sum*);
     intervals::interval interval_of_mul(const nex_mul*);
diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index c3a63c232..2124c2081 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -82,6 +82,7 @@ public:
     #ifdef Z3DEBUG
     virtual void sort() {};
     #endif
+    bool virtual is_linear() const = 0;
 };
 #if Z3DEBUG
 bool operator<(const nex& a , const nex& b);
@@ -107,6 +108,7 @@ public:
     bool contains(lpvar j) const { return j == m_j; }
     int get_degree() const { return 1; }
     virtual void simplify(nex** e) { *e = this; }
+    bool virtual is_linear() const { return true; }
 };
 
 class nex_scalar : public nex {
@@ -124,6 +126,7 @@ public:
     
     int get_degree() const { return 0; }
     virtual void simplify(nex** e) { *e = this; }
+    bool is_linear() const { return true; }
 
 };
 
@@ -267,6 +270,19 @@ public:
         return true;
     }
 
+    bool is_linear() const {
+        SASSERT(is_simplified());
+        if (children().size() > 2)
+            return false;
+
+        SASSERT(children().size() == 2);
+        for (auto e : children()) {
+            if (e->is_scalar())
+                return true;
+        }
+        return false;
+    }
+
 #ifdef Z3DEBUG
     virtual void sort() {
         for (nex * c : m_children) {
@@ -294,7 +310,7 @@ public:
     bool is_linear() const {
         TRACE("nex_details", tout << *this << "\n";);
         for (auto  e : children()) {
-            if (e->get_degree() > 1)
+            if (!e->is_linear())
                 return false;
         }
         TRACE("nex_details", tout << "linear\n";);