Murphy Berzish
|
da68c3213c
|
Unicode for Z3str3 (#4981)
* z3str3: remove hard-coded char set
* z3str3: remove hard-coded char set
* z3str3: use char abstraction
* z3str3: scope management for unicode chars
* add QF_CHAR for z3str3
* z3str3: remove hard-coded char set
* z3str3: use char abstraction
* z3str3: scope management for unicode chars
* add QF_CHAR for z3str3
* z3str3: add 'char' string solver case
* z3str3: fix mk_char using the wrong ast manager
* z3str3: fix refcounted character vectors
|
2021-01-29 06:14:38 -08:00 |
|
Nikolaj Bjorner
|
cfcd7f18a9
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-01-28 17:09:12 -08:00 |
|
Nikolaj Bjorner
|
afc4c700b1
|
move directory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-01-28 14:49:15 -08:00 |
|
Nikolaj Bjorner
|
42e601483d
|
add selected updates #4981
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-01-28 13:43:30 -08:00 |
|
Nikolaj Bjorner
|
e3d634807b
|
move common routines for quantifiers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-01-28 13:23:40 -08:00 |
|
Nikolaj Bjorner
|
5414030875
|
#4939 escape character
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-01-28 11:57:00 -08:00 |
|
Nikolaj Bjorner
|
f48fb8d3e8
|
it just works
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-01-28 11:12:05 -08:00 |
|
Nikolaj Bjorner
|
8a229bf684
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-01-27 22:39:02 -08:00 |
|
Nikolaj Bjorner
|
49aebdbb02
|
adding unicode fixup base on #4939 discussion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-01-27 20:21: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
|
579caab025
|
na
|
2021-01-27 19:35:34 -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 |
|
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 |
|
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
|
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
|
dafee71500
|
reshuffle unicode support to use global parameter, and use bit-vectors on demand
|
2021-01-21 14:24:26 -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 |
|
Nikolaj Bjorner
|
48058e706f
|
fix #4951
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-01-20 02:21:42 -08:00 |
|
Nikolaj Bjorner
|
fa4869e400
|
fix #4949 - and/or get rewritten depending on parameters for rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2021-01-20 01:08:54 -08:00 |
|