From e9202913935e84511fc890a8044e295c5da1f124 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 11 Feb 2025 10:45:36 -1000 Subject: [PATCH] fixing the default parameters of dio and rename m_gomory_cuts to m_cuts Signed-off-by: Lev Nachmanson --- src/math/lp/lp_api.h | 4 ++-- src/math/lp/lp_settings.cpp | 1 + src/math/lp/lp_settings.h | 2 +- src/sat/smt/arith_solver.cpp | 2 +- src/smt/theory_lra.cpp | 1 - 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h index 325bc980b..778a8b7ac 100644 --- a/src/math/lp/lp_api.h +++ b/src/math/lp/lp_api.h @@ -105,7 +105,7 @@ namespace lp_api { unsigned m_bound_propagations2; unsigned m_assert_diseq; unsigned m_assert_eq; - unsigned m_gomory_cuts; + unsigned m_cuts; unsigned m_assume_eqs; unsigned m_branch; unsigned m_bv_axioms; @@ -126,7 +126,7 @@ namespace lp_api { st.update("arith-bound-propagations-cheap", m_bound_propagations2); st.update("arith-diseq", m_assert_diseq); st.update("arith-eq", m_assert_eq); - st.update("arith-gomory-cuts", m_gomory_cuts); + st.update("arith-cuts", m_cuts); st.update("arith-assume-eqs", m_assume_eqs); st.update("arith-branch", m_branch); st.update("arith-bv-axioms", m_bv_axioms); diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 32686dd0b..cd82e2ed9 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -33,5 +33,6 @@ void lp::lp_settings::updt_params(params_ref const& _p) { m_simplex_strategy = static_cast(p.arith_simplex_strategy()); m_nlsat_delay = p.arith_nl_delay(); m_dio_eqs = p.arith_lp_dio_eqs(); + m_dio_enable_gomory_cuts = p.arith_lp_dio_cuts_enable_gomory(); m_dio_branching_period = p.arith_lp_dio_branching_period(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 17733bb05..a2fcce9ba 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -251,7 +251,7 @@ private: bool m_print_external_var_name = false; bool m_propagate_eqs = false; bool m_dio_eqs = false; - bool m_dio_enable_gomory_cuts = true; + bool m_dio_enable_gomory_cuts = false; bool m_dio_enable_hnf_cuts = true; unsigned m_dio_branching_period = 100; // do branching rarere diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 3efdfec4a..813faba3d 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1192,7 +1192,7 @@ namespace arith { } case lp::lia_move::cut: { TRACE("arith", tout << "cut\n";); - ++m_stats.m_gomory_cuts; + ++m_stats.m_cuts; // m_explanation implies term <= k reset_evidence(); for (auto ev : m_explanation) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 20fb35a0b..ec83cc0d1 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1911,7 +1911,6 @@ public: if (ctx().get_fparams().m_arith_ignore_int) return FC_GIVEUP; TRACE("arith", tout << "cut\n";); - ++m_stats.m_gomory_cuts; // m_explanation implies term <= k reset_evidence(); for (auto ev : m_explanation) {