1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 defined_names.cpp
7
8 Abstract:
9
10 <abstract>
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2008-01-14.
15
16 Revision History:
17
18 --*/
19 #include "util/obj_hashtable.h"
20 #include "ast/normal_forms/defined_names.h"
21 #include "ast/used_vars.h"
22 #include "ast/rewriter/var_subst.h"
23 #include "ast/ast_smt2_pp.h"
24 #include "ast/ast_pp.h"
25 #include "ast/ast_util.h"
26 #include "ast/array_decl_plugin.h"
27
28 struct defined_names::impl {
29 typedef obj_map<expr, app *> expr2name;
30 typedef obj_map<expr, proof *> expr2proof;
31 ast_manager & m;
32 symbol m_z3name;
33
34 /**
35 \brief Mapping from expressions to their names. A name is an application.
36 If the expression does not have free variables, then the name is just a constant.
37 */
38 expr2name m_expr2name;
39 /**
40 \brief Mapping from expressions to the apply-def proof.
41 That is, for each expression e, m_expr2proof[e] is the
42 proof e and m_expr2name[2] are observ. equivalent.
43
44 This mapping is not used if proof production is disabled.
45 */
46 expr2proof m_expr2proof;
47
48 /**
49 \brief Domain of m_expr2name. It is used to keep the expressions
50 alive and for backtracking
51 */
52 expr_ref_vector m_exprs;
53 expr_ref_vector m_names; //!< Range of m_expr2name. It is used to keep the names alive.
54 proof_ref_vector m_apply_proofs; //!< Range of m_expr2proof. It is used to keep the def-intro proofs alive.
55
56
57 unsigned_vector m_lims; //!< Backtracking support.
58
59 impl(ast_manager & m, char const * prefix);
60 virtual ~impl();
61
62 app * gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names);
63 void cache_new_name(expr * e, app * name);
64 void cache_new_name_intro_proof(expr * e, proof * pr);
65 void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref & result, symbol const& qid = symbol::null);
66 void bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref_buffer & result, symbol const& qid = symbol::null);
67 virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> & var_names, expr_ref & new_def);
68 bool mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr);
69 void push_scope();
70 void pop_scope(unsigned num_scopes);
71 void reset();
72
get_num_namesdefined_names::impl73 unsigned get_num_names() const { return m_names.size(); }
get_name_decldefined_names::impl74 func_decl * get_name_decl(unsigned i) const { return to_app(m_names.get(i))->get_decl(); }
75 };
76
77 struct defined_names::pos_impl : public defined_names::impl {
pos_impldefined_names::pos_impl78 pos_impl(ast_manager & m, char const * fresh_prefix):impl(m, fresh_prefix) {}
79 void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> & var_names, expr_ref & new_def) override;
80
81 };
82
83
impl(ast_manager & m,char const * prefix)84 defined_names::impl::impl(ast_manager & m, char const * prefix):
85 m(m),
86 m_exprs(m),
87 m_names(m),
88 m_apply_proofs(m) {
89 if (prefix)
90 m_z3name = prefix;
91 }
92
~impl()93 defined_names::impl::~impl() {
94 }
95
96 /**
97 \brief Given an expression \c e that may contain free variables, return an application (sk x_1 ... x_n),
98 where sk is a fresh variable name, and x_i's are the free variables of \c e.
99
100 Store in var_sorts and var_names information about the free variables of \c e. This data
101 is used to create an universal quantifier over the definition of the new name.
102 */
gen_name(expr * e,sort_ref_buffer & var_sorts,buffer<symbol> & var_names)103 app * defined_names::impl::gen_name(expr * e, sort_ref_buffer & var_sorts, buffer<symbol> & var_names) {
104 used_vars uv;
105 uv(e);
106 unsigned num_vars = uv.get_max_found_var_idx_plus_1();
107 ptr_buffer<expr> new_args;
108 ptr_buffer<sort> domain;
109 for (unsigned i = 0; i < num_vars; i++) {
110 sort * s = uv.get(i);
111 if (s) {
112 domain.push_back(s);
113 new_args.push_back(m.mk_var(i, s));
114 var_sorts.push_back(s);
115 }
116 else {
117 var_sorts.push_back(m.mk_bool_sort()); // could be any sort.
118 }
119 var_names.push_back(symbol(i));
120 }
121
122 sort * range = m.get_sort(e);
123 func_decl * new_skolem_decl = m.mk_fresh_func_decl(m_z3name, symbol::null, domain.size(), domain.c_ptr(), range);
124 app * n = m.mk_app(new_skolem_decl, new_args.size(), new_args.c_ptr());
125 if (is_lambda(e)) {
126 m.add_lambda_def(new_skolem_decl, to_quantifier(e));
127 }
128 return n;
129 }
130
131 /**
132 \brief Cache \c n as a name for expression \c e.
133 */
cache_new_name(expr * e,app * n)134 void defined_names::impl::cache_new_name(expr * e, app * n) {
135 m_expr2name.insert(e, n);
136 m_exprs.push_back(e);
137 m_names.push_back(n);
138 }
139
140 /**
141 \brief Cache \c pr as a proof that m_expr2name[e] is a name for expression \c e.
142 */
cache_new_name_intro_proof(expr * e,proof * pr)143 void defined_names::impl::cache_new_name_intro_proof(expr * e, proof * pr) {
144 SASSERT(m_expr2name.contains(e));
145 m_expr2proof.insert(e, pr);
146 m_apply_proofs.push_back(pr);
147 }
148
149 /**
150 \brief Given a definition conjunct \c def of the name \c name, store in \c result this definition.
151 A quantifier is added around \c def_conjunct, if sorts and names are not empty.
152 In this case, The application \c name is used as a pattern for the new quantifier.
153 */
bound_vars(sort_ref_buffer const & sorts,buffer<symbol> const & names,expr * def_conjunct,app * name,expr_ref & result,symbol const & qid)154 void defined_names::impl::bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref & result, symbol const& qid) {
155 SASSERT(sorts.size() == names.size());
156 if (sorts.empty())
157 result = def_conjunct;
158 else {
159 expr * patterns[1] = { m.mk_pattern(name) };
160 quantifier_ref q(m);
161 q = m.mk_forall(sorts.size(),
162 sorts.c_ptr(),
163 names.c_ptr(),
164 def_conjunct,
165 1, qid, symbol::null,
166 1, patterns);
167 TRACE("mk_definition_bug", tout << "before elim_unused_vars:\n" << mk_ismt2_pp(q, m) << "\n";);
168 result = elim_unused_vars(m, q, params_ref());
169 TRACE("mk_definition_bug", tout << "after elim_unused_vars:\n" << result << "\n";);
170 }
171 }
172
173 /**
174 \brief Given a definition conjunct \c def of the name \c name, store in \c result this definition.
175 A quantifier is added around \c def_conjunct, if sorts and names are not empty.
176 In this case, The application \c name is used as a pattern for the new quantifier.
177 */
bound_vars(sort_ref_buffer const & sorts,buffer<symbol> const & names,expr * def_conjunct,app * name,expr_ref_buffer & result,symbol const & qid)178 void defined_names::impl::bound_vars(sort_ref_buffer const & sorts, buffer<symbol> const & names, expr * def_conjunct, app * name, expr_ref_buffer & result, symbol const& qid) {
179 expr_ref tmp(m);
180 bound_vars(sorts, names, def_conjunct, name, tmp, qid);
181 result.push_back(tmp);
182 }
183
184 #define MK_OR m.mk_or
185 #define MK_NOT m.mk_not
186 #define MK_EQ m.mk_eq
187
mk_definition(expr * e,app * n,sort_ref_buffer & var_sorts,buffer<symbol> & var_names,expr_ref & new_def)188 void defined_names::impl::mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> & var_names, expr_ref & new_def) {
189 expr_ref_buffer defs(m);
190 if (m.is_bool(e)) {
191 bound_vars(var_sorts, var_names, MK_OR(MK_NOT(n), e), n, defs);
192 bound_vars(var_sorts, var_names, MK_OR(n, MK_NOT(e)), n, defs);
193 }
194 else if (m.is_term_ite(e)) {
195 bound_vars(var_sorts, var_names, MK_OR(MK_NOT(to_app(e)->get_arg(0)), MK_EQ(n, to_app(e)->get_arg(1))), n, defs);
196 bound_vars(var_sorts, var_names, MK_OR(to_app(e)->get_arg(0), MK_EQ(n, to_app(e)->get_arg(2))), n, defs);
197 }
198 else if (is_lambda(e)) {
199 // n(y) = \x . M[x,y]
200 // =>
201 // n(y)[x] = M, forall x y
202 //
203 // NB. The pattern is incomplete.
204 // consider store(a, i, v) == \lambda j . if i = j then v else a[j]
205 // the instantiation rules for store(a, i, v) are:
206 // store(a, i, v)[j] = if i = j then v else a[j] with patterns {a[j], store(a, i, v)} { store(a, i, v)[j] }
207 // The first pattern is not included.
208 // TBD use a model-based scheme for exracting instantiations instead of
209 // using multi-patterns.
210 //
211
212 quantifier* q = to_quantifier(e);
213 expr_ref_vector args(m);
214 expr_ref n2(m), n3(m);
215 var_shifter vs(m);
216 vs(n, q->get_num_decls(), n2);
217 args.push_back(n2);
218 var_sorts.append(q->get_num_decls(), q->get_decl_sorts());
219 var_names.append(q->get_num_decls(), q->get_decl_names());
220 for (unsigned i = 0; i < q->get_num_decls(); ++i) {
221 args.push_back(m.mk_var(q->get_num_decls() - i - 1, q->get_decl_sort(i)));
222 }
223 array_util autil(m);
224 func_decl * f = nullptr;
225 if (autil.is_as_array(n2, f)) {
226 n3 = m.mk_app(f, args.size()-1, args.c_ptr() + 1);
227 }
228 else {
229 n3 = autil.mk_select(args.size(), args.c_ptr());
230 }
231 bound_vars(var_sorts, var_names, MK_EQ(q->get_expr(), n3), to_app(n3), defs, m.lambda_def_qid());
232
233 }
234 else {
235 bound_vars(var_sorts, var_names, MK_EQ(e, n), n, defs);
236 }
237 new_def = mk_and(m, defs.size(), defs.c_ptr());
238 }
239
240
mk_definition(expr * e,app * n,sort_ref_buffer & var_sorts,buffer<symbol> & var_names,expr_ref & new_def)241 void defined_names::pos_impl::mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> & var_names, expr_ref & new_def) {
242 bound_vars(var_sorts, var_names, MK_OR(MK_NOT(n), e), n, new_def);
243 }
244
mk_name(expr * e,expr_ref & new_def,proof_ref & new_def_pr,app_ref & n,proof_ref & pr)245 bool defined_names::impl::mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
246 TRACE("mk_definition_bug", tout << "making name for:\n" << mk_ismt2_pp(e, m) << "\n";);
247
248 app * n_ptr;
249 if (m_expr2name.find(e, n_ptr)) {
250 TRACE("mk_definition_bug", tout << "name for expression is already cached..., returning false...\n";);
251 n = n_ptr;
252 if (m.proofs_enabled()) {
253 proof * pr_ptr = nullptr;
254 m_expr2proof.find(e, pr_ptr);
255 SASSERT(pr_ptr);
256 pr = pr_ptr;
257 }
258 return false;
259 }
260 else {
261 sort_ref_buffer var_sorts(m);
262 buffer<symbol> var_names;
263
264 n = gen_name(e, var_sorts, var_names);
265 cache_new_name(e, n);
266
267 TRACE("mk_definition_bug", tout << "name: " << mk_ismt2_pp(n, m) << "\n";);
268 // variables are in reverse order in quantifiers
269 std::reverse(var_sorts.c_ptr(), var_sorts.c_ptr() + var_sorts.size());
270 std::reverse(var_names.c_ptr(), var_names.c_ptr() + var_names.size());
271
272 mk_definition(e, n, var_sorts, var_names, new_def);
273
274 TRACE("mk_definition_bug", tout << "new_def:\n" << mk_ismt2_pp(new_def, m) << "\n";);
275
276 if (m.proofs_enabled()) {
277 new_def_pr = m.mk_def_intro(new_def);
278 pr = m.mk_apply_def(e, n, new_def_pr);
279 cache_new_name_intro_proof(e, pr);
280 }
281 return true;
282 }
283 }
284
push_scope()285 void defined_names::impl::push_scope() {
286 SASSERT(m_exprs.size() == m_names.size());
287 m_lims.push_back(m_exprs.size());
288 }
289
pop_scope(unsigned num_scopes)290 void defined_names::impl::pop_scope(unsigned num_scopes) {
291 unsigned lvl = m_lims.size();
292 SASSERT(num_scopes <= lvl);
293 unsigned new_lvl = lvl - num_scopes;
294 unsigned old_sz = m_lims[new_lvl];
295 unsigned sz = m_exprs.size();
296 SASSERT(old_sz <= sz);
297 SASSERT(sz == m_names.size());
298 while (old_sz != sz) {
299 --sz;
300 if (m.proofs_enabled()) {
301 m_expr2proof.erase(m_exprs.back());
302 m_apply_proofs.pop_back();
303 }
304 m_expr2name.erase(m_exprs.back());
305 m_exprs.pop_back();
306 m_names.pop_back();
307 }
308 SASSERT(m_exprs.size() == old_sz);
309 m_lims.shrink(new_lvl);
310 }
311
reset()312 void defined_names::impl::reset() {
313 m_expr2name.reset();
314 m_expr2proof.reset();
315 m_exprs.reset();
316 m_names.reset();
317 m_apply_proofs.reset();
318 m_lims.reset();
319 }
320
defined_names(ast_manager & m,char const * fresh_prefix)321 defined_names::defined_names(ast_manager & m, char const * fresh_prefix) {
322 m_impl = alloc(impl, m, fresh_prefix);
323 m_pos_impl = alloc(pos_impl, m, fresh_prefix);
324 }
325
~defined_names()326 defined_names::~defined_names() {
327 dealloc(m_impl);
328 dealloc(m_pos_impl);
329 }
330
mk_name(expr * e,expr_ref & new_def,proof_ref & new_def_pr,app_ref & n,proof_ref & pr)331 bool defined_names::mk_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
332 return m_impl->mk_name(e, new_def, new_def_pr, n, pr);
333 }
334
mk_pos_name(expr * e,expr_ref & new_def,proof_ref & new_def_pr,app_ref & n,proof_ref & pr)335 bool defined_names::mk_pos_name(expr * e, expr_ref & new_def, proof_ref & new_def_pr, app_ref & n, proof_ref & pr) {
336 return m_pos_impl->mk_name(e, new_def, new_def_pr, n, pr);
337 }
338
mk_definition(expr * e,app * n)339 expr_ref defined_names::mk_definition(expr * e, app * n) {
340 ast_manager& m = m_impl->m;
341 sort_ref_buffer var_sorts(m);
342 expr_ref new_def(m);
343 buffer<symbol> var_names;
344 m_impl->mk_definition(e, n, var_sorts, var_names, new_def);
345 return new_def;
346 }
347
push()348 void defined_names::push() {
349 m_impl->push_scope();
350 m_pos_impl->push_scope();
351 }
352
pop(unsigned num_scopes)353 void defined_names::pop(unsigned num_scopes) {
354 m_impl->pop_scope(num_scopes);
355 m_pos_impl->pop_scope(num_scopes);
356 }
357
reset()358 void defined_names::reset() {
359 m_impl->reset();
360 m_pos_impl->reset();
361 }
362
get_num_names() const363 unsigned defined_names::get_num_names() const {
364 return m_impl->get_num_names() + m_pos_impl->get_num_names();
365 }
366
get_name_decl(unsigned i) const367 func_decl * defined_names::get_name_decl(unsigned i) const {
368 SASSERT(i < get_num_names());
369 unsigned n1 = m_impl->get_num_names();
370 return i < n1 ? m_impl->get_name_decl(i) : m_pos_impl->get_name_decl(i - n1);
371 }
372
373
374
375
376
377