1 /*++
2 Copyright (c) 2007 Microsoft Corporation
3 
4 Module Name:
5 
6     var_subst.cpp
7 
8 Abstract:
9 
10     Variable substitution.
11 
12 Author:
13 
14     Leonardo (leonardo) 2008-01-10
15 
16 Notes:
17 
18 --*/
19 #include "ast/rewriter/var_subst.h"
20 #include "ast/rewriter/expr_safe_replace.h"
21 #include "ast/ast_ll_pp.h"
22 #include "ast/ast_pp.h"
23 #include "ast/ast_smt2_pp.h"
24 #include "ast/well_sorted.h"
25 #include "ast/for_each_expr.h"
26 
operator ()(expr * n,unsigned num_args,expr * const * args)27 expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args) {
28     ast_manager& m = m_reducer.m();
29     expr_ref result(m);
30     if (is_ground(n) || num_args == 0) {
31         result = n;
32         //application does not have free variables or nested quantifiers.
33         //There is no need to print the bindings here?
34         SCTRACE("bindings", is_trace_enabled("coming_from_quant"),
35                 tout << "(ground)\n";
36                         for (unsigned i = 0; i < num_args; i++) {
37                             if (args[i]) {
38                                 tout << i << ": " << mk_ismt2_pp(args[i], result.m()) << ";\n";
39                             }
40                         }
41                         tout.flush(););
42 
43         return result;
44     }
45     if (has_quantifiers(n)) {
46         expr_safe_replace rep(m);
47         for (unsigned k = 0; k < num_args; ++k) {
48             expr* arg = args[k];
49             if (arg)
50                 rep.insert(m.mk_var(m_std_order ? num_args - k - 1 : k, arg->get_sort()), arg);
51         }
52         rep(n, result);
53         return result;
54     }
55     SASSERT(is_well_sorted(result.m(), n));
56     m_reducer.reset();
57     if (m_std_order)
58         m_reducer.set_inv_bindings(num_args, args);
59     else
60         m_reducer.set_bindings(num_args, args);
61     m_reducer(n, result);
62     SASSERT(is_well_sorted(m, result));
63     TRACE("var_subst_bug",
64           tout << "m_std_order: " << m_std_order << "\n" << mk_ismt2_pp(n, m) << "\nusing\n";
65           for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m) << "\n";
66           tout << "\n------>\n";
67           tout << result << "\n";);
68     return result;
69 }
70 
unused_vars_eliminator(ast_manager & m,params_ref const & params)71 unused_vars_eliminator::unused_vars_eliminator(ast_manager & m, params_ref const & params) :
72     m(m), m_subst(m), m_params(params)
73 {
74     m_ignore_patterns_on_ground_qbody = m_params.get_bool("ignore_patterns_on_ground_qbody", true);
75 }
76 
operator ()(quantifier * q)77 expr_ref unused_vars_eliminator::operator()(quantifier* q) {
78     expr_ref result(m);
79     SASSERT(is_well_sorted(m, q));
80     TRACE("elim_unused_vars", tout << expr_ref(q, m) << "\n";);
81     if (is_lambda(q)) {
82         result = q;
83         return result;
84     }
85     if (m_ignore_patterns_on_ground_qbody && is_ground(q->get_expr())) {
86         // Ignore patterns if the body is a ground formula.
87         result = q->get_expr();
88         return result;
89     }
90     if (!q->may_have_unused_vars()) {
91         result = q;
92         return result;
93     }
94     unsigned num_decls = q->get_num_decls();
95     m_used.reset();
96     m_used.set_num_decls(num_decls);
97     m_used.process(q->get_expr());
98     unsigned num_patterns = q->get_num_patterns();
99     for (unsigned i = 0; i < num_patterns; i++)
100         m_used.process(q->get_pattern(i));
101     unsigned num_no_patterns = q->get_num_no_patterns();
102     for (unsigned i = 0; i < num_no_patterns; i++)
103         m_used.process(q->get_no_pattern(i));
104 
105 
106     if (m_used.uses_all_vars(num_decls)) {
107         q->set_no_unused_vars();
108         result = q;
109         return result;
110     }
111 
112     ptr_buffer<sort>  used_decl_sorts;
113     buffer<symbol>    used_decl_names;
114     for (unsigned i = 0; i < num_decls; ++i) {
115         if (m_used.contains(num_decls - i - 1)) {
116             used_decl_sorts.push_back(q->get_decl_sort(i));
117             used_decl_names.push_back(q->get_decl_name(i));
118         }
119     }
120 
121     unsigned         num_removed = 0;
122     expr_ref_buffer  var_mapping(m);
123     int              next_idx = 0;
124     unsigned         sz = m_used.get_max_found_var_idx_plus_1();
125 
126     for (unsigned i = 0; i < num_decls; ++i) {
127         sort * s = m_used.contains(i);
128         if (s) {
129             var_mapping.push_back(m.mk_var(next_idx, s));
130             next_idx++;
131         }
132         else {
133             num_removed++;
134             var_mapping.push_back(nullptr);
135         }
136     }
137     // (VAR 0) is in the first position of var_mapping.
138 
139     for (unsigned i = num_decls; i < sz; i++) {
140         sort * s = m_used.contains(i);
141         if (s)
142             var_mapping.push_back(m.mk_var(i - num_removed, s));
143         else
144             var_mapping.push_back(nullptr);
145     }
146 
147     // Remark:
148     // (VAR 0) should be in the last position of var_mapping.
149     // ...
150     // (VAR (var_mapping.size() - 1)) should be in the first position.
151     std::reverse(var_mapping.data(), var_mapping.data() + var_mapping.size());
152 
153     expr_ref  new_expr(m);
154 
155     new_expr = m_subst(q->get_expr(), var_mapping.size(), var_mapping.data());
156 
157     if (num_removed == num_decls) {
158         result = new_expr;
159         return result;
160     }
161 
162     expr_ref_buffer new_patterns(m);
163     expr_ref_buffer new_no_patterns(m);
164 
165     for (unsigned i = 0; i < num_patterns; i++) {
166         new_patterns.push_back(m_subst(q->get_pattern(i), var_mapping.size(), var_mapping.data()));
167     }
168     for (unsigned i = 0; i < num_no_patterns; i++) {
169         new_no_patterns.push_back(m_subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.data()));
170     }
171 
172     result = m.mk_quantifier(q->get_kind(),
173                              used_decl_sorts.size(),
174                              used_decl_sorts.data(),
175                              used_decl_names.data(),
176                              new_expr,
177                              q->get_weight(),
178                              q->get_qid(),
179                              q->get_skid(),
180                              num_patterns,
181                              new_patterns.data(),
182                              num_no_patterns,
183                              new_no_patterns.data());
184     to_quantifier(result)->set_no_unused_vars();
185     SASSERT(is_well_sorted(m, result));
186     return result;
187 }
188 
elim_unused_vars(ast_manager & m,quantifier * q,params_ref const & params)189 expr_ref elim_unused_vars(ast_manager & m, quantifier * q, params_ref const & params) {
190     unused_vars_eliminator el(m, params);
191     expr_ref result = el(q);
192     TRACE("elim_unused_vars", tout << expr_ref(q, m) << " -> " << result << "\n";);
193     return result;
194 }
195 
instantiate(ast_manager & m,quantifier * q,expr * const * exprs)196 expr_ref instantiate(ast_manager & m, quantifier * q, expr * const * exprs) {
197     var_subst subst(m);
198     expr_ref new_expr(m), result(m);
199     new_expr = subst(q->get_expr(), q->get_num_decls(), exprs);
200     TRACE("var_subst", tout << mk_pp(q, m) << "\n" << new_expr << "\n";);
201     inv_var_shifter shift(m);
202     shift(new_expr, q->get_num_decls(), result);
203     SASSERT(is_well_sorted(m, result));
204     TRACE("instantiate_bug", tout << mk_ismt2_pp(q, m) << "\nusing\n";
205           for (unsigned i = 0; i < q->get_num_decls(); i++) tout << mk_ismt2_pp(exprs[i], m) << "\n";
206           tout << "\n----->\n" << mk_ismt2_pp(result, m) << "\n";);
207     return result;
208 }
209 
get_free_vars_offset(expr_sparse_mark & mark,ptr_vector<expr> & todo,unsigned offset,expr * e,ptr_vector<sort> & sorts)210 static void get_free_vars_offset(expr_sparse_mark& mark, ptr_vector<expr>& todo, unsigned offset, expr* e, ptr_vector<sort>& sorts) {
211     todo.push_back(e);
212     while (!todo.empty()) {
213         e = todo.back();
214         todo.pop_back();
215         if (mark.is_marked(e)) {
216             continue;
217         }
218         mark.mark(e, true);
219         switch(e->get_kind()) {
220         case AST_QUANTIFIER: {
221             quantifier* q = to_quantifier(e);
222             expr_sparse_mark mark1;
223             ptr_vector<expr> todo1;
224             get_free_vars_offset(mark1, todo1, offset+q->get_num_decls(), q->get_expr(), sorts);
225             break;
226         }
227         case AST_VAR: {
228             var* v = to_var(e);
229             if (v->get_idx() >= offset) {
230                 unsigned idx = v->get_idx()-offset;
231                 if (sorts.size() <= idx) {
232                     sorts.resize(idx+1);
233                 }
234                 if (!sorts[idx]) {
235                     sorts[idx] = v->get_sort();
236                 }
237                 SASSERT(sorts[idx] == v->get_sort());
238             }
239             break;
240         }
241         case AST_APP: {
242             for (expr* arg : *to_app(e))
243                 todo.push_back(arg);
244             break;
245         }
246         default:
247             UNREACHABLE();
248         }
249     }
250 }
251 
252 
get_free_vars(expr * e,ptr_vector<sort> & sorts)253 void get_free_vars(expr* e, ptr_vector<sort>& sorts) {
254     expr_sparse_mark mark;
255     ptr_vector<expr> todo;
256     get_free_vars_offset(mark, todo, 0, e, sorts);
257 }
258 
get_free_vars(expr_sparse_mark & mark,ptr_vector<expr> & todo,expr * e,ptr_vector<sort> & sorts)259 void get_free_vars(expr_sparse_mark& mark, ptr_vector<expr>& todo, expr* e, ptr_vector<sort>& sorts) {
260     get_free_vars_offset(mark, todo, 0, e, sorts);
261 }
262 
reset()263 void expr_free_vars::reset() {
264     m_mark.reset();
265     m_sorts.reset();
266     SASSERT(m_todo.empty());
267 }
268 
set_default_sort(sort * s)269 void expr_free_vars::set_default_sort(sort *s) {
270     for (unsigned i = 0; i < m_sorts.size(); ++i) {
271         if (!m_sorts[i]) m_sorts[i] = s;
272     }
273 }
274 
operator ()(expr * e)275 void expr_free_vars::operator()(expr* e) {
276     reset();
277     get_free_vars_offset(m_mark, m_todo, 0, e, m_sorts);
278 }
279 
accumulate(expr * e)280 void expr_free_vars::accumulate(expr* e) {
281     SASSERT(m_todo.empty());
282     get_free_vars_offset(m_mark, m_todo, 0, e, m_sorts);
283 }
284