mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Code Activity

Randomize should_* decision gates in int_solver

Browse source 
Replace deterministic m_number_of_calls % period gates with
settings().random_next(period) == 0 for should_find_cube,
should_find_lcube, should_solve_dioph_eq and should_hnf_cut,
matching the existing should_gomory_cut approach. This keeps the
same expected 1/period firing rate while avoiding phase-locking
with the search. Removes the now-unused m_number_of_calls member.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-06-19 07:11:43 -07:00
parent a75c860899
commit 029ce10d22
1 changed files with 8 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -34,7 +34,6 @@ namespace lp {
int_solver& lia;
lar_solver& lra;
lar_core_solver& lrac;
unsigned m_number_of_calls = 0;
lar_term m_t; // the term to return in the cut
bool m_upper; // cut is an upper bound
explanation *m_ex; // the conflict explanation
@ -195,7 +194,11 @@ namespace lp {
lp_settings& settings() { return lra.settings(); }
bool should_find_cube() {
return m_number_of_calls % settings().m_int_find_cube_period == 0;
// Draw the decision at random instead of using a fixed "every k-th
// call" modulus, mirroring should_gomory_cut: a deterministic period
// can phase-lock with the search, while randomizing the gate (same
// 1/period expected rate) breaks that resonance.
return settings().random_next(settings().m_int_find_cube_period) == 0;
}
// The largest cube test is throttled exponentially: when the polyhedron
@ -203,7 +206,7 @@ namespace lp {
// later, after more constraints are added, so each failure doubles the
// period and a success resets it.
bool should_find_lcube() {
return settings().lcube() && m_number_of_calls % m_lcube_period == 0;
return settings().lcube() && settings().random_next(m_lcube_period) == 0;
}
lia_move find_lcube() {
@ -229,14 +232,14 @@ namespace lp {
}
bool should_solve_dioph_eq() {
return lia.settings().dio() && (m_number_of_calls % settings().dio_calls_period() == 0);
return lia.settings().dio() && (settings().random_next(settings().dio_calls_period()) == 0);
}
// HNF
bool should_hnf_cut() {
return (!settings().dio() || settings().dio_enable_hnf_cuts())
&& settings().enable_hnf() && m_number_of_calls % settings().hnf_cut_period() == 0;
&& settings().enable_hnf() && settings().random_next(settings().hnf_cut_period()) == 0;
}
lia_move hnf_cut() {
@ -269,7 +272,6 @@ namespace lp {
if (settings().get_cancel_flag())
return lia_move::undef;
++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();