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

17153 commits

Author SHA1 Message Date
Nikolaj Bjorner
e4697fe18e remove set cardinality operators from array theory. Make final-check use priority levels 
Issue #7502 shows that running nlsat eagerly during final check can block quantifier instantiation.
To give space for quantifier instances we introduce two levels for final check such that nlsat is only applied in the second and final level.
 2026-02-18 20:56:51 -08:00
Nikolaj Bjorner
7b9eb2a92f fix second byref to bool 2026-02-18 20:56:03 -08:00
Nikolaj Bjorner
c033f432d8 remove references to set_has_size 2026-02-18 20:56:03 -08:00
Nikolaj Bjorner
58d86c2798 use c_bool instead of c_int for sign 2026-02-18 20:56:02 -08:00
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
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
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
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