Implement finite_sets_decl_plugin with complete operator support

[Copilot]

• Understand the finite_sets_decl_plugin specification from header file
• Review similar decl_plugin implementations (array_decl_plugin, dl_decl_plugin)
• Implement finite_sets_decl_plugin.h with class declaration and operators
• Implement finite_sets_decl_plugin.cpp with plugin logic
• Add finite_sets_decl_plugin.cpp to build system (CMakeLists.txt)
• Register the plugin in reg_decl_plugins.cpp
• Build and test the implementation
• Create and run verification tests
• Add set.singleton operator

Summary

Successfully implemented the finite_sets_decl_plugin with all operations specified in the header file, including the newly added set.singleton operator.

Implemented Operations:

• set.empty: Create empty set of a given element type
• set.singleton: Create a set containing a single element (NEW)
• set.union: Union of two sets
• set.intersect: Intersection of two sets
• set.difference: Set difference
• set.in: Membership test
• set.size: Get set size (returns Int)
• set.subset: Subset test
• set.map: Map a function over set elements
• set.filter: Filter set by predicate
• set.range: Create integer range set

Changes Made:

1. Implemented finite_sets_decl_plugin.h with complete class declaration
2. Implemented finite_sets_decl_plugin.cpp with all operators
3. Registered plugin in reg_decl_plugins.cpp
4. Added to build system in src/ast/CMakeLists.txt
5. Created comprehensive tests in src/test/finite_sets.cpp
6. Added set.singleton operator per feedback
7. All tests pass successfully

Original prompt

Add functionality to finite_set_decl_plugin.h and finite_set_decl_plugin.cpp to support the signature specified in the header file.

---

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.

[NikolajBjorner]

@copilot take also into account the new operator set.singleton that was added to the header file

[Copilot]

@copilot take also into account the new operator set.singleton that was added to the header file

Added set.singleton operator with signature S -> (FiniteSet S). The operator creates a singleton set containing a single element. Implementation includes:

• Operator enum and symbol definitions
• mk_singleton function that validates arity and creates appropriate FiniteSet sort
• Recognizer function is_singleton
• Utility function mk_singleton in finite_sets_util
• Test coverage for the new operator

All tests pass successfully. Commit: d8beab9