1 /*++
2 Copyright (c) 2015 Microsoft Corporation
3 
4 Module Name:
5 
6     qe_mbp.cpp
7 
8 Abstract:
9 
10     Model-based projection utilities
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner) 2015-5-29
15 
16 Revision History:
17 
18 
19 --*/
20 
21 #include "ast/rewriter/expr_safe_replace.h"
22 #include "ast/ast_pp.h"
23 #include "ast/ast_util.h"
24 #include "ast/occurs.h"
25 #include "ast/rewriter/th_rewriter.h"
26 #include "ast/expr_functors.h"
27 #include "ast/for_each_expr.h"
28 #include "ast/scoped_proof.h"
29 #include "qe/qe_mbp.h"
30 #include "qe/mbp/mbp_arith.h"
31 #include "qe/mbp/mbp_arrays.h"
32 #include "qe/mbp/mbp_datatypes.h"
33 #include "qe/qe_lite.h"
34 #include "model/model_pp.h"
35 #include "model/model_evaluator.h"
36 
37 
38 using namespace qe;
39 
40 
41 class mbproj::impl {
42     ast_manager& m;
43     params_ref                      m_params;
44     th_rewriter                     m_rw;
45     ptr_vector<mbp::project_plugin> m_plugins;
46 
47     // parameters
48     bool m_reduce_all_selects;
49     bool m_dont_sub;
50 
add_plugin(mbp::project_plugin * p)51     void add_plugin(mbp::project_plugin* p) {
52         family_id fid = p->get_family_id();
53         SASSERT(!m_plugins.get(fid, nullptr));
54         m_plugins.setx(fid, p, nullptr);
55     }
56 
get_plugin(app * var)57     mbp::project_plugin* get_plugin(app* var) {
58         family_id fid = m.get_sort(var)->get_family_id();
59         return m_plugins.get(fid, nullptr);
60     }
61 
solve(model & model,app_ref_vector & vars,expr_ref_vector & lits)62     bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
63         expr_mark is_var, is_rem;
64         if (vars.empty()) {
65             return false;
66         }
67         bool reduced = false;
68         for (expr* v : vars)
69             is_var.mark(v);
70         expr_ref tmp(m), t(m), v(m);
71 
72         for (unsigned i = 0; i < lits.size(); ++i) {
73             expr* e = lits.get(i), * l, * r;
74             if (m.is_eq(e, l, r) && reduce_eq(is_var, l, r, v, t)) {
75                 reduced = true;
76                 mbp::project_plugin::erase(lits, i);
77                 expr_safe_replace sub(m);
78                 sub.insert(v, t);
79                 is_rem.mark(v);
80                 for (unsigned j = 0; j < lits.size(); ++j) {
81                     sub(lits.get(j), tmp);
82                     m_rw(tmp);
83                     lits[j] = tmp;
84                 }
85             }
86         }
87         if (reduced) {
88             unsigned j = 0;
89             for (app* v : vars)
90                 if (!is_rem.is_marked(v))
91                     vars[j++] = v;
92             vars.shrink(j);
93         }
94         return reduced;
95     }
96 
reduce_eq(expr_mark & is_var,expr * l,expr * r,expr_ref & v,expr_ref & t)97     bool reduce_eq(expr_mark& is_var, expr* l, expr* r, expr_ref& v, expr_ref& t) {
98         if (is_var.is_marked(r))
99             std::swap(l, r);
100         if (is_var.is_marked(l)) {
101             contains_app cont(m, to_app(l));
102             if (!cont(r)) {
103                 v = to_app(l);
104                 t = r;
105                 return true;
106             }
107         }
108         return false;
109     }
110 
filter_variables(model & model,app_ref_vector & vars,expr_ref_vector & lits,expr_ref_vector & unused_lits)111     void filter_variables(model& model, app_ref_vector& vars, expr_ref_vector& lits, expr_ref_vector& unused_lits) {
112         expr_mark lit_visited;
113         mbp::project_plugin::mark_rec(lit_visited, lits);
114         unsigned j = 0;
115         for (app* var : vars)
116             if (lit_visited.is_marked(var))
117                 vars[j++] = var;
118         vars.shrink(j);
119     }
120 
project_bools(model & mdl,app_ref_vector & vars,expr_ref_vector & fmls)121     void project_bools(model& mdl, app_ref_vector& vars, expr_ref_vector& fmls) {
122         expr_safe_replace sub(m);
123         expr_ref val(m);
124         model_evaluator eval(mdl, m_params);
125         eval.set_model_completion(true);
126         unsigned j = 0;
127         for (app* var : vars) {
128             if (m.is_bool(var))
129                 sub.insert(var, eval(var));
130             else
131                 vars[j++] = var;
132         }
133         if (j == vars.size())
134             return;
135         vars.shrink(j);
136         j = 0;
137         for (expr* fml : fmls) {
138             sub(fml, val);
139             m_rw(val);
140             if (!m.is_true(val)) {
141                 TRACE("qe", tout << mk_pp(fml, m) << " -> " << val << "\n";);
142                 fmls[j++] = val;
143             }
144         }
145         fmls.shrink(j);
146     }
147 
148 
subst_vars(model_evaluator & eval,app_ref_vector const & vars,expr_ref & fml)149     void subst_vars(model_evaluator& eval, app_ref_vector const& vars, expr_ref& fml) {
150         expr_safe_replace sub(m);
151         for (app* v : vars)
152             sub.insert(v, eval(v));
153         sub(fml);
154     }
155 
156     struct index_term_finder {
157         ast_manager& m;
158         array_util       m_array;
159         app_ref          m_var;
160         expr_ref_vector& m_res;
161 
index_term_findermbproj::impl::index_term_finder162         index_term_finder(ast_manager& mgr, app* v, expr_ref_vector& res) :
163             m(mgr), m_array(m), m_var(v, m), m_res(res) {}
164 
operator ()mbproj::impl::index_term_finder165         void operator() (var* n) {}
operator ()mbproj::impl::index_term_finder166         void operator() (quantifier* n) {}
operator ()mbproj::impl::index_term_finder167         void operator() (app* n) {
168             expr* e1, * e2;
169             if (m_array.is_select(n)) {
170                 for (expr* arg : *n) {
171                     if (m.get_sort(arg) == m.get_sort(m_var) && arg != m_var)
172                         m_res.push_back(arg);
173                 }
174             }
175             else if (m.is_eq(n, e1, e2)) {
176                 if (e1 == m_var)
177                     m_res.push_back(e2);
178                 else if (e2 == m_var)
179                     m_res.push_back(e1);
180             }
181         }
182     };
183 
project_var(model_evaluator & eval,app * var,expr_ref & fml)184     bool project_var(model_evaluator& eval, app* var, expr_ref& fml) {
185         expr_ref val = eval(var);
186 
187         TRACE("mbqi_project_verbose", tout << "MBQI: var: " << mk_pp(var, m) << "\n" << "fml: " << fml << "\n";);
188         expr_ref_vector terms(m);
189         index_term_finder finder(m, var, terms);
190         for_each_expr(finder, fml);
191 
192         TRACE("mbqi_project_verbose", tout << "terms:\n" << terms;);
193 
194         for (expr* term : terms) {
195             expr_ref tval = eval(term);
196 
197             TRACE("mbqi_project_verbose", tout << "term: " << mk_pp(term, m) << " tval: " << tval << " val: " << val << "\n";);
198 
199             // -- if the term does not contain an occurrence of var
200             // -- and is in the same equivalence class in the model
201             if (tval == val && !occurs(var, term)) {
202                 TRACE("mbqi_project",
203                     tout << "MBQI: replacing " << mk_pp(var, m) << " with " << mk_pp(term, m) << "\n";);
204                 expr_safe_replace sub(m);
205                 sub.insert(var, term);
206                 sub(fml);
207                 return true;
208             }
209         }
210 
211         TRACE("mbqi_project",
212             tout << "MBQI: failed to eliminate " << mk_pp(var, m) << " from " << fml << "\n";);
213 
214         return false;
215     }
216 
project_vars(model & M,app_ref_vector & vars,expr_ref & fml)217     void project_vars(model& M, app_ref_vector& vars, expr_ref& fml) {
218         model_evaluator eval(M);
219         eval.set_model_completion(false);
220         // -- evaluate to initialize eval cache
221         eval(fml);
222         unsigned j = 0;
223         for (app* v : vars)
224             if (!project_var(eval, v, fml))
225                 vars[j++] = v;
226         vars.shrink(j);
227     }
228 
229 public:
230 
maximize(expr_ref_vector const & fmls,model & mdl,app * t,expr_ref & ge,expr_ref & gt)231     opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) {
232         mbp::arith_project_plugin arith(m);
233         return arith.maximize(fmls, mdl, t, ge, gt);
234     }
235 
extract_literals(model & model,app_ref_vector const & vars,expr_ref_vector & fmls)236     void extract_literals(model& model, app_ref_vector const& vars, expr_ref_vector& fmls) {
237         mbp::project_plugin proj(m);
238         proj.extract_literals(model, vars, fmls);
239     }
240 
impl(ast_manager & m,params_ref const & p)241     impl(ast_manager& m, params_ref const& p) :m(m), m_params(p), m_rw(m) {
242         add_plugin(alloc(mbp::arith_project_plugin, m));
243         add_plugin(alloc(mbp::datatype_project_plugin, m));
244         add_plugin(alloc(mbp::array_project_plugin, m));
245         updt_params(p);
246     }
247 
~impl()248     ~impl() {
249         std::for_each(m_plugins.begin(), m_plugins.end(), delete_proc<mbp::project_plugin>());
250     }
251 
updt_params(params_ref const & p)252     void updt_params(params_ref const& p) {
253         m_params.append(p);
254         m_reduce_all_selects = m_params.get_bool("reduce_all_selects", false);
255         m_dont_sub = m_params.get_bool("dont_sub", false);
256     }
257 
preprocess_solve(model & model,app_ref_vector & vars,expr_ref_vector & fmls)258     void preprocess_solve(model& model, app_ref_vector& vars, expr_ref_vector& fmls) {
259         extract_literals(model, vars, fmls);
260         bool change = true;
261         while (change && !vars.empty()) {
262             change = solve(model, vars, fmls);
263             for (auto* p : m_plugins) {
264                 if (p && p->solve(model, vars, fmls)) {
265                     change = true;
266                 }
267             }
268         }
269     }
270 
validate_model(model & model,expr_ref_vector const & fmls)271     bool validate_model(model& model, expr_ref_vector const& fmls) {
272         expr_ref val(m);
273         model_evaluator eval(model);
274         for (expr* f : fmls) {
275             VERIFY(!model.is_false(f));
276         }
277         return true;
278     }
279 
operator ()(bool force_elim,app_ref_vector & vars,model & model,expr_ref_vector & fmls)280     void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls) {
281         SASSERT(validate_model(model, fmls));
282         expr_ref val(m), tmp(m);
283         app_ref var(m);
284         expr_ref_vector unused_fmls(m);
285         bool progress = true;
286         preprocess_solve(model, vars, fmls);
287         filter_variables(model, vars, fmls, unused_fmls);
288         project_bools(model, vars, fmls);
289         while (progress && !vars.empty() && !fmls.empty() && m.limit().inc()) {
290             app_ref_vector new_vars(m);
291             progress = false;
292             for (mbp::project_plugin* p : m_plugins) {
293                 if (p)
294                     (*p)(model, vars, fmls);
295             }
296             while (!vars.empty() && !fmls.empty() && m.limit().inc()) {
297                 var = vars.back();
298                 vars.pop_back();
299                 mbp::project_plugin* p = get_plugin(var);
300                 if (p && (*p)(model, var, vars, fmls)) {
301                     progress = true;
302                 }
303                 else {
304                     new_vars.push_back(var);
305                 }
306             }
307             if (!progress && !new_vars.empty() && !fmls.empty() && force_elim && m.limit().inc()) {
308                 var = new_vars.back();
309                 new_vars.pop_back();
310                 expr_safe_replace sub(m);
311                 val = model(var);
312                 sub.insert(var, val);
313                 unsigned j = 0;
314                 for (expr* f : fmls) {
315                     sub(f, tmp);
316                     m_rw(tmp);
317                     if (!m.is_true(tmp))
318                         fmls[j++] = tmp;
319                 }
320                 fmls.shrink(j);
321                 progress = true;
322             }
323             if (!m.limit().inc())
324                 return;
325             vars.append(new_vars);
326             if (progress) {
327                 preprocess_solve(model, vars, fmls);
328             }
329         }
330         if (fmls.empty()) {
331             vars.reset();
332         }
333         fmls.append(unused_fmls);
334         SASSERT(validate_model(model, fmls));
335         TRACE("qe", tout << vars << " " << fmls << "\n";);
336     }
337 
do_qe_lite(app_ref_vector & vars,expr_ref & fml)338     void do_qe_lite(app_ref_vector& vars, expr_ref& fml) {
339         qe_lite qe(m, m_params, false);
340         qe(vars, fml);
341         m_rw(fml);
342         TRACE("qe", tout << "After qe_lite:\n" << fml << "\n" << "Vars: " << vars << "\n";);
343         SASSERT(!m.is_false(fml));
344     }
345 
do_qe_bool(model & mdl,app_ref_vector & vars,expr_ref & fml)346     void do_qe_bool(model& mdl, app_ref_vector& vars, expr_ref& fml) {
347         expr_ref_vector fmls(m);
348         fmls.push_back(fml);
349         project_bools(mdl, vars, fmls);
350         fml = mk_and(fmls);
351     }
352 
spacer(app_ref_vector & vars,model & mdl,expr_ref & fml)353     void spacer(app_ref_vector& vars, model& mdl, expr_ref& fml) {
354         TRACE("qe", tout << "Before projection:\n" << fml << "\n" << "Vars: " << vars << "\n";);
355 
356         model_evaluator eval(mdl, m_params);
357         eval.set_model_completion(true);
358         app_ref_vector other_vars(m);
359         app_ref_vector array_vars(m);
360         array_util arr_u(m);
361         arith_util ari_u(m);
362 
363         flatten_and(fml);
364 
365         while (!vars.empty()) {
366 
367             do_qe_lite(vars, fml);
368 
369             do_qe_bool(mdl, vars, fml);
370 
371             // sort out vars into bools, arith (int/real), and arrays
372             for (app* v : vars) {
373                 if (arr_u.is_array(v)) {
374                     array_vars.push_back(v);
375                 }
376                 else {
377                     other_vars.push_back(v);
378                 }
379             }
380 
381             TRACE("qe", tout << "Array vars: " << array_vars << "\n";);
382 
383             vars.reset();
384 
385             // project arrays
386             mbp::array_project_plugin ap(m);
387             ap(mdl, array_vars, fml, vars, m_reduce_all_selects);
388             SASSERT(array_vars.empty());
389             m_rw(fml);
390             SASSERT(!m.is_false(fml));
391 
392             TRACE("qe",
393                 tout << "extended model:\n" << mdl;
394                 tout << "Vars: " << vars << "\n";);
395         }
396 
397         // project reals, ints and other variables.
398         if (!other_vars.empty()) {
399             TRACE("qe", tout << "Other vars: " << other_vars << "\n" << mdl;);
400 
401             expr_ref_vector fmls(m);
402             flatten_and(fml, fmls);
403 
404             (*this)(false, other_vars, mdl, fmls);
405             fml = mk_and(fmls);
406             m_rw(fml);
407 
408             TRACE("qe",
409                 tout << "Projected other vars:\n" << fml << "\n";
410             tout << "Remaining other vars:\n" << other_vars << "\n";);
411             SASSERT(!m.is_false(fml));
412         }
413 
414         if (!other_vars.empty()) {
415             project_vars(mdl, other_vars, fml);
416             m_rw(fml);
417         }
418 
419         // substitute any remaining other vars
420         if (!m_dont_sub && !other_vars.empty()) {
421             subst_vars(eval, other_vars, fml);
422             TRACE("qe", tout << "After substituting remaining other vars:\n" << fml << "\n";);
423             // an extra round of simplification because subst_vars is not simplifying
424             m_rw(fml);
425             other_vars.reset();
426         }
427 
428         SASSERT(!eval.is_false(fml));
429 
430         vars.reset();
431         vars.append(other_vars);
432     }
433 
434 };
435 
mbproj(ast_manager & m,params_ref const & p)436 mbproj::mbproj(ast_manager& m, params_ref const& p) {
437     scoped_no_proof _sp(m);
438     m_impl = alloc(impl, m, p);
439 }
440 
~mbproj()441 mbproj::~mbproj() {
442     dealloc(m_impl);
443 }
444 
updt_params(params_ref const & p)445 void mbproj::updt_params(params_ref const& p) {
446     m_impl->updt_params(p);
447 }
448 
get_param_descrs(param_descrs & r)449 void mbproj::get_param_descrs(param_descrs& r) {
450     r.insert("reduce_all_selects", CPK_BOOL, "(default: false) reduce selects");
451     r.insert("dont_sub", CPK_BOOL, "(default: false) disable substitution of values for free variables");
452 }
453 
operator ()(bool force_elim,app_ref_vector & vars,model & mdl,expr_ref_vector & fmls)454 void mbproj::operator()(bool force_elim, app_ref_vector& vars, model& mdl, expr_ref_vector& fmls) {
455     scoped_no_proof _sp(fmls.get_manager());
456     (*m_impl)(force_elim, vars, mdl, fmls);
457 }
458 
spacer(app_ref_vector & vars,model & mdl,expr_ref & fml)459 void mbproj::spacer(app_ref_vector& vars, model& mdl, expr_ref& fml) {
460     scoped_no_proof _sp(fml.get_manager());
461     m_impl->spacer(vars, mdl, fml);
462 }
463 
solve(model & model,app_ref_vector & vars,expr_ref_vector & fmls)464 void mbproj::solve(model& model, app_ref_vector& vars, expr_ref_vector& fmls) {
465     scoped_no_proof _sp(fmls.get_manager());
466     m_impl->preprocess_solve(model, vars, fmls);
467 }
468 
maximize(expr_ref_vector const & fmls,model & mdl,app * t,expr_ref & ge,expr_ref & gt)469 opt::inf_eps mbproj::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) {
470     scoped_no_proof _sp(fmls.get_manager());
471     return m_impl->maximize(fmls, mdl, t, ge, gt);
472 }
473