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

1533 commits

Author SHA1 Message Date
Nikolaj Bjorner
dc0b2a8acf remove extension model converter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 17:25:35 -08:00
Nikolaj Bjorner
0d15b6abb7 add stubs for converting assertions, consolidate filter_model_converter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 14:51:13 -08:00
Nikolaj Bjorner
58be777307 fix #1358 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 20:32:37 -08:00
Nikolaj Bjorner
454e12fc49 update to vector format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-10 15:28:16 -08:00
Nikolaj Bjorner
ee3ed3a27a Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-11-09 09:55:41 -08:00
Nikolaj Bjorner
700f413e26 updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-09 09:55:37 -08:00
Nikolaj Bjorner
75b8d10f48 add backtrack level to cuber interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-08 21:44:21 -08:00
Nikolaj Bjorner
2746528aab fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-07 17:16:36 -08:00
Nikolaj Bjorner
1a687a31b6 missing files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-07 11:29:51 -08:00
Nikolaj Bjorner
303157d3b7 allow incremental mode override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 15:00:52 -08:00
Nuno Lopes
861a0745c1 remove a few unneded mem allocations 2017-11-06 10:36:10 +00:00
Nikolaj Bjorner
5813e22032 fix race condition, exception handling/throwing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-05 18:24:15 -08:00
Nikolaj Bjorner
9a4fb4ff76 remove ad-hoc parameters, deprecating dimacs cube mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-05 14:08:55 -08:00
Nikolaj Bjorner
70ee030228 updates to parallel tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-05 10:53:25 -08:00
Nikolaj Bjorner
e46e9cf86d work on parallel-tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-04 15:56:05 -05:00
Nikolaj Bjorner
59ea11b1a3 cube and conquer parallel tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-04 13:40:31 -05:00
Nikolaj Bjorner
6df3e47b07 disable symbol fixing in pretty printer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 09:53:47 -05:00
Nikolaj Bjorner
fd49a0c89c added facility to persist model transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 00:05:52 -05:00
Nikolaj Bjorner
caaf0ba33c model-add/del 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-01 22:32:22 -05:00
Nikolaj Bjorner
3de8c193ea implementing model updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-30 16:11:51 -05:00
Nikolaj Bjorner
92b5301b7f adding Cube method to .NET API, removing lookahead and get-lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-29 08:57:24 -07:00
Nikolaj Bjorner
e4b595d490 add solver pool abstraction for Spacer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:10:20 -07:00
Nikolaj Bjorner
b72225d7d0 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 15:16:59 -07:00
Nikolaj Bjorner
637a0fa139 unused warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 08:49:25 -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
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
b63754e362 adding explicit assignment for auto-generated function. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-15 21:16:54 -07:00
Nuno Lopes
9b54b4e784 fix vector<> to support non-POD types 
adjust code to std::move and avoid unnecessary/illegal
 2017-10-16 00:54:29 +01:00
Nikolaj Bjorner
4d48811efd updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-13 11:22:47 -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
1a6f8c2fad working on parallel solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-10 16:35:05 -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
a0cd6e0fca adding outline for parallel tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-09 16:47:23 -07:00
Nikolaj Bjorner
c1b243a8e3 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 19:24:30 +01:00
Nikolaj Bjorner
deba7d4d6e use idom for checking dominator relationships 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 14:35:44 +01:00
Nikolaj Bjorner
b898b07795 distinguish simplify_rec from simplify immediate argument 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 11:12:09 +01:00
Nikolaj Bjorner
76c309a595 disable caching of simplifier when applied to direct arguments of terms. Caching is only valid when applied to dominator children 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 00:20:58 +01:00
Nikolaj Bjorner
cabdc1f64c merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 00:09:28 +01:00
Nikolaj Bjorner
a18236bc7f have quantifier equality take names into account 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 00:07:53 +01:00
Nuno Lopes
1d12a9c86d dom_simplifier: fix dominator computation 2017-10-06 18:19:37 +01:00
Nikolaj Bjorner
31c6b3eb5b fix leak 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 16:07:25 +01:00
Nikolaj Bjorner
c3f615dbfc reverse arguments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 16:03:43 +01:00
Nikolaj Bjorner
2634be01aa adding backwards pass 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 13:43:01 +01:00
Nikolaj Bjorner
755ca46df6 adding bv_bounds tactic dominator style 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 12:15:41 +01:00
Nikolaj Bjorner
cb548404bc bail out dominators after log number of steps 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 12:08:37 +01:00
Nikolaj Bjorner
6df628edc7 pin elements in expr2depth 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 11:45:29 +01:00
Nikolaj Bjorner
eac659f748 deal with empty set of post-orders 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-06 11:34:14 +01:00