From b53896f6b35cf2df8ea030f2ec4e3ddb95cf2bc5 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 6 Oct 2025 16:16:25 +0000 Subject: [PATCH] Add is_finite_set helper and parameter count validation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/finite_set_decl_plugin.cpp | 12 +++++++++--- src/ast/finite_set_decl_plugin.h | 1 + 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index 8604142ee..e03c05480 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -90,9 +90,15 @@ sort * finite_set_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, par return nullptr; } +bool finite_set_decl_plugin::is_finite_set(sort* s) const { + return s->get_family_id() == m_family_id && s->get_decl_kind() == FINITE_SET_SORT; +} + sort * finite_set_decl_plugin::get_element_sort(sort* finite_set_sort) const { - if (finite_set_sort->get_family_id() != m_family_id || - finite_set_sort->get_decl_kind() != FINITE_SET_SORT) { + if (!is_finite_set(finite_set_sort)) { + return nullptr; + } + if (finite_set_sort->get_num_parameters() != 1) { return nullptr; } parameter const* params = finite_set_sort->get_parameters(); @@ -160,7 +166,7 @@ void finite_set_decl_plugin::get_sort_names(svector& sort_names, s } expr * finite_set_decl_plugin::get_some_value(sort * s) { - if (s->get_family_id() == m_family_id && s->get_decl_kind() == FINITE_SET_SORT) { + if (is_finite_set(s)) { // Return empty set for the given sort sort* element_sort = get_element_sort(s); if (element_sort) { diff --git a/src/ast/finite_set_decl_plugin.h b/src/ast/finite_set_decl_plugin.h index c03f59a17..851239558 100644 --- a/src/ast/finite_set_decl_plugin.h +++ b/src/ast/finite_set_decl_plugin.h @@ -57,6 +57,7 @@ class finite_set_decl_plugin : public decl_plugin { func_decl * mk_empty(sort* element_sort); func_decl * mk_finite_set_op(decl_kind k, unsigned arity, sort * const * domain, sort* range); sort * get_element_sort(sort* finite_set_sort) const; + bool is_finite_set(sort* s) const; public: finite_set_decl_plugin();