mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-04 11:06:45 +00:00
Code Activity
20140 commits 57 branches 53 tags 190 MiB
Commit graph

20140 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
4b5fb2607f try reordering before analyzing bounds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 13:08:52 -10:00
Lev Nachmanson
9529275e2f parameter correct order experiment 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 13:08:52 -10:00
dependabot[bot]
0018f5aafa
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>
 2025-11-24 14:42:34 -08:00
Lev Nachmanson
97f7e6fac4 remove the debug print 2025-11-24 07:54:06 -10:00
Lev Nachmanson
98a3d2af15 remove the exit statement 2025-11-24 07:51:11 -10:00
Lev Nachmanson
cc3328be8d disable add_zero_disc(disc) by default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
784ea42521 optionally call add_zero_assumption on a vanishing discriminant 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
ac58f53703 restart projection when found a non-trivial nullified polynomial, and remove is_square_free 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
82f0cfb7cc refactoring 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
26a472fb3c remove unused code 2025-11-24 06:41:06 -10:00
Lev Nachmanson
0886513de1 remve add_zero_assumption from pcs() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
fe6b777638 improve logging 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
ebecfb8e6f handle the case with no roots in add_zero_assumption 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
2768962aa8 improve log_lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
0ee272a9d1 log for smtrat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
6856a61a83 use indexed root expressions id add_zero_assumption 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
eeb83d48dc add coefficients from the elim_vanishing to m_todo 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
573ab2bbbf remove unused method 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
c6eb9d7eb7 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
8e4557647f t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
847f471015 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
36c711d95b t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
c8959dc67a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
7eb18771c2 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
bce477530a t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
27f4150e2e t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
5fec29f4cd t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
54c23bb446 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
d0fea0b714 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
3c07fa40a6 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
a512005d5c better state 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Lev Nachmanson
f49f5376b0 unsound lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-11-24 06:41:06 -10:00
Guido Martínez
32e9440855
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.
 2025-11-23 16:42:05 -08:00
Nikolaj Bjorner
662e4293a5 check cancelation in invariant checker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-23 09:09:55 -08:00
Nikolaj Bjorner
7395152632
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>
 2025-11-23 08:59:55 -08:00
dependabot[bot]
9c588afefe
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>
 2025-11-21 19:33:47 -08:00
dependabot[bot]
053d951cff
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>
 2025-11-21 19:33:33 -08:00
dependabot[bot]
d094cb6c80
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>
 2025-11-21 19:32:46 -08:00
Copilot
62cd39729f
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>
 2025-11-16 11:46:16 -08:00
Nikolaj Bjorner
59eec25102 fix #8024 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-16 10:08:21 -08:00
Nikolaj Bjorner
81211254eb strengthen filter for unknown by checking relevancy of parents #8022 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-15 17:14:00 -08:00
Nikolaj Bjorner
bf6ff56fd6 update package lock 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-15 16:56:18 -08:00
Nikolaj Bjorner
bd2ead977e add back statistics to smt-parallel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-15 16:49:22 -08:00
Josh Berdine
5690be8cfc
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>
 2025-11-15 16:36:32 -08:00
Josh Berdine
28b31cfe91
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>
 2025-11-15 16:21:08 -08:00
Josh Berdine
43525481f0
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>
 2025-11-15 16:19:39 -08:00
Nikolaj Bjorner
6d19c045d8 fix infinite loop in update function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-15 15:47:33 -08:00
Nikolaj Bjorner
11fb5c7dc4 comment out parameter check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-04 16:11:58 -08:00
Nikolaj Bjorner
2503b35dc6 check propagate ineqs setting before applying simplifier 2025-11-04 15:57:02 -08:00
Copilot
fc7660d0b5
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>
 2025-11-04 09:48:20 -08:00