From 819979db6746388e6ff8ad67e7ff679a318c41c7 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 14 Oct 2025 08:55:02 +0000 Subject: [PATCH] Fix finite_set_decl_plugin bug and complete implementation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/finite_set_decl_plugin.cpp | 4 +++- src/ast/rewriter/finite_set_axioms.cpp | 10 +++++++--- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index 3a3a96bce..e5b9ee61b 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -139,7 +139,9 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param m_manager->raise_exception("set.empty requires one sort parameter"); return nullptr; } - range = to_sort(parameters[0].get_ast()); + sort* element_sort = to_sort(parameters[0].get_ast()); + parameter param(element_sort); + range = m_manager->mk_sort(m_family_id, FINITE_SET_SORT, 1, ¶m); } return mk_empty(range); case OP_FINITE_SET_SINGLETON: diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp index 18d97637d..5a9c4c5d8 100644 --- a/src/ast/rewriter/finite_set_axioms.cpp +++ b/src/ast/rewriter/finite_set_axioms.cpp @@ -24,11 +24,15 @@ Revision History: #include "ast/rewriter/finite_set_axioms.h" // a ~ set.empty => not (x in a) +// x is an element, generate axiom that x is not in any empty set of x's type void finite_set_axioms::in_empty_axiom(expr *x) { - expr_ref_vector clause(m); - sort* s = x->get_sort(); - expr_ref empty_set(u.mk_empty(s), m); + // Generate: not (x in empty_set) + // where empty_set is the empty set of x's type + sort* elem_sort = x->get_sort(); + expr_ref empty_set(u.mk_empty(elem_sort), m); expr_ref x_in_empty(u.mk_in(x, empty_set), m); + + expr_ref_vector clause(m); clause.push_back(m.mk_not(x_in_empty)); m_add_clause(clause); }