mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
14610 commits 49 branches 53 tags 182 MiB
Commit graph

14610 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
1e4e887221 propagate cheap eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Nikolaj Bjorner
865dfe0590 own refs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-12 17:07:06 -07:00
Jack Yao
55cd1e996c
add sat option for doing a global simplification before the bounded search and the main CDCL search loop. The option is also used for the sat-preprocess tacitc (#4514) 
Co-authored-by: rainoftime <rainoftime@gmail.com>
 2020-06-12 16:45:50 -07:00
Nikolaj Bjorner
41430cd128 register unhandled expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-12 16:12:24 -07:00
Nikolaj Bjorner
2613f74baa fix #4494 2020-06-11 00:05:19 -07:00
Nikolaj Bjorner
5a2b6d9c92 bounds on loop expressions 2020-06-11 00:04:41 -07:00
Nikolaj Bjorner
b0da5409c1 substitute into non-ground regexes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-09 14:58:25 -07:00
Nikolaj Bjorner
bac4726531 remove redundant method 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-09 14:40:17 -07:00
Nikolaj Bjorner
571e345d07 add mkStringSort 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-09 14:39:02 -07:00
Nikolaj Bjorner
e3d45b9850 refcount leaks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-09 14:19:26 -07:00
Nikolaj Bjorner
4fdfc65b37 tune seq rewriting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-09 13:30:39 -07:00
Nikolaj Bjorner
08cc5bc2e5 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-09 11:39:26 -07:00
calebstanford-msr
1fd567d1e9
fix bug in seq rewriter op_cache::find (#4509) 
* remove unneeded reverse case in derivative; placeholder for generalized lifted derivative

* experimental tweaks to RE rewriter to improve performance

* if-then-else lifting
(broken code -- preserving this commit in case this idea is useful later)

* if-then-else derivative optimizations: new approach templates

* implement if-then-else BDD normal form for derivatives
(code compiles but is still buggy)

* remove std::cout debugging for PR

* Revert "remove std::cout debugging for PR"

This reverts commit c7bdc44d31.

* debugging

* fix derivative interaction with reverse; add flags for left/right derivative and lifting over union/intersection

* remove debugging statements for PR

* Revert "remove debugging statements for PR"

This reverts commit 38e85a7288.

* revert some purely cosmetic changes from upstream; fix a bug

* revert unnecessary changes

* remove some redundant rewrites and add a new one for str.in_re(s, comp(r))

* add disabled rewrite for complement

* fix bug in op cache find (result was not saved)

* remove debugging std::cout for PR
 2020-06-09 11:36:31 -07:00
Nuno Lopes
ec1e733ef2 fix crash in qe_array ref counting due to wrong assignment operator of ptr_vector being called 
thanks to Arie Gurfinkel for reporting this
 2020-06-09 10:02:27 +01:00
Nikolaj Bjorner
5f9973d8c4 fix #4508 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-07 16:28:53 -07:00
Nikolaj Bjorner
d2a12f6db5 tuning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-07 12:52:13 -07:00
FabianWolff
cfed69caae
Remove __DATE__ to make the build more reproducible (#4505) 2020-06-07 12:28:39 -07:00
FabianWolff
30a3618ebf
Fix build failure on riscv64 (#4506) 2020-06-07 12:27:54 -07:00
Nuno Lopes
1809ee5107 fix regression in FPA internalization 2020-06-07 15:50:53 +01:00
Nikolaj Bjorner
ba1ca33637 normalization of union/intersection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-06 12:54:44 -07:00
Nikolaj Bjorner
ccea27de35 add nullable propagation instead of waiting for length assignment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-06 12:11:04 -07:00
Nikolaj Bjorner
65b6ccd651 add nullable propagation instead of waiting for length assignment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-06 11:32:43 -07:00
Nikolaj Bjorner
1b9fcc7098 integrate ite-normalized derivatives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-05 17:28:48 -07:00
Nikolaj Bjorner
4dbf7b183d inline conditions with derivative computation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-05 13:51:31 -07:00
Nikolaj Bjorner
a32fabf5ee fix #4403 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-05 13:51:31 -07:00
Andrew V. Jones
bb9cd5dd49
Ensure that the 'OUTPUT' locations in CMake for Python examples is accurate (#4499) 
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
 2020-06-04 15:04:01 -07:00
Nikolaj Bjorner
59e388ece1 handle bind proof constructor and print lambda 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 11:59:59 -07:00
Nikolaj Bjorner
e52eed325c close #4450 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 09:22:38 -07:00
Nikolaj Bjorner
57086edc42 close #4432 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 03:06:58 -07:00
Nikolaj Bjorner
f999c14a1e close #4429 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 01:33:28 -07:00
Nikolaj Bjorner
278e004385 fix #4428, and then there were none, almost 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 01:28:26 -07:00
Nikolaj Bjorner
80d5d66158 handling cancelation #4425 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 01:12:04 -07:00
Nikolaj Bjorner
9f8887cc2e throw from push #4425 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 01:05:23 -07:00
Nikolaj Bjorner
b013df9a9f fix #4431 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-04 00:47:27 -07:00
Nikolaj Bjorner
b29d5f9b5d fix #4436 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 21:21:01 -07:00
Nikolaj Bjorner
9ca5b3f304 fix #4449 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 21:10:07 -07:00
Nikolaj Bjorner
cbf089e10d fix #4448 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 19:41:25 -07:00
Nikolaj Bjorner
ae2f0ca85b fix #4448 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 19:40:26 -07:00
Nikolaj Bjorner
743573aac5 fix #4447, or mask it 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 19:32:05 -07:00
Nikolaj Bjorner
af90992858 fix #4404 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 17:01:36 -07:00
Nikolaj Bjorner
f986ae97bd fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 15:12:08 -07:00
Nikolaj Bjorner
d50fc6976b fix #4430 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 13:47:59 -07:00
Andrew V. Jones
9fac010d8e
Fixing build errors when building test-z3 (#4496) 
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
 2020-06-03 13:34:43 -07:00
Nuno Lopes
e844aef896 remove a few more copy constructors, though still not enough to enable the assertion in vector 
I give up for now; there are too many copies left for little return..
 2020-06-03 20:32:13 +01:00
Nikolaj Bjorner
e2b2b7f82e na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 12:29:29 -07:00
Nikolaj Bjorner
3a7df2c6ef fix various nullability checks in seq_regex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 12:28:32 -07:00
Nikolaj Bjorner
377dbad3b9 fix #4435 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 10:27:08 -07:00
Nikolaj Bjorner
8ae42b5ae1 fix #4433 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 10:23:26 -07:00
Nikolaj Bjorner
f5cd4e3ac0 janitor services 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 10:15:55 -07:00
Nikolaj Bjorner
38176256c4 fix #4434 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 10:12:49 -07:00