From ad9ecad73cab634b5349fa144be80f73059de4c4 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 11 Jul 2019 12:43:47 -0700
Subject: [PATCH] test horner

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/horner.h   |  2 +-
 src/math/lp/nla_expr.h | 35 ++++++++++++++++++++++++-----------
 src/test/lp/lp.cpp     | 23 ++++++++++++++++++++++-
 3 files changed, 47 insertions(+), 13 deletions(-)

diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h
index b83a371d8..ef0ead28d 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -28,9 +28,9 @@ class core;
 
 
 class horner : common {
-    typedef nla_expr<rational> nex;
     intervals m_intervals;
 public:
+    typedef nla_expr<rational> nex;
     
     horner(core *core);
     void horner_lemmas();
diff --git a/src/math/lp/nla_expr.h b/src/math/lp/nla_expr.h
index 6d10d8c76..2724e6276 100644
--- a/src/math/lp/nla_expr.h
+++ b/src/math/lp/nla_expr.h
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #pragma once
+#include <initializer_list>
 #include "math/lp/nla_defs.h"
 namespace nla {
 enum class expr_type { SUM, MUL, VAR, SCALAR, UNDEF };
@@ -157,21 +158,33 @@ public:
         m_children.push_back(e);
     }
 
-    
-    static nla_expr sum(const nla_expr& v, const nla_expr & w) {
-        nla_expr r(expr_type::SUM);
-        r.add_child(v);
-        r.add_child(w);
-        return r;
+    void add_child(const T& k) {
+        m_children.push_back(scalar(k));
     }
-    static nla_expr mul(const nla_expr& v, const nla_expr & w) {
-        nla_expr r(expr_type::MUL);
-        r.add_child(v);
-        r.add_child(w);
+
+    void add_children() { }
+
+    template <typename K, typename ...Args>
+    void add_children(K e, Args ...  es) {
+        add_child(e);
+        add_children(es ...);
+    }
+
+    template <typename K, typename ... Args>
+    static nla_expr sum(K e, Args ... es) {
+        nla_expr r(expr_type::SUM);
+        r.add_children(e, es...);
         return r;
     }
 
-    static nla_expr mul(const T& v, const nla_expr & w) {
+    template <typename K, typename ... Args>
+    static nla_expr mul(K e, Args ... es) {
+        nla_expr r(expr_type::MUL);
+        r.add_children(e, es...);
+        return r;
+    }
+
+    static nla_expr mul(const T& v, nla_expr & w) {
         if (v == 1)
             return w;
         nla_expr r(expr_type::MUL);
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 5caad4936..12b02ae3f 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -55,6 +55,7 @@
 #include "math/lp/general_matrix.h"
 #include "math/lp/lp_bound_propagator.h"
 #include "math/lp/nla_solver.h"
+#include "math/lp/horner.h"
 namespace nla {
 void test_order_lemma();
 void test_monotone_lemma();
@@ -64,6 +65,17 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors();
 void test_basic_lemma_for_mon_zero_from_factors_to_monomial();
 void test_basic_lemma_for_mon_neutral_from_monomial_to_factors();
 void test_basic_lemma_for_mon_neutral_from_factors_to_monomial();
+
+void test_cn() {
+    typedef horner::nex nex;
+    enable_trace("nla_cn");
+
+    nex a = nex::var(0), b = nex::var(1), c = nex::var(2), d = nex::var(3), e = nex::var(4);
+    nex aad = nex::mul(a, a, d);
+    
+    
+}
+
 }
 
 namespace lp {
@@ -71,7 +83,7 @@ unsigned seed = 1;
 
 class my_bound_propagator : public lp_bound_propagator {
 public:
-    my_bound_propagator(lar_solver & ls): lp_bound_propagator(ls, nullptr) {}
+    my_bound_propagator(lar_solver & ls): lp_bound_propagator(ls) {}
     void consume(mpq const& v, lp::constraint_index j) override {}
 };
 
@@ -1907,6 +1919,7 @@ void test_replace_column() {
 
 
 void setup_args_parser(argument_parser & parser) {
+    parser.add_option_with_help_string("-nla_cn", "test cross nornmal form");
     parser.add_option_with_help_string("-nla_blfmz_mf", "test_basic_lemma_for_mon_zero_from_factor_to_monomial");
     parser.add_option_with_help_string("-nla_blfmz_fm", "test_basic_lemma_for_mon_zero_from_monomials_to_factor");
     parser.add_option_with_help_string("-nla_order", "test nla_solver order lemma");
@@ -3570,6 +3583,7 @@ void test_nla_order_lemma() {
     nla::test_order_lemma();
 }
 
+
 void test_lp_local(int argn, char**argv) {
     
     // initialize_util_module();
@@ -3586,6 +3600,13 @@ void test_lp_local(int argn, char**argv) {
 
     args_parser.print();
     
+    if (args_parser.option_is_used("-nla_cn")) {
+#ifdef Z3DEBUG
+        nla::test_cn();
+#endif
+        return finalize(0);
+    }
+
     if (args_parser.option_is_used("-nla_order")) {
 #ifdef Z3DEBUG
         test_nla_order_lemma();