From aefd7eefb6c5e1263977c4afbfd5b74bc5242096 Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Mon, 26 Nov 2018 08:08:42 -0800
Subject: [PATCH] simplify factorization

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/util/lp/factorization.cpp | 12 ++++++------
 src/util/lp/factorization.h   | 16 ++++++----------
 src/util/lp/nla_solver.cpp    |  9 +++------
 3 files changed, 15 insertions(+), 22 deletions(-)

diff --git a/src/util/lp/factorization.cpp b/src/util/lp/factorization.cpp
index 405f3b210..8522e7caf 100644
--- a/src/util/lp/factorization.cpp
+++ b/src/util/lp/factorization.cpp
@@ -4,13 +4,13 @@ namespace nla {
 
 void const_iterator_mon::init_vars_by_the_mask(unsigned_vector & k_vars, unsigned_vector & j_vars) const {
     // the last element for m_factorization.m_rooted_vars goes to k_vars
-    SASSERT(m_mask.size() + 1  == m_ff->m_cmon.vars().size());
-    k_vars.push_back(m_ff->m_cmon.vars().back()); 
+    SASSERT(m_mask.size() + 1  == m_ff->m_vars.size());
+    k_vars.push_back(m_ff->m_vars.back()); 
     for (unsigned j = 0; j < m_mask.size(); j++) {
         if (m_mask[j]) {
-            k_vars.push_back(m_ff->m_cmon.vars()[j]);
+            k_vars.push_back(m_ff->m_vars[j]);
         } else {
-            j_vars.push_back(m_ff->m_cmon.vars()[j]);
+            j_vars.push_back(m_ff->m_vars[j]);
         }
     }
 }
@@ -54,7 +54,7 @@ const_iterator_mon::reference const_iterator_mon::operator*() const {
     unsigned j, k; rational sign;
     if (!get_factors(j, k, sign))
         return factorization();
-    return create_binary_factorization(j, k, m_ff->m_cmon.coeff() * sign);
+    return create_binary_factorization(j, k, sign);
 }
             
 void const_iterator_mon::advance_mask() {
@@ -113,7 +113,7 @@ factorization const_iterator_mon::create_binary_factorization(lpvar j, lpvar k,
 
 factorization const_iterator_mon::create_full_factorization() const {
     factorization f;
-    f.vars() = m_ff->m_mon.vars();
+    f.vars() = m_ff->m_vars;
     f.sign() = rational(1);
     return f;
 }
diff --git a/src/util/lp/factorization.h b/src/util/lp/factorization.h
index 878bf6416..0b2898a83 100644
--- a/src/util/lp/factorization.h
+++ b/src/util/lp/factorization.h
@@ -75,27 +75,23 @@ struct const_iterator_mon {
 };
 
 struct factorization_factory {
-        // returns true if found
+    const svector<lpvar>& m_vars;
+    // returns true if found
     virtual bool find_monomial_of_vars(const svector<lpvar>& vars, monomial& m, rational & sign) const = 0;
-    unsigned           m_i_mon;
-    const monomial&    m_mon;
-    monomial_coeff m_cmon;
 
-    factorization_factory(unsigned i_mon, const monomial& mon, const monomial_coeff& cmon) :
-        m_i_mon(i_mon),
-        m_mon(mon),
-        m_cmon(cmon) {
+    factorization_factory(const svector<lpvar>& vars) :
+        m_vars(vars) {
     }
 
     const_iterator_mon begin() const {
         // we keep the last element always in the first factor to avoid
         // repeating a pair twice
-        svector<bool> mask(m_mon.vars().size() - 1, false);
+        svector<bool> mask(m_vars.size() - 1, false);
         return const_iterator_mon(mask, this);
     }
     
     const_iterator_mon end() const {
-        svector<bool> mask(m_mon.vars().size() - 1, true);
+        svector<bool> mask(m_vars.size() - 1, true);
         auto it = const_iterator_mon(mask, this);
         it.m_full_factorization_returned = true;
         return it;
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 6e6a44d57..7dd3d7abc 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -478,12 +478,9 @@ struct solver::imp {
     struct factorization_factory_imp: factorization_factory {
         const imp&         m_imp;
         
-        factorization_factory_imp(unsigned i_mon, const imp& s) :
-            factorization_factory(i_mon,
-                s.m_monomials[i_mon],
-                s.canonize_monomial(s.m_monomials[i_mon])
-                ),
-                m_imp(s) { }
+        factorization_factory_imp(const svector<lpvar>& m_vars, const imp& s) :
+            factorization_factory(m_vars),
+            m_imp(s) { }
         
          bool find_monomial_of_vars(const svector<lpvar>& vars, monomial& m, rational & sign) const {
             auto it = m_imp.m_rooted_monomials_map.find(vars);