From 6c5f7741b2d100d325228db1de5d1960fc20ea0f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 14 Aug 2013 11:55:23 -0700
Subject: [PATCH] more on polynorm

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_dl.cpp |   2 +-
 src/test/polynorm.cpp | 109 ++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 110 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp
index 9c3489aec..4ef1bd8e0 100644
--- a/src/smt/theory_dl.cpp
+++ b/src/smt/theory_dl.cpp
@@ -91,7 +91,7 @@ namespace smt {
                 rational val;
                 if (ctx.e_internalized(rep_of) && th_bv && 
                     th_bv->get_fixed_value(rep_of.get(), val)) {
-                        result = m_th.u().mk_numeral(val.get_int64(), s);
+                    result = m_th.u().mk_numeral(val.get_int64(), s);
                 }
                 else {
                     result = m_th.u().mk_numeral(0, s);
diff --git a/src/test/polynorm.cpp b/src/test/polynorm.cpp
index 092ac022a..3593e98ce 100644
--- a/src/test/polynorm.cpp
+++ b/src/test/polynorm.cpp
@@ -2,6 +2,7 @@
 #include "smt2parser.h"
 #include "arith_decl_plugin.h"
 #include "reg_decl_plugins.h"
+#include "arith_rewriter.h"
 #include "ast_pp.h"
 
 
@@ -27,6 +28,114 @@ static char const* example1 = "(= (+ (- (* x x) (* 2 y)) y) 0)";
 static char const* example2 = "(= (+ 4 3 (- (* x x) (* 2 y)) y) 0)";
 
 
+class poly_nf {
+    expr_ref        m_coefficient;
+    expr_ref_vector m_coefficients;
+    expr_ref_vector m_factors;
+public:
+    poly_nf(ast_manager& m):
+        m_coefficient(m),
+        m_coefficients(m),
+        m_factors(m) {}
+    
+    expr_ref& coefficient() { return m_coefficient; }
+    expr_ref_vector& coefficients() { return m_coefficients; }
+    expr_ref_vector& factors() { return m_factors; }
+
+    void reset() {
+        m_coefficient.reset();
+        m_coefficients.reset();
+        m_factors.reset();
+    }
+
+};
+
+class polynorm {
+    ast_manager&   m;
+    arith_util     m_arith;
+    arith_rewriter m_arith_rw;
+    th_rewriter    m_rw;
+public:
+    polynorm(ast_manager& m): m(m), m_arith(m), m_arith_rw(m), m_rw(m) {}
+
+private:
+    expr_ref_vector mk_fresh_constants(unsigned num, sort* s) {
+        expr_ref_vector result(m);
+        for (unsigned i = 0; i < num; ++i) {
+            result.push_back(m.mk_fresh_const("fresh", s));
+        }
+        return result;
+    }
+
+    expr_ref_vector mk_fresh_reals(unsigned num) {
+        return mk_fresh_constants(num, m_arith.mk_real());
+    }
+
+    expr_ref mk_mul(unsigned num_args, expr* const* args) {
+        expr_ref result(m);
+        m_arith_rw.mk_mul(num_args, args, result);
+        return result;
+    }
+
+    void nf(expr_ref& term, obj_hashtable<expr>& constants, poly_nf& poly) {
+
+        expr_ref_vector& factors = poly.factors();
+        expr_ref_vector& coefficients = poly.coefficients();
+        expr_ref& coefficient = poly.coefficient();
+
+        m_rw(term);
+
+        if (m_arith.is_add(term)) {
+            factors.append(to_app(term)->get_num_args(), to_app(term)->get_args());
+        }
+        else {
+            factors.push_back(term);
+        }
+        for (unsigned i = 0; i < factors.size(); ++i) {
+            expr* f = factors[i].get();
+            unsigned num_args = 1;
+            expr* const* args = &f;
+            if (m_arith.is_mul(f)) {
+                num_args = to_app(f)->get_num_args();
+                args = to_app(f)->get_args();
+            }
+            for (unsigned j = 0; j < num_args; ++j) {
+                if (m_arith.is_numeral(args[j]) || constants.contains(args[j])) {
+                    //consts.push_back(args[j]);
+                }
+                else {
+                    // vars.push_back(args[j]);
+                }
+                // deal with the relevant corner cases.
+            }
+#if 0
+            rational r;
+            if (m_arith.is_mul(f) && m_arith.is_numeral(to_app(f)->get_arg(0), r)) {
+                coefficients.push_back(r);            
+                factors[i] = mk_mul(to_app(f)->get_num_args()-1, to_app(f)->get_args()+1);
+            }
+            else if (m_arith.is_numeral(f, r)) {
+                factors[i] = factors.back();
+                factors.pop_back();
+                SASSERT(coefficient.is_zero());
+                SASSERT(!r.is_zero());
+                coefficient = r;
+                --i; // repeat examining 'i'
+            }
+            else {
+                coefficients.push_back(rational(1));
+            }
+#endif
+        }
+
+        TRACE("polynorm",
+              tout << mk_pp(coefficient, m) << "\n";
+              for (unsigned i = 0; i < factors.size(); ++i) {
+                  tout << mk_pp(factors[i].get(), m) << " * " << mk_pp(coefficients[i].get(), m) << "\n";
+              });
+    }
+};
+
 // ast
 ///  sort : ast
 ///  func_decl : ast