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

20168 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
ab227c83b2 remove deprecated set_has_size 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-27 15:11:59 -08:00
Nikolaj Bjorner
8ba77dfc6b remove deprecated set_has_size 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-27 15:10:20 -08:00
Nikolaj Bjorner
682865df24 remove deprecated set_has_size 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-27 15:07:27 -08:00
Nikolaj Bjorner
449ce1a012 remove deprecated set_has_size 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-27 15:04:40 -08:00
Josh Berdine
aecf10b3ac
Fix _in vs _out def_API param for Z3_solver_get_levels (#8050) 
Signed-off-by: Josh Berdine <josh@berdine.net>
 2025-11-27 15:00:38 -08:00
Nikolaj Bjorner
f98fd2a137 refine givup conditions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-27 14:59:48 -08:00
Nikolaj Bjorner
482fa7dadf insert theory only once 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-27 10:34:01 -08:00
Nikolaj Bjorner
62b3668beb 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.
 2025-11-26 15:35:19 -08:00
Nikolaj Bjorner
28dc71c75e fix second byref to bool 2025-11-26 14:40:11 -08:00
Nikolaj Bjorner
ed8b92411e remove references to set_has_size 2025-11-26 13:57:24 -08:00
Nikolaj Bjorner
fab414a7ab use c_bool instead of c_int for sign 2025-11-26 13:55:06 -08:00
Nikolaj Bjorner
233184944c fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-26 09:43:52 -08:00
Nikolaj Bjorner
8298302358 python type fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-26 09:35:07 -08:00
Nikolaj Bjorner
55fc9cb9e1 fix dotnet build errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-26 09:29:59 -08:00
Nikolaj Bjorner
d1272defeb fix warnings in nla_pp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-25 21:48:23 -08:00
Nikolaj Bjorner
324fb2194b fix warnings in nra_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-25 21:46:51 -08:00
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
15274cdf53 fix type for BoolPtr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-25 21:15:51 -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
e178b9fc62 update java API code to work with boolean pointers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-11-25 20:54:49 -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
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