mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity
14589 commits 46 branches 52 tags 178 MiB
Commit graph

14589 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
287bccde30 disable new incomplete functionality for master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-19 15:56:57 -07:00
Nikolaj Bjorner
1ce63363ba fix #4400 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-19 15:56:08 -07:00
Nikolaj Bjorner
7756e2c6d5
in progress (#4386) 
* initial work on replacing str in regex check

* finish rewriter for empty string in regex

* remove unnecessary argument in mk_regexp_contains_emptystr; initial template for eval_regexp_derivative

* progress on string in regexp general check using derivatives

* added recursive nullable and derivative funcitons, partially working

* remove tests from z3test

* fix rewriting infinite loop and some failing simplify checks

* several fixes addressing comments for z3 main branch PR #4386

* redo derivative to return an expr_ref, and null on failure

Co-authored-by: calebstanford-msr <t-casta@microsoft.com>
 2020-05-19 15:55:19 -07:00
Nikolaj Bjorner
b3366bae5a remove test-examples from MacOS build, re-add maxsat example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-19 13:52:44 -07:00
Nikolaj Bjorner
fca44ff3f2 fix #4394 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-19 13:40:03 -07:00
Nikolaj Bjorner
72d129eb75 #4396 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-19 13:13:09 -07:00
Lev Nachmanson
af2f74c05f
smarter explanation.h (#4385) 
* smarter explanation.h

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* clean explanation API

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* suppress warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* disable the warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-19 12:38:44 -07:00
Alexey Vishnyakov
3b0c40044f
SINGLE_THREAD: do not use pthread if possible (#4382) 2020-05-19 09:45:41 -07:00
Nikolaj Bjorner
5fe0eeda63 disable regressions in ST mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-19 09:37:06 -07:00
Nuno Lopes
232f1b5fbe fix a gcc 10 warning 2020-05-19 14:44:14 +01:00
Nikolaj Bjorner
0f8f886389 use single return pattern 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 20:27:50 -07:00
Nikolaj Bjorner
bc03ffb800 typing error 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 20:19:33 -07:00
Nikolaj Bjorner
7f22eb594e don't pretend to handle new operators #4387 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 20:04:43 -07:00
Nikolaj Bjorner
e525543bd0 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 19:47:13 -07:00
Nikolaj Bjorner
d26ef08c69 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 19:41:37 -07:00
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