diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 9e9d1add14..1144922bfb 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -63,6 +63,7 @@ namespace lp { unsigned_vector m_row_bounds_to_replay; u_dependency_manager m_dependencies; svector m_tmp_dependencies; + ptr_vector m_tmp_witnesses; u_dependency* m_crossed_bounds_deps = nullptr; lpvar m_crossed_bounds_column = null_lpvar; @@ -1132,6 +1133,32 @@ namespace lp { ex.push_back(ci); } + // Linearize the bound witnesses of all fixed columns in the row together, so the + // mark bits walk each dependency sub-DAG shared between columns only once. + // When lp.batch_explain_fixed_in_row is disabled, fall back to explaining each + // fixed column independently (the pre-batching behavior). + void lar_solver::explain_fixed_in_row(unsigned row, explanation& ex) { + if (!settings().batch_explain_fixed_in_row()) { + for (auto const& c : get_row(row)) + if (column_is_fixed(c.var())) + explain_fixed_column(c.var(), ex); + return; + } + auto& witnesses = m_imp->m_tmp_witnesses; + witnesses.reset(); + for (auto const& c : get_row(row)) { + if (!column_is_fixed(c.var())) + continue; + const column& ul = m_imp->m_columns[c.var()]; + witnesses.push_back(ul.lower_bound_witness()); + witnesses.push_back(ul.upper_bound_witness()); + } + m_imp->m_tmp_dependencies.reset(); + m_imp->m_dependencies.linearize(witnesses, m_imp->m_tmp_dependencies); + for (auto ci : m_imp->m_tmp_dependencies) + ex.push_back(ci); + } + void lar_solver::remove_fixed_vars_from_base() { // this will allow to disable and restore the tracking of the touched rows flet f(get_core_solver().m_r_solver.m_touched_rows, nullptr); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 79c729e5d1..4588f1772f 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -521,6 +521,7 @@ public: } void explain_fixed_column(unsigned j, explanation& ex); + void explain_fixed_in_row(unsigned row, explanation& ex); u_dependency* join_deps(u_dependency* a, u_dependency *b) { return dep_manager().mk_join(a, b); } const constraint_set & constraints() const; void push(); diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 2568c51fbd..3df2fbf741 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -248,22 +248,16 @@ public: void explain_fixed_in_row(unsigned row, explanation& ex) { TRACE(eq, tout << lp().get_row(row) << std::endl); - for (const auto& c : lp().get_row(row)) - if (lp().column_is_fixed(c.var())) - lp().explain_fixed_column(c.var(), ex); + lp().explain_fixed_in_row(row, ex); } unsigned explain_fixed_in_row_and_get_base(unsigned row, explanation& ex) { - unsigned base = UINT_MAX; TRACE(eq, tout << lp().get_row(row) << std::endl); - for (const auto& c : lp().get_row(row)) { - if (lp().column_is_fixed(c.var())) { - lp().explain_fixed_column(c.var(), ex); - } - else if (lp().is_base(c.var())) { + lp().explain_fixed_in_row(row, ex); + unsigned base = UINT_MAX; + for (const auto& c : lp().get_row(row)) + if (!lp().column_is_fixed(c.var()) && lp().is_base(c.var())) base = c.var(); - } - } return base; } diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index 29a10c2d52..89c9730bc0 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -15,5 +15,6 @@ def_module_params(module_name='lp', ('lcube_flips', UINT, 16, 'maximal number of coordinate flips when repairing the rounded largest cube center, only relevant when lcube is true'), ('int_hammer_period', UINT, 4, 'period (in final_check calls) for the integer cut/cube heuristics (find_cube, hnf, gomory); a smaller value calls them more often'), ('random_hammers', BOOL, True, 'draw the periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio) at random with the same 1/period rate instead of a deterministic every-k-th-call modulus'), + ('batch_explain_fixed_in_row', BOOL, True, 'linearize the bound witnesses of all fixed columns in a row in a single dependency pass (de-duplicating shared sub-DAGs) instead of explaining each fixed column independently'), )) diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index affc299788..14e60a5b9f 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -46,6 +46,7 @@ void lp::lp_settings::updt_params(params_ref const& _p) { m_dio_calls_period_decrease = lp_p.dio_calls_period_decrease(); m_dio_run_gcd = lp_p.dio_run_gcd(); m_random_hammers = lp_p.random_hammers(); + m_batch_explain_fixed_in_row = lp_p.batch_explain_fixed_in_row(); m_lcube = lp_p.lcube(); m_lcube_flips = lp_p.lcube_flips(); unsigned hammer_period = lp_p.int_hammer_period(); diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index bc1f2044f5..5aeb645b78 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -268,6 +268,7 @@ private: unsigned m_dio_calls_period_decrease = 2; bool m_dio_run_gcd = true; bool m_random_hammers = true; + bool m_batch_explain_fixed_in_row = true; bool m_lcube = true; unsigned m_lcube_flips = 16; public: @@ -279,6 +280,8 @@ public: unsigned & dio_calls_period_decrease() { return m_dio_calls_period_decrease; } bool random_hammers() const { return m_random_hammers; } bool & random_hammers() { return m_random_hammers; } + bool batch_explain_fixed_in_row() const { return m_batch_explain_fixed_in_row; } + bool & batch_explain_fixed_in_row() { return m_batch_explain_fixed_in_row; } bool print_external_var_name() const { return m_print_external_var_name; } bool propagate_eqs() const { return m_propagate_eqs;} unsigned hnf_cut_period() const { return m_hnf_cut_period; }