mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-07 16:31:55 +00:00
Code Activity

Add is_finite_set helper and parameter count validation

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-10-06 16:16:25 +00:00
parent 86949bf373
commit b53896f6b3
2 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/finite_set_decl_plugin.cpp
View file

@ -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<builtin_name>& 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) {

1
src/ast/finite_set_decl_plugin.h
View file

@ -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();