From 1e625db84b2772a4b1c47b383a86d3ab4c244859 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 5 Jul 2019 13:22:54 -0700
Subject: [PATCH] fix a bug in nla_expr

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/gomory.cpp |  7 +++++++
 src/math/lp/horner.cpp | 10 +++++++---
 src/math/lp/nla_expr.h |  6 +-----
 3 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index ea7914b5a..a21279714 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -259,6 +259,13 @@ class gomory::imp {
     }
 
 public:
+    void dump(std::ostream& out) {
+        out << "applying cut at:\n"; print_linear_combination_indices_only<row_strip<mpq>, mpq>(m_row, out); out << std::endl;
+        for (auto & p : m_row) {
+            m_int_solver.m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), out);
+        }
+        out << "inf_col = " << m_inf_col << std::endl;
+    }
 
     lia_move create_cut() {
         TRACE("gomory_cut",
diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index c5c000d90..eb90ec027 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -181,6 +181,7 @@ nex horner::split_with_var(const nex& e, lpvar j) {
         r.add_child(cross_nested_of_sum(a));
         return r;
     }
+    TRACE("nla_cn", tout << "b = " << b << "\n";);
     return nex::sum(nex::mul(cross_nested_of_sum(a), nex::var(j)), b);    
 }
 
@@ -203,7 +204,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););
+    TRACE("nla_cn", tout << "row="; m_core->print_term(row, tout) << "\n";);
     nex e;
     if (row.size() > 1) {
         e.type() = expr_type::SUM;
@@ -216,6 +217,7 @@ 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()));
     }
+    std::cout << "ops\n";
     SASSERT(false);
     return e;
 }
@@ -231,7 +233,8 @@ void horner::set_interval_for_scalar(interv& a, const T& v) {
 }
 
 interv horner::interval_of_expr(const nex& e) {
-    TRACE("nla_cn_details", tout << e.type() << " e=" << e << std::endl;);
+    
+    TRACE("nla_cn", tout << e.type() << " e=" << e << std::endl;);
     interv a;
     switch (e.type()) {
     case expr_type::SCALAR:
@@ -252,7 +255,8 @@ interv 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]);    
+    interv a = interval_of_expr(es[0]);
+    //    std::cout << "a" << std::endl;
     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]);
diff --git a/src/math/lp/nla_expr.h b/src/math/lp/nla_expr.h
index 12405572b..6d10d8c76 100644
--- a/src/math/lp/nla_expr.h
+++ b/src/math/lp/nla_expr.h
@@ -151,11 +151,7 @@ public:
         }
     }
     nla_expr(expr_type t): m_type(t) {}
-    nla_expr() {
-#if Z3DEBUG
-        m_type = expr_type::UNDEF;
-#endif
-    }
+    nla_expr(): m_type(expr_type::UNDEF) {}
     
     void add_child(const nla_expr& e) {
         m_children.push_back(e);