3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Commit graph

14863 commits

Author SHA1 Message Date
Nikolaj Bjorner
a526eea123 doc/api not doc/html
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-27 20:01:46 -08:00
Nikolaj Bjorner
e61949059d compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-27 19:50:34 -08:00
Nikolaj Bjorner
1800b48258 zip doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-01-27 19:38:51 -08:00
Nikolaj Bjorner
579caab025 na 2021-01-27 19:35:34 -08:00
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