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

add parameter m_dio_calls_period

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-04-04 19:56:13 -07:00 • committed by Lev Nachmanson
parent ae97ee09d9
commit 8db9f52386
5 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/dioph_eq.cpp
View file

@ -2333,6 +2333,8 @@ namespace lp {
ret = branching_on_undef();
m_max_of_branching_iterations = (unsigned)m_max_of_branching_iterations / 2;
if (ret == lia_move::undef)
lra.settings().dio_calls_period() *= 2;
return ret;
}

4
src/math/lp/int_solver.cpp
View file

@ -41,7 +41,6 @@ namespace lp {
mpq m_k; // the right side of the cut
hnf_cutter m_hnf_cutter;
unsigned m_hnf_cut_period;
unsigned m_dioph_eq_period;
dioph_eq m_dio;
int_gcd_test m_gcd;
@ -51,7 +50,6 @@ namespace lp {
imp(int_solver& lia): lia(lia), lra(lia.lra), lrac(lia.lrac), m_hnf_cutter(lia), m_dio(lia), m_gcd(lia) {
m_hnf_cut_period = settings().hnf_cut_period();
m_dioph_eq_period = settings().m_dioph_eq_period;
}
bool has_lower(unsigned j) const {
@ -193,7 +191,7 @@ namespace lp {
}
bool should_solve_dioph_eq() {
return lia.settings().dio_eqs() && m_number_of_calls % m_dioph_eq_period == 0;
return lia.settings().dio_eqs() && (m_number_of_calls % settings().dio_calls_period() == 0);
}
// HNF

1
src/math/lp/lp_params_helper.pyg
View file

@ -7,5 +7,6 @@ def_module_params(module_name='lp',
('dio_cuts_enable_gomory', BOOL, False, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
('dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, only relevant when dioph_eq is true'),
('dio_calls_period', UINT, 1, 'Period of calling the Diophantine handler in the final_check()'),
))

1
src/math/lp/lp_settings.cpp
View file

@ -39,4 +39,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
m_dio_enable_hnf_cuts = lp_p.dio_cuts_enable_hnf();
m_dio_branching_period = lp_p.dio_branching_period();m_dump_bound_lemmas = p.arith_dump_bound_lemmas();
m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums();
m_dio_calls_period = lp_p.dio_calls_period();
}

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

@ -243,7 +243,6 @@ public:
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;
unsigned m_dioph_eq_period = 1;
private:
unsigned m_hnf_cut_period = 4;
bool m_int_run_gcd_test = true;
@ -262,8 +261,11 @@ private:
unsigned m_dio_report_branch_with_term_tigthening_period = 10000000; // period of reporting the branch with term tigthening
bool m_dump_bound_lemmas = false;
bool m_dio_ignore_big_nums = false;
unsigned m_dio_calls_period = 1;
public:
unsigned dio_calls_period() const { return m_dio_calls_period; }
unsigned & dio_calls_period() { return m_dio_calls_period; }
bool print_external_var_name() const { return m_print_external_var_name; }
bool propagate_eqs() const { return m_propagate_eqs;}
unsigned hnf_cut_period() const { return m_hnf_cut_period; }