remove many methods dealing with double

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/binary_heap_priority_queue.cpp

@@ -23,15 +23,12 @@ namespace lp {
 template binary_heap_priority_queue<int>::binary_heap_priority_queue(unsigned int);
 template unsigned binary_heap_priority_queue<int>::dequeue();
 template void binary_heap_priority_queue<int>::enqueue(unsigned int, int const&);
-template void binary_heap_priority_queue<double>::enqueue(unsigned int, double const&);
 template void binary_heap_priority_queue<mpq>::enqueue(unsigned int, mpq const&);
 template void binary_heap_priority_queue<int>::remove(unsigned int);
 template unsigned binary_heap_priority_queue<numeric_pair<mpq> >::dequeue();
-template unsigned binary_heap_priority_queue<double>::dequeue();
 template unsigned binary_heap_priority_queue<mpq>::dequeue();
 template void binary_heap_priority_queue<numeric_pair<mpq> >::enqueue(unsigned int, numeric_pair<mpq> const&);
 template void binary_heap_priority_queue<numeric_pair<mpq> >::resize(unsigned int);
-template void lp::binary_heap_priority_queue<double>::resize(unsigned int);
 template binary_heap_priority_queue<unsigned int>::binary_heap_priority_queue(unsigned int);
 template void binary_heap_priority_queue<unsigned>::resize(unsigned int);
 template unsigned binary_heap_priority_queue<unsigned int>::dequeue();

src/math/lp/conversion_helper.h

@@ -31,28 +31,5 @@ struct conversion_helper {
     }
 };
 
-template<>
-struct conversion_helper <double> {
-    static double get_upper_bound(const column_info<mpq> & ci) {
-        if (!ci.upper_bound_is_strict())
-            return ci.get_upper_bound().get_double();
-        double eps = 0.00001;
-        if (!ci.lower_bound_is_set())
-            return ci.get_upper_bound().get_double() - eps;
-        eps = std::min((ci.get_upper_bound() - ci.get_lower_bound()).get_double() / 1000, eps);
-        return ci.get_upper_bound().get_double() - eps;
-    }
-
-    static double get_lower_bound(const column_info<mpq> & ci) {
-        if (!ci.lower_bound_is_strict())
-            return ci.get_lower_bound().get_double();
-        double eps = 0.00001;
-        if (!ci.upper_bound_is_set())
-            return ci.get_lower_bound().get_double() + eps;
-        eps = std::min((ci.get_upper_bound() - ci.get_lower_bound()).get_double() / 1000, eps);
-        return ci.get_lower_bound().get_double() + eps;
-    }
-
-};
 
 }

src/math/lp/core_solver_pretty_printer.cpp

@@ -19,9 +19,6 @@ Revision History:
 --*/
 #include "math/lp/numeric_pair.h"
 #include "math/lp/core_solver_pretty_printer_def.h"
-template lp::core_solver_pretty_printer<double, double>::core_solver_pretty_printer(const lp::lp_core_solver_base<double, double> &, std::ostream & out);
-template void lp::core_solver_pretty_printer<double, double>::print();
-template lp::core_solver_pretty_printer<double, double>::~core_solver_pretty_printer();
 template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::core_solver_pretty_printer(const lp::lp_core_solver_base<lp::mpq, lp::mpq> &, std::ostream & out);
 template void lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::print();
 template lp::core_solver_pretty_printer<lp::mpq, lp::mpq>::~core_solver_pretty_printer();

src/math/lp/dense_matrix.cpp

@@ -21,11 +21,6 @@ Revision History:
 #include "math/lp/dense_matrix_def.h"
 #ifdef Z3DEBUG
 #include "util/vector.h"
-template lp::dense_matrix<double, double> lp::operator*<double, double>(lp::matrix<double, double>&, lp::matrix<double, double>&);
-template void lp::dense_matrix<double, double>::apply_from_left(vector<double> &);
-template lp::dense_matrix<double, double>::dense_matrix(lp::matrix<double, double> const*);
-template lp::dense_matrix<double, double>::dense_matrix(unsigned int, unsigned int);
-template lp::dense_matrix<double, double>& lp::dense_matrix<double, double>::operator=(lp::dense_matrix<double, double> const&);
 template lp::dense_matrix<lp::mpq, lp::mpq>::dense_matrix(unsigned int, unsigned int);
 template lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::dense_matrix(lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> > const*);
 template void lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::apply_from_left(vector<lp::mpq>&);
