mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
19997 commits 49 branches 53 tags 182 MiB
Commit graph

19997 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Jakob Rath
02ff7efe25 Remove unused method 2023-12-01 15:51:53 +01:00
Jakob Rath
6ce63154d2 each overlapping variable needs to be explained only once 2023-12-01 15:49:39 +01:00
Jakob Rath
e1d23642bc Fix dependency tracking for viable_fallback 
now takes into account explanations for overlapping variables
 2023-12-01 15:45:23 +01:00
Jakob Rath
555ac49023 shortcut 2023-12-01 15:23:48 +01:00
Jakob Rath
878d4a2fd0 Collect relevant entries 2023-12-01 15:18:57 +01:00
Jakob Rath
7987ac4475 check for full intervals 2023-12-01 15:14:16 +01:00
Jakob Rath
a3bf994aa4 viable: store origin pvar in entry 2023-12-01 13:19:20 +01:00
Jakob Rath
828f74db73 slicing::explain_simple_overlap 2023-12-01 13:15:45 +01: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
Nikolaj Bjorner
41a3196c89 fix #7024 2023-11-29 13:35:30 -08:00
Nikolaj Bjorner
d469c1054e remove separate to_add_literal queue 2023-11-29 12:45:43 -08:00
Nikolaj Bjorner
e972eb33b2 #6523 - contains_ptr bug regarding etable reinserts 2023-11-29 10:44:36 -08:00
Jakob Rath
cf9b7bed0c imports 2023-11-29 16:03:47 +01:00
Jakob Rath
e76c6b0fdc fix test 2023-11-29 15:04:23 +01:00
Jakob Rath
872459170f viable fallback with overlaps 2023-11-29 15:04:23 +01:00
Jakob Rath
27bc858509 univariate solver: support constraints on lower bits 2023-11-29 15:04:23 +01:00
Jakob Rath
c29d04d431 fix compiler error (2) 2023-11-29 15:04:23 +01:00
Jakob Rath
923e4b4bd9 fix compile error 2023-11-29 15:04:23 +01:00
Jakob Rath
79d77bc690 exit conditions 2023-11-29 15:04:23 +01:00
Jakob Rath
590e9b0fb1 outer loop, to continue search after recursive call 2023-11-29 15:04:23 +01:00
Jakob Rath
5d3a5a94e8 update progress 2023-11-29 15:04:23 +01:00
Jakob Rath
179da49379 fix 2023-11-29 15:04:23 +01:00
Jakob Rath
0b98a76177 refinement 2023-11-29 15:04:23 +01:00
Jakob Rath
203df6babb fix recursion in case of large gap 2023-11-29 15:04:23 +01:00
Jakob Rath
39bee180de store bit-intervals that were used 2023-11-29 15:04:23 +01:00
Jakob Rath
3740e766f7 check bits for next_val 2023-11-29 15:04:23 +01:00
Jakob Rath
2a3c8d2b82 find_on_layer: refactor interval loop 2023-11-29 15:04:22 +01:00
Jakob Rath
91a47b262b find_on_layer: fixed bits refinement 2023-11-29 15:04:22 +01:00
Jakob Rath
6fa3af29c6 return entry from refine_bits 2023-11-29 15:04:22 +01:00