mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Code Activity
13886 commits 23 branches 48 tags 156 MiB
Commit graph

13886 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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