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

fix build warnings part 7, disable LRA for regression t201.smt2

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-11 09:28:59 -07:00
parent 9b3e2a9afe
commit 7e004fe331
4 changed files with 25 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_setup.cpp
View file

@ -725,8 +725,8 @@ namespace smt {
void setup::setup_r_arith() { void setup::setup_r_arith() {
// to disable theory lra // to disable theory lra
// m_context.register_plugin(alloc(smt::theory_mi_arith, 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)); // m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
} }
void setup::setup_mi_arith() { void setup::setup_mi_arith() {

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

@ -80,14 +80,11 @@ public:
} }
lar_solver() : m_mpq_lar_core_solver( lar_solver() : m_status(OPTIMAL),
m_settings,
*this
),
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_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) { void set_propagate_bounds_on_pivoted_rows_mode(bool v) {

28
src/util/lp/lp_primal_core_solver.h
View file

@ -32,21 +32,21 @@ class lp_primal_core_solver:public lp_core_solver_base<T, X> {
public: public:
// m_sign_of_entering is set to 1 if the entering variable needs // m_sign_of_entering is set to 1 if the entering variable needs
// to grow and is set to -1 otherwise // to grow and is set to -1 otherwise
unsigned m_column_norm_update_counter; unsigned m_column_norm_update_counter;
T m_enter_price_eps; T m_enter_price_eps;
int m_sign_of_entering_delta; int m_sign_of_entering_delta;
vector<breakpoint<X>> m_breakpoints; vector<breakpoint<X>> m_breakpoints;
binary_heap_priority_queue<X> m_breakpoint_indices_queue; binary_heap_priority_queue<X> m_breakpoint_indices_queue;
indexed_vector<T> m_beta; // see Swietanowski working vector beta for column norms indexed_vector<T> m_beta; // see Swietanowski working vector beta for column norms
T m_epsilon_of_reduced_cost; T m_epsilon_of_reduced_cost;
vector<T> m_costs_backup; vector<T> m_costs_backup;
T m_converted_harris_eps; T m_converted_harris_eps;
unsigned m_inf_row_index_for_tableau; unsigned m_inf_row_index_for_tableau;
bool m_bland_mode_tableau; bool m_bland_mode_tableau;
int_set m_left_basis_tableau; int_set m_left_basis_tableau;
unsigned m_bland_mode_threshold; unsigned m_bland_mode_threshold;
unsigned m_left_basis_repeated; unsigned m_left_basis_repeated;
vector<unsigned> m_leaving_candidates; vector<unsigned> m_leaving_candidates;
// T m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance); // T m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance);
std::list<unsigned> m_non_basis_list; std::list<unsigned> m_non_basis_list;
void sort_non_basis(); void sort_non_basis();
@ -906,8 +906,8 @@ public:
low_bound_values, low_bound_values,
upper_bound_values), upper_bound_values),
m_epsilon_of_reduced_cost(T(1)/T(10000000)), 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())) { if (!(numeric_traits<T>::precise())) {
m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance); m_converted_harris_eps = convert_struct<T, double>::convert(this->m_settings.harris_feasibility_tolerance);

11
src/util/lp/mps_reader.h
View file

@ -93,12 +93,12 @@ template <typename T, typename X>
class mps_reader { class mps_reader {
enum row_type { Cost, Less_or_equal, Greater_or_equal, Equal }; enum row_type { Cost, Less_or_equal, Greater_or_equal, Equal };
struct bound { struct bound {
T m_low;
T m_upper;
bool m_low_is_set; bool m_low_is_set;
T m_low;
bool m_upper_is_set; bool m_upper_is_set;
T m_upper;
bool m_value_is_fixed; bool m_value_is_fixed;
T m_fixed_value; T m_fixed_value;
bool m_free; bool m_free;
// constructor // constructor
bound() : m_low(numeric_traits<T>::zero()), bound() : m_low(numeric_traits<T>::zero()),
@ -132,8 +132,8 @@ class mps_reader {
} }
}; };
std::string m_file_name;
bool m_is_OK; bool m_is_OK;
std::string m_file_name;
std::unordered_map<std::string, row *> m_rows; std::unordered_map<std::string, row *> m_rows;
std::unordered_map<std::string, column *> m_columns; std::unordered_map<std::string, column *> m_columns;
std::unordered_map<std::string, unsigned> m_names_to_var_index; std::unordered_map<std::string, unsigned> m_names_to_var_index;
@ -747,7 +747,8 @@ public:
mps_reader(std::string file_name): mps_reader(std::string file_name):
m_is_OK(true), 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_cost_line_count(0),
m_line_number(0), m_line_number(0),
m_message_stream(& std::cout) {} m_message_stream(& std::cout) {}