From 5d2ba2fce13a2b20beab4724afd1b8daabfb7fba Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 3 Jul 2019 19:21:03 -0700
Subject: [PATCH] progress in horner's heuristic

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/horner.cpp | 31 ++++++++++++++++++-------------
 1 file changed, 18 insertions(+), 13 deletions(-)

diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index f07f774ef..c5c000d90 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -20,6 +20,7 @@
 
 #include "math/lp/horner.h"
 #include "math/lp/nla_core.h"
+#include "math/lp/lp_utils.h"
 
 namespace nla {
 typedef nla_expr<rational> nex;
@@ -41,7 +42,7 @@ void horner::lemma_on_row(const T& row) {
         return;
     nex e = create_expr_from_row(row);
     TRACE("nla_cn", tout << "cross nested e = " << e << std::endl;);
-    intervals::interval a = interval_of_expr(e);
+    interv a = interval_of_expr(e);
     TRACE("nla_cn", tout << "interval a = ";  m_intervals.display(tout, a) << "\n";);
     check_interval_for_conflict(a, row);
 }
@@ -202,6 +203,7 @@ nex horner::cross_nested_of_sum(const nex& e) {
 }
 
 template <typename T> nex horner::create_expr_from_row(const T& row) {
+    TRACE("nla_cn", tout << "row="; m_core->m_lar_solver.print_term_as_indices(row, tout););
     nex e;
     if (row.size() > 1) {
         e.type() = expr_type::SUM;
@@ -228,7 +230,7 @@ void horner::set_interval_for_scalar(interv& a, const T& v) {
     m_intervals.set_upper_is_inf(a, false);
 }
 
-intervals::interval horner::interval_of_expr(const nex& e) {
+interv horner::interval_of_expr(const nex& e) {
     TRACE("nla_cn_details", tout << e.type() << " e=" << e << std::endl;);
     interv a;
     switch (e.type()) {
@@ -251,25 +253,24 @@ intervals::interval horner::interval_of_expr(const nex& e) {
 template <typename T>
 interv horner::interval_of_mul(const vector<nla_expr<T>>& es) {    
     interv a = interval_of_expr(es[0]);    
-    if (m_intervals.is_zero(a)) {
-        TRACE("nla_cn", m_intervals.display(tout, a) << "\ngot zero for " << es[0] << "\n";);
-        return a;
-    }
     TRACE("nla_cn", tout << "es[0]= "<< es[0] << std::endl << "a = "; m_intervals.display(tout, a); tout << "\n";);
     for (unsigned k = 1; k < es.size(); k++) {
         interv b = interval_of_expr(es[k]);
-        if (m_intervals.is_zero(b)) {
-            TRACE("nla_cn", m_intervals.display(tout, b) << "\ngot zero for " << es[k] << "\n";);
-            return b;
-        }
         interv c;
         interval_deps deps;
         m_intervals.mul(a, b, c, deps);
         m_intervals.set(a, c);
         m_intervals.add_deps(a, b, deps, a);
+        TRACE("nla_cn", tout << "es["<< k << "] = " << es[k] << std::endl << "a = "; m_intervals.display(tout, a); tout << "\n";);
+        if (m_intervals.is_zero(a)) {
+            TRACE("nla_cn", tout << "got zero\n"; );
+            break;
+        }
     }
     TRACE("nla_cn",
-          for (const auto &e : es) tout << e;
+          for (const auto &e : es) {
+              tout << "("<< e << ")";
+          }
           tout << " interv a = ";
           m_intervals.display(tout, a) << "\n";);
     return a;
@@ -292,10 +293,14 @@ interv horner::interval_of_sum(const vector<nla_expr<T>>& es) {
         }
         interv c;
         interval_deps deps;
+        TRACE("nla_cn_details", tout << "a = "; m_intervals.display(tout, a) << "\nb = "; m_intervals.display(tout, b) << "\n";);
         m_intervals.add(a, b, c, deps);
+        TRACE("nla_cn_details", tout << "c = "; m_intervals.display(tout, c); tout << "\n";);
         m_intervals.set(a, c);
+        TRACE("nla_cn_details", tout << "a = "; m_intervals.display(tout, a); tout << "\n";);
+        
         m_intervals.add_deps(a, b, deps, a);
-        TRACE("nla_cn_details", tout << "interv = "; m_intervals.display(tout, a); tout << "\n";);
+        TRACE("nla_cn_details", tout << "final a with deps = "; m_intervals.display(tout, a); tout << "\n";);
         if (m_intervals.is_inf(a)) {
             TRACE("nla_cn_details", tout << "got infinity\n";);            
             return a;
@@ -311,7 +316,7 @@ void horner::set_var_interval(lpvar v, interv& b) {
     
 }
 template <typename T> 
-void horner::check_interval_for_conflict(const intervals::interval& i, const T& row) {
+void horner::check_interval_for_conflict(const interv& i, const T& row) {
     if (m_intervals.check_interval_for_conflict_on_zero(i)) {
         TRACE("nla_cn", print_lemma(tout););
     }  else {