1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 macro_finder_tactic.cpp 7 8 Abstract: 9 10 Macro finder 11 12 Author: 13 14 Christoph (cwinter) 2012-10-26 15 16 Notes: 17 18 --*/ 19 #include "tactic/tactical.h" 20 #include "ast/macros/macro_manager.h" 21 #include "ast/macros/macro_finder.h" 22 #include "tactic/generic_model_converter.h" 23 #include "tactic/ufbv/macro_finder_tactic.h" 24 25 class macro_finder_tactic : public tactic { 26 27 struct imp { 28 ast_manager & m_manager; 29 bool m_elim_and; 30 31 imp(ast_manager & m, params_ref const & p) : 32 m_manager(m), 33 m_elim_and(false) { 34 updt_params(p); 35 } 36 37 ast_manager & m() const { return m_manager; } 38 39 40 void operator()(goal_ref const & g, 41 goal_ref_buffer & result) { 42 tactic_report report("macro-finder", *g); 43 TRACE("macro-finder", g->display(tout);); 44 45 bool produce_proofs = g->proofs_enabled(); 46 bool unsat_core_enabled = g->unsat_core_enabled(); 47 macro_manager mm(m_manager); 48 macro_finder mf(m_manager, mm); 49 50 expr_ref_vector forms(m_manager), new_forms(m_manager); 51 proof_ref_vector proofs(m_manager), new_proofs(m_manager); 52 expr_dependency_ref_vector deps(m_manager), new_deps(m_manager); 53 unsigned size = g->size(); 54 for (unsigned idx = 0; idx < size; idx++) { 55 forms.push_back(g->form(idx)); 56 proofs.push_back(g->pr(idx)); 57 deps.push_back(g->dep(idx)); 58 } 59 60 mf(forms, proofs, deps, new_forms, new_proofs, new_deps); 61 62 g->reset(); 63 for (unsigned i = 0; i < new_forms.size(); i++) 64 g->assert_expr(new_forms.get(i), 65 produce_proofs ? new_proofs.get(i) : nullptr, 66 unsat_core_enabled ? new_deps.get(i) : nullptr); 67 68 generic_model_converter * evmc = alloc(generic_model_converter, mm.get_manager(), "macro_finder"); 69 unsigned num = mm.get_num_macros(); 70 for (unsigned i = 0; i < num; i++) { 71 expr_ref f_interp(mm.get_manager()); 72 func_decl * f = mm.get_macro_interpretation(i, f_interp); 73 evmc->add(f, f_interp); 74 } 75 g->add(evmc); 76 g->inc_depth(); 77 result.push_back(g.get()); 78 } 79 80 void updt_params(params_ref const & p) { 81 m_elim_and = p.get_bool("elim_and", false); 82 } 83 }; 84 85 imp * m_imp; 86 params_ref m_params; 87 public: 88 macro_finder_tactic(ast_manager & m, params_ref const & p): 89 m_params(p) { 90 m_imp = alloc(imp, m, p); 91 } 92 93 tactic * translate(ast_manager & m) override { 94 return alloc(macro_finder_tactic, m, m_params); 95 } 96 97 ~macro_finder_tactic() override { 98 dealloc(m_imp); 99 } 100 101 void updt_params(params_ref const & p) override { 102 m_params = p; 103 m_imp->updt_params(p); 104 } 105 106 void collect_param_descrs(param_descrs & r) override { 107 insert_max_memory(r); 108 insert_produce_models(r); 109 insert_produce_proofs(r); 110 r.insert("elim_and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier."); 111 } 112 113 void operator()(goal_ref const & in, 114 goal_ref_buffer & result) override { 115 (*m_imp)(in, result); 116 } 117 118 void cleanup() override { 119 ast_manager & m = m_imp->m(); 120 imp * d = alloc(imp, m, m_params); 121 std::swap(d, m_imp); 122 dealloc(d); 123 } 124 125 126 }; 127 128 tactic * mk_macro_finder_tactic(ast_manager & m, params_ref const & p) { 129 return alloc(macro_finder_tactic, m, p); 130 } 131