mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
18921 commits 49 branches 53 tags 182 MiB
Commit graph

18921 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
561d3e8eb9 rename polysat files to exclude namespace 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 16:21:01 -08:00
Nikolaj Bjorner
a2d64e8441 fix internalization for quot/rem 2023-12-16 16:20:59 -08:00
Nikolaj Bjorner
2a3cfe0cb9 dbg 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 16:20:25 -08:00
Nikolaj Bjorner
a5491804c7 integrating int-blaster 2023-12-16 16:20:23 -08:00
Nikolaj Bjorner
d72938ba9a integrate intblast solver 2023-12-16 16:18:08 -08:00
Nikolaj Bjorner
81411a5fcb start intblast solver 2023-12-16 16:17:21 -08:00
Nikolaj Bjorner
30edeb85ba include dependency in cmakelist 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 16:14:10 -08:00
Nikolaj Bjorner
ab668cbe6c deal with build errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 16:14:08 -08:00
Nikolaj Bjorner
fd6e9a0118 remove stale file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 16:13:19 -08:00
Nikolaj Bjorner
ed3c9e1f27 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 16:13:19 -08:00
Nikolaj Bjorner
17c7f2e826 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 16:13:19 -08:00
Nikolaj Bjorner
920f494a0c fixed fixme 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 16:13:19 -08:00
Nikolaj Bjorner
75e83b8c1e allow tracking values of constraints 2023-12-16 16:13:19 -08:00
Nikolaj Bjorner
0dd4f0cf71 working on viable 2023-12-16 16:13:17 -08:00
Nikolaj Bjorner
30c874d301 updates to viable 2023-12-16 16:12:50 -08:00
Nikolaj Bjorner
e9c86bf3a3 remove include to bv-params 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 16:12:50 -08:00
Nikolaj Bjorner
c0a8da34af update viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 16:12:50 -08:00
Nikolaj Bjorner
faa6c14610 remove stale files 2023-12-16 16:12:49 -08:00
Nikolaj Bjorner
81c6f00c99 reorganize polysat functionality to use abstract solver interface 
make dependency be self-contained
 2023-12-16 16:12:49 -08:00
Nikolaj Bjorner
837e111d93 porting viable 2023-12-16 16:12:49 -08:00
Nikolaj Bjorner
c7d6a8e570 porting viable 2023-12-16 16:12:46 -08:00
Nikolaj Bjorner
6a0f407019 add log helper to util 2023-12-16 16:12:13 -08:00
Nikolaj Bjorner
c41477aadb port forbidden intervals 2023-12-16 16:12:13 -08:00
Nikolaj Bjorner
4bcd2e038f port over ule_constraint 2023-12-16 16:12:12 -08:00
Nikolaj Bjorner
1465f1d974 tidy' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 16:12:12 -08:00
Nikolaj Bjorner
d0d9b4dd17 tidy' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 16:12:12 -08:00
Nikolaj Bjorner
2c7e5e1730 n/a 2023-12-16 16:12:12 -08:00
Nikolaj Bjorner
a9550a3899 n/a 2023-12-16 16:12:12 -08:00
Nikolaj Bjorner
971594baec allow propagation on equalities and literals that are not assigned. 2023-12-16 16:12:12 -08:00
Nikolaj Bjorner
44506096f7 tidy 2023-12-16 16:12:12 -08:00
Nikolaj Bjorner
28820c8e0c v2 of polysat 2023-12-16 16:12:12 -08:00
Nikolaj Bjorner
bdc40b1f5f na 2023-12-16 16:10:06 -08:00
Nikolaj Bjorner
d0a59f3740 intblast with lazy expansion of shl, ashr, lshr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 15:12:57 -08:00
Bruce Mitchener
50e0fd3ba6
Use noexcept more. (#7058) 2023-12-16 12:14:53 +00:00
Nikolaj Bjorner
275e72a358 refactor for handling cores 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-15 16:28:59 -08:00
Nikolaj Bjorner
657dcdeb61 ps 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-15 16:02:13 -08:00
Nikolaj Bjorner
b44ab2f620 add rewriters for and 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-15 14:55:02 -08:00
Nikolaj Bjorner
a6e08b22f8 add rewrites for band 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-15 14:54:20 -08:00
Nikolaj Bjorner
4778f27b46 revert to standard solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-15 14:33:23 -08:00
Nikolaj Bjorner
d0b03a1526 work on ashr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-15 14:30:13 -08:00
Nikolaj Bjorner
a3f3abb8f2 use suggestion from #7047 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-15 13:59:06 -08:00
Nikolaj Bjorner
9293923b8a Add intblast solver 2023-12-15 13:50:38 -08:00
Nikolaj Bjorner
faa3a7ab4f updates to poly 2023-12-15 13:50:26 -08:00
Nikolaj Bjorner
196409b302 refactor polysat core / solver interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-15 10:40:02 -08:00
Nikolaj Bjorner
922358b9ba import pdd updates from polysat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-15 08:59:05 -08:00
Nikolaj Bjorner
0520558fc0 port updated pdd from polysat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-15 08:54:03 -08:00
Christoph M. Wintersteiger
2e83352d42
Fix bug in fp.round_to_integral (#7060) 2023-12-15 08:34:27 -08:00
Bruce Mitchener
e90a844508
Use override more. (#7059) 2023-12-15 08:44:57 +00:00
Nikolaj Bjorner
3c21e3ae42 add and fix axioms 2023-12-14 20:12:09 -08:00
Nikolaj Bjorner
ce1acd8c41 fix encoding bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-14 19:30:21 -08:00