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