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] 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