mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-17 03:16:17 +00:00
Code Activity

trying to fix build problems

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-21 15:17:50 -07:00
parent 3de940423f
commit 6fac8aa40c
3 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/simplex/sparse_matrix.h
View file

@ -102,7 +102,7 @@ namespace simplex {
void compress(manager& m, vector<column> & cols); void compress(manager& m, vector<column> & cols);
void compress_if_needed(manager& m, vector<column> & cols); void compress_if_needed(manager& m, vector<column> & cols);
void save_var_pos(svector<int> & result_map, unsigned_vector& idxs) const; void save_var_pos(svector<int> & 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; int get_idx_of(var_t v) const;
}; };
@ -123,7 +123,7 @@ namespace simplex {
void reset(); void reset();
void compress(vector<_row> & rows); void compress(vector<_row> & rows);
void compress_if_needed(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 const * get_first_col_entry() const;
col_entry & add_col_entry(int & pos_idx); col_entry & add_col_entry(int & pos_idx);
void del_col_entry(unsigned idx); void del_col_entry(unsigned idx);

3
src/math/simplex/sparse_matrix_def.h
View file

@ -205,6 +205,7 @@ namespace simplex {
} }
} }
#if 0
/** /**
\brief Special version of compress, that is used when the column contain \brief Special version of compress, that is used when the column contain
only one entry located at position singleton_pos. only one entry located at position singleton_pos.
@ -221,7 +222,7 @@ namespace simplex {
m_first_free_idx = -1; m_first_free_idx = -1;
m_entries.shrink(1); m_entries.shrink(1);
} }
#endif
template<typename Ext> template<typename Ext>
const typename sparse_matrix<Ext>::col_entry * const typename sparse_matrix<Ext>::col_entry *
sparse_matrix<Ext>::column::get_first_col_entry() const { sparse_matrix<Ext>::column::get_first_col_entry() const {

3
src/smt/theory_diff_logic.cpp
View file

@ -21,6 +21,7 @@ Revision History:
#include"rational.h" #include"rational.h"
#include"theory_diff_logic_def.h" #include"theory_diff_logic_def.h"
#include"sparse_matrix_def.h"
namespace smt { namespace smt {
@ -34,5 +35,5 @@ template class theory_diff_logic<srdl_ext>;
namespace simplex { namespace simplex {
template class simplex<mpq_ext>; template class simplex<mpq_ext>;
template class sparse_matrix<mpq_ext>;
}; };