1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 elim_term_ite_tactic.cpp
7
8 Abstract:
9
10 Eliminate term if-then-else by adding
11 new fresh auxiliary variables.
12
13 Author:
14
15 Leonardo (leonardo) 2011-12-29
16
17 Notes:
18
19 --*/
20 #include "tactic/tactical.h"
21 #include "ast/normal_forms/defined_names.h"
22 #include "ast/rewriter/rewriter_def.h"
23 #include "tactic/generic_model_converter.h"
24
25 class elim_term_ite_tactic : public tactic {
26
27 struct rw_cfg : public default_rewriter_cfg {
28 ast_manager & m;
29 defined_names m_defined_names;
30 ref<generic_model_converter> m_mc;
31 goal * m_goal;
32 unsigned long long m_max_memory; // in bytes
33 bool m_produce_models;
34 unsigned m_num_fresh;
35
max_steps_exceededelim_term_ite_tactic::rw_cfg36 bool max_steps_exceeded(unsigned num_steps) const {
37 if (memory::get_allocation_size() > m_max_memory)
38 throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
39 return false;
40 }
41
reduce_appelim_term_ite_tactic::rw_cfg42 br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
43 if (!m.is_term_ite(f))
44 return BR_FAILED;
45 expr_ref new_ite(m);
46 new_ite = m.mk_app(f, num, args);
47
48 expr_ref new_def(m);
49 proof_ref new_def_pr(m);
50 app_ref _result(m);
51 if (m_defined_names.mk_name(new_ite, new_def, new_def_pr, _result, result_pr)) {
52 m_goal->assert_expr(new_def, new_def_pr, nullptr);
53 m_num_fresh++;
54 if (m_produce_models) {
55 if (!m_mc)
56 m_mc = alloc(generic_model_converter, m, "elim_term_ite");
57 m_mc->hide(_result->get_decl());
58 }
59 }
60 result = _result.get();
61 return BR_DONE;
62 }
63
rw_cfgelim_term_ite_tactic::rw_cfg64 rw_cfg(ast_manager & _m, params_ref const & p):
65 m(_m),
66 m_defined_names(m, nullptr /* don't use prefix */) {
67 updt_params(p);
68 m_goal = nullptr;
69 m_num_fresh = 0;
70 }
71
updt_paramselim_term_ite_tactic::rw_cfg72 void updt_params(params_ref const & p) {
73 m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
74 }
75 };
76
77 struct rw : public rewriter_tpl<rw_cfg> {
78 rw_cfg m_cfg;
79
rwelim_term_ite_tactic::rw80 rw(ast_manager & m, params_ref const & p):
81 rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg),
82 m_cfg(m, p) {
83 }
84 };
85
86 struct imp {
87 ast_manager & m;
88 rw m_rw;
89
impelim_term_ite_tactic::imp90 imp(ast_manager & _m, params_ref const & p):
91 m(_m),
92 m_rw(m, p) {
93 }
94
95
updt_paramselim_term_ite_tactic::imp96 void updt_params(params_ref const & p) {
97 m_rw.cfg().updt_params(p);
98 }
99
operator ()elim_term_ite_tactic::imp100 void operator()(goal_ref const & g,
101 goal_ref_buffer & result) {
102 tactic_report report("elim-term-ite", *g);
103 bool produce_proofs = g->proofs_enabled();
104 m_rw.cfg().m_produce_models = g->models_enabled();
105
106 m_rw.m_cfg.m_num_fresh = 0;
107 m_rw.m_cfg.m_goal = g.get();
108 expr_ref new_curr(m);
109 proof_ref new_pr(m);
110 unsigned size = g->size();
111 for (unsigned idx = 0; idx < size; idx++) {
112 expr * curr = g->form(idx);
113 m_rw(curr, new_curr, new_pr);
114 if (produce_proofs) {
115 proof * pr = g->pr(idx);
116 new_pr = m.mk_modus_ponens(pr, new_pr);
117 }
118 g->update(idx, new_curr, new_pr, g->dep(idx));
119 }
120 g->add(m_rw.m_cfg.m_mc.get());
121 report_tactic_progress(":elim-term-ite-consts", m_rw.m_cfg.m_num_fresh);
122 g->inc_depth();
123 result.push_back(g.get());
124 }
125 };
126
127 imp * m_imp;
128 params_ref m_params;
129 public:
elim_term_ite_tactic(ast_manager & m,params_ref const & p)130 elim_term_ite_tactic(ast_manager & m, params_ref const & p):
131 m_params(p) {
132 m_imp = alloc(imp, m, p);
133 }
134
~elim_term_ite_tactic()135 ~elim_term_ite_tactic() override {
136 dealloc(m_imp);
137 }
138
translate(ast_manager & m)139 tactic * translate(ast_manager & m) override {
140 return alloc(elim_term_ite_tactic, m, m_params);
141 }
142
updt_params(params_ref const & p)143 void updt_params(params_ref const & p) override {
144 m_params = p;
145 m_imp->m_rw.cfg().updt_params(p);
146 }
147
collect_param_descrs(param_descrs & r)148 void collect_param_descrs(param_descrs & r) override {
149 insert_max_memory(r);
150 insert_max_steps(r);
151 r.insert("max_args", CPK_UINT,
152 "(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic.");
153 }
154
operator ()(goal_ref const & in,goal_ref_buffer & result)155 void operator()(goal_ref const & in,
156 goal_ref_buffer & result) override {
157 (*m_imp)(in, result);
158 }
159
cleanup()160 void cleanup() override {
161 ast_manager & m = m_imp->m;
162 m_imp->~imp();
163 m_imp = new (m_imp) imp(m, m_params);
164 }
165
166 };
167
mk_elim_term_ite_tactic(ast_manager & m,params_ref const & p)168 tactic * mk_elim_term_ite_tactic(ast_manager & m, params_ref const & p) {
169 return clean(alloc(elim_term_ite_tactic, m, p));
170 }
171