mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
19086 commits 23 branches 48 tags 157 MiB
Commit graph

19086 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
a88daf246e fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-25 23:45:14 -07:00
Nikolaj Bjorner
ba1630f380 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-25 23:40:05 -07:00
Nikolaj Bjorner
848bfb14a1 use common infrastructure for sls-smt 2024-10-25 23:29:26 -07:00
Nikolaj Bjorner
894bfc7e17 fixes 2024-10-25 22:46:15 -07:00
Nikolaj Bjorner
22ab598d73 bug fixes 2024-10-25 17:26:33 -07:00
Nikolaj Bjorner
ef95b4eaf2 add plugin to smt_context, factor out sls_smt_plugin functionality. 2024-10-25 17:15:05 -07:00
Nikolaj Bjorner
f453cdec92 update log level 2024-10-22 09:58:36 -07:00
Nikolaj Bjorner
93086143b3 fix dirty flag setting 2024-10-21 19:57:47 -07:00
Nikolaj Bjorner
b0dd83cc60 debugging parallel integration 2024-10-21 13:27:01 -07:00
Nikolaj Bjorner
185ddd6488 Track shared variables using a unit set 2024-10-20 17:54:44 -07:00
Nikolaj Bjorner
59b0e46d99 rename aux functions 2024-10-20 16:46:19 -07:00
Nikolaj Bjorner
cc430987b7 add value transfer option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-20 16:38:00 -07:00
Nikolaj Bjorner
68ee5108d8 update the interface in sls_solver to transfer phase between SAT and SLS 2024-10-20 15:42:26 -07:00
Nikolaj Bjorner
a48044c6e0 adding model-based sls for datatatypes 2024-10-20 10:20:38 -07:00
Nikolaj Bjorner
3f33e2c098 delay distinct axiom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-18 15:41:42 -07:00
Nikolaj Bjorner
6c3fe3cf46 saturate worklist 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-18 14:05:10 -07:00
Nikolaj Bjorner
a72ad44200 fixup interpretation building 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-18 13:34:55 -07:00
Nikolaj Bjorner
aa2292d5c4 fixes to occurs check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-18 10:41:27 -07:00
Nikolaj Bjorner
5864fcba6b fixing model construction for underspecified operators 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-18 09:34:49 -07:00
Nikolaj Bjorner
7b42ab5264 redo dfs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-17 12:59:59 -07:00
Nikolaj Bjorner
69c28f8652 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-17 11:35:31 -07:00
Nikolaj Bjorner
0218a15f2e fixup finite domain search 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-16 20:59:28 -07:00
Nikolaj Bjorner
8ababafe42 fixup finite domain search 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-16 20:41:20 -07:00
Nikolaj Bjorner
6143070157 add missing factory plugins to model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-16 19:47:13 -07:00
Nikolaj Bjorner
0755b2b5f7 axiomatize dt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-16 19:01:20 -07:00
Nikolaj Bjorner
180614330a Refactor context management, improve datatype handling, and enhance logging in sls plugins. 2024-10-15 20:33:53 -07:00
Nikolaj Bjorner
af687532aa updated sls-datatype 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-15 16:59:34 -07:00
Nikolaj Bjorner
295be7579c added cycle detection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-15 13:39:45 -07:00
Nikolaj Bjorner
a4275dfb15 dt updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-15 09:36:07 -07:00
Nikolaj Bjorner
b551f22aca adt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-14 21:17:57 -07:00
Nikolaj Bjorner
5fdf300557 adding dt plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-14 17:55:52 -07:00
Nikolaj Bjorner
ef20237edd fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-14 11:31:34 -07:00
Nikolaj Bjorner
54cce7b10b restore use of value_hash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-14 10:46:31 -07:00
Nikolaj Bjorner
f136d46fb4 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-13 19:23:05 -07:00
Nikolaj Bjorner
04824786be fix test for new signature of flip 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-13 15:26:08 -07:00
Nikolaj Bjorner
c1b9a3cc9e allow for alternating 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-13 13:32:56 -07:00
Nikolaj Bjorner
9b54254fa2 throttle save model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-12 19:09:25 -07:00
Nikolaj Bjorner
2bd335db81 alternate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-12 16:11:05 -07:00
Nikolaj Bjorner
609c46395f recover shift-weight loop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-12 15:29:48 -07:00
Nikolaj Bjorner
1765141261 fx 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-12 12:19:55 -07:00
Nikolaj Bjorner
766b9df4e2 fixup handling of disequality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-12 10:25:19 -07:00
Nikolaj Bjorner
d7b82366c6 avoid units 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-11 19:33:39 -07:00
Nikolaj Bjorner
2af713e4db fixing incremental 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-11 16:50:31 -07:00
Nikolaj Bjorner
46252b669c fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-11 16:17:54 -07:00
Nikolaj Bjorner
9eb6f97e6b fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-11 15:18:36 -07:00
Nikolaj Bjorner
d2ce7b0ea2 break build again 2024-10-11 14:53:12 -07:00
Nikolaj Bjorner
d278a1651d fix build 2024-10-11 14:28:36 -07:00
Nikolaj Bjorner
9b6c161ad2 break sls build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-11 14:02:42 -07:00
Nikolaj Bjorner
2ecb1c8b94 fix sls build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-11 14:02:06 -07:00
Nikolaj Bjorner
73f09fe94a updated package 2024-10-11 11:06:03 -07:00