mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity
8897 commits 49 branches 53 tags 182 MiB
Commit graph

8897 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
42749e7b22 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-10-19 22:19:12 -07:00
Nikolaj Bjorner
76eed064eb bug fixes, prepare for retaining blocked clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-19 22:19:05 -07:00
Nikolaj Bjorner
d50e9355be Merge pull request #7 from TheRealNebus/opt 
Opt
 2017-10-19 20:08:30 -07:00
Miguel Neves
d58f42c821 Merge 2017-10-19 20:02:05 -07:00
Miguel Neves
3dd5630255 Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt 2017-10-19 19:53:25 -07:00
Miguel Neves
ba6b024ac4 Reverted to March_CU like lookahead 2017-10-19 19:52:56 -07:00
Murphy Berzish
ce1c8f7be2 remove debug code 2017-10-19 17:01:10 -04:00
Nikolaj Bjorner
d2e27f6f1f remove redundant and wrong range type, in extension to changes made for #1223 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-19 11:25:44 -07:00
Nikolaj Bjorner
c9f540b066 additional array functions exposed over API, ping #1223 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-19 11:08:48 -07:00
Nikolaj Bjorner
d76566bf83 Merge pull request #1312 from stanciuadrian/patch-1 
Update README.md
 2017-10-19 09:28:59 -07:00
Nikolaj Bjorner
636f740b1a fixup bdd reordering, assertions and perf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-18 19:32:49 -07:00
Nikolaj Bjorner
553bf74f47 testing bdd for elim-vars 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-18 17:38:39 -07:00
Nikolaj Bjorner
dc6ed64da1 testing bdd for elim-vars 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-18 17:37:38 -07:00
Murphy Berzish
abdb41c5df add special case handling for string constant backpropagation in theory_str 
avoid a crash when asserting that a constant string is equal to itself
by not generating this assert in the first place
 2017-10-18 16:09:10 -04:00
Nikolaj Bjorner
6155362571 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-10-18 08:57:43 -07:00
Nikolaj Bjorner
edea879864 expose missed propagations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-18 08:57:32 -07:00
Nikolaj Bjorner
80f24c29ab debugging reordering 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-18 08:52:03 -07:00
Adrian Stanciu
45c60ed55c Update README.md 
Corrected path to Z3 Python interface
 2017-10-18 14:50:44 +03:00
Nikolaj Bjorner
8811d78415 compress elimination stack representation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 21:28:48 -07:00
Miguel Neves
cf2512ce90 Added literal promotion 2017-10-17 16:03:58 -07:00
Nikolaj Bjorner
e0e7836c12 working on BDD reordering 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 14:20:49 -07:00
Nikolaj Bjorner
4944a86478 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-10-17 13:25:21 -07:00
Nikolaj Bjorner
43f8214453 local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 13:25:08 -07:00
Nikolaj Bjorner
f39a4ece0d Merge pull request #6 from TheRealNebus/opt 
Lookahead clause size optimization. Fixed some missing propagations
 2017-10-17 13:22:40 -07:00
Miguel Neves
806690571e Lookahead clause size optimization. Fixed some missing propagations 2017-10-17 13:15:34 -07:00
Nikolaj Bjorner
7f590b5419 gift for Nuno 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 10:27:58 -07:00
Nikolaj Bjorner
448cf8c31d fix scope accounting for dom simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 10:14:26 -07:00
Nikolaj Bjorner
42e9a0156b add elimination stack for model reconstruction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 04:52:06 -07:00
Nikolaj Bjorner
da4e8118b2 adding elim sequences 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 17:58:56 -07:00
Nuno Lopes
4e92caa553 nnf: let's try a different version of compatible frames wo/ copying 2017-10-16 22:33:23 +01:00
Christoph M. Wintersteiger
01f642a6f3 Backward compatibility 2017-10-16 18:19:55 +01:00
Nikolaj Bjorner
019edcb822 frame, again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:35:00 -07:00
Nikolaj Bjorner
5f9891c235 moving out construction of expr_ref 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:29:26 -07:00
Nikolaj Bjorner
a93f1f88cc trying to fix mac build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:23:50 -07:00
Nikolaj Bjorner
256c9d76d3 add macro for _Exit under WINDOWS 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:14:10 -07:00
Nikolaj Bjorner
b36f512879 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-16 09:07:44 -07:00
Christoph M. Wintersteiger
a10ad79f2b Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-16 17:07:10 +01:00
Christoph M. Wintersteiger
f9adf8e62a Backwards compatibility 2017-10-16 17:07:03 +01:00
Nikolaj Bjorner
d9ccb3928e fix debug build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:05:25 -07:00
Christoph M. Wintersteiger
cda03b4238 Whitespace 2017-10-16 17:01:09 +01:00
Nikolaj Bjorner
6327bd2c08 Merge pull request #1289 from delcypher/travis_ci_enable_asan_ubsan_build 
[TravisCI] Enable UBSan and ASan configurations
 2017-10-16 08:54:25 -07:00
Christoph M. Wintersteiger
0169417c64 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-16 16:40:39 +01:00
Dan Liew
7c99721b60 [TravisCI] Don't run Python regression tests under ASan for now. 
The script that runs them doesn't propagate LD_PRELOAD and so the
tests fail.
 2017-10-16 13:21:03 +01:00
Dan Liew
a1b6316e2e [TravisCI] Try to unbreak running Python regression tests under ASan. 2017-10-16 09:49:54 +01:00
Dan Liew
8835b54d16 [TravisCI] Add ASan/UBSan configuration that runs unit tests. 2017-10-16 08:56:17 +01:00
Dan Liew
88fb31ac08 [TravisCI] Add RUN_API_EXAMPLES option so that we can disable 
building/running examples in some configurations.
 2017-10-16 08:56:17 +01:00
Dan Liew
dbb7f616c1 More LSan workarounds. 2017-10-16 08:56:17 +01:00
Dan Liew
e51ce8bcaf [TravisCI] Try again to not show suppressions by default 2017-10-16 08:56:17 +01:00
Dan Liew
ead6e56d15 [TravisCI] Swap run_quiet and run_non_native_binding. In the 
previous order `grep` inside `run_quiet` would get ASan LD_PRELOAD'ed
which would sometimes fail.
 2017-10-16 08:56:17 +01:00
Dan Liew
ecadef6e48 [TravisCI] Try to fix case in run_quiet where the script would fail 
with.

```
-ne: unary operator expected
```
 2017-10-16 08:56:17 +01:00