mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-04 22:36:10 +00:00
Code Activity

lp: linearly recover dio_calls_period on missed dio calls

Browse source 
Increment dio_calls_period by one on each call where the diophantine
solver is not triggered (until it returns to the initial period),
gradually re-enabling dio solving after it was backed off, instead of
leaving the period at its doubled value indefinitely.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-06-21 14:53:55 -07:00
parent 6e5639f79d
commit 9f290ca0b8
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -238,7 +238,10 @@ namespace lp {
} }
bool should_solve_dioph_eq() { bool should_solve_dioph_eq() {
return lia.settings().dio() && hit_period(settings().dio_calls_period()); bool ret = lia.settings().dio() && hit_period(settings().dio_calls_period());
if (!ret && lia.settings().dio_calls_period() > m_initial_dio_calls_period)
lia.settings().dio_calls_period() ++;
return ret;
} }
// HNF // HNF