* Initial plan
* Add mkLastIndexOf method and CharSort support to Java API
- Added mkLastIndexOf method to Context.java for extracting last index of sub-string
- Added Z3_CHAR_SORT case to Sort.java's create() method switch statement
- Added test file to verify both fixes work correctly
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix author field in test file
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Delete examples/java/TestJavaAPICompleteness.java
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Initial plan
* Add finite_set_value_factory implementation
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Remove unused dl_decl_plugin variable and include
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update copyright and add TODOs in finite_set_value_factory
Updated copyright information and added TODO comments for handling in finite_set_value_factory methods.
* Update copyright information in finite_set_value_factory.h
Updated copyright year from 2006 to 2025.
* Implement finite_set_value_factory using array_util to create singleton sets
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Simplify empty set creation in finite_set_value_factory
Refactor finite_set_value_factory to simplify empty set handling and remove array-specific logic.
* Change family ID for finite_set_value_factory
* Fix build error by restoring array_decl_plugin include and implementation
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update finite_set_value_factory.h
* Add SASSERT for finite set check in factory
Added assertion to check if the sort is a finite set.
* Rename member variable from m_util to u
* Refactor finite_set_value_factory for value handling
* Use register_value instead of direct set insertion
Replaced direct insertion into set with register_value calls.
* Update finite_set_value_factory.cpp
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Initial plan
* Add Z3_decl_kind enumeration for finite_set operators
- Added Z3_OP_FINITE_SET_* enumeration values (0xc000 range) to z3_api.h
- Added documentation for all 13 finite_set operators
- Added translation cases in api_ast.cpp for mapping internal finite_set
enum values to external Z3_decl_kind values
- All operators tested and working correctly
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Improve documentation for Z3_OP_FINITE_SET_EXT and Z3_OP_FINITE_SET_MAP_INVERSE
- Clarified that Z3_OP_FINITE_SET_EXT returns a witness element demonstrating
two sets are different (extensionality)
- Clarified that Z3_OP_FINITE_SET_MAP_INVERSE relates to pre-image reasoning
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Enabling Control Flow Guard by default for MSVC on Windows, with options to disable it.
* Fix configuration error for non-MSVC compilers.
* Reviewed and updated configuration for Python build and added comment for CFG.
When the inputs are already the same sort, we can skip most of the
coercion logic and just return.
Currently, `_coerce_exprs` is by far the most expensive part of
building up many common Z3 ASTs, so this fast-path is a substantial
speedup for many use-cases.
* Initial plan
* Add finite_set_value_factory implementation
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Remove unused dl_decl_plugin variable and include
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update copyright and add TODOs in finite_set_value_factory
Updated copyright information and added TODO comments for handling in finite_set_value_factory methods.
* Update copyright information in finite_set_value_factory.h
Updated copyright year from 2006 to 2025.
* Implement finite_set_value_factory using array_util to create singleton sets
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Simplify empty set creation in finite_set_value_factory
Refactor finite_set_value_factory to simplify empty set handling and remove array-specific logic.
* Change family ID for finite_set_value_factory
* Fix build error by restoring array_decl_plugin include and implementation
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update finite_set_value_factory.h
* Add SASSERT for finite set check in factory
Added assertion to check if the sort is a finite set.
* Rename member variable from m_util to u
* Refactor finite_set_value_factory for value handling
* Use register_value instead of direct set insertion
Replaced direct insertion into set with register_value calls.
* Update finite_set_value_factory.cpp
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Initial plan
* Update Z3_mk_datatype_sort API to accept array of parameters
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update language bindings for parametric datatype sort API
- Python: Updated DatatypeSort() to accept optional params list
- OCaml: Added mk_sort_ref_p/mk_sort_ref_ps for parametric datatypes
- .NET: Added MkDatatypeSortRef() methods with optional params
- Java: Added mkDatatypeSortRef() methods with optional params
- All changes maintain backward compatibility
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix .NET build error - rename params to parameters
The 'params' keyword is reserved in C#, causing compilation errors.
Renamed parameter from 'params' to 'parameters' in MkDatatypeSortRef methods.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add unit test for parametric datatypes
Added test_parametric_datatype.cpp to demonstrate polymorphic datatypes.
The test creates two concrete instantiations of a generic pair concept:
- pair_int_real with fields (first:Int, second:Real)
- pair_real_int with fields (first:Real, second:Int)
Then verifies that accessors work correctly and type checking is enforced.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Implement polymorphic type variables support for parametric datatypes
- Modified datatype_decl_plugin to allow type variables as parameters
- Updated mk_datatype_decl to extract type variables from field sorts
- Type variables are collected in order of first appearance
- Revised unit test to use Z3_mk_type_variable for polymorphic datatypes
- Test creates pair datatype with type variables alpha and beta
- Successfully instantiates with concrete types (pair Int Real) and (pair Real Int)
- Verifies accessor types match and equality terms are well-typed
- All tests pass
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add Z3_mk_polymorphic_datatype API and refactor datatype creation
- Added new API Z3_mk_polymorphic_datatype to z3_api.h
- Renamed static mk_datatype_decl to api_datatype_decl in api_datatype.cpp
- Modified api_datatype_decl to accept explicit type parameters
- Updated all callers to use renamed function
- Added test_polymorphic_datatype_api demonstrating new API usage
- Both tests pass successfully
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Remove type variable collection logic from constructors
Removed the logic for collecting type variables from field sorts based on constructors.
* Update comments on parameter handling in api_datatype.cpp
Clarify usage of parameters in API documentation.
* Fix OCaml build error - use list instead of array for mk_datatype_sort
Changed mk_sort_ref to pass empty list [] instead of empty array [||].
Changed mk_sort_ref_p to pass params list directly instead of converting to array.
Z3native.mk_datatype_sort expects a list, not an array.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add polymorphic datatype example to C++ examples
Added polymorphic_datatype_example() demonstrating:
- Creating type variables alpha and beta with Z3_mk_type_variable
- Defining parametric Pair datatype with fields of type alpha and beta
- Instantiating with concrete types (Pair Int Real) and (Pair Real Int)
- Getting constructors and accessors from instantiated datatypes
- Creating constants and expressions using the polymorphic types
- Verifying type correctness with equality (= (first p1) (second p2))
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
