mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-19 15:04:42 +00:00
Code Activity
20236 commits 45 branches 58 tags 178 MiB
Commit graph

20236 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
79f83154a3 parameter correct order experiment 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:56:00 -08:00
dependabot[bot]
7592db1362 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](https://github.com/actions/checkout/compare/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] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-02-18 20:56:00 -08:00
Lev Nachmanson
80acfbeea3 remove the debug print 2026-02-18 20:56:00 -08:00
Lev Nachmanson
7d48a7318e remove the exit statement 2026-02-18 20:56:00 -08:00
Lev Nachmanson
b582b2f32e disable add_zero_disc(disc) by default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:56:00 -08:00
Lev Nachmanson
1f3d61b6f4 optionally call add_zero_assumption on a vanishing discriminant 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:56:00 -08:00
Lev Nachmanson
a94373981a restart projection when found a non-trivial nullified polynomial, and remove is_square_free 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:56:00 -08:00
Lev Nachmanson
7909e2498a refactoring 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
c9add31da7 remove unused code 2026-02-18 20:55:59 -08:00
Lev Nachmanson
d2dd7f9df5 remve add_zero_assumption from pcs() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
8f97785498 improve logging 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
82958565ed handle the case with no roots in add_zero_assumption 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
08ca76533a improve log_lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
b088b3e7c0 log for smtrat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
0179ed855d use indexed root expressions id add_zero_assumption 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
50e4452e62 add coefficients from the elim_vanishing to m_todo 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
f0b292dd16 remove unused method 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
d088bd669e t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:59 -08:00
Lev Nachmanson
5dd3034000 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
f60d62794a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
905210b165 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
50d8a8049a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
37a5df8d95 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
602e7e906b t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
235c9b5d5a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
5bb0bf94c9 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
a9c84c7950 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
b4850019f2 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
4e38c440bd t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
b2a1293fe2 better state 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Lev Nachmanson
d93caa9c7f unsound lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:55:58 -08:00
Guido Martínez
5b41cac7c6 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.
 2026-02-18 20:55:57 -08:00
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