mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

remove unused column function field, #1021

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-16 21:27:43 -07:00
parent ceec81de0b
commit 4069e76ab0
1 changed files with 16 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/util/lp/lar_solver.h
View file

@ -52,7 +52,6 @@ class lar_solver : public column_namer {
vector<lar_term*> m_orig_terms; vector<lar_term*> m_orig_terms;
const var_index m_terms_start_index; const var_index m_terms_start_index;
indexed_vector<mpq> m_column_buffer; indexed_vector<mpq> m_column_buffer;
std::function<column_type (unsigned)> m_column_type_function;
public: public:
lar_core_solver m_mpq_lar_core_solver; lar_core_solver m_mpq_lar_core_solver;
unsigned constraint_count() const { unsigned constraint_count() const {
@ -83,7 +82,6 @@ public:
lar_solver() : m_status(OPTIMAL), lar_solver() : m_status(OPTIMAL),
m_infeasible_column_index(-1), m_infeasible_column_index(-1),
m_terms_start_index(1000000), m_terms_start_index(1000000),
m_column_type_function ([this] (unsigned j) {return m_mpq_lar_core_solver.m_column_types()[j];}),
m_mpq_lar_core_solver(m_settings, *this) m_mpq_lar_core_solver(m_settings, *this)
{} {}