Nikolaj Bjorner
|
ff34d84b35
|
ranges are never nullable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 19:41:04 -07:00 |
|
Nikolaj Bjorner
|
6e55880601
|
constant folding
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 19:38:21 -07:00 |
|
Nikolaj Bjorner
|
5bbf05c93c
|
kleene
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 19:35:31 -07:00 |
|
Nikolaj Bjorner
|
fcd2bc605c
|
try to make template parsing work
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 19:17:36 -07:00 |
|
Nikolaj Bjorner
|
323a752bbf
|
disable maxsat. for a mysterious reason it started failing on a single macos build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 19:16:32 -07:00 |
|
Nikolaj Bjorner
|
55225824ee
|
remove std::mutex, replace by util/mutex.h in api_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 19:15:11 -07:00 |
|
Nikolaj Bjorner
|
10edee48f3
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 19:11:59 -07:00 |
|
Nikolaj Bjorner
|
9d6c870e97
|
remove case with hi = 0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 19:11:35 -07:00 |
|
Nikolaj Bjorner
|
f8d328b1fb
|
add nullable, get-head-tail with Caleb
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 19:10:00 -07:00 |
|
Nikolaj Bjorner
|
c40c4313a4
|
parens
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 18:07:40 -07:00 |
|
Nikolaj Bjorner
|
5844964d95
|
rename temporary macro
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 17:17:51 -07:00 |
|
Nikolaj Bjorner
|
8e8e9be25f
|
st
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 16:49:43 -07:00 |
|
Nikolaj Bjorner
|
c2a59a89af
|
thanks to https://github.com/Z3Prover/z3/pull/4382#issuecomment-630468832_
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 15:32:23 -07:00 |
|
Nikolaj Bjorner
|
801eb47fae
|
remove thread dependency in symbol.cpp on single thread #4382
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 15:16:08 -07:00 |
|
Nikolaj Bjorner
|
ff10afd226
|
remove thread dependency in symbol.cpp on single thread #4382
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 15:11:24 -07:00 |
|
Nikolaj Bjorner
|
f538ee3fe2
|
another module level ifdef for #4382
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 15:07:39 -07:00 |
|
Nikolaj Bjorner
|
fd57faee7c
|
another module level ifdef for #4382
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 15:03:58 -07:00 |
|
Nikolaj Bjorner
|
c8c02060ee
|
another module level ifdef for #4382
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 15:01:27 -07:00 |
|
Nikolaj Bjorner
|
d603bd7e3b
|
disable selected functionality in SINGLE_THREAD mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 14:47:33 -07:00 |
|
Nikolaj Bjorner
|
1072bf1536
|
deal with unsigned / bignum #4361
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-18 14:42:06 -07:00 |
|
Nikolaj Bjorner
|
78a4717c06
|
fix #4359 and regression to #3270
|
2020-05-18 12:41:42 -07:00 |
|
Murphy Berzish
|
1c760b04cf
|
re.range with non-unit arguments is the empty language (#4360)
|
2020-05-17 19:08:50 -07:00 |
|
Murphy Berzish
|
152d6338f8
|
fix hex digit radix in unicode escape (#4356)
|
2020-05-17 19:07:51 -07:00 |
|
Nikolaj Bjorner
|
1def58bc9f
|
optional unicode mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-17 19:06:34 -07:00 |
|
Nikolaj Bjorner
|
30f17b1509
|
fix #4355
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-17 12:28:30 -07:00 |
|
Nikolaj Bjorner
|
951c769fc9
|
fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-17 12:20:33 -07:00 |
|
Nikolaj Bjorner
|
1bfc12d6e6
|
initial stab at independent unicode module
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-17 11:42:39 -07:00 |
|
Nikolaj Bjorner
|
fc8dfe3e40
|
seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-17 05:35:32 -07:00 |
|
Nikolaj Bjorner
|
34cc60410f
|
additional str/re operators, remove encoding option from zstring
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-17 05:08:36 -07:00 |
|
Nikolaj Bjorner
|
b2bfb1faea
|
fix nla_monotone lemmas again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-16 17:26:54 -07:00 |
|
Murphy Berzish
|
3147be66fe
|
z3str3: fix up regex heuristics (#4342)
fixes #4308, partially fixes #4309
|
2020-05-16 17:17:32 -07:00 |
|
Nikolaj Bjorner
|
bfb38451d1
|
add unicode encoding back
|
2020-05-16 17:11:47 -07:00 |
|
Nikolaj Bjorner
|
cd64967706
|
fix #4317
|
2020-05-16 17:11:47 -07:00 |
|
Lev Nachmanson
|
aaf05f18ab
|
fix a bug in an simplifying interval expressions with terms
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-16 15:19:32 -07:00 |
|
Nikolaj Bjorner
|
363690791a
|
update TBD
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-16 14:34:39 -07:00 |
|
Murphy Berzish
|
6f0a367357
|
add SMTLIB2.6 names for QF_SLIA and string-int conversion operators (#4341)
|
2020-05-16 14:31:47 -07:00 |
|
Nikolaj Bjorner
|
21c4d451d8
|
parse RegLan
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-16 14:26:53 -07:00 |
|
Lev Nachmanson
|
d3c00ca2c3
|
change mode to executable to some py files
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-16 14:12:16 -07:00 |
|
Nikolaj Bjorner
|
4753d93bb7
|
add some of the SMTLIB2.6 conventions and features to strings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-16 14:00:02 -07:00 |
|
Nikolaj Bjorner
|
1ab2ad07be
|
outline of unicode parsing #4333
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-16 13:36:43 -07:00 |
|
Nikolaj Bjorner
|
937afbf95b
|
draft rewrite
|
2020-05-16 12:43:26 -07:00 |
|
Nikolaj Bjorner
|
843b6cf149
|
fix #4336 - check return values of eval, they can be null due to cancelation
|
2020-05-16 12:43:26 -07:00 |
|
Nikolaj Bjorner
|
a3f56f0d95
|
revert 'fix'
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-16 12:43:26 -07:00 |
|
Nuno Lopes
|
e6ee58b628
|
restore exec bit on a few more script; trying to unbreak buildbots
|
2020-05-16 20:15:10 +01:00 |
|
Nuno Lopes
|
0313cf6d4c
|
restore exec bit on configure & scripts/*.sh
|
2020-05-16 20:07:36 +01:00 |
|
Nikolaj Bjorner
|
2822922d36
|
fix regression with mainintaing signs for monotonicity lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-16 11:17:40 -07:00 |
|
Nikolaj Bjorner
|
d352c61e01
|
fix regression with mainintaing signs for monotonicity lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-16 11:17:39 -07:00 |
|
Lev Nachmanson
|
cd833e892f
|
avoid iterations on std::unordered_set
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-16 08:55:15 -07:00 |
|
Murphy Berzish
|
ce07138008
|
Merge pull request #4325 from mtrberzi/issue4322
ignore true/false/null literals during theory case split propagation
|
2020-05-15 20:42:33 -05:00 |
|
Murphy Berzish
|
fcbcad6c10
|
Merge pull request #4320 from mtrberzi/mc-rational
z3str3: use rational in place of unsigned during model construction
|
2020-05-15 20:42:19 -05:00 |
|