diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index cfe146b84..1c9f0fde8 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -102,7 +102,7 @@ namespace simplex { void compress(manager& m, vector & cols); void compress_if_needed(manager& m, vector & cols); void save_var_pos(svector & result_map, unsigned_vector& idxs) const; - bool is_coeff_of(var_t v, numeral const & expected) const; + //bool is_coeff_of(var_t v, numeral const & expected) const; int get_idx_of(var_t v) const; }; @@ -123,7 +123,7 @@ namespace simplex { void reset(); void compress(vector<_row> & rows); void compress_if_needed(vector<_row> & rows); - void compress_singleton(vector<_row> & rows, unsigned singleton_pos); + //void compress_singleton(vector<_row> & rows, unsigned singleton_pos); col_entry const * get_first_col_entry() const; col_entry & add_col_entry(int & pos_idx); void del_col_entry(unsigned idx); diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h index 561025303..277165138 100644 --- a/src/math/simplex/sparse_matrix_def.h +++ b/src/math/simplex/sparse_matrix_def.h @@ -205,6 +205,7 @@ namespace simplex { } } +#if 0 /** \brief Special version of compress, that is used when the column contain only one entry located at position singleton_pos. @@ -221,7 +222,7 @@ namespace simplex { m_first_free_idx = -1; m_entries.shrink(1); } - +#endif template const typename sparse_matrix::col_entry * sparse_matrix::column::get_first_col_entry() const { diff --git a/src/smt/theory_diff_logic.cpp b/src/smt/theory_diff_logic.cpp index fd5bbd5da..f1f00833b 100644 --- a/src/smt/theory_diff_logic.cpp +++ b/src/smt/theory_diff_logic.cpp @@ -21,6 +21,7 @@ Revision History: #include"rational.h" #include"theory_diff_logic_def.h" +#include"sparse_matrix_def.h" namespace smt { @@ -34,5 +35,5 @@ template class theory_diff_logic; namespace simplex { template class simplex; - +template class sparse_matrix; };