- api_fpa.cpp: add RETURN_Z3(nullptr) after SET_ERROR_CODE in Z3_mk_fpa_sort to prevent fall-through to mk_float_sort with invalid params
- api_seq.cpp: add null check for str in Z3_mk_string; add null check for str when sz>0 in Z3_mk_lstring; add lo<=hi validation in Z3_mk_re_loop
- api_array.cpp: add explicit n==0 validation in Z3_mk_array_sort_n
- api_solver.cpp: rename local variable 'c' to avoid shadowing Z3_context param in Z3_solver_propagate_created/decide/on_binding; move init_solver call inside file-exists branches of Z3_solver_from_file
- api_ast.cpp: add null check for target in Z3_translate; add null check for _from/_to arrays when num_exprs>0 in Z3_substitute
- api_model.cpp: add CHECK_NON_NULL(m) in Z3_add_func_interp; add CHECK_NON_NULL(a) in Z3_model_get_const_interp; add null check for target in Z3_model_translate
- api_opt.cpp: add null check for weight string in Z3_optimize_assert_soft
- api_quant.cpp: add num_patterns==0 validation in Z3_mk_pattern
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.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>
An initial update to support polymorphism from SMTLIB3 and the API (so far C, Python).
The WIP SMTLIB3 format is assumed to be supporting the following declaration
```
(declare-type-var A)
```
Whenever A is used in a type signature of a function/constant or bound quantified variable, it is taken to mean that all instantiations of A are included in the signature and assertions.
For example, if the function f is declared with signature A -> A, then there is a version of f for all instances of A.
The semantics of polymorphism appears to follow previous proposals: the instances are effectively different functions.
This may clash with some other notions, such as the type signature forall 'a . 'a -> 'a would be inhabited by a unique function (the identity), while this is not enforced in this version (and hopefully never because it is more busy work).
The C API has the function 'Z3_mk_type_variable' to create a type variable and applying functions modulo polymorphic type signatures is possible.
The kind Z3_TYPE_VAR is added to sort discriminators.
This version is considered as early alpha. It passes a first rudimentary unit test involving quantified axioms, declare-fun, define-fun, and define-fun-rec.
