diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index c2bb0800e..fc6e9c3e7 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -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; } diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index 75bd7c333..3e393dc03 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -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'), )) diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 42df22724..ea662f111 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -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(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(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index de7f61469..82af740d0 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -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); } diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 813faba3d..cd280d158 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -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()); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 72fac2371..657775a6a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -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()); }