mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity
18306 commits 23 branches 48 tags 156 MiB
Commit graph

18306 commits

This branch
This branch
All branches
Author SHA1 Message Date
Asger Hautop Drewsen a9513c1998
Improve BoolRef addition (#7045) 2023-12-05 09:12:25 -08:00
NikolajBjorner 7c81ee0890 fix case of README.md in nuget 
Signed-off-by: NikolajBjorner <nbjorner@microsoft.com>
 2023-12-05 09:02:08 -08:00
NikolajBjorner 669f665f24 update release pipeline 
Signed-off-by: NikolajBjorner <nbjorner@microsoft.com>
 2023-12-05 08:19:20 -08:00
NikolajBjorner aa2e54c5a4 update release pipeline 
Signed-off-by: NikolajBjorner <nbjorner@microsoft.com>
 2023-12-05 08:18:33 -08:00
NikolajBjorner 23fcb4376f readme 
Signed-off-by: NikolajBjorner <nbjorner@microsoft.com>
 2023-12-05 08:03:28 -08:00
NikolajBjorner f5ae8c324c make a readme file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-05 08:01:59 -08:00
Michał Górny 9ad4d50b5d
Use built-in importlib.resources on Python 3.9+ (#7042) 
Use built-in `importlib.resources` module rather than the external
`importlib_resources` package on Python 3.9 and newer.  The latter
is only intended as a backport for old Python versions, and since modern
Linux distributions may no longer support such old Python versions,
they also no longer provide importlib_resources (this is the case
on Gentoo).
 2023-12-05 07:49:32 -08:00
Asger Hautop Drewsen 764f0d54a4
Overload xor operator for BoolRef (#7043) 2023-12-05 07:48:57 -08:00
Rui Chen 4d4359f78a
fix shebang syntax issue (#7044) 2023-12-05 07:48:15 -08:00
Nikolaj Bjorner 389aea3330 update release notes, update version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-04 19:48:43 -08:00
Nikolaj Bjorner 5e3f1d988b update release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-04 19:38:52 -08:00
Nikolaj Bjorner 4a9b38e531 clean up nla_grobner 2023-12-04 17:08:17 -08:00
Nikolaj Bjorner 84a7a79e90 fix #7037 2023-12-04 17:08:01 -08:00
Nikolaj Bjorner f98b42ae42 install importlib-resources for ubuntu doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-04 10:33:29 -08:00
Nikolaj Bjorner de75692cb0 install importlib-resources for ubuntu doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-04 10:32:02 -08:00
Nikolaj Bjorner f7415bb677 install importlib-resources for ubuntu doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-04 10:32:02 -08:00
Nikolaj Bjorner 17913f3ec8 remove braces 2023-12-04 10:32:02 -08:00
Andrey Andreyevich Bienkowski 18f14921ba
Clarify optimizer guarantees (#7030) 
* Clarify optimizer guarantees (python)

* Clarify optimization guarantees (OCaml)

* Clarify optimizer guarantees (java)

* Clarify optimizer guarantees (.net)
 2023-12-04 09:32:26 -08:00
Christoph M. Wintersteiger 6910a4e18c
Fix to_fp_signed (#7034) 2023-12-03 16:38:06 -08:00
Nikolaj Bjorner ea3628e50b remove hoist functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-03 16:28:43 -08:00
Nikolaj Bjorner bd8bed1759 handle ac-op in legacy special relations procedure by adding warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-03 12:55:37 -08:00
Nikolaj Bjorner 1b1ebaa3b0 minor simplification during internalization 2023-12-03 12:43:39 -08:00
Nikolaj Bjorner 36725383d3 minor simplification of terms during internalization. 2023-12-03 12:43:14 -08:00
Nikolaj Bjorner f06e07ad0a fix cone of influence computation for terms with nested variables 
exposed by #7027, but generally missing. It is less likely to be exposed if input is normalized by distributing multiplication over addition.
 2023-12-03 12:42:42 -08:00
Nikolaj Bjorner 25dd29907b refine no-effect predicate to include value of ret 2023-12-03 12:41:21 -08:00
Nikolaj Bjorner 9cc2ce42f7 #7027 
fix lossy function declaration inclusion functionality exposed when fixing a bug for incomplete model generation.
 2023-12-03 11:14:18 -08:00
Nikolaj Bjorner a8f3396b24 #7033 2023-12-03 10:34:16 -08:00
Nikolaj Bjorner 965bee5801 fix build 2023-12-02 19:52:59 -08:00
Nikolaj Bjorner 1de25ed09c pending files 2023-12-02 19:43:51 -08:00
Nikolaj Bjorner b22daa9816 missing header 2023-12-02 19:39:43 -08:00
Nikolaj Bjorner 362d299a5c #7027 2023-12-02 19:34:36 -08:00
Nikolaj Bjorner ba8d8f0af7 Disable hoist entirely, it is bad on QF_LIA and does not help on other observed cases 2023-12-02 15:40:47 -08:00
Nikolaj Bjorner 585d027668 remove assert #7032 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-02 14:12:41 -08:00
Nikolaj Bjorner 331507c4cd #7027 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-02 12:05:06 -08:00
Nikolaj Bjorner 7eab26e3ef try with missed bounds 2023-12-02 10:48:40 -08:00
Nikolaj Bjorner 5c1e7f7112 fix #7029 2023-12-02 10:48:40 -08:00
Alexander Grund ed5ab54ab6
CMake: Improve handling of git hash/describe (#7028) 
Only check for and depend on the .git folder if requested.
Only warn about disabling when enabled.
Only add git hash to version if valid.
 2023-12-02 09:47:57 -08:00
Nikolaj Bjorner a15a7cee7b touch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-01 14:13:05 -08:00
Nikolaj Bjorner faf14012ba Regressions reported by Guido 2023-12-01 13:32:13 -08:00
Nikolaj Bjorner 99e2794a6d update output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-30 17:20:43 -08:00
Nikolaj Bjorner 8a0dec1a4b fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-30 14:08:29 -08:00
Nikolaj Bjorner b52fd8d954 add EUF plugin framework. 
plugin setting allows adding equality saturation within the E-graph propagation without involving externalizing theory solver dispatch. It makes equality saturation independent of SAT integration.
Add a special relation operator to support ad-hoc AC symbols.
 2023-11-30 13:58:30 -08:00
Lev Nachmanson 5784c2da79 remove an unnecessary if 2023-11-30 08:59:05 -10:00
Alper Altuntas d540d881ef
Add __enter__ and __exit__ methods to Solver class (#7025) 
To enable the usage of the with statement for the Solver class
instances, this commit adds __enter__ and __exit__ methods.
The with statement should offer a more concise and safer
alternative to explicit usage of push() and pop() methods.
 2023-11-30 08:35:08 -08:00
Nikolaj Bjorner 26440ed3d8 deal with ubuntu/clang warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-29 15:45:19 -08:00
Nikolaj Bjorner e9abdbb7a4 fix #7011 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-29 15:08:08 -08:00
Nikolaj Bjorner 9efe6f6afa fix regression in fix for #7006 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-29 14:54:54 -08:00
Nikolaj Bjorner faa2d8ac6c re-enable delayed literal propagation 2023-11-29 14:00:37 -08:00
Nikolaj Bjorner 2f01b5b567 re-enable delayed literal propagation 2023-11-29 14:00:17 -08:00
Nikolaj Bjorner 4289cfac8d revert some fixes to euf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-29 13:47:59 -08:00