mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-01 00:39:52 +00:00
Code Activity
20192 commits 49 branches 53 tags 193 MiB
Commit graph

20192 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
3cff4d3410 refactor 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
f46cc6814a add trace tag for levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
1066f3ea3b pass nlsat::solver to levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
9a11697167 use new display functions 2025-12-03 11:16:25 -10:00
Lev Nachmanson
b4dcf0afd7 create free function display functions 2025-12-03 11:16:25 -10:00
Lev Nachmanson
2c35dae2e2 pass pmanager 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
a79c0a7901 pass anum_manager to levelwise, crash on sign 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
856c71acb2 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
2216825f43 more accurate init of the relation between polynomial properties 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
5e1572d610 use std::map instead of std::unordered_map 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
2c5a7c965f t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
0d8d77277f define symbolic_interval 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
6ef4743015 more scaffolding 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
80f2a8b17c closer to the paper 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
7cd68fee7b scaffolding 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
b64ce02dc2 scaffoldin 2025-12-03 11:16:25 -10:00
Lev Nachmanson
cdbc89964f t2 2025-12-03 11:16:25 -10:00
Lev Nachmanson
d3a576411f t1 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
1035c95234 t0 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 11:16:25 -10:00
Lev Nachmanson
52949f2d79 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-03 06:49:00 -10:00
Copilot
595513611e
Disable C++98 compatibility warnings for Clang builds (#8060) 
* Initial plan

* Disable C++98 compatibility warnings for Clang to fix vcpkg build freeze

Add -Wno-c++98-compat and -Wno-c++98-compat-pedantic flags to prevent
excessive warning output when building with clang-cl or when -Weverything
is enabled. These warnings are not useful for Z3 since it requires C++20.

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-12-03 08:27:25 -08:00
Lev Nachmanson
7de648ff81 remove unused *_signed_project() methods 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-12-02 18:46:16 -10:00
Nikolaj Bjorner
a5488cf6e7 fix #8054 
inherit denominators when evaluating polynomials
 2025-11-30 07:51:06 -08:00
Nikolaj Bjorner
3712d1e0f1 fix #8055 2025-11-29 15:39:50 -08:00
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