From 0728b81e9e272848abcef628c965f9c8ee1f408e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 27 Dec 2023 08:33:51 -1000 Subject: [PATCH] add parameter lp_settings.m_gomory_simplify --- src/math/lp/gomory.cpp | 2 +- src/math/lp/int_solver.cpp | 2 +- src/math/lp/lp_settings.cpp | 1 + src/math/lp/lp_settings.h | 2 ++ src/smt/params/smt_params_helper.pyg | 1 + 5 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 130ba631e..f5331ea05 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -328,7 +328,7 @@ public: if (m_t.is_empty()) return report_conflict_from_gomory_cut(); TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t.coeffs_as_vector(), tout << "gomory cut: "); tout << " >= " << m_k << std::endl;); - if (some_int_columns) + if (lia.lra.settings().m_gomory_simplify && some_int_columns) simplify_inequality(); m_dep = nullptr; diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index bf0ae64dd..5c480cbb3 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -198,7 +198,7 @@ namespace lp { if (r == lia_move::undef) lra.move_non_basic_columns_to_bounds(); if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut(); - if (r == lia_move::undef && should_gomory_cut()) r = gomory(*this).get_gomory_cuts(1); + if (r == lia_move::undef && should_gomory_cut()) r = gomory(*this).get_gomory_cuts(2); if (r == lia_move::undef) r = int_branch(*this)(); if (settings().get_cancel_flag()) r = lia_move::undef; diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index b72b837fd..71193914f 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -32,4 +32,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) { report_frequency = p.arith_rep_freq(); m_simplex_strategy = static_cast(p.arith_simplex_strategy()); m_nlsat_delay = p.arith_nl_delay(); + m_gomory_simplify = p.arith_gomory_simplify(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index a0cb485b5..fef30cb6d 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -187,6 +187,7 @@ private: random_gen m_rand; public: + bool m_gomory_simplify = false; void updt_params(params_ref const& p); bool enable_hnf() const { return m_enable_hnf; } unsigned nlsat_delay() const { return m_nlsat_delay; } @@ -214,6 +215,7 @@ public: bool backup_costs = true; unsigned column_number_threshold_for_using_lu_in_lar_solver = 4000; unsigned m_int_gomory_cut_period = 4; + bool m_gomory_simpliy = false; unsigned m_int_find_cube_period = 4; private: unsigned m_hnf_cut_period = 4; diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 455dd9240..8ae679e43 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -84,6 +84,7 @@ def_module_params(module_name='smt', ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'), ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), + ('arith.gomory_simplify', BOOL, False, 'simplify gomory term'), ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'), ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),