mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-21 16:16:38 +00:00
Code Activity
18382 commits 23 branches 48 tags 157 MiB
Commit graph

18382 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 14935529b8 add readme under content 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 20:04:48 -08:00
Nikolaj Bjorner c33859d729 try adding readme again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 20:04:48 -08:00
Nikolaj Bjorner 165d81cac4 follow error message to put dependencies in setup args 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 20:04:47 -08:00
Nikolaj Bjorner dd271563d3 add version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 20:04:47 -08:00
Nikolaj Bjorner 7b145f36bd try add name to project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 20:04:47 -08:00
Nikolaj Bjorner 2323a5f9d2 try fix suggested in #7041 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 20:04:47 -08:00
Nikolaj Bjorner dc83c5b28d fix #7049 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 20:04:47 -08:00
Nikolaj Bjorner 96f84c6b44 kludge to fixup osver in python for Mac 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 20:04:47 -08:00
Nikolaj Bjorner f91655ce15 fix divergence reported by Guido Martinez 2023-12-13 20:04:47 -08:00
Nikolaj Bjorner e5375c4071 fuzz fixes to semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 17:19:16 -08:00
Nikolaj Bjorner 236ec01b78 disable from python build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 14:17:19 -08:00
Nikolaj Bjorner 03730b2aad new files 2023-12-13 14:16:35 -08:00
Nikolaj Bjorner 5dfe86fc2d bugfixes in intblast solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 14:13:16 -08:00
Nikolaj Bjorner 5fdfd4f3f4 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 08:17:21 -08:00
Nikolaj Bjorner c6a8ae1e8c include nyis 2023-12-12 18:00:43 -08:00
Nikolaj Bjorner 34229eaa8e na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-12 16:37:39 -08:00
Nikolaj Bjorner 35eb95b447 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-12 15:42:39 -08:00
Nikolaj Bjorner 40e93d7478 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-12 15:09:08 -08:00
Nikolaj Bjorner 9b435eda90 fixes 2023-12-12 14:53:10 -08:00
Nikolaj Bjorner 7247bbb78f na/ 2023-12-12 14:42:34 -08:00
Nikolaj Bjorner 06ebf9a02a n/a 2023-12-12 14:41:31 -08:00
Nikolaj Bjorner 4cadf6d9f2 preparing intblaster as self-contained solver. 
add activate and propagate to constraints
support axiomatized operators band, lsh, rshl, rsha
 2023-12-12 11:11:37 -08:00
Nikolaj Bjorner c72780d9b9 b-and, stats, reinsert variable to heap, debugging 2023-12-11 20:22:23 -08:00
Nikolaj Bjorner b72575148f axioms for b-and 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-11 15:45:54 -08:00
Nikolaj Bjorner 15bae80cea handle more intblast cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-11 15:00:06 -08:00
Nikolaj Bjorner 727a738958 new files 2023-12-11 14:51:31 -08:00
Nikolaj Bjorner 17c480f837 adding band 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-11 14:51:21 -08:00
Nikolaj Bjorner 5622b13ed3 working on model extraction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-11 12:53:51 -08:00
Nikolaj Bjorner 9373e1b7f5 intblast debugging 2023-12-11 10:00:11 -08:00
Nikolaj Bjorner f89de2b455 more internalize cases 2023-12-10 23:49:23 -08:00
Nikolaj Bjorner 286932684a sign and zero extend 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-10 23:15:03 -08:00
Nikolaj Bjorner dc690307ff sign and zero extend 2023-12-10 23:14:24 -08:00
Nikolaj Bjorner 6518d71c6d rename polysat files to exclude namespace 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-10 22:47:27 -08:00
Nikolaj Bjorner 83c71b4943 fix internalization for quot/rem 2023-12-10 22:21:14 -08:00
Nikolaj Bjorner 21121f14a5 dbg 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-10 20:48:46 -08:00
Nikolaj Bjorner 701671466b integrating int-blaster 2023-12-10 19:55:25 -08:00
Nikolaj Bjorner 09c2e0dd6e integrate intblast solver 2023-12-10 13:00:43 -08:00
Nikolaj Bjorner 9931c811ca start intblast solver 2023-12-10 12:31:10 -08:00
Nikolaj Bjorner d64a2bdbed include dependency in cmakelist 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-10 10:27:22 -08:00
Nikolaj Bjorner b56a8fa264 deal with build errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-10 10:03:43 -08:00
Nikolaj Bjorner 7ba5d2024d remove stale file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-09 17:26:32 -08:00
Nikolaj Bjorner 21ef689918 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-09 17:16:31 -08:00
Nikolaj Bjorner 207735d55c n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-09 17:14:59 -08:00
Nikolaj Bjorner 2b49bd189a fixed fixme 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-09 16:20:35 -08:00
Nikolaj Bjorner 09eac8e371 allow tracking values of constraints 2023-12-09 16:15:24 -08:00
Nikolaj Bjorner 0c2ecf8b90 working on viable 2023-12-09 13:10:47 -08:00
Nikolaj Bjorner 94ba85bb12 updates to viable 2023-12-09 12:08:02 -08:00
Nikolaj Bjorner 683a5dda37 remove include to bv-params 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-09 10:58:54 -08:00
Nikolaj Bjorner 70bddb35be update viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-09 09:44:05 -08:00
Nikolaj Bjorner bff51b699d remove stale files 2023-12-09 09:39:59 -08:00