* 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>
* Initial plan
* Implement cardinality computation for finite_set sorts
- Modified mk_sort in finite_set_decl_plugin.cpp to compute 2^|s| for finite base sorts
- If base sort size > 30, mark finite_set sort as very_big
- Added comprehensive tests to verify sort size calculations
- All tests pass successfully
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Update finite_set_decl_plugin.cpp
* Fix unit tests for infinite base sorts
Updated test to check is_infinite() instead of is_very_big() for FiniteSet(Int) since infinite element sorts now result in infinite FiniteSet sorts (not very_big). Also updated comment to clarify the behavior.
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>
* Initial plan
* Add C API for finite sets
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add Python bindings for finite sets
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add C++ bindings for finite sets
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add documentation for finite set API
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>
Instead of asserting theory axioms lazily we create them on the fly and allow propagation eagerly.
The approach uses a waterfall model as follows:
- terms are created: they are inserted into an index for (set.in x S) axiom creation.
- two terms are merged by an equality.
Loop over all new opportunities for axiom instantiation
New axioms are added to a queue of recently created axioms.
- an atomic formula was asserted by the SAT solver.
Update the watch list to find new propagations.
During propagation recently created axioms are either inserted into a propagation queue, or inserted into a watch list.
They are inserted into a propagation queue all or all but one literal is assigned to false.
They are inserted into a watch list if at least two literals are unassigned
They are dropped if the axiom contains a literal that is assigned to true
The propagation queue is processed by by asserting the theory axiom to the core.
Also add some elementary statistics.
A breaking change is to change the datatype for undo-trail in smt_context to not use a custom data-structure.
This can likely cause regressions. For example, the region allocator now comes from the stack_trail instead of being
owned within smt_context with a different declaration order. smt_context could crash during destruction or maybe even pop.
We take the risk as the change is overdue.
Add swap method to ref_vector.
