From 540ea825b0a3b36a653af723e517d536295e268b Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Mon, 8 Oct 2018 16:37:10 -0700
Subject: [PATCH] cleanup nla_solver

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/util/lp/factorization.cpp | 22 +++++++++++-----------
 src/util/lp/factorization.h   | 14 +++++++-------
 2 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/src/util/lp/factorization.cpp b/src/util/lp/factorization.cpp
index d6baa6138..849bd64fa 100644
--- a/src/util/lp/factorization.cpp
+++ b/src/util/lp/factorization.cpp
@@ -2,7 +2,7 @@
 #include "util/lp/factorization.h"
 namespace nla {
 
-void const_iterator::init_vars_by_the_mask(unsigned_vector & k_vars, unsigned_vector & j_vars) const {
+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()); 
@@ -15,7 +15,7 @@ void const_iterator::init_vars_by_the_mask(unsigned_vector & k_vars, unsigned_ve
     }
 }
             
-bool const_iterator::get_factors(unsigned& k, unsigned& j, rational& sign) const {
+bool const_iterator_mon::get_factors(unsigned& k, unsigned& j, rational& sign) const {
     unsigned_vector k_vars;
     unsigned_vector j_vars;
     init_vars_by_the_mask(k_vars, j_vars);
@@ -47,7 +47,7 @@ bool const_iterator::get_factors(unsigned& k, unsigned& j, rational& sign) const
     return true;
 }
 
-const_iterator::reference const_iterator::operator*() const {
+const_iterator_mon::reference const_iterator_mon::operator*() const {
     if (m_full_factorization_returned == false)  {
         return create_full_factorization();
     }
@@ -57,7 +57,7 @@ const_iterator::reference const_iterator::operator*() const {
     return create_binary_factorization(j, k, m_ff->m_cmon.coeff() * sign);
 }
             
-void const_iterator::advance_mask() {
+void const_iterator_mon::advance_mask() {
     if (!m_full_factorization_returned) {
         m_full_factorization_returned = true;
         return;
@@ -74,23 +74,23 @@ void const_iterator::advance_mask() {
 }
 
             
-const_iterator::self_type const_iterator::operator++() {  self_type i = *this; operator++(1); return i;  }
-const_iterator::self_type const_iterator::operator++(int) { advance_mask(); return *this; }
+const_iterator_mon::self_type const_iterator_mon::operator++() {  self_type i = *this; operator++(1); return i;  }
+const_iterator_mon::self_type const_iterator_mon::operator++(int) { advance_mask(); return *this; }
 
-const_iterator::const_iterator(const svector<bool>& mask, const factorization_factory *f) : 
+const_iterator_mon::const_iterator_mon(const svector<bool>& mask, const factorization_factory *f) : 
     m_mask(mask),
     m_ff(f) ,
     m_full_factorization_returned(false)
 {}
             
-bool const_iterator::operator==(const const_iterator::self_type &other) const {
+bool const_iterator_mon::operator==(const const_iterator_mon::self_type &other) const {
     return
         m_full_factorization_returned == other.m_full_factorization_returned &&
         m_mask == other.m_mask;
 }
-bool const_iterator::operator!=(const const_iterator::self_type &other) const { return !(*this == other); }
+bool const_iterator_mon::operator!=(const const_iterator_mon::self_type &other) const { return !(*this == other); }
             
-factorization const_iterator::create_binary_factorization(lpvar j, lpvar k, rational const& sign) const {
+factorization const_iterator_mon::create_binary_factorization(lpvar j, lpvar k, rational const& sign) const {
     // todo : the current explanation is an overkill
     // std::function<void (expl_set&)> explain = [&](expl_set& exp){
     //                                               const imp & impl = m_ff->m_impf;
@@ -111,7 +111,7 @@ factorization const_iterator::create_binary_factorization(lpvar j, lpvar k, rati
     return f;
 }
 
-factorization const_iterator::create_full_factorization() const {
+factorization const_iterator_mon::create_full_factorization() const {
     factorization f;
     f.vars() = m_ff->m_mon.vars();
     f.sign() = rational(1);
diff --git a/src/util/lp/factorization.h b/src/util/lp/factorization.h
index 2bd660be2..fd2974f9b 100644
--- a/src/util/lp/factorization.h
+++ b/src/util/lp/factorization.h
@@ -41,14 +41,14 @@ public:
     const lpvar* end() const { return m_vars.end(); }
 };
 
-struct const_iterator {
+struct const_iterator_mon {
     // fields
     svector<bool>                  m_mask;
     const factorization_factory *  m_ff;
     bool                           m_full_factorization_returned;
 
     //typedefs
-    typedef const_iterator self_type;
+    typedef const_iterator_mon self_type;
     typedef factorization value_type;
     typedef const factorization reference;
     typedef int difference_type;
@@ -64,7 +64,7 @@ struct const_iterator {
     self_type operator++();
     self_type operator++(int);
 
-    const_iterator(const svector<bool>& mask, const factorization_factory *f);
+    const_iterator_mon(const svector<bool>& mask, const factorization_factory *f);
     
     bool operator==(const self_type &other) const;
     bool operator!=(const self_type &other) const;
@@ -87,16 +87,16 @@ struct factorization_factory {
         m_cmon(cmon) {
     }
 
-    const_iterator begin() const {
+    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);
-        return const_iterator(mask, this);
+        return const_iterator_mon(mask, this);
     }
     
-    const_iterator end() const {
+    const_iterator_mon end() const {
         svector<bool> mask(m_mon.vars().size() - 1, true);
-        auto it = const_iterator(mask, this);
+        auto it = const_iterator_mon(mask, this);
         it.m_full_factorization_returned = true;
         return it;
     }