From 9d66c844afd4ef7eb92829df1340a294def977a7 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 19 Jan 2026 01:53:05 +0000 Subject: [PATCH 1/3] Initial plan From f04723ca27e3060976c729bfe94488b189c3f0f9 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 19 Jan 2026 01:56:22 +0000 Subject: [PATCH 2/3] Add finite_set.lattice_refutation parameter to smt_params_helper.pyg Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/params/smt_params_helper.pyg | 1 + src/smt/theory_finite_set.cpp | 6 ++++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 451a07964..001681149 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -114,6 +114,7 @@ def_module_params(module_name='smt', ('up.persist_clauses', BOOL, False, 'replay propagated clauses below the levels they are asserted'), ('array.weak', BOOL, False, 'weak array theory'), ('array.extensional', BOOL, True, 'extensional array theory'), + ('finite_set.lattice_refutation', BOOL, True, 'enable lattice refutation for finite set theory'), ('clause_proof', BOOL, False, 'record a clausal proof'), ('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'), ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transitivity of equalities'), diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index 0d572e9d1..c98af1945 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -260,7 +260,8 @@ namespace smt { ctx.push_trail(push_back_vector(m_eqs)); m_find.merge(v1, v2); // triggers merge_eh, which triggers incremental generation of theory axioms } - m_lattice_refutation.add_equality(v1, v2); + if (ctx.get_fparams().m_finite_set_lattice_refutation) + m_lattice_refutation.add_equality(v1, v2); // Check if Z3 has a boolean variable for it TRACE(finite_set, tout << "new_eq_eh_r1: " << n1->get_root() << "r2: "<< n2->get_root() <<"\n";); @@ -287,7 +288,8 @@ namespace smt { ctx.push_trail(push_back_vector(m_diseqs)); m_axioms.extensionality_axiom(e1, e2); } - m_lattice_refutation.add_disequality(v1,v2); + if (ctx.get_fparams().m_finite_set_lattice_refutation) + m_lattice_refutation.add_disequality(v1,v2); } // From 111b82af8035ec50783a815b1d10a0ade96dd6a2 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 19 Jan 2026 02:06:16 +0000 Subject: [PATCH 3/3] Add finite_set.lattice_refutation parameter implementation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/params/smt_params.cpp | 1 + src/params/smt_params.h | 1 + src/smt/theory_finite_set_lattice_refutation.cpp | 2 +- 3 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/params/smt_params.cpp b/src/params/smt_params.cpp index a80483d0f..399e1e357 100644 --- a/src/params/smt_params.cpp +++ b/src/params/smt_params.cpp @@ -51,6 +51,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_core_validate = p.core_validate(); m_sls_enable = p.sls_enable(); m_sls_parallel = p.sls_parallel(); + m_finite_set_lattice_refutation = p.finite_set_lattice_refutation(); m_logic = _p.get_sym("logic", m_logic); m_string_solver = p.string_solver(); m_up_persist_clauses = p.up_persist_clauses(); diff --git a/src/params/smt_params.h b/src/params/smt_params.h index 68ab50ffe..473d017ef 100644 --- a/src/params/smt_params.h +++ b/src/params/smt_params.h @@ -114,6 +114,7 @@ struct smt_params : public preprocessor_params, symbol m_proof_log; bool m_sls_enable = false; bool m_sls_parallel = true; + bool m_finite_set_lattice_refutation = true; // ----------------------------------- // diff --git a/src/smt/theory_finite_set_lattice_refutation.cpp b/src/smt/theory_finite_set_lattice_refutation.cpp index 0f467aaa9..f80bb4a01 100644 --- a/src/smt/theory_finite_set_lattice_refutation.cpp +++ b/src/smt/theory_finite_set_lattice_refutation.cpp @@ -12,7 +12,7 @@ Module Name: #include "smt/smt_theory.h" #include "smt/theory_finite_set.h" #include "smt/smt_context.h" -#include "iostream" +#include const int NUM_WORDS = 5; // some example have shown, the introduction of large conflict clauses can severely slow down refutation