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

cube heuristics: count bail-infeasible SAT escape

Browse source 
int_cube and int_cube_lll both have a secondary success path where
the inner LP becomes infeasible after tightening but, after pop and
move_non_basic_columns_to_bounds, the basic integer variables happen
to be integer-valued; that returned sat without being counted.

Adds two stats:
  arith-cube-success-bail-sat
  arith-lll-cube-success-bail-sat

So 'success' now means the rounding path and 'success-bail-sat'
means the move-to-bounds escape.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-05-15 14:32:44 -07:00
parent 8da9fc9779
commit 66231210a9
3 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/int_cube.cpp
View file

@ -45,7 +45,11 @@ namespace lp {
lra.pop();
lra.move_non_basic_columns_to_bounds();
// it can happen that we found an integer solution here
return !lra.r_basis_has_inf_int()? lia_move::sat: lia_move::undef;
if (!lra.r_basis_has_inf_int()) {
lia.settings().stats().m_cube_success_bail_sat++;
return lia_move::sat;
}
return lia_move::undef;
}
lra.pop();
lra.round_to_integer_solution();

6
src/math/lp/int_cube_lll.cpp
View file

@ -429,7 +429,11 @@ namespace lp {
TRACE(lll_cube, tout << "cannot find a feasible solution\n";);
lra.pop();
lra.move_non_basic_columns_to_bounds();
return !lra.r_basis_has_inf_int() ? lia_move::sat : lia_move::undef;
if (!lra.r_basis_has_inf_int()) {
lia.settings().stats().m_lll_cube_success_bail_sat++;
return lia_move::sat;
}
return lia_move::undef;
}
save_x_J();
lra.pop();

4
src/math/lp/lp_settings.h
View file

@ -112,8 +112,10 @@ struct statistics {
unsigned m_gcd_conflicts = 0;
unsigned m_cube_calls = 0;
unsigned m_cube_success = 0;
unsigned m_cube_success_bail_sat = 0;
unsigned m_lll_cube_calls = 0;
unsigned m_lll_cube_success = 0;
unsigned m_lll_cube_success_bail_sat = 0;
unsigned m_lll_cube_bail_collect = 0;
unsigned m_lll_cube_bail_build = 0;
unsigned m_lll_cube_bail_basis = 0;
@ -160,8 +162,10 @@ struct statistics {
st.update("arith-gcd-conflict", m_gcd_conflicts);
st.update("arith-cube-calls", m_cube_calls);
st.update("arith-cube-success", m_cube_success);
st.update("arith-cube-success-bail-sat", m_cube_success_bail_sat);
st.update("arith-lll-cube-calls", m_lll_cube_calls);
st.update("arith-lll-cube-success", m_lll_cube_success);
st.update("arith-lll-cube-success-bail-sat", m_lll_cube_success_bail_sat);
st.update("arith-lll-cube-bail-collect", m_lll_cube_bail_collect);
st.update("arith-lll-cube-bail-build", m_lll_cube_bail_build);
st.update("arith-lll-cube-bail-basis", m_lll_cube_bail_basis);