mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-23 08:47:37 +00:00
Code Activity
21692 commits 69 branches 58 tags 180 MiB
Commit graph

21692 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
9fcede1285 check cancelation in invariant checker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:55:57 -08:00
Nikolaj Bjorner
64439a8134 factor out coi, use polynomial elaboration for nlsat solver (#8039) 
* factor out coi, use polynomial elaboration for nlsat solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove unused functionality

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:55:57 -08:00
dependabot[bot]
59a347dee1 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](https://github.com/actions/download-artifact/compare/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] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-02-18 20:55:57 -08:00
dependabot[bot]
4bd61d3ed9 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](https://github.com/actions/setup-python/compare/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] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-02-18 20:55:57 -08:00
dependabot[bot]
835b89ba9c 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](https://github.com/actions/upload-artifact/compare/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] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-02-18 20:55:57 -08:00
Copilot
cc913af282 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 <3085284+NikolajBjorner@users.noreply.github.com>

* 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 <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>
 2026-02-18 20:55:57 -08:00
Nikolaj Bjorner
0d11ec4d51 fix #8024 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:55:57 -08:00
Nikolaj Bjorner
f26b408cec strengthen filter for unknown by checking relevancy of parents #8022 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:55:57 -08:00
Nikolaj Bjorner
5e3b63d751 update package lock 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:55:57 -08:00
Nikolaj Bjorner
b443e90e24 add back statistics to smt-parallel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:55:57 -08:00
Josh Berdine
2a785bf291 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 <josh@berdine.net>
 2026-02-18 20:55:56 -08:00
Josh Berdine
8c0af7eb37 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 <josh@berdine.net>
 2026-02-18 20:55:56 -08:00
Josh Berdine
a74121a905 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 <josh@berdine.net>
 2026-02-18 20:55:56 -08:00
Nikolaj Bjorner
01362bf055 fix infinite loop in update function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:55:56 -08:00
Nikolaj Bjorner
eecfb47330 comment out parameter check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:55:56 -08:00
Nikolaj Bjorner
385dcb6de0 check propagate ineqs setting before applying simplifier 2026-02-18 20:55:56 -08:00
Copilot
0f12eb1ab3 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 <3085284+NikolajBjorner@users.noreply.github.com>

* Add test for new Java string replace operations

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Remove author field from test file header

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Delete examples/java/StringReplaceTest.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>
 2026-02-18 20:55:56 -08:00
Lev Nachmanson
1bd95a3453 add tests showing shortcomings of factorization 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:55 -08:00
Lev Nachmanson
07501f7c1f change logic NRA->ALL in log_lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:55 -08:00
Nikolaj Bjorner
7eebf35939 disable nuget 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:55:55 -08:00
Nikolaj Bjorner
17aae99931 update centos version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:55:50 -08:00
Nikolaj Bjorner
e38869e776 Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985) 
This reverts commit 05ffc0a77b.
 2026-02-18 20:55:23 -08:00
Copilot
ef5dced019 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 <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>
 2026-02-18 20:53:44 -08:00
Nikolaj Bjorner
33d4d38dee update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:37:48 -08:00
Lev Nachmanson
1e985ea96e enable optional failure in levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 13:14:59 -10:00
Nikolaj Bjorner
ddb49568d3
Merge pull request #8683 from Z3Prover/copilot/fix-build-error-z3 
Fix OCaml binding call to solver_get_levels
 2026-02-18 14:57:51 -08:00
Lev Nachmanson
aff0a82914 disable control over what added in handle_nullified_poly 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 12:47:42 -10:00
copilot-swe-agent[bot]
366b197c2b Fix OCaml build error in solver_get_levels 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 22:21:58 +00:00
copilot-swe-agent[bot]
b384f74574 Initial plan 2026-02-18 22:12:24 +00:00
Lev Nachmanson
d1461de8a7 fix nlsat.cpp and enable control over what added in handle_nullified_poly 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 12:02:56 -10:00
Nikolaj Bjorner
02b6aeb097
Merge pull request #8681 from Z3Prover/copilot/fix-discussion-issues-8680 
Add missing solver and model APIs to Go and OCaml bindings
 2026-02-18 13:26:42 -08:00
Nikolaj Bjorner
6c02a3b6bb
Delete examples/go/test_new_api_additions.go 2026-02-18 13:25:52 -08:00
Lev Nachmanson
799fc9e8c4 hook up a test 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 10:59:41 -10:00
Lev Nachmanson
d8f2b5ca01 add new polynomials from handle_nullified to m_todo 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 10:54:39 -10:00
Nikolaj Bjorner
9d3cc4afc9 remove deprecated workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 12:00:18 -08:00
Nikolaj Bjorner
672d243f0f
Merge pull request #8682 from Z3Prover/copilot/fix-docs-and-update-script 
Add Go API link to documentation index and prevent content overwrite
 2026-02-18 11:56:18 -08:00
copilot-swe-agent[bot]
9499b1089c Add --go flag to mk_api_doc.py calls and remove go directory overwrite code 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 19:30:07 +00:00
copilot-swe-agent[bot]
4335b9f545 Initial plan 2026-02-18 19:27:55 +00:00
Lev Nachmanson
df419c137d fix the test 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 07:47:16 -10:00
copilot-swe-agent[bot]
c74acb59a9 Add test for new Go API methods 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 17:45:38 +00:00
copilot-swe-agent[bot]
ac10af417a Add missing API methods to Go and OCaml bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-18 17:28:12 +00:00
copilot-swe-agent[bot]
f4606b1f2d Initial plan 2026-02-18 17:23:26 +00:00
Lev Nachmanson
b60e0e0dd3 keep literals alive 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 07:23:22 -10:00
Lev Nachmanson
138828259a add a test with compute_conflict_explanation call 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 07:08:56 -10:00
Nikolaj Bjorner
fa8d60c94f
Merge pull request #8677 from Z3Prover/copilot/fix-code-quality-issues 
Fix A3 static analysis findings: replace assertions with proper error handling
 2026-02-18 08:44:29 -08:00
Nikolaj Bjorner
c9720aa330 fixup docs.ytml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 08:36:03 -08:00
Lev Nachmanson
05029c6f03 work on nl testing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 06:33:52 -10:00
Nikolaj Bjorner
a077371520 update go doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 08:27:47 -08:00
Nikolaj Bjorner
82b34e319b update a3-python to fix issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 08:16:56 -08:00
Lev Nachmanson
7aa1ba1905 a bug fix in levelwise with the section case, where a discriminant was not added, and adding new tests for levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-17 20:00:53 -10:00