3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Commit graph

7829 commits

Author SHA1 Message Date
Nikolaj Bjorner
d9ccb3928e fix debug build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-16 09:05:25 -07:00
Nikolaj Bjorner
00a401260e fixing cce
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-15 21:19:02 -07:00
Nikolaj Bjorner
9f9ae4427d add cce
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-15 15:13:43 -07:00
Nikolaj Bjorner
46fa245324 more agressive variable elimination
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-14 18:33:38 -07:00
Nikolaj Bjorner
1109316621 fixing projection
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-14 15:53:25 -07:00
Nikolaj Bjorner
d36406f845 adding BDD-based variable elimination routine
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-14 15:12:02 -07:00
Nikolaj Bjorner
09fdfcc963 adding bdd package
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-14 11:40:20 -07:00
Nikolaj Bjorner
d7b6373601 adding bdd package
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-14 10:41:17 -07:00
Nikolaj Bjorner
64ea473bc7 adding bdd
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-13 18:03:35 -07:00
Nikolaj Bjorner
4f7147dd78 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-10-13 11:22:58 -07:00
Nikolaj Bjorner
4d48811efd updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-13 11:22:47 -07:00
Nikolaj Bjorner
6bcf158be2 Merge pull request #5 from TheRealNebus/opt
Opt
2017-10-13 18:10:55 +01:00
Miguel Neves
4394ce96ae More failed literals 2017-10-13 09:15:28 -07:00
Nikolaj Bjorner
708e8669fa fix faulty merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-13 07:41:31 -07:00
Miguel Neves
56d785df94 Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt 2017-10-12 16:15:35 -07:00
Miguel Neves
56496ead2f Commit 2017-10-12 16:14:56 -07:00
Nikolaj Bjorner
25c1b41c51 tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-12 15:56:09 -07:00
Nikolaj Bjorner
f86b85274a merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-12 15:52:06 -07:00
Nikolaj Bjorner
b95f8acba9 Merge pull request #4 from TheRealNebus/opt
Opt
2017-10-12 23:47:55 +01:00
Nikolaj Bjorner
a658e46b1f removing failed literal macro
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-12 15:46:25 -07:00
Miguel Neves
bdce957ac8 Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt 2017-10-12 15:34:56 -07:00
Miguel Neves
611a13e8b3 Changed lookahead backtrack. Parent lookahead re-use fix 2017-10-12 14:34:42 -07:00
Nikolaj Bjorner
4adf4d4ac2 micro opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-12 12:08:54 -07:00
Nikolaj Bjorner
5afef07f40 remove traces of old n-ary representation, add checks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-12 08:37:49 -07:00
Nikolaj Bjorner
99b232a4c5 fix lookahead with ba extension
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-11 17:30:21 -07:00
Nikolaj Bjorner
81ad69214c fixing lookahead/ba + parallel
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-11 17:06:28 -07:00
Nikolaj Bjorner
79ceaa1d13 fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-11 13:17:57 -07:00
Nikolaj Bjorner
97f37613c2 parallel
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-11 07:50:04 -07:00
Nikolaj Bjorner
d2395ad897 merge with Miguel's fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-10 16:47:07 -07:00
Nikolaj Bjorner
1a6f8c2fad working on parallel solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-10 16:35:05 -07:00
Miguel Neves
01897831fb Dynamic delta trigger decrease 2017-10-10 15:59:53 -07:00
Nikolaj Bjorner
09ea370ea3 update C-example that fails to not use longjumps. Issue #1297
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-10 12:06:19 -07:00
Nikolaj Bjorner
8b32c15ac9 use clause structure for nary
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-10 11:49:31 -07:00
Nikolaj Bjorner
7f693186a0 trying to address leak reported in #1297
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-10 07:10:04 -07:00
Nikolaj Bjorner
a0cd6e0fca adding outline for parallel tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-09 16:47:23 -07:00
Nikolaj Bjorner
cae414e575 fixes for #1296, removing COMPILE_TIME_ASSERT
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-09 13:59:44 -07:00
Nikolaj Bjorner
42de274307 bug fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-09 07:49:20 -07:00
Nikolaj Bjorner
79b2a4f605 bug fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-09 07:22:02 -07:00
Nikolaj Bjorner
f85c02600f remove verificaiton code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 16:07:58 -07:00
Nikolaj Bjorner
f359f23885 another fix for #1288
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 15:47:06 -07:00
Nikolaj Bjorner
10e4235b4c bug fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 14:35:31 -07:00
Nikolaj Bjorner
356835533a clean up debug output
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 10:47:15 -07:00
Nikolaj Bjorner
d2ec927844 fix build break
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 12:34:08 +01:00
Nikolaj Bjorner
06d75a616f fix #1288, again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 11:40:17 +01:00
Nikolaj Bjorner
22fa108ffd fix #1288, again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 11:07:22 +01:00
Nikolaj Bjorner
1371caace2 fix #1287, again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 11:05:57 +01:00
Nikolaj Bjorner
52217f0600 fix #1290
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 10:56:05 +01:00
Nikolaj Bjorner
c72b3356c1 fix #1286
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 10:41:02 +01:00
Nikolaj Bjorner
6f7f957a26 likely fix for #1287
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 10:38:02 +01:00
Nikolaj Bjorner
a5ecf87ab8 fix #1288
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-10-08 10:32:38 +01:00