mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-19 16:53:18 +00:00
Code Activity
20152 commits 79 branches 53 tags 204 MiB
Commit graph

16947 commits

Author SHA1 Message Date
Nikolaj Bjorner
1c3fb49878 port dotnet to use bool sorts from API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-25 21:44:41 -08:00
Nikolaj Bjorner
eecd052730 port to BoolPtr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-25 21:08:43 -08:00
Nikolaj Bjorner
39e427a229 remove unused 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-25 21:06:11 -08:00
Nikolaj Bjorner
8346bb6679 open_log returns bool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-25 20:48:57 -08:00
Nikolaj Bjorner
bcf2c0b3a9 update doc test string 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-25 20:15:48 -08:00
Josh Berdine
239e0949db
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>
 2025-11-25 18:11:38 -08:00
Josh Berdine
4af83e8501
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>
 2025-11-25 18:10:38 -08:00
Josh Berdine
4401abbb4a
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>
 2025-11-25 18:08:17 -08:00
Nikolaj Bjorner
40d8d5ad9a apply gcd test also before saturation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-24 18:08:30 -08:00
Nikolaj Bjorner
01afda6378 use edit distance for simplified error messaging on wrong trace tags 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-24 15:46:38 -08:00
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
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
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
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