mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

make gcd call in dio optional

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-04-08 16:10:17 -07:00
parent 019da2308e
commit 7ee3415150
6 changed files with 21 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -185,19 +185,19 @@ namespace lp {
}
bool should_gomory_cut() {
bool dio_allows_gomory = !settings().dio_eqs() || settings().dio_enable_gomory_cuts() ||
bool dio_allows_gomory = !settings().dio() || settings().dio_enable_gomory_cuts() ||
m_dio.some_terms_are_ignored();
return dio_allows_gomory && m_number_of_calls % settings().m_int_gomory_cut_period == 0;
}
bool should_solve_dioph_eq() {
return lia.settings().dio_eqs() && (m_number_of_calls % settings().dio_calls_period() == 0);
return lia.settings().dio() && (m_number_of_calls % settings().dio_calls_period() == 0);
}
// HNF
bool should_hnf_cut() {
return (!settings().dio_eqs() || settings().dio_enable_hnf_cuts())
return (!settings().dio() || settings().dio_enable_hnf_cuts())
&& settings().enable_hnf() && m_number_of_calls % settings().hnf_cut_period() == 0;
}

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

@ -2,11 +2,12 @@ def_module_params(module_name='lp',
class_name='lp_params_helper',
description='linear programming parameters',
export=True,
params=(('dio_eqs', BOOL, False, 'use Diophantine equalities'),
params=(('dio', BOOL, False, 'use Diophantine equalities'),
('dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'),
('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_run_gcd', BOOL, True, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'),
))

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

@ -34,11 +34,12 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
report_frequency = p.arith_rep_freq();
m_simplex_strategy = static_cast<lp::simplex_strategy_enum>(p.arith_simplex_strategy());
m_nlsat_delay = p.arith_nl_delay();
m_dio_eqs = lp_p.dio_eqs();
m_dio = lp_p.dio();
m_dio_enable_gomory_cuts = lp_p.dio_cuts_enable_gomory();
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();
m_dio_run_gcd = lp_p.dio_run_gcd();
}

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

@ -218,8 +218,12 @@ public:
void updt_params(params_ref const& p);
bool enable_hnf() const { return m_enable_hnf; }
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; }
bool int_run_gcd_test() const {
if (!m_dio)
return m_int_run_gcd_test;
return m_dio_run_gcd;
}
void set_run_gcd_test(bool v) { m_int_run_gcd_test = v; }
unsigned reps_in_scaler = 20;
int c_partial_pivoting = 10; // this is the constant c from page 410
unsigned depth_of_rook_search = 4;
@ -254,7 +258,7 @@ private:
bool m_enable_hnf = true;
bool m_print_external_var_name = false;
bool m_propagate_eqs = false;
bool m_dio_eqs = false;
bool m_dio = false;
bool m_dio_enable_gomory_cuts = false;
bool m_dio_enable_hnf_cuts = true;
unsigned m_dio_branching_period = 100; // do branching rarely
@ -262,7 +266,7 @@ private:
bool m_dump_bound_lemmas = false;
bool m_dio_ignore_big_nums = false;
unsigned m_dio_calls_period = 4;
bool m_dio_run_gcd = true;
public:
unsigned dio_calls_period() const { return m_dio_calls_period; }
unsigned & dio_calls_period() { return m_dio_calls_period; }
@ -272,9 +276,10 @@ public:
void set_hnf_cut_period(unsigned period) { m_hnf_cut_period = period; }
unsigned random_next() { return m_rand(); }
unsigned random_next(unsigned u ) { return m_rand(u); }
bool dio_eqs() { return m_dio_eqs; }
bool dio_enable_gomory_cuts() const { return m_dio_eqs && m_dio_enable_gomory_cuts; }
bool dio_enable_hnf_cuts() const { return m_dio_eqs && m_dio_enable_hnf_cuts; }
bool dio() { return m_dio; }
bool dio_enable_gomory_cuts() const { return m_dio && m_dio_enable_gomory_cuts; }
bool dio_run_gcd() const { return m_dio && m_dio_run_gcd; }
bool dio_enable_hnf_cuts() const { return m_dio && m_dio_enable_hnf_cuts; }
unsigned dio_branching_period() const { return m_dio_branching_period; }
bool dio_ignore_big_nums() const { return m_dio_ignore_big_nums; }
void set_random_seed(unsigned s) { m_rand.set_seed(s); }

2
src/sat/smt/arith_solver.cpp
View file

@ -35,7 +35,7 @@ namespace arith {
lp().updt_params(ctx.s().params());
lp().settings().set_resource_limit(m_resource_limit);
lp().settings().bound_propagation() = bound_prop_mode::BP_NONE != propagation_mode();
lp().settings().int_run_gcd_test() = get_config().m_arith_gcd_test;
lp().settings().set_run_gcd_test(get_config().m_arith_gcd_test);
lp().settings().set_random_seed(get_config().m_random_seed);
m_lia = alloc(lp::int_solver, *m_solver.get());

2
src/smt/theory_lra.cpp
View file

@ -871,7 +871,7 @@ public:
unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;
lp().set_cut_strategy(branch_cut_ratio);
lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test;
lp().settings().set_run_gcd_test(ctx().get_fparams().m_arith_gcd_test);
lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
m_lia = alloc(lp::int_solver, *m_solver.get());
}