From ff7e22c05541627f80a52206d04b3ff7f6a70dac Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 7 Jul 2026 10:15:07 -0700 Subject: [PATCH 1/2] make the batch explanation of fixed in row the default --- src/math/lp/lar_solver.cpp | 8 -------- src/math/lp/lp_params_helper.pyg | 1 - src/math/lp/lp_settings.cpp | 1 - src/math/lp/lp_settings.h | 3 --- 4 files changed, 13 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 1144922bfb..d743c5342d 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1135,15 +1135,7 @@ namespace lp { // 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)) { diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index 89c9730bc0..29a10c2d52 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -15,6 +15,5 @@ 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 14e60a5b9f..affc299788 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -46,7 +46,6 @@ 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 5aeb645b78..bc1f2044f5 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -268,7 +268,6 @@ 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: @@ -280,8 +279,6 @@ 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; } From 334f4fa32b48c354eba7f2ee77baa64d7e798a1e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Jul 2026 11:30:33 -0700 Subject: [PATCH 2/2] reduce leaks for sorts --- src/ast/polymorphism_inst.cpp | 4 +++- src/cmd_context/tptp_frontend.cpp | 6 +++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/ast/polymorphism_inst.cpp b/src/ast/polymorphism_inst.cpp index c34f03585c..5070f66d67 100644 --- a/src/ast/polymorphism_inst.cpp +++ b/src/ast/polymorphism_inst.cpp @@ -57,9 +57,11 @@ namespace polymorphism { m_assertions.push_back(e); t.push(push_back_vector(m_assertions)); u.collect_type_vars(e, inst.m_tvs); + auto* init = alloc(substitution, m); inst.m_subst = alloc(substitutions); - inst.m_subst->insert(alloc(substitution, m)); + inst.m_subst->insert(init); m_instances.insert(e, inst); + t.push(new_obj_trail(init)); t.push(new_obj_trail(inst.m_subst)); t.push(insert_map(m_instances, e)); } diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index 8ab6b31672..ff656b7ef4 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -553,8 +553,10 @@ class tptp_parser { // Multi-argument A * B > C is represented as Array(A, Array(B, C)) (curried). sort* get_ho_sort(ptr_vector const& domain, sort* range) { sort* s = range; - for (int i = (int)domain.size() - 1; i >= 0; --i) + for (int i = (int)domain.size() - 1; i >= 0; --i) { s = m_array.mk_array_sort(domain[i], s); + m_pinned_sorts.push_back(s); + } return s; } @@ -1369,6 +1371,7 @@ class tptp_parser { sort* arg_sort = arg->get_sort(); sort* result_sort = m.is_bool(arg_sort) ? m.mk_bool_sort() : m_univ; sort* arr_sort = m_array.mk_array_sort(arg_sort, result_sort); + m_pinned_sorts.push_back(arr_sort); e = coerce_arg(e, arr_sort); } else { // Array but domain may not match arg sort — coerce arg @@ -2217,6 +2220,7 @@ class tptp_parser { // If arg is Bool-sorted, result is likely Bool too (modal/connective application) sort* result_sort = m.is_bool(arg_sort) ? m.mk_bool_sort() : m_univ; sort* arr_sort = m_array.mk_array_sort(arg_sort, result_sort); + m_pinned_sorts.push_back(arr_sort); e = coerce_arg(e, arr_sort); } else { // Array but domain may not match arg sort — coerce arg