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

17809 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
c8aab1972a have nightly generate doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 16:05:41 -08:00
Nikolaj Bjorner
3d4a43f07b have nightly generate doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 16:04:08 -08:00
Nikolaj Bjorner
7068ccdebd have nightly generate doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 16:01:42 -08:00
Nikolaj Bjorner
d08814a1fe have nightly generate doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 15:57:01 -08:00
Nikolaj Bjorner
909257f856 remove family id externals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:48:24 -08:00
Nikolaj Bjorner
d3564f5b50 move unicode toggle to char-plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:42:19 -08:00
Nikolaj Bjorner
0c770e25df na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:29:38 -08:00
Nikolaj Bjorner
e969bd1c97 fully remove seq-based characters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:26:44 -08:00
Nikolaj Bjorner
8d8fe872ad remove plugin status to theory_seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 06:22:25 -08:00
Nikolaj Bjorner
696b3c79b9 fixes to self-contained character unicode 2021-01-27 06:13:37 -08:00
Nikolaj Bjorner
d0f1d8f59e move to unicode as stand-alone theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-27 05:46:45 -08:00
Nikolaj Bjorner
ecba26beae missing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-26 17:07:46 -08:00
Nikolaj Bjorner
32058d9c68 add char_decl_plugin 2021-01-26 16:43:03 -08:00
Nikolaj Bjorner
20332c6d3e adding char decl plugin for separate theory treatment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-26 16:28:44 -08:00
Nikolaj Bjorner
33714ceb40 use _ 2021-01-26 14:56:48 -08:00
Nikolaj Bjorner
e26e38b654 add error generation for #4977 2021-01-26 14:55:42 -08:00
Nikolaj Bjorner
8ed1992029 char value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-26 11:29:40 -08:00
Nikolaj Bjorner
a0b7879dd9 handle signed characters convertions into unsigned numbers 2021-01-26 11:20:28 -08:00
Nikolaj Bjorner
7dd7d83a36 make it easier to use string literals 2021-01-26 11:01:03 -08:00
Nikolaj Bjorner
31b7ad3012 prepare char utilities as a stand-alone theory 2021-01-26 10:34:10 -08:00
Matteo Nicoli
785fab74f4
Create bubble_sort.py (#4976) 2021-01-26 09:42:17 -08:00
Nikolaj Bjorner
dccfecb488 generator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-25 19:18:55 -08:00
Nikolaj Bjorner
4b6d7ca097 working on mam 2021-01-25 17:54:53 -08:00
Nikolaj Bjorner
f33d6f89b9 fix #4973 2021-01-25 12:20:27 -08:00
Nikolaj Bjorner
2646e0a1c0 have add_soft accept an interable of Booleans. 2021-01-25 12:17:35 -08:00
Nikolaj Bjorner
7d60d8462d patch for Sturm sequence bug #4961 2021-01-24 12:58:25 -08:00
Asger Gitz-Johansen
2d1684bc2d
Added the SUBMODULE_DIR_NAME variable for better submodule support (#4959) 
* Added the CMAKE_MODULE_DIR_NAME variable for better submodule support

* It should be called SUBMODULE_DIR_NAME instead
 2021-01-23 13:05:28 -08:00
Nikolaj Bjorner
47cb1d1207 remove bit-vector dependencies in theory_str_mc. See discussion #4939 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-23 13:03:06 -08:00
Nikolaj Bjorner
e4cec19f03 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-23 12:16:00 -08:00
Nikolaj Bjorner
96f1f4a567 rename to seq_char instead of seq_unicode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-23 12:12:06 -08:00
Artem Alekseev
7e668e9a1f
Fix build (#4960) 2021-01-23 11:13:10 -08:00
Nikolaj Bjorner
03fd251ccb streamline unicode/ascii toggling. Fix bit-width for unicode to 18 2021-01-23 11:11:44 -08:00
Nikolaj Bjorner
90eb4de526 track reference counts of allocated characters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-23 10:42:43 -08:00
Nikolaj Bjorner
6edabd6c03 egraph 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-22 18:11:27 -08:00
Nikolaj Bjorner
680b185872 adding ematching engine, fixing seq_unicode 2021-01-22 17:10:45 -08:00
Nikolaj Bjorner
db17ae03c6 early return, statistics, remove unused field 2021-01-21 23:53:34 -08:00
Nikolaj Bjorner
4c82350ca4 na 2021-01-21 23:35:04 -08:00
Nikolaj Bjorner
2051cac3a3 tidy 2021-01-21 23:34:47 -08:00
Nikolaj Bjorner
d2abc9ed0f remove comment #4956 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-21 22:18:24 -08:00
pcarbonn
0eb04df834
fix #4956 (#4958) 2021-01-21 22:16:49 -08:00
Nikolaj Bjorner
4e8ba8b160 regression fix, fix unicode mode 2021-01-21 22:06:15 -08:00
Nikolaj Bjorner
64ba44d2ac fix underflow bug when subtracting unsigned numbers 2021-01-21 21:01:02 -08:00
Nikolaj Bjorner
987efced76 upgrade compilers 2021-01-21 14:25:08 -08:00
Nikolaj Bjorner
6f09ecb229 set version 2021-01-21 14:24:58 -08:00
Nikolaj Bjorner
dafee71500 reshuffle unicode support to use global parameter, and use bit-vectors on demand 2021-01-21 14:24:26 -08:00
Nikolaj Bjorner
fb48481860 update version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 12:51:48 -08:00
Nikolaj Bjorner
517d907567 Update release.yml for Azure Pipelines 2021-01-20 12:06:47 -08:00
Nikolaj Bjorner
af914f101e change to macos latest 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 10:19:00 -08:00
Nikolaj Bjorner
c5432dbd88 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-20 09:12:09 -08:00
Nuno Lopes
3a572edb9c fix build 2021-01-20 10:42:29 +00:00