* parameter eval order

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

* parameter eval order

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

* parameter eval order

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

* parameter eval order

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

* parameter eval order

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

* parameter eval order

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

* parameter eval order

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

* Bump github/codeql-action from 3 to 4 (#7971)

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>

* Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype (#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]>

* trim parametric datatype test

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

* restore single cell

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

* restore the method behavior

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

* setting up python tuning experiment, not done

* Add finite_set_value_factory for creating finite set values in model generation (#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]>

* Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985)

This reverts commit 05ffc0a.

* Update arith_rewriter.cpp

fix memory leak introduced by update to ensure determinism

* update pythonnn prototyping experiment, need to add a couple more things

* add explicit constructors for nightly mac build failure

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

* build fixes

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

* fixes

* fix some more things but now it hangs

* change multithread to multiprocess seems to have resolved current deadlock

* fix some bugs, it seems to run now

* fix logic about checking clauses individually, and add proof prefix clause selection (naively) via the OnClause hook

* disable manylinux until segfault is resolved

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

* add the  "noexcept" keyword to value_score=(value_score&&) declaration

* expose a status flag for clauses but every single one is being coded as an assumption...

* Add a fast-path to _coerce_exprs. (#7995)

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.

* Bump actions/setup-node from 5 to 6 (#7994)

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>

* Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988)

* 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.

* try exponential delay in grobner

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

* throttle grobner method more actively

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

* enable always add all coeffs in nlsat

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

* disable centos build until resolved

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

* update centos version

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

* Add missing mkLastIndexOf method and CharSort case to Java API (#8002)

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

* Fix author field in test file

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

* Delete examples/java/TestJavaAPICompleteness.java

---------

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

* Bump actions/download-artifact from 5 to 6 (#7999)

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

---
updated-dependencies:
- dependency-name: actions/download-artifact
  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>

* Bump actions/upload-artifact from 4 to 5 (#7998)

Bumps [actions/upload-artifact](https://github.com/actions/upload-artifact) from 4 to 5.
- [Release notes](https://github.com/actions/upload-artifact/releases)
- [Commits](actions/upload-artifact@v4...v5)

---
updated-dependencies:
- dependency-name: actions/upload-artifact
  dependency-version: '5'
  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>

* initial parameter probe thread setup in C++

* fix build break introduced when adding support for polymorphic datatypes

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

* renemable Centos AMD nightly

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

* more param tuning setup

* fix C++ example and add polymorphic interface for C++

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

* update release notes

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

* bump version for release

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

* setting up the param probe solvers and mutation generator

* adding the learned clauses from the internalizer

* fix some things for clause replay

* score the param probes, but i can't figure out how to access the relevant solver statistics fields from the statistics obj

* set up pattern to notify batch manager so worker threads can update their params according
ly

* add a getter for solver stats. it compiles but still everything is untested

* bugfix

* updates to param tuning

* remove the getter for solver statistics since we're getting the vals directly from the context

* disable nuget

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

* change logic NRA->ALL in log_lemma

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

* merge

* patch fix for default manager construction so it can be used to create the param tuning context without segfault

* add tests showing shortcomings of factorization

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

* still debugging threading issues where we can't create nested param tuners or it spins infinitely. added flag for this. but now there is segfault on the probe_ctx.check() call

* Add missing string replace operations to Java API (#8011)

* Initial plan

* Add C API and Java bindings for str.replace_all, str.replace_re, str.replace_all_re

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

* Add test for new Java string replace operations

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

* Remove author field from test file header

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

* Delete examples/java/StringReplaceTest.java

---------

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

* make param tuning singlethreaded to resolve segfault when spawning subprocesses ffor nested ctx checks

* check propagate ineqs setting before applying simplifier

* comment out parameter check

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

* add some toggle-able params to smt_parallel_params.pyg for doing the param tuning experiments on QF_RDL. set up this logic in the smt_parallel files

* add bash scripts to run param experiments on an QF_RDL example to get datapoints

* fix bug about param protocol iteration only happening once, and add new user param to toggle for only running param tuning thread without parallel solving (just to test if it's finding good settings)

* add results of exhaustive param testing for QF_RDL_abz5_1200

* fix infinite loop in update function

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

* Add check that argument of Z3_is_algebraic_number is_expr (#8027)

To make sure that the `to_expr` cast is safe.

Signed-off-by: Josh Berdine <[email protected]>

* Add Z3_fpa_is_numeral to the API (#8026)

This is analogous to Z3_fpa_is_numeral_nan, Z3_fpa_is_numeral_inf, etc. and
can be needed to check that inputs are valid before calling those functions.

Signed-off-by: Josh Berdine <[email protected]>

* Make rcf is_rational and is_rational_function operations handle zero (#8025)

The representation of the zero rcf numeral is nullptr, and the is_rational
and is_rational_function operations are not expecting to be called with
nullptr. But there isn't a way to test for that in the API, other than
checking if Z3_rcf_num_to_string returns "0".

This patch adds a couple conditions so that is_rational and
is_rational_function operations handle zero. Maybe this isn't the desired
change. For instance, the is_zero operation could instead be exposed in the
API and preconditions added to the relevant operations.

Signed-off-by: Josh Berdine <[email protected]>

* add back statistics to smt-parallel

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

* update package lock

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

* strengthen filter for unknown by checking relevancy of parents #8022

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

* fix #8024

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

* Fix NuGet package missing Microsoft.Z3.dll due to inverted replace() logic (#8029)

* Initial plan

* Fix NuGet packaging and add GitHub Actions workflow

- Fixed critical bug in mk_nuget_task.py replace() function
- Created comprehensive GitHub Actions workflow for building NuGet packages

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

* Add documentation and improve code comments

- Added comprehensive README for NuGet build workflow
- Added detailed comments explaining the replace() function fix
- Verified all Python syntax is correct

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

---------

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

* small bugfix in searchtree?

* Delete sweep_results_QF_RDL_abz5_1200.csv

* fix escape quotes

* Bump actions/upload-artifact from 4 to 5 (#8034)

Bumps [actions/upload-artifact](https://github.com/actions/upload-artifact) from 4 to 5.
- [Release notes](https://github.com/actions/upload-artifact/releases)
- [Commits](actions/upload-artifact@v4...v5)

---
updated-dependencies:
- dependency-name: actions/upload-artifact
  dependency-version: '5'
  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>

* Bump actions/setup-python from 5 to 6 (#8033)

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

---
updated-dependencies:
- dependency-name: actions/setup-python
  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>

* Bump actions/download-artifact from 4 to 6 (#8032)

Bumps [actions/download-artifact](https://github.com/actions/download-artifact) from 4 to 6.
- [Release notes](https://github.com/actions/download-artifact/releases)
- [Commits](actions/download-artifact@v4...v6)

---
updated-dependencies:
- dependency-name: actions/download-artifact
  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>

* factor out coi, use polynomial elaboration for nlsat solver (#8039)

* factor out coi, use polynomial elaboration for nlsat solver

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

* remove unused functionality

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

---------

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

* check cancelation in invariant checker

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

* mk_util.py: fix --gprof option (#8040)

The addition of -fomit-frame-pointer was missing a space (which broke
the command line), but also this option should be added only if -pg is
*not* given, as they are incompatible. So, just remove this line to fix
the --gprof flag in configure.

Also, this option is implied by any level of `-O`, so there is no need
to pass it explicitly in most cases. It could be added to debug,
non-profile builds, but I'm not sure that's useful.

* unsound lemma

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

* better state

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* remove unused method

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

* add coefficients from the elim_vanishing to m_todo

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

* use indexed root expressions id add_zero_assumption

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

* log for smtrat

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

* improve log_lemma

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

* handle the case with no roots in add_zero_assumption

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

* improve logging

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

* remve add_zero_assumption from pcs()

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

* remove unused code

* refactoring

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

* restart projection when found a non-trivial nullified polynomial, and remove is_square_free

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

* optionally call add_zero_assumption on a vanishing discriminant

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

* disable add_zero_disc(disc) by default

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

* remove the exit statement

* remove the debug print

* Bump actions/checkout from 5 to 6 (#8043)

Bumps [actions/checkout](https://github.com/actions/checkout) from 5 to 6.
- [Release notes](https://github.com/actions/checkout/releases)
- [Changelog](https://github.com/actions/checkout/blob/main/CHANGELOG.md)
- [Commits](actions/checkout@v5...v6)

---
updated-dependencies:
- dependency-name: actions/checkout
  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>

* parameter correct order experiment

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

* try reordering before analyzing bounds

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

* use edit distance for simplified error messaging on wrong trace tags

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

* apply gcd test also before saturation

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

* Return bool instead of int from Z3_rcf_interval (#8046)

In the underlying realclosure implementation, the interval operations for
{`lower`,`upper`}`_is_`{`inf`,`open`} return `bool` results. Currently these
are cast to `int` when surfacing them to the API. This patch keeps them at
type `bool` through to `Z3_rcf_interval`.

Signed-off-by: Josh Berdine <[email protected]>

* Return sign from Z3_fpa_get_numeral_sign as bool instead of int (#8047)

The underlying `mpf_manager::sgn` function returns a `bool`, and functions
such as `Z3_mk_fpa_numeral_int_uint` take the sign as a `bool`.

Signed-off-by: Josh Berdine <[email protected]>

* Return bool instead of int in extra_API for Z3_open_log (#8048)

The C declaration returns `bool`.

Signed-off-by: Josh Berdine <[email protected]>

* update doc test string

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

* open_log returns bool

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

* update java API code to work with boolean pointers

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

* remove unused

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

* port to BoolPtr

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

* fix type for BoolPtr

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

* port dotnet to use bool sorts from API

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

* fix warnings in nra_solver

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

* fix warnings in nla_pp

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

* fix dotnet build errors

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

* python type fixes

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

* fix build warnings

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

* use c_bool instead of c_int for sign

* remove references to set_has_size

* fix second byref to bool

* remove set cardinality operators from array theory. Make final-check use priority levels

Issue #7502 shows that running nlsat eagerly during final check can block quantifier instantiation.
To give space for quantifier instances we introduce two levels for final check such that nlsat is only applied in the second and final level.

* insert theory only once

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

* refine givup conditions

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

* Fix _in vs _out def_API param for Z3_solver_get_levels (#8050)

Signed-off-by: Josh Berdine <[email protected]>

* remove deprecated set_has_size

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

* remove deprecated set_has_size

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

* remove deprecated set_has_size

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

* remove deprecated set_has_size

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

* fix #8055

* fix #8054

inherit denominators when evaluating polynomials

* remove unused *_signed_project() methods

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

* Disable C++98 compatibility warnings for Clang builds (#8060)

* Initial plan

* Disable C++98 compatibility warnings for Clang to fix vcpkg build freeze

Add -Wno-c++98-compat and -Wno-c++98-compat-pedantic flags to prevent
excessive warning output when building with clang-cl or when -Weverything
is enabled. These warnings are not useful for Z3 since it requires C++20.

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

---------

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

* fix the build

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

* allow parsing declared arrays without requiring explicit select

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

* disable preprocessing only after formulas are internalized

* bring in nikolaj's preprocessing patch from master

* don't unfold recursive defs if there is an uninterpreted subterm, #7671

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

* remove stale experimental code #8063

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

* Implement Z3_optimize_translate for context translation (#8072)

* Initial plan

* Implement Z3_optimize_translate functionality

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

* Fix compilation errors and add tests for optimize translate

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

* Revert changes to opt_solver.cpp as requested

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

---------

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

* Search tree core resolution optimization (#8066)

* Add cube tree optimization about resolving cores recursively up the path, to prune. Also integrate asms into the tree so they're not tracked separately (#7960)

* draft attempt at optimizing cube tree with resolvents. have not tested/ran yet

* adding comments

* fix bug about needing to bubble resolvent upwards to highest ancestor

* fix bug where we need to cover the whole resolvent in the path when bubbling up

* clean up comments

* close entire tree when sibling resolvent is empty

* integrate asms directly into cube tree, remove separate tracking

* try to fix bug about redundant resolutions, merging close and try_resolve_upwards into once function

* separate the logic again to avoid mutual recursion

* Refactor search tree closure and resolution logic

Refactor close_with_core to simplify logic and remove unnecessary parameters. Update sibling resolvent computation and try_resolve_upwards for clarity.

* apply formatting

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

* Refactor close_with_core to use current node in lambda

* Fix formatting issues in search_tree.h

* fix build issues

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

* Update smt_parallel.cpp

* Change loop variable type in unsat core processing

* Change method to retrieve unsat core from root

---------

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

* Typescript typedef and doc fixes (#8073)

* Fix Typescript typedef to allow `new Context`

* fix init() tsdoc example using nonexistent sat import

* Revert "Typescript typedef and doc fixes (#8073)" (#8077)

This reverts commit 6cfbcd1.

* Typescript typedef and doc fixes take 2 (#8078)

* Fix Typescript typedef to allow `new Context`

* fix init() tsdoc example using nonexistent sat import

* Fix DEL character (0x7F) not being escaped in string literals (#8080)

* Initial plan

* Fix DEL character encoding in string literals

Change condition from `ch >= 128` to `ch >= 127` to include the DEL
character (U+007F, 127) in escaped output. This ensures that the
non-printable DEL control character is properly escaped as \u{7f}
instead of being printed directly.

Also add test cases for DEL and other control characters.

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

---------

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

* Add GitHub Actions workflow to publish JavaScript/TypeScript API documentation (#8084)

* Initial plan

* Add GitHub Actions workflow to build and publish documentation

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

* Refine documentation workflow to use mk_api_doc.py and install doxygen

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

* Clarify documentation generation step name

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

---------

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

* Bump actions/cache from 4 to 5 (#8081)

Bumps [actions/cache](https://github.com/actions/cache) from 4 to 5.
- [Release notes](https://github.com/actions/cache/releases)
- [Changelog](https://github.com/actions/cache/blob/main/RELEASES.md)
- [Commits](actions/cache@v4...v5)

---
updated-dependencies:
- dependency-name: actions/cache
  dependency-version: '5'
  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>

* Bump actions/download-artifact from 6 to 7 (#8082)

Bumps [actions/download-artifact](https://github.com/actions/download-artifact) from 6 to 7.
- [Release notes](https://github.com/actions/download-artifact/releases)
- [Commits](actions/download-artifact@v6...v7)

---
updated-dependencies:
- dependency-name: actions/download-artifact
  dependency-version: '7'
  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>

* Build native Z3 for x64 before generating docs (#8086)

* Initial plan

* Build Z3 for ubuntu x64 and invoke JS build scripts in docs workflow

- Modified docs.yml to build Z3 natively for ubuntu-latest x64 before documentation generation
- Removed default working directory to allow explicit working-directory per step
- Added step to build Z3 using python scripts/mk_make.py
- Kept emscripten setup as required for wasm build
- Modified mk_api_doc.py to invoke npm run build:ts and npm run build:wasm as described in src/api/js/README.md
- mk_api_doc.py now runs the full build process (TypeScript + wasm) before generating documentation

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

* Source emsdk environment before generating documentation

- Added source command to ensure emscripten tools are in PATH when mk_api_doc.py runs npm scripts
- This ensures emcc and other emscripten tools are available for npm run build:wasm

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

* Revert changes to mk_api_doc.py

- Removed npm run build:ts and npm run build:wasm calls from mk_api_doc.py
- Reverted to only calling npm run docs as before

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

---------

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

* Bump actions/upload-artifact from 5 to 6 (#8083)

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

---
updated-dependencies:
- dependency-name: actions/upload-artifact
  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>

* build the ts bindings

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

* build the ts bindings

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

* Update docs.yml

* Update docs.yml

* Add defaults for job run working directory

* Update docs.yml

* BLD: Add CMake option to build Python bindings without rebuilding libz3 (redux) (#8088)

* Add CMake option to build only Python bindings without rebuilding libz3

Introduce Z3_BUILD_LIBZ3_CORE option (default ON) to control whether libz3 is built.
When set to OFF with Z3_BUILD_PYTHON_BINDINGS=ON, only Python bindings are built
using a pre-installed libz3 library. This is useful for package managers like
conda-forge to avoid rebuilding libz3 for each Python version.

Changes:
- Add Z3_BUILD_LIBZ3_CORE option in src/CMakeLists.txt
- When OFF, find and use pre-installed libz3 as imported target
- Update Python bindings CMakeLists.txt to handle both built and imported libz3
- Add documentation in README-CMake.md with usage examples

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

* Fix CMake export issues when building only Python bindings

Conditionally export Z3_EXPORTED_TARGETS only when Z3_BUILD_LIBZ3_CORE=ON
to avoid errors when building Python bindings without building libz3.

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

* Disable executable and test builds when not building libz3 core

When Z3_BUILD_LIBZ3_CORE=OFF, automatically disable Z3_BUILD_EXECUTABLE
and Z3_BUILD_TEST_EXECUTABLES to avoid build/install errors.

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

* only build src/ folder if Z3_BUILD_LIBZ3_CORE is TRUE

* move z3 python bindings to main CMake

* move more logic to main CMakeLists.txt

* move Z3_API_HEADER_FILES_TO_SCAN to main CMakeLists.txt

---------

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

* merge

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

* Fix docs.yml workflow: remove conflicting native build step (#8091)

* Initial plan

* Fix docs.yml workflow to properly build and deploy documentation

- Remove `no-install: true` from setup-emsdk step to properly install emscripten
- Remove `working-directory: src/api/js` from setup-emsdk step (not needed)
- Remove manual emsdk install/activate/source commands from Build wasm step
- Remove redundant native Z3 build step that conflicted with wasm build
- Simplify Generate Documentation step by removing redundant source command

The main issue was that the native Z3 build was creating a Makefile in the build/
directory before the wasm build ran. The wasm build script then saw the Makefile
existed and skipped the emconfigure step, but the native Makefile doesn't have a
libz3.a target, causing the build to fail. Removing the native build allows the
wasm build to properly configure its own build with emscripten.

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

---------

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

* fix #8092

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

* use new arithmetic solver for AUFLIA, fixes #8090

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

* Fix docs.yml workflow: resolve WASM/native library conflict in documentation generation (#8093)

* Initial plan

* Fix docs.yml: Build native Z3 Python bindings before WASM to avoid library conflicts

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

---------

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

* Update docs.yml

* Update docs.yml

* Add working directory for wasm build step

* Simplify CI workflow by removing emscripten steps

Removed unnecessary steps for emscripten setup and TypeScript/WASM build in the CI workflow.

* Deploy docs to z3prover.github.io organization pages (#8094)

* Initial plan

* Deploy docs to z3prover.github.io organization pages

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

---------

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

* Update docs.yml

* Update publish directory for documentation deployment

* Modify docs.yml for deployment settings

Updated the GitHub Actions workflow for documentation deployment, changing the publish directory and removing the push trigger.

* fix indentation

* docs with ml bindings

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

* Fix docs.yml workflow: update actions to v4 (#8095)

* Initial plan

* Fix docs.yml workflow: update GitHub Actions to valid versions

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

---------

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

* update doc

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

* updated with env ocaml

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

* include paramters

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

* enable js

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

* Modify docs.yml to generate JS documentation

Updated documentation generation script to include JavaScript output.

* Update docs.yml

* try adding wasm as separate step

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

* fix build dir

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

* set build be configurable by env

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

* Fix Z3BUILD environment variable in docs workflow

* Refactor documentation workflow to simplify installation

Remove redundant command for installing Python package.

* make build directory configurable

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

* set build directory

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

* na

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

* Fix docs.yml workflow: specify working directory for npm commands (#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]>

* Update docs.yml

* fix #8097

* flight test copilot generated slop?

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

* indent

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

* naming convention

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

* update to macos-latest

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

* next flight test

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

* remove flight test

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

* Some changes to improve LIA performance (#8101)

* 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]>

* fix #8102

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

* fix #8076

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

* assert entry_invariant only when all changes are done

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

* fix #8099 (again)

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

* fixes to finite domain arrays

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

* reduce rdl tunable params

* new RDL scoring

* remove pop to base lvl for tuner

* scaling m_max_prefix_conflicts

* try to mutate pairs

* go back to single param flip version

* new scoring

* change some scoring strategies, add LIA and NIA param tuning

* fix big about updt_params automatically spawning new parallel objects in param generator checks

---------

Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: dependabot[bot] <[email protected]>
Signed-off-by: Nikolaj Bjorner <[email protected]>
Signed-off-by: Josh Berdine <[email protected]>
Co-authored-by: Lev Nachmanson <[email protected]>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Co-authored-by: Copilot <[email protected]>
Co-authored-by: NikolajBjorner <[email protected]>
Co-authored-by: Nikolaj Bjorner <[email protected]>
Co-authored-by: Nelson Elhage <[email protected]>
Co-authored-by: hwisungi <[email protected]>
Co-authored-by: Josh Berdine <[email protected]>
Co-authored-by: Guido Martínez <[email protected]>
Co-authored-by: Chris Cowan <[email protected]>
Co-authored-by: h-vetinari <[email protected]>
Co-authored-by: Ilana Shapiro <[email protected]>
Co-authored-by: Ilana Shapiro <[email protected]>
Co-authored-by: Ilana Shapiro <[email protected]>
Co-authored-by: Ilana Shapiro <[email protected]>

The underlying `mpf_manager::sgn` function returns a `bool`, and functions
such as `Z3_mk_fpa_numeral_int_uint` take the sign as a `bool`.

Signed-off-by: Josh Berdine <[email protected]>