@@ -35,6 +30,5 @@ template lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::dense_matrix(uns
 template lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >& lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::operator=(lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> > const&);
 template lp::dense_matrix<lp::mpq, lp::numeric_pair<lp::mpq> > lp::operator*<lp::mpq, lp::numeric_pair<lp::mpq> >(lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&, lp::matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&);
 template void lp::dense_matrix<lp::mpq, lp::numeric_pair< lp::mpq> >::apply_from_right( vector< lp::mpq> &);
-template void lp::dense_matrix<double,double>::apply_from_right(vector<double> &);
 template void lp::dense_matrix<lp::mpq, lp::mpq>::apply_from_left(vector<lp::mpq>&);
 #endif

src/math/lp/dense_matrix.h

@@ -90,11 +90,7 @@ class dense_matrix: public matrix<T, X> {
 
     void set_elem(unsigned i, unsigned j, const T& val) {  m_values[i * m_n + j] = val;  }
 
-    // This method pivots row i to row i0 by muliplying row i by
-    //   alpha and adding it to row i0.
-    void pivot_row_to_row(unsigned i, const T& alpha, unsigned i0,
-                          const double & pivot_epsilon);
-
+    // This method pivots
     void swap_columns(unsigned a, unsigned b);
 
     void swap_rows(unsigned a, unsigned b);

src/math/lp/dense_matrix_def.h

@@ -150,17 +150,6 @@ template <typename T, typename X> void dense_matrix<T, X>::apply_from_left_to_X(
     }
 }
 
-// This method pivots row i to row i0 by muliplying row i by
-//   alpha and adding it to row i0.
-template <typename T, typename X> void dense_matrix<T, X>::pivot_row_to_row(unsigned i, const T& alpha, unsigned i0,
-                                                                            const double & pivot_epsilon) {
-    for (unsigned j = 0; j < m_n; j++) {
-        m_values[i0 * m_n + j] += m_values[i * m_n + j] * alpha;
-        if (fabs(m_values[i0 + m_n + j]) < pivot_epsilon) {
-            m_values[i0 + m_n + j] = numeric_traits<T>::zero();;
-        }
-    }
-}
 
 template <typename T, typename X> void dense_matrix<T, X>::swap_columns(unsigned a, unsigned b) {
     for (unsigned i = 0; i < m_m; i++) {

src/math/lp/indexed_vector.cpp

@@ -20,10 +20,6 @@ Revision History:
 #include "util/vector.h"
 #include "math/lp/indexed_vector_def.h"
 namespace lp {
-template void indexed_vector<double>::clear();
-template void indexed_vector<double>::clear_all();
-template void indexed_vector<double>::erase_from_index(unsigned int);
-template void indexed_vector<double>::set_value(const double&, unsigned int);
 template void indexed_vector<mpq>::clear();
 template void indexed_vector<unsigned>::clear();
 template void indexed_vector<mpq>::clear_all();
@@ -32,22 +28,8 @@ template void indexed_vector<mpq>::resize(unsigned int);
 template void indexed_vector<unsigned>::resize(unsigned int);
 template void indexed_vector<mpq>::set_value(const mpq&, unsigned int);
 template void indexed_vector<unsigned>::set_value(const unsigned&, unsigned int);
-#ifdef Z3DEBUG
-template bool indexed_vector<unsigned>::is_OK() const;
-template bool indexed_vector<double>::is_OK() const;
-template bool indexed_vector<mpq>::is_OK() const;
-template bool indexed_vector<lp::numeric_pair<mpq> >::is_OK() const;
-#endif
 template void lp::indexed_vector< lp::mpq>::print(std::basic_ostream<char,struct std::char_traits<char> > &);
-template void lp::indexed_vector<double>::print(std::basic_ostream<char,struct std::char_traits<char> > &);
 template void lp::indexed_vector<lp::numeric_pair<lp::mpq> >::print(std::ostream&);
 }
-// template void lp::print_vector<double, vectro>(vector<double> const&, std::ostream&);
-// template void lp::print_vector<unsigned int>(vector<unsigned int> const&, std::ostream&);
-// template void lp::print_vector<std::string>(vector<std::string> const&, std::ostream&);
-// template void lp::print_vector<lp::numeric_pair<lp::mpq> >(vector<lp::numeric_pair<lp::mpq>> const&, std::ostream&);
-template void lp::indexed_vector<double>::resize(unsigned int);
-// template void lp::print_vector< lp::mpq>(vector< lp::mpq> const &, std::basic_ostream<char, std::char_traits<char> > &);
-// template void lp::print_vector<std::pair<lp::mpq, unsigned int> >(vector<std::pair<lp::mpq, unsigned int>> const&, std::ostream&);
 template void lp::indexed_vector<lp::numeric_pair<lp::mpq> >::erase_from_index(unsigned int);
 

src/math/lp/indexed_vector.h

@@ -99,47 +99,9 @@ class indexed_vector {
         return m_data[i];
     }
 
-    void clean_up() {
-#if 0==1
-        for (unsigned k = 0; k < m_index.size(); k++) {
-            unsigned i = m_index[k];
-            T & v = m_data[i];
-            if (lp_settings::is_eps_small_general(v, 1e-14)) {
-                v = zero_of_type<T>();
-                m_index.erase(m_index.begin() + k--);
-            }
-        }
-#endif
-       vector<unsigned> index_copy;
-       for (unsigned i : m_index) {
-           T & v = m_data[i];
-           if (!lp_settings::is_eps_small_general(v, 1e-14)) {
-               index_copy.push_back(i);
-           } else if (!numeric_traits<T>::is_zero(v)) {
-               v = zero_of_type<T>();
-           }
-       }
-       m_index = index_copy;
-    }
-
 
     void erase_from_index(unsigned j);
-
-    void add_value_at_index_with_drop_tolerance(unsigned j, const T& val_to_add) {
-        T & v = m_data[j];
-        bool was_zero = is_zero(v);
-        v += val_to_add;
-        if (lp_settings::is_eps_small_general(v, 1e-14)) {
-            v = zero_of_type<T>();
-            if (!was_zero) {
-                erase_from_index(j);
-            }
-        } else {
-            if (was_zero)
-                m_index.push_back(j);
-        }
-    }
-
+
     void add_value_at_index(unsigned j, const T& val_to_add) {
         T & v = m_data[j];
         bool was_zero = is_zero(v);
@@ -153,18 +115,6 @@ class indexed_vector {
         }
     }
 
-    void restore_index_and_clean_from_data() {
-        m_index.resize(0);
-        for (unsigned i = 0; i < m_data.size(); i++) {
-            T & v = m_data[i];
-            if (lp_settings::is_eps_small_general(v, 1e-14)) {
-                v = zero_of_type<T>();
-            } else {
-                m_index.push_back(i);
-            }
-        }
-    }
-
     struct ival {
         unsigned m_var;
         const T & m_coeff;
@@ -215,9 +165,6 @@ class indexed_vector {
     }
 
 
-#ifdef Z3DEBUG
-    bool is_OK() const;
-#endif
     void print(std::ostream & out);
 };
 }

src/math/lp/indexed_vector_def.h

@@ -43,7 +43,7 @@ template <typename T>
 void indexed_vector<T>::resize(unsigned data_size) {
     clear();
     m_data.resize(data_size, numeric_traits<T>::zero());
-    lp_assert(is_OK());
+
 }
 
 template <typename T>
@@ -72,33 +72,6 @@ void indexed_vector<T>::erase_from_index(unsigned j) {
         m_index.erase(it);
 }
 
-#ifdef Z3DEBUG
-template <typename T>
-bool indexed_vector<T>::is_OK() const {
-    return true;
-    const double drop_eps = 1e-14;
-    for (unsigned i = 0; i < m_data.size(); i++) {
-        if (!is_zero(m_data[i]) && lp_settings::is_eps_small_general(m_data[i], drop_eps)) {
-            return false;
-        }
-        if (lp_settings::is_eps_small_general(m_data[i], drop_eps) != (std::find(m_index.begin(), m_index.end(), i) == m_index.end())) {
-            return false;
-        }
-    }
-
-    std::unordered_set<unsigned> s;
-    for (unsigned i : m_index) {
-        //no duplicates!!!
-        if (s.find(i) != s.end())
-            return false;
-        s.insert(i);
-        if (i >= m_data.size())
-            return false;
-    }
-
-    return true;
-}
-#endif
 template <typename T>
 void indexed_vector<T>::print(std::ostream & out) {
     out << "m_index " << std::endl;

src/math/lp/lar_core_solver.h

@@ -27,8 +27,7 @@ class lar_core_solver  {
     int m_infeasible_sum_sign; // todo: get rid of this field
     vector<numeric_pair<mpq>> m_right_sides_dummy;
     vector<mpq> m_costs_dummy;
-    vector<double> m_d_right_sides_dummy;
-    vector<double> m_d_costs_dummy;
+
 public:
     stacked_value<simplex_strategy_enum> m_stacked_simplex_strategy;
     stacked_vector<column_type> m_column_types;
@@ -45,10 +44,6 @@ class lar_core_solver  {
     stacked_vector<unsigned> m_r_rows_nz;
 
     // d - solver fields, for doubles
-    vector<double> m_d_x; // the solution in doubles
-    vector<double> m_d_lower_bounds;
-    vector<double> m_d_upper_bounds;
-    static_matrix<double, double> m_d_A;
     stacked_vector<unsigned> m_d_pushed_basis;
     vector<unsigned> m_d_basis;
     vector<unsigned> m_d_nbasis;
@@ -146,7 +141,7 @@ class lar_core_solver  {
         m_r_lower_bounds.push();
         m_r_upper_bounds.push();
 
-        m_d_A.push();
+
 
     }
 
@@ -185,10 +180,6 @@ class lar_core_solver  {
         m_r_solver.m_costs.resize(m_r_A.column_count());
         m_r_solver.m_d.resize(m_r_A.column_count());
 
-        m_d_A.pop(k);
-        // doubles
-
-        m_d_x.resize(m_d_A.column_count());
         pop_basis(k);
         m_stacked_simplex_strategy.pop(k);
         settings().set_simplex_strategy(m_stacked_simplex_strategy);
@@ -279,15 +270,7 @@ class lar_core_solver  {
     }
 
 
-    void create_double_matrix(static_matrix<double, double> & A) {
-        for (unsigned i = 0; i < m_r_A.row_count(); i++) {
-            auto & row = m_r_A.m_rows[i];
-            for (row_cell<mpq> & c : row) {
-                A.add_new_element(i, c.var(), c.coeff().get_double());
-            }
-        }
-    }
-
+
     void fill_basis_d(
                       vector<unsigned>& basis_d,
                       vector<int>& heading_d,
@@ -308,27 +291,6 @@ class lar_core_solver  {
         }
     }
 
-    void get_bounds_for_double_solver() {
-        unsigned n = m_n();
-        m_d_lower_bounds.resize(n);
-        m_d_upper_bounds.resize(n);
-        double delta = find_delta_for_strict_boxed_bounds().get_double();
-        if (delta > 0.000001)
-            delta = 0.000001;
-        for (unsigned j = 0; j < n; j++) {
-            if (lower_bound_is_set(j)) {
-                const auto & lb = m_r_solver.m_lower_bounds[j];
-                m_d_lower_bounds[j] = lb.x.get_double() + delta * lb.y.get_double();
-            }
-            if (upper_bound_is_set(j)) {
-                const auto & ub = m_r_solver.m_upper_bounds[j];
-                m_d_upper_bounds[j] = ub.x.get_double() + delta * ub.y.get_double();
-                lp_assert(!lower_bound_is_set(j) || (m_d_upper_bounds[j] >= m_d_lower_bounds[j]));
-            }
-        }
-    }
-
-
 
     bool lower_bound_is_set(unsigned j) const {
         switch (m_column_types[j]) {