From 7e004fe331878e1f507806be4c39f47353c1ce64 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 11 May 2017 09:28:59 -0700
Subject: [PATCH] fix build warnings part 7, disable LRA for regression
t201.smt2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/smt_setup.cpp | 4 ++--
src/util/lp/lar_solver.h | 9 +++------
src/util/lp/lp_primal_core_solver.h | 28 ++++++++++++++--------------
src/util/lp/mps_reader.h | 11 ++++++-----
4 files changed, 25 insertions(+), 27 deletions(-)
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 6b9402761..be6ab3064 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -725,8 +725,8 @@ namespace smt {
void setup::setup_r_arith() {
// to disable theory lra
- // m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
- m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
+ m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
+ // m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
}
void setup::setup_mi_arith() {
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 173000fd1..e2b1eb682 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -80,14 +80,11 @@ public:
}
- lar_solver() : m_mpq_lar_core_solver(
- m_settings,
- *this
- ),
- m_status(OPTIMAL),
+ lar_solver() : m_status(OPTIMAL),
m_infeasible_column_index(-1),
m_terms_start_index(1000000),
- m_column_type_function ([this] (unsigned j) {return m_mpq_lar_core_solver.m_column_types()[j];})
+ 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)
{}
void set_propagate_bounds_on_pivoted_rows_mode(bool v) {
diff --git a/src/util/lp/lp_primal_core_solver.h b/src/util/lp/lp_primal_core_solver.h
index e4d869289..e1b7445b0 100644
--- a/src/util/lp/lp_primal_core_solver.h
+++ b/src/util/lp/lp_primal_core_solver.h
@@ -32,21 +32,21 @@ class lp_primal_core_solver:public lp_core_solver_base<T, X> {
public:
// m_sign_of_entering is set to 1 if the entering variable needs
// to grow and is set to -1 otherwise
- unsigned m_column_norm_update_counter;
- T m_enter_price_eps;
- int m_sign_of_entering_delta;
+ unsigned m_column_norm_update_counter;
+ T m_enter_price_eps;
+ int m_sign_of_entering_delta;
vector<breakpoint<X>> m_breakpoints;
binary_heap_priority_queue<X> m_breakpoint_indices_queue;
indexed_vector<T> m_beta; // see Swietanowski working vector beta for column norms
- T m_epsilon_of_reduced_cost;
- vector<T> m_costs_backup;
- T m_converted_harris_eps;
- unsigned m_inf_row_index_for_tableau;
- bool m_bland_mode_tableau;
- int_set m_left_basis_tableau;
- unsigned m_bland_mode_threshold;
- unsigned m_left_basis_repeated;
- vector<unsigned> m_leaving_candidates;
+ T m_epsilon_of_reduced_cost;
+ vector<T> m_costs_backup;
+ T m_converted_harris_eps;
+ unsigned m_inf_row_index_for_tableau;
+ bool m_bland_mode_tableau;
+ int_set m_left_basis_tableau;
+ unsigned m_bland_mode_threshold;
+ unsigned m_left_basis_repeated;
+ vector<unsigned> m_leaving_candidates;
// T m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance);
std::list<unsigned> m_non_basis_list;
void sort_non_basis();
@@ -906,8 +906,8 @@ public:
low_bound_values,
upper_bound_values),
m_epsilon_of_reduced_cost(T(1)/T(10000000)),
- m_bland_mode_threshold(1000),
- m_beta(A.row_count()) {
+ m_beta(A.row_count()),
+ m_bland_mode_threshold(1000) {
if (!(numeric_traits<T>::precise())) {
m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance);
diff --git a/src/util/lp/mps_reader.h b/src/util/lp/mps_reader.h
index 7a5c88f83..da5db6145 100644
--- a/src/util/lp/mps_reader.h
+++ b/src/util/lp/mps_reader.h
@@ -93,12 +93,12 @@ template <typename T, typename X>
class mps_reader {
enum row_type { Cost, Less_or_equal, Greater_or_equal, Equal };
struct bound {
+ T m_low;
+ T m_upper;
bool m_low_is_set;
- T m_low;
bool m_upper_is_set;
- T m_upper;
bool m_value_is_fixed;
- T m_fixed_value;
+ T m_fixed_value;
bool m_free;
// constructor
bound() : m_low(numeric_traits<T>::zero()),
@@ -132,8 +132,8 @@ class mps_reader {
}
};
- std::string m_file_name;
bool m_is_OK;
+ std::string m_file_name;
std::unordered_map<std::string, row *> m_rows;
std::unordered_map<std::string, column *> m_columns;
std::unordered_map<std::string, unsigned> m_names_to_var_index;
@@ -747,7 +747,8 @@ public:
mps_reader(std::string file_name):
m_is_OK(true),
- m_file_name(file_name), m_file_stream(file_name),
+ m_file_name(file_name),
+ m_file_stream(file_name),
m_cost_line_count(0),
m_line_number(0),
m_message_stream(& std::cout) {}