diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index e127a53d15d..1016c972b2e 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1378,6 +1378,15 @@ namespace lp { return m_mpq_lar_core_solver.column_is_free(j); } + // column is at lower or upper bound, lower and upper bound are different. + // the lower/upper bound is not strict. + // the LP obtained by making the bound strict is infeasible + // -> the column has to be fixed + bool is_fixed_at_bound(column_index const& j) { + NOT_IMPLEMENTED_YET(); + return false; + } + // below is the initialization functionality of lar_solver bool lar_solver::strategy_is_undecided() const { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 10ca16d0a9f..76d8528a0aa 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -365,8 +365,10 @@ class lar_solver : public column_namer { verbose_stream() << i << ": " << get_row(i) << "\n"; } } + + bool is_fixed_at_bound(column_index const& j); - bool is_fixed(column_index const& j) const { return column_is_fixed(j); } + bool is_fixed(column_index const& j) const { return column_is_fixed(j); } inline column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); } bool external_is_used(unsigned) const; void pop(unsigned k); diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 5234e3bf0e3..c213333e0e3 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -163,11 +163,11 @@ struct lp_settings { }; default_lp_resource_limit m_default_resource_limit; - lp_resource_limit* m_resource_limit; + lp_resource_limit* m_resource_limit = nullptr; // used for debug output - std::ostream* m_debug_out; + std::ostream* m_debug_out = nullptr; // used for messages, for example, the computation progress messages - std::ostream* m_message_out; + std::ostream* m_message_out = nullptr; statistics m_stats; random_gen m_rand; @@ -178,40 +178,40 @@ struct lp_settings { unsigned nlsat_delay() const { return m_nlsat_delay; } bool int_run_gcd_test() const { return m_int_run_gcd_test; } bool& int_run_gcd_test() { return m_int_run_gcd_test; } - unsigned reps_in_scaler { 20 }; - int c_partial_pivoting { 10 }; // this is the constant c from page 410 - unsigned depth_of_rook_search { 4 }; - bool using_partial_pivoting { true }; + unsigned reps_in_scaler = 20; + int c_partial_pivoting = 10; // this is the constant c from page 410 + unsigned depth_of_rook_search = 4; + bool using_partial_pivoting = true; - unsigned percent_of_entering_to_check { 5 }; // we try to find a profitable column in a percentage of the columns - bool use_scaling { true }; - unsigned max_number_of_iterations_with_no_improvements { 2000000 }; + unsigned percent_of_entering_to_check = 5; // we try to find a profitable column in a percentage of the columns + bool use_scaling = true; + unsigned max_number_of_iterations_with_no_improvements = 2000000; double time_limit; // the maximum time limit of the total run time in seconds // end of dual section - bool m_bound_propagation { true }; - bool presolve_with_double_solver_for_lar { true }; + bool m_bound_propagation = true; + bool presolve_with_double_solver_for_lar = true; simplex_strategy_enum m_simplex_strategy; - int report_frequency { 1000 }; - bool print_statistics { false }; - unsigned column_norms_update_frequency { 12000 }; - bool scale_with_ratio { true }; - unsigned max_row_length_for_bound_propagation { 300 }; - bool backup_costs { true }; - unsigned column_number_threshold_for_using_lu_in_lar_solver { 4000 }; - unsigned m_int_gomory_cut_period { 4 }; - unsigned m_int_find_cube_period { 4 }; + int report_frequency = 1000; + bool print_statistics = false; + unsigned column_norms_update_frequency = 12000; + bool scale_with_ratio = true; + unsigned max_row_length_for_bound_propagation = 300; + bool backup_costs = true; + unsigned column_number_threshold_for_using_lu_in_lar_solver = 4000; + unsigned m_int_gomory_cut_period = 4; + unsigned m_int_find_cube_period = 4; private: - unsigned m_hnf_cut_period { 4 }; - bool m_int_run_gcd_test { true }; + unsigned m_hnf_cut_period = 4; + bool m_int_run_gcd_test = true; public: - unsigned limit_on_rows_for_hnf_cutter { 75 }; - unsigned limit_on_columns_for_hnf_cutter { 150 }; + unsigned limit_on_rows_for_hnf_cutter = 75; + unsigned limit_on_columns_for_hnf_cutter = 150; private: unsigned m_nlsat_delay; - bool m_enable_hnf { true }; - bool m_print_external_var_name { false }; - bool m_propagate_eqs { false }; + bool m_enable_hnf = true; + bool m_print_external_var_name = false; + bool m_propagate_eqs = false; public: bool print_external_var_name() const { return m_print_external_var_name; } bool propagate_eqs() const { return m_propagate_eqs;} @@ -244,25 +244,12 @@ struct lp_settings { std::ostream* get_debug_ostream() { return m_debug_out; } std::ostream* get_message_ostream() { return m_message_out; } statistics& stats() { return m_stats; } - statistics const& stats() const { return m_stats; } - - - - + statistics const& stats() const { return m_stats; } // the method of lar solver to use - simplex_strategy_enum simplex_strategy() const { - return m_simplex_strategy; - } - - void set_simplex_strategy(simplex_strategy_enum s) { - m_simplex_strategy = s; - } - - - bool use_tableau_rows() const { - return m_simplex_strategy == simplex_strategy_enum::tableau_rows; - } + simplex_strategy_enum simplex_strategy() const { return m_simplex_strategy; } + void set_simplex_strategy(simplex_strategy_enum s) { m_simplex_strategy = s; } + bool use_tableau_rows() const { return m_simplex_strategy == simplex_strategy_enum::tableau_rows; } #ifdef Z3DEBUG static unsigned ddd; // used for debugging diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index bea08011697..f5a10f94215 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1595,8 +1595,10 @@ class theory_lra::imp { CTRACE("arith", is_eq(v1, v2) && n1->get_root() != n2->get_root(), tout << "assuming eq: v" << v1 << " = v" << v2 << "\n";); - if (is_eq(v1, v2) && n1->get_root() != n2->get_root() && th.assume_eq(n1, n2)) + if (is_eq(v1, v2) && n1->get_root() != n2->get_root() && th.assume_eq(n1, n2)) { + ++m_stats.m_assume_eqs; return true; + } } return false; } @@ -1690,13 +1692,12 @@ class theory_lra::imp { switch (m_final_check_idx) { case 0: - if (assume_eqs()) { - ++m_stats.m_assume_eqs; - st = FC_CONTINUE; - } + st = check_lia(); break; case 1: - st = check_lia(); + if (assume_eqs()) + st = FC_CONTINUE; + break; case 2: switch (check_nla()) {