Signed-off-by: Lev Nachmanson <[email protected]>

Signed-off-by: Lev Nachmanson <[email protected]>

Signed-off-by: Lev Nachmanson <[email protected]>

Signed-off-by: Lev Nachmanson <[email protected]>

Signed-off-by: Lev Nachmanson <[email protected]>

Signed-off-by: Lev Nachmanson <[email protected]>

Bumps [github/codeql-action](https://github.com/github/codeql-action) from 3 to 4.
- [Release notes](https://github.com/github/codeql-action/releases)
- [Changelog](https://github.com/github/codeql-action/blob/main/CHANGELOG.md)
- [Commits](github/codeql-action@v3...v4)

---
updated-dependencies:
- dependency-name: github/codeql-action
  dependency-version: '4'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

… add Z3_mk_polymorphic_datatype (Z3Prover#7966)

* Initial plan

* Update Z3_mk_datatype_sort API to accept array of parameters

Co-authored-by: NikolajBjorner <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

---------

Co-authored-by: copilot-swe-agent[bot] <[email protected]>
Co-authored-by: NikolajBjorner <[email protected]>
Co-authored-by: Nikolaj Bjorner <[email protected]>

Signed-off-by: Nikolaj Bjorner <[email protected]>

Signed-off-by: Lev Nachmanson <[email protected]>

Signed-off-by: Lev Nachmanson <[email protected]>

…generation (Z3Prover#7981)

* Initial plan

* Add finite_set_value_factory implementation

Co-authored-by: NikolajBjorner <[email protected]>

* Remove unused dl_decl_plugin variable and include

Co-authored-by: NikolajBjorner <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

* 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] <[email protected]>
Co-authored-by: NikolajBjorner <[email protected]>
Co-authored-by: Nikolaj Bjorner <[email protected]>

…n model …" (Z3Prover#7985)

This reverts commit 05ffc0a.

fix memory leak introduced by update to ensure determinism

Signed-off-by: Nikolaj Bjorner <[email protected]>

Signed-off-by: Nikolaj Bjorner <[email protected]>

…dlock

…lause selection (naively) via the OnClause hook

Signed-off-by: Nikolaj Bjorner <[email protected]>

…as an assumption...

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.

Bumps [actions/setup-node](https://github.com/actions/setup-node) from 5 to 6.
- [Release notes](https://github.com/actions/setup-node/releases)
- [Commits](actions/setup-node@v5...v6)

---
updated-dependencies:
- dependency-name: actions/setup-node
  dependency-version: '6'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

Signed-off-by: Nikolaj Bjorner <[email protected]>

…Prover#8098)

* Initial plan

* Fix docs.yml build by adding working-directory to npm steps

Co-authored-by: NikolajBjorner <[email protected]>

---------

Co-authored-by: copilot-swe-agent[bot] <[email protected]>
Co-authored-by: NikolajBjorner <[email protected]>

Signed-off-by: Nikolaj Bjorner <[email protected]>

Signed-off-by: Nikolaj Bjorner <[email protected]>

Signed-off-by: Nikolaj Bjorner <[email protected]>

Signed-off-by: Nikolaj Bjorner <[email protected]>

Signed-off-by: Nikolaj Bjorner <[email protected]>

Signed-off-by: Nikolaj Bjorner <[email protected]>

* add user params

* inprocessing flag

* playing around with clause sharing with some arith constraints (complicated version commented out)

* collect shared clauses inside share units after pop to base level (might help NIA)

* dont collect clauses twice

* dont pop to base level when sharing units, manual filter

* clean up code

---------

Co-authored-by: Ilana Shapiro <[email protected]>

Signed-off-by: Nikolaj Bjorner <[email protected]>

remove unsound "optimization" for correction sets. It misses feasible solutions

Signed-off-by: Lev Nachmanson <[email protected]>

Signed-off-by: Nikolaj Bjorner <[email protected]>

- relevancy could be off and array solver doesn't compensate, Z3Prover#7544
- enforce equalities across store for small domain axioms Z3Prover#8065

… in param generator checks