mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-03 09:50:23 +00:00
Code Activity

adjust the frequency of dio calls

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-05-14 08:17:39 -07:00
parent 15a3818fce
commit f680242620
3 changed files with 15 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2085,15 +2085,6 @@ namespace lp {
}
while (ret == lia_move::continue_with_check);
if (ret != lia_move::undef)
return ret;
if (ret == lia_move::undef) {
lra.settings().dio_calls_period() *= 2;
if (lra.settings().dio_calls_period() >= 16) {
lra.settings().dio_enable_gomory_cuts() = true;
lra.settings().set_run_gcd_test(true);
}
}
return ret;
}

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

@ -43,13 +43,15 @@ namespace lp {
unsigned m_hnf_cut_period;
dioph_eq m_dio;
int_gcd_test m_gcd;
unsigned m_initial_dio_calls_period;
bool column_is_int_inf(unsigned j) const {
return lra.column_is_int(j) && (!lia.value_is_int(j));
}
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_initial_dio_calls_period = settings().dio_calls_period();
}
bool has_lower(unsigned j) const {
@ -173,8 +175,18 @@ namespace lp {
if (r == lia_move::conflict) {
m_dio.explain(*this->m_ex);
lia.settings().dio_calls_period() = m_initial_dio_calls_period;
lia.settings().dio_enable_gomory_cuts() = false;
lia.settings().set_run_gcd_test(false);
return lia_move::conflict;
}
}
if (r == lia_move::undef) {
lia.settings().dio_calls_period() *= 2;
if (lra.settings().dio_calls_period() >= 16) {
lia.settings().dio_enable_gomory_cuts() = true;
lia.settings().set_run_gcd_test(true);
}
}
return r;
}

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

@ -7,7 +7,7 @@ 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, 4, 'Period of calling the Diophantine handler in the final_check()'),
('dio_calls_period', UINT, 1, 'Period of calling the Diophantine handler in the final_check()'),
('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'),
))