mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-30 21:57:46 +00:00
Code Activity

Revert "try fixed int patch period"

Browse source 
This reverts commit 3e2027ec11.
This commit is contained in:
Lev Nachmanson 2026-02-07 10:45:15 -10:00
parent 013172d25c
commit 73696725e4
3 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -54,7 +54,6 @@ namespace lp {
m_hnf_cut_period = settings().hnf_cut_period(); m_hnf_cut_period = settings().hnf_cut_period();
m_initial_dio_calls_period = settings().dio_calls_period(); m_initial_dio_calls_period = settings().dio_calls_period();
m_patch_period = settings().m_int_patch_period; m_patch_period = settings().m_int_patch_period;
SASSERT(m_patch_period > 0);
} }
bool has_lower(unsigned j) const { bool has_lower(unsigned j) const {
@ -160,7 +159,8 @@ namespace lp {
} }
bool should_patch() { bool should_patch() {
return m_number_of_calls % m_patch_period == 0; // period == 0 means no throttling (old behavior)
return settings().m_int_patch_period == 0 || m_number_of_calls % m_patch_period == 0;
} }
lia_move patch_basic_columns() { lia_move patch_basic_columns() {
@ -172,8 +172,12 @@ namespace lp {
patch_basic_column(j); patch_basic_column(j);
if (!lra.has_inf_int()) { if (!lra.has_inf_int()) {
lia.settings().stats().m_patches_success++; lia.settings().stats().m_patches_success++;
m_patch_period = std::max(1u, settings().m_int_patch_period);
return lia_move::sat; return lia_move::sat;
} }
// Only throttle if enabled (period > 0)
if (settings().m_int_patch_period > 0 && m_patch_period < 16)
m_patch_period *= 2;
return lia_move::undef; return lia_move::undef;
} }

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

@ -9,6 +9,6 @@ def_module_params(module_name='lp',
('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, 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()'), ('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'), ('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'),
('int_patch_period', UINT, 1, 'Skip int_patch_period - 1 calls and then call the patching'), ('int_patch_period', UINT, 0, 'Period for patching integer columns (0 = no throttling, 1 = throttle adaptively)'),
)) ))

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

@ -239,7 +239,7 @@ public:
unsigned column_number_threshold_for_using_lu_in_lar_solver = 4000; unsigned column_number_threshold_for_using_lu_in_lar_solver = 4000;
unsigned m_int_gomory_cut_period = 4; unsigned m_int_gomory_cut_period = 4;
unsigned m_int_find_cube_period = 4; unsigned m_int_find_cube_period = 4;
unsigned m_int_patch_period = 1; unsigned m_int_patch_period = 0;
private: private:
unsigned m_hnf_cut_period = 4; unsigned m_hnf_cut_period = 4;
bool m_int_run_gcd_test = true; bool m_int_run_gcd_test = true;