mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-30 04:18:53 +00:00
Code Activity

lp: verbose log of dio_calls_period evolution (-v:2)

Browse source 
Trace dio_calls_period at each change point (conflict reset, undef
double, idle decrease) under IF_VERBOSE level 2, to inspect the
adaptive period controller on long-running instances.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-06-23 08:00:25 -07:00
parent 660ae575ea
commit 294b6ce18a
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -180,6 +180,8 @@ 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";);
return lia_move::conflict;
}
if (r == lia_move::undef) {
@ -188,6 +190,9 @@ 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";);
}
return r;
}
@ -243,6 +248,8 @@ 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";);
}
return ret;
}