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

20504 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
08babfff60 fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:02 -08:00
Nikolaj Bjorner
032a3a879b python type fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:02 -08:00
Nikolaj Bjorner
ee88359f50 fix dotnet build errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:02 -08:00
Nikolaj Bjorner
0c1ff55adf fix warnings in nla_pp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:02 -08:00
Nikolaj Bjorner
2fd89c5921 fix warnings in nra_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:02 -08:00
Nikolaj Bjorner
c66628e6e1 port dotnet to use bool sorts from API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:02 -08:00
Nikolaj Bjorner
abd9b4c05d fix type for BoolPtr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:02 -08:00
Nikolaj Bjorner
f0e0beedb1 port to BoolPtr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:02 -08:00
Nikolaj Bjorner
a0ed6096eb remove unused 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:01 -08:00
Nikolaj Bjorner
8a88356fa5 update java API code to work with boolean pointers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:01 -08:00
Nikolaj Bjorner
913779d507 open_log returns bool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:01 -08:00
Nikolaj Bjorner
0fcc7b5123 update doc test string 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:01 -08:00
Josh Berdine
f0cb79fc21 Return bool instead of int in extra_API for Z3_open_log (#8048) 
The C declaration returns `bool`.

Signed-off-by: Josh Berdine <josh@berdine.net>
 2026-02-18 20:56:01 -08:00
Josh Berdine
d8ac364bf7 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 <josh@berdine.net>
 2026-02-18 20:56:01 -08:00
Josh Berdine
2b1583a7f0 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 <josh@berdine.net>
 2026-02-18 20:56:01 -08:00
Nikolaj Bjorner
66141dfdfa apply gcd test also before saturation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:00 -08:00
Nikolaj Bjorner
b50286084e use edit distance for simplified error messaging on wrong trace tags 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:56:00 -08:00
Lev Nachmanson
f8ce742890 try reordering before analyzing bounds 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-18 20:56:00 -08:00
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