mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

fallback to Gomory cuts and gcd conflicts if dio fails

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-04-21 17:10:32 -07:00
parent cc1bb0a255
commit a1673f2bdd
3 changed files with 7 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2038,8 +2038,13 @@ namespace lp {
if (ret != lia_move::undef) if (ret != lia_move::undef)
return ret; return ret;
if (ret == lia_move::undef) if (ret == lia_move::undef) {
lra.settings().dio_calls_period() *= 2; lra.settings().dio_calls_period() *= 2;
if (lra.settings().dio_calls_period() >= 16) {
lra.settings().dio_enable_gomory_cuts() = true;
lra.settings().set_run_gcd_test(true);
}
}
return ret; return ret;
} }

1
src/math/lp/lp_settings.cpp
View file

@ -37,7 +37,6 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
m_dio = lp_p.dio(); m_dio = lp_p.dio();
m_dio_enable_gomory_cuts = lp_p.dio_cuts_enable_gomory(); m_dio_enable_gomory_cuts = lp_p.dio_cuts_enable_gomory();
m_dio_enable_hnf_cuts = lp_p.dio_cuts_enable_hnf(); m_dio_enable_hnf_cuts = lp_p.dio_cuts_enable_hnf();
m_dio_branching_period = lp_p.dio_branching_period();
m_dump_bound_lemmas = p.arith_dump_bound_lemmas(); m_dump_bound_lemmas = p.arith_dump_bound_lemmas();
m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums(); m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums();
m_dio_calls_period = lp_p.dio_calls_period(); m_dio_calls_period = lp_p.dio_calls_period();

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

@ -133,13 +133,7 @@ struct statistics {
unsigned m_fixed_eqs = 0; unsigned m_fixed_eqs = 0;
unsigned m_dio_calls = 0; unsigned m_dio_calls = 0;
unsigned m_dio_tighten_conflicts = 0; unsigned m_dio_tighten_conflicts = 0;
unsigned m_dio_branch_iterations= 0;
unsigned m_dio_branching_depth = 0;
unsigned m_dio_branch_from_proofs = 0;
unsigned m_dio_branching_infeasibles = 0;
unsigned m_dio_rewrite_conflicts = 0; unsigned m_dio_rewrite_conflicts = 0;
unsigned m_dio_branching_sats = 0;
unsigned m_dio_branching_conflicts = 0;
unsigned m_bounds_tightening_conflicts = 0; unsigned m_bounds_tightening_conflicts = 0;
unsigned m_bounds_tightenings = 0; unsigned m_bounds_tightenings = 0;
::statistics m_st = {}; ::statistics m_st = {};
@ -176,14 +170,7 @@ struct statistics {
st.update("arith-bounds-improvements", m_nla_bounds_improvements); st.update("arith-bounds-improvements", m_nla_bounds_improvements);
st.update("arith-dio-calls", m_dio_calls); st.update("arith-dio-calls", m_dio_calls);
st.update("arith-dio-tighten-conflicts", m_dio_tighten_conflicts); st.update("arith-dio-tighten-conflicts", m_dio_tighten_conflicts);
st.update("arith-dio-branch-iterations", m_dio_branch_iterations);
st.update("arith-dio-branch-depths", m_dio_branching_depth);
st.update("arith-dio-branch-from-proofs", m_dio_branch_from_proofs);
st.update("arith-dio-branching-infeasibles", m_dio_branching_infeasibles);
st.update("arith-dio-rewrite-conflicts", m_dio_rewrite_conflicts); st.update("arith-dio-rewrite-conflicts", m_dio_rewrite_conflicts);
st.update("arith-dio-branching-sats", m_dio_branching_sats);
st.update("arith-dio-branching-depth", m_dio_branching_depth);
st.update("arith-dio-branching-conflicts", m_dio_branching_conflicts);
st.update("arith-bounds-tightening-conflicts", m_bounds_tightening_conflicts); st.update("arith-bounds-tightening-conflicts", m_bounds_tightening_conflicts);
st.update("arith-bounds-tightenings", m_bounds_tightenings); st.update("arith-bounds-tightenings", m_bounds_tightenings);
st.copy(m_st); st.copy(m_st);
@ -261,8 +248,6 @@ private:
bool m_dio = false; bool m_dio = false;
bool m_dio_enable_gomory_cuts = false; bool m_dio_enable_gomory_cuts = false;
bool m_dio_enable_hnf_cuts = true; bool m_dio_enable_hnf_cuts = true;
unsigned m_dio_branching_period = 100; // do branching rarely
unsigned m_dio_report_branch_with_term_tigthening_period = 10000000; // period of reporting the branch with term tigthening
bool m_dump_bound_lemmas = false; bool m_dump_bound_lemmas = false;
bool m_dio_ignore_big_nums = false; bool m_dio_ignore_big_nums = false;
unsigned m_dio_calls_period = 4; unsigned m_dio_calls_period = 4;
@ -277,13 +262,12 @@ public:
unsigned random_next() { return m_rand(); } unsigned random_next() { return m_rand(); }
unsigned random_next(unsigned u ) { return m_rand(u); } unsigned random_next(unsigned u ) { return m_rand(u); }
bool dio() { return m_dio; } bool dio() { return m_dio; }
bool & dio_enable_gomory_cuts() { return m_dio_enable_gomory_cuts; }
bool dio_enable_gomory_cuts() const { return m_dio && m_dio_enable_gomory_cuts; } bool dio_enable_gomory_cuts() const { return m_dio && m_dio_enable_gomory_cuts; }
bool dio_run_gcd() const { return m_dio && m_dio_run_gcd; } bool dio_run_gcd() const { return m_dio && m_dio_run_gcd; }
bool dio_enable_hnf_cuts() const { return m_dio && m_dio_enable_hnf_cuts; } bool dio_enable_hnf_cuts() const { return m_dio && m_dio_enable_hnf_cuts; }
unsigned dio_branching_period() const { return m_dio_branching_period; }
bool dio_ignore_big_nums() const { return m_dio_ignore_big_nums; } bool dio_ignore_big_nums() const { return m_dio_ignore_big_nums; }
void set_random_seed(unsigned s) { m_rand.set_seed(s); } void set_random_seed(unsigned s) { m_rand.set_seed(s); }
unsigned dio_report_branch_with_term_tigthening_period() const { return m_dio_report_branch_with_term_tigthening_period; }
bool bound_progation() const { bool bound_progation() const {
return m_bound_propagation; return m_bound_propagation;
} }