mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

ensure assume-eqs is invoked after check-lia statically

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-04-26 11:16:15 -07:00
parent d2e3e4895e
commit ef943347ee
4 changed files with 51 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/lp/lar_solver.cpp
View file

@ -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 {

4
src/math/lp/lar_solver.h
View file

@ -365,8 +365,10 @@ public:
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);

77
src/math/lp/lp_settings.h
View file

@ -163,11 +163,11 @@ private:
};
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 @@ public:
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 @@ public:
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

13
src/smt/theory_lra.cpp
View file

@ -1595,8 +1595,10 @@ public:
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 @@ public:
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()) {