1 /*++
2 Copyright (c) 2013 Microsoft Corporation
3 
4 Module Name:
5 
6     dl_transforms.cpp
7 
8 Abstract:
9 
10     Default transformations.
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner) 2013-08-28.
15 
16 Revision History:
17 
18     Extracted from dl_context
19 
20 --*/
21 
22 #include "muz/transforms/dl_transforms.h"
23 #include "muz/base/dl_rule_transformer.h"
24 #include "muz/transforms/dl_mk_coi_filter.h"
25 #include "muz/transforms/dl_mk_filter_rules.h"
26 #include "muz/transforms/dl_mk_interp_tail_simplifier.h"
27 #include "muz/transforms/dl_mk_rule_inliner.h"
28 #include "muz/transforms/dl_mk_bit_blast.h"
29 #include "muz/transforms/dl_mk_array_blast.h"
30 #include "muz/transforms/dl_mk_karr_invariants.h"
31 #include "muz/transforms/dl_mk_magic_symbolic.h"
32 #include "muz/transforms/dl_mk_quantifier_abstraction.h"
33 #include "muz/transforms/dl_mk_quantifier_instantiation.h"
34 #include "muz/transforms/dl_mk_subsumption_checker.h"
35 #include "muz/transforms/dl_mk_scale.h"
36 #include "muz/transforms/dl_mk_array_eq_rewrite.h"
37 #include "muz/transforms/dl_mk_array_instantiation.h"
38 #include "muz/transforms/dl_mk_elim_term_ite.h"
39 #include "muz/base/fp_params.hpp"
40 
41 namespace datalog {
42 
apply_default_transformation(context & ctx)43     void apply_default_transformation(context& ctx) {
44         flet<bool> _enable_bv(ctx.bind_vars_enabled(), false);
45 
46         rule_transformer transf(ctx);
47         ctx.ensure_closed();
48         transf.reset();
49         transf.register_plugin(alloc(datalog::mk_coi_filter, ctx));
50         transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, ctx));
51 
52         if (ctx.get_params().xform_instantiate_arrays()) {
53             transf.register_plugin(alloc(datalog::mk_array_instantiation, ctx, 34999));
54         }
55         if(ctx.get_params().xform_transform_arrays())
56             transf.register_plugin(alloc(datalog::mk_array_eq_rewrite, ctx, 34998));
57         if (ctx.get_params().xform_quantify_arrays()) {
58             transf.register_plugin(alloc(datalog::mk_quantifier_abstraction, ctx, 38000));
59         }
60         transf.register_plugin(alloc(datalog::mk_quantifier_instantiation, ctx, 37000));
61 
62         if (ctx.get_params().datalog_subsumption()) {
63             transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 35005));
64         }
65         transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 35000));
66         transf.register_plugin(alloc(datalog::mk_coi_filter, ctx, 34990));
67         transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, ctx, 34980));
68 
69         //and another round of inlining
70         if (ctx.get_params().datalog_subsumption()) {
71             transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34975));
72         }
73         transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34970));
74         transf.register_plugin(alloc(datalog::mk_coi_filter, ctx, 34960));
75         transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, ctx, 34950));
76 
77         if (ctx.get_params().datalog_subsumption()) {
78             transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34940));
79             transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34930));
80             transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34920));
81             transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34910));
82             transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34900));
83             transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34890));
84             transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34880));
85         }
86         else {
87             transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34930));
88         }
89 
90         transf.register_plugin(alloc(datalog::mk_bit_blast, ctx, 35000));
91         transf.register_plugin(alloc(datalog::mk_karr_invariants, ctx, 36010));
92         transf.register_plugin(alloc(datalog::mk_scale, ctx, 36030));
93         if (!ctx.get_params().xform_quantify_arrays()) {
94             transf.register_plugin(alloc(datalog::mk_array_blast, ctx, 35999));
95         }
96         if (ctx.get_params().xform_magic()) {
97             transf.register_plugin(alloc(datalog::mk_magic_symbolic, ctx, 36020));
98         }
99 
100         transf.register_plugin(alloc(datalog::mk_elim_term_ite, ctx, 35010));
101         ctx.transform_rules(transf);
102     }
103 }
104