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