diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index c8a1d1da33..30674a5f6d 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -180,8 +180,9 @@ namespace lp { lia.settings().dio_calls_period() = m_initial_dio_calls_period; lia.settings().dio_enable_gomory_cuts() = false; lia.settings().set_run_gcd_test(false); - IF_VERBOSE(2, verbose_stream() << "dio_period: call " << m_number_of_calls - << " conflict reset period=" << lia.settings().dio_calls_period() << "\n";); + if (lia.settings().dio_calls_period_trace()) + verbose_stream() << "dio_period: call " << m_number_of_calls + << " conflict reset period=" << lia.settings().dio_calls_period() << "\n"; return lia_move::conflict; } if (r == lia_move::undef) { @@ -190,14 +191,29 @@ namespace lp { lia.settings().dio_enable_gomory_cuts() = true; lia.settings().set_run_gcd_test(true); } - IF_VERBOSE(2, verbose_stream() << "dio_period: call " << m_number_of_calls - << " undef double period=" << lia.settings().dio_calls_period() - << (lia.settings().dio_enable_gomory_cuts() ? " (gomory+gcd on)" : "") << "\n";); + if (lia.settings().dio_calls_period_trace()) + verbose_stream() << "dio_period: call " << m_number_of_calls + << " undef double period=" << lia.settings().dio_calls_period() + << (lia.settings().dio_enable_gomory_cuts() ? " (gomory+gcd on)" : "") << "\n"; } return r; } lp_settings& settings() { return lra.settings(); } + + void trace_hammer(char const* name, lia_move r) { + if (r == lia_move::undef || !settings().dio_calls_period_trace()) + return; + char const* res = + r == lia_move::sat ? "sat" : + r == lia_move::branch ? "branch" : + r == lia_move::cut ? "cut" : + r == lia_move::conflict ? "conflict" : + r == lia_move::continue_with_check ? "continue" : + r == lia_move::cancelled ? "cancelled" : "undef"; + verbose_stream() << "hammer: call " << m_number_of_calls + << " " << name << " -> " << res << "\n"; + } // Decide whether a periodic heuristic fires on this call. When // random_hammers is enabled the gate is drawn at random with the same @@ -248,8 +264,9 @@ namespace lp { unsigned dec = settings().dio_calls_period_decrease(); unsigned& period = lia.settings().dio_calls_period(); period = period > m_initial_dio_calls_period + dec ? period - dec : m_initial_dio_calls_period; - IF_VERBOSE(2, verbose_stream() << "dio_period: call " << m_number_of_calls - << " idle decrease period=" << period << "\n";); + if (settings().dio_calls_period_trace()) + verbose_stream() << "dio_period: call " << m_number_of_calls + << " idle decrease period=" << period << "\n"; } return ret; } @@ -285,6 +302,7 @@ namespace lp { if (m_gcd.should_apply() || (settings().dio() && m_dio.some_terms_are_ignored())) r = m_gcd(); + trace_hammer("gcd", r); check_return_helper pc(lra); @@ -293,13 +311,14 @@ namespace lp { ++m_number_of_calls; if (r == lia_move::undef) r = patch_basic_columns(); - if (r == lia_move::undef && should_find_cube()) r = int_cube(lia)(); - if (r == lia_move::undef && should_find_lcube()) r = find_lcube(); + trace_hammer("patch", r); + if (r == lia_move::undef && should_find_cube()) { r = int_cube(lia)(); trace_hammer("cube", r); } + if (r == lia_move::undef && should_find_lcube()) { r = find_lcube(); trace_hammer("lcube", r); } if (r == lia_move::undef) lra.move_non_basic_columns_to_bounds(); - if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut(); - if (r == lia_move::undef && should_gomory_cut()) r = gomory(lia).get_gomory_cuts(2); + if (r == lia_move::undef && should_hnf_cut()) { r = hnf_cut(); trace_hammer("hnf", r); } if (r == lia_move::undef && should_solve_dioph_eq()) r = solve_dioph_eq(); - if (r == lia_move::undef) r = int_branch(lia)(); + if (r == lia_move::undef && should_gomory_cut()) { r = gomory(lia).get_gomory_cuts(2); trace_hammer("gomory", r); } + if (r == lia_move::undef) { r = int_branch(lia)(); trace_hammer("branch", r); } if (settings().get_cancel_flag()) r = lia_move::undef; return r; } diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index c3d109f80a..74ad1b1ad6 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -9,6 +9,7 @@ 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_calls_period', UINT, 1, 'Period of calling the Diophantine handler in the final_check()'), ('dio_calls_period_decrease', UINT, 2, 'Amount by which dio_calls_period is decreased on each final_check() call where the Diophantine handler is not triggered, until it returns to its initial value'), + ('dio_calls_period_trace', BOOL, False, 'Trace the evolution of dio_calls_period (the Diophantine call guard) to the verbose stream at each change point: conflict reset, undef doubling, and idle decrease'), ('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'), ('lcube', BOOL, True, 'use the largest cube test for integer feasibility'), ('lcube_flips', UINT, 16, 'maximal number of coordinate flips when repairing the rounded largest cube center, only relevant when lcube is true'), diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 9ffa9bb149..9a8acadf6a 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -43,6 +43,7 @@ void lp::lp_settings::updt_params(params_ref const& _p) { m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums(); m_dio_calls_period = lp_p.dio_calls_period(); m_dio_calls_period_decrease = lp_p.dio_calls_period_decrease(); + m_dio_calls_period_trace = lp_p.dio_calls_period_trace(); m_dio_run_gcd = lp_p.dio_run_gcd(); m_random_hammers = lp_p.random_hammers(); m_lcube = lp_p.lcube(); diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index a50c3ba8cd..667223a867 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -264,6 +264,7 @@ private: bool m_dio_ignore_big_nums = false; unsigned m_dio_calls_period = 4; unsigned m_dio_calls_period_decrease = 2; + bool m_dio_calls_period_trace = false; bool m_dio_run_gcd = true; bool m_random_hammers = true; bool m_lcube = true; @@ -275,6 +276,8 @@ public: unsigned & dio_calls_period() { return m_dio_calls_period; } unsigned dio_calls_period_decrease() const { return m_dio_calls_period_decrease; } unsigned & dio_calls_period_decrease() { return m_dio_calls_period_decrease; } + bool dio_calls_period_trace() const { return m_dio_calls_period_trace; } + bool & dio_calls_period_trace() { return m_dio_calls_period_trace; } bool random_hammers() const { return m_random_hammers; } bool & random_hammers() { return m_random_hammers; } bool print_external_var_name() const { return m_print_external_var_name; }