1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 probe.cpp
7
8 Abstract:
9
10 Evaluates/Probes a goal.
11
12 A probe is used to build tactics (aka strategies) that
13 makes decisions based on the structure of a goal.
14
15 Author:
16
17 Leonardo de Moura (leonardo) 2011-10-13.
18
19 Revision History:
20
21 --*/
22 #include "tactic/probe.h"
23 #include "ast/arith_decl_plugin.h"
24 #include "ast/bv_decl_plugin.h"
25 #include "tactic/goal_util.h"
26 #include "ast/rewriter/bv_rewriter.h"
27
28 class memory_probe : public probe {
29 public:
operator ()(goal const & g)30 result operator()(goal const & g) override {
31 return result(static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024));
32 }
33 };
34
mk_memory_probe()35 probe * mk_memory_probe() {
36 return alloc(memory_probe);
37 }
38
39 class depth_probe : public probe {
40 public:
operator ()(goal const & g)41 result operator()(goal const & g) override {
42 return result(g.depth());
43 }
44 };
45
46 class size_probe : public probe {
47 public:
operator ()(goal const & g)48 result operator()(goal const & g) override {
49 return result(g.size());
50 }
51 };
52
53 class num_exprs_probe : public probe {
54 public:
operator ()(goal const & g)55 result operator()(goal const & g) override {
56 return result(g.num_exprs());
57 }
58 };
59
mk_depth_probe()60 probe * mk_depth_probe() {
61 return alloc(depth_probe);
62 }
63
mk_size_probe()64 probe * mk_size_probe() {
65 return alloc(size_probe);
66 }
67
mk_num_exprs_probe()68 probe * mk_num_exprs_probe() {
69 return alloc(num_exprs_probe);
70 }
71
72 class unary_probe : public probe {
73 protected:
74 probe * m_p;
75 public:
unary_probe(probe * p)76 unary_probe(probe * p):
77 m_p(p) {
78 SASSERT(p);
79 p->inc_ref();
80 }
81
~unary_probe()82 ~unary_probe() override {
83 m_p->dec_ref();
84 }
85
86 };
87
88 class bin_probe : public probe {
89 protected:
90 probe * m_p1;
91 probe * m_p2;
92 public:
bin_probe(probe * p1,probe * p2)93 bin_probe(probe * p1, probe * p2):
94 m_p1(p1),
95 m_p2(p2) {
96 SASSERT(p1);
97 SASSERT(p2);
98 p1->inc_ref();
99 p2->inc_ref();
100 }
101
~bin_probe()102 ~bin_probe() override {
103 m_p1->dec_ref();
104 m_p2->dec_ref();
105 }
106 };
107
108 class not_probe : public unary_probe {
109 public:
not_probe(probe * p)110 not_probe(probe * p):unary_probe(p) {}
operator ()(goal const & g)111 result operator()(goal const & g) override {
112 return result(!m_p->operator()(g).is_true());
113 }
114 };
115
116 class and_probe : public bin_probe {
117 public:
and_probe(probe * p1,probe * p2)118 and_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
operator ()(goal const & g)119 result operator()(goal const & g) override {
120 return result(m_p1->operator()(g).is_true() && m_p2->operator()(g).is_true());
121 }
122 };
123
124 class or_probe : public bin_probe {
125 public:
or_probe(probe * p1,probe * p2)126 or_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
operator ()(goal const & g)127 result operator()(goal const & g) override {
128 return result(m_p1->operator()(g).is_true() || m_p2->operator()(g).is_true());
129 }
130 };
131
132 class eq_probe : public bin_probe {
133 public:
eq_probe(probe * p1,probe * p2)134 eq_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
operator ()(goal const & g)135 result operator()(goal const & g) override {
136 return result(m_p1->operator()(g).get_value() == m_p2->operator()(g).get_value());
137 }
138 };
139
140 class le_probe : public bin_probe {
141 public:
le_probe(probe * p1,probe * p2)142 le_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
operator ()(goal const & g)143 result operator()(goal const & g) override {
144 return result(m_p1->operator()(g).get_value() <= m_p2->operator()(g).get_value());
145 }
146 };
147
148 class add_probe : public bin_probe {
149 public:
add_probe(probe * p1,probe * p2)150 add_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
operator ()(goal const & g)151 result operator()(goal const & g) override {
152 return result(m_p1->operator()(g).get_value() + m_p2->operator()(g).get_value());
153 }
154 };
155
156 class sub_probe : public bin_probe {
157 public:
sub_probe(probe * p1,probe * p2)158 sub_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
operator ()(goal const & g)159 result operator()(goal const & g) override {
160 return result(m_p1->operator()(g).get_value() - m_p2->operator()(g).get_value());
161 }
162 };
163
164 class mul_probe : public bin_probe {
165 public:
mul_probe(probe * p1,probe * p2)166 mul_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
operator ()(goal const & g)167 result operator()(goal const & g) override {
168 return result(m_p1->operator()(g).get_value() * m_p2->operator()(g).get_value());
169 }
170 };
171
172 class div_probe : public bin_probe {
173 public:
div_probe(probe * p1,probe * p2)174 div_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
operator ()(goal const & g)175 result operator()(goal const & g) override {
176 return result(m_p1->operator()(g).get_value() / m_p2->operator()(g).get_value());
177 }
178 };
179
180 class const_probe : public probe {
181 double m_val;
182 public:
const_probe(double v)183 const_probe(double v):m_val(v) {}
184
operator ()(goal const & g)185 result operator()(goal const & g) override {
186 return result(m_val);
187 }
188 };
189
mk_const_probe(double v)190 probe * mk_const_probe(double v) {
191 return alloc(const_probe, v);
192 }
193
mk_not(probe * p)194 probe * mk_not(probe * p) {
195 return alloc(not_probe, p);
196 }
197
mk_and(probe * p1,probe * p2)198 probe * mk_and(probe * p1, probe * p2) {
199 return alloc(and_probe, p1, p2);
200 }
201
mk_or(probe * p1,probe * p2)202 probe * mk_or(probe * p1, probe * p2) {
203 return alloc(or_probe, p1, p2);
204 }
205
mk_implies(probe * p1,probe * p2)206 probe * mk_implies(probe * p1, probe * p2) {
207 return mk_or(mk_not(p1), p2);
208 }
209
mk_eq(probe * p1,probe * p2)210 probe * mk_eq(probe * p1, probe * p2) {
211 return alloc(eq_probe, p1, p2);
212 }
213
mk_neq(probe * p1,probe * p2)214 probe * mk_neq(probe * p1, probe * p2) {
215 return mk_not(mk_eq(p1, p2));
216 }
217
mk_le(probe * p1,probe * p2)218 probe * mk_le(probe * p1, probe * p2) {
219 return alloc(le_probe, p1, p2);
220 }
221
mk_ge(probe * p1,probe * p2)222 probe * mk_ge(probe * p1, probe * p2) {
223 return mk_le(p2, p1);
224 }
225
mk_lt(probe * p1,probe * p2)226 probe * mk_lt(probe * p1, probe * p2) {
227 return mk_not(mk_ge(p1, p2));
228 }
229
mk_gt(probe * p1,probe * p2)230 probe * mk_gt(probe * p1, probe * p2) {
231 return mk_lt(p2, p1);
232 }
233
mk_add(probe * p1,probe * p2)234 probe * mk_add(probe * p1, probe * p2) {
235 return alloc(add_probe, p1, p2);
236 }
237
mk_mul(probe * p1,probe * p2)238 probe * mk_mul(probe * p1, probe * p2) {
239 return alloc(mul_probe, p1, p2);
240 }
241
mk_sub(probe * p1,probe * p2)242 probe * mk_sub(probe * p1, probe * p2) {
243 return alloc(sub_probe, p1, p2);
244 }
245
mk_div(probe * p1,probe * p2)246 probe * mk_div(probe * p1, probe * p2) {
247 return alloc(div_probe, p1, p2);
248 }
249
250 struct is_non_propositional_predicate {
251 struct found {};
252 ast_manager & m;
253
is_non_propositional_predicateis_non_propositional_predicate254 is_non_propositional_predicate(ast_manager & _m):m(_m) {}
operator ()is_non_propositional_predicate255 void operator()(var *) { throw found(); }
operator ()is_non_propositional_predicate256 void operator()(quantifier *) { throw found(); }
operator ()is_non_propositional_predicate257 void operator()(app * n) {
258 if (!m.is_bool(n))
259 throw found();
260
261 family_id fid = n->get_family_id();
262 if (fid == m.get_basic_family_id())
263 return;
264
265 if (is_uninterp_const(n))
266 return;
267
268 throw found();
269 }
270 };
271
272 struct is_non_qfbv_predicate {
273 struct found {};
274 ast_manager & m;
275 bv_util u;
276
is_non_qfbv_predicateis_non_qfbv_predicate277 is_non_qfbv_predicate(ast_manager & _m):m(_m), u(m) {}
278
operator ()is_non_qfbv_predicate279 void operator()(var *) { throw found(); }
280
operator ()is_non_qfbv_predicate281 void operator()(quantifier *) { throw found(); }
282
operator ()is_non_qfbv_predicate283 void operator()(app * n) {
284 if (!m.is_bool(n) && !u.is_bv(n))
285 throw found();
286 family_id fid = n->get_family_id();
287 if (fid == m.get_basic_family_id())
288 return;
289 if (fid == u.get_family_id()) {
290 if (n->get_decl_kind() == OP_BSDIV0 ||
291 n->get_decl_kind() == OP_BUDIV0 ||
292 n->get_decl_kind() == OP_BSREM0 ||
293 n->get_decl_kind() == OP_BUREM0 ||
294 n->get_decl_kind() == OP_BSMOD0)
295 throw found();
296 return;
297 }
298 if (is_uninterp_const(n))
299 return;
300 throw found();
301 }
302 };
303
304 class is_propositional_probe : public probe {
305 public:
operator ()(goal const & g)306 result operator()(goal const & g) override {
307 return !test<is_non_propositional_predicate>(g);
308 }
309 };
310
311
312 class is_qfbv_probe : public probe {
313 public:
operator ()(goal const & g)314 result operator()(goal const & g) override {
315 return !test<is_non_qfbv_predicate>(g);
316 }
317 };
318
mk_is_propositional_probe()319 probe * mk_is_propositional_probe() {
320 return alloc(is_propositional_probe);
321 }
322
mk_is_qfbv_probe()323 probe * mk_is_qfbv_probe() {
324 return alloc(is_qfbv_probe);
325 }
326
327 struct is_non_qfaufbv_predicate {
328 struct found {};
329 ast_manager & m;
330 bv_util m_bv_util;
331 array_util m_array_util;
332
is_non_qfaufbv_predicateis_non_qfaufbv_predicate333 is_non_qfaufbv_predicate(ast_manager & _m) : m(_m), m_bv_util(_m), m_array_util(_m) {}
334
operator ()is_non_qfaufbv_predicate335 void operator()(var *) { throw found(); }
336
operator ()is_non_qfaufbv_predicate337 void operator()(quantifier *) { throw found(); }
338
operator ()is_non_qfaufbv_predicate339 void operator()(app * n) {
340 if (!m.is_bool(n) && !m_bv_util.is_bv(n) && !m_array_util.is_array(n))
341 throw found();
342 family_id fid = n->get_family_id();
343 if (fid == m.get_basic_family_id())
344 return;
345 if (fid == m_bv_util.get_family_id() || fid == m_array_util.get_family_id())
346 return;
347 if (is_uninterp(n))
348 return;
349
350 throw found();
351 }
352 };
353
354 class is_qfaufbv_probe : public probe {
355 public:
operator ()(goal const & g)356 result operator()(goal const & g) override {
357 return !test<is_non_qfaufbv_predicate>(g);
358 }
359 };
360
mk_is_qfaufbv_probe()361 probe * mk_is_qfaufbv_probe() {
362 return alloc(is_qfaufbv_probe);
363 }
364
365
366 struct is_non_qfufbv_predicate {
367 struct found {};
368 ast_manager & m;
369 bv_util m_bv_util;
370
is_non_qfufbv_predicateis_non_qfufbv_predicate371 is_non_qfufbv_predicate(ast_manager & _m) : m(_m), m_bv_util(_m) {}
372
operator ()is_non_qfufbv_predicate373 void operator()(var *) { throw found(); }
374
operator ()is_non_qfufbv_predicate375 void operator()(quantifier *) { throw found(); }
376
operator ()is_non_qfufbv_predicate377 void operator()(app * n) {
378 if (!m.is_bool(n) && !m_bv_util.is_bv(n))
379 throw found();
380 family_id fid = n->get_family_id();
381 if (fid == m.get_basic_family_id())
382 return;
383 if (fid == m_bv_util.get_family_id())
384 return;
385 if (is_uninterp(n))
386 return;
387
388 throw found();
389 }
390 };
391
392 class is_qfufbv_probe : public probe {
393 public:
operator ()(goal const & g)394 result operator()(goal const & g) override {
395 return !test<is_non_qfufbv_predicate>(g);
396 }
397 };
398
mk_is_qfufbv_probe()399 probe * mk_is_qfufbv_probe() {
400 return alloc(is_qfufbv_probe);
401 }
402
403
404
405 class num_consts_probe : public probe {
406 bool m_bool; // If true, track only boolean constants. Otherwise, track only non boolean constants.
407 char const * m_family; // (Ignored if m_bool == true), if != 0 and m_bool == true, then track only constants of the given family.
408 struct proc {
409 ast_manager & m;
410 bool m_bool;
411 family_id m_fid;
412 unsigned m_counter;
procnum_consts_probe::proc413 proc(ast_manager & _m, bool b, char const * family):m(_m), m_bool(b), m_counter(0) {
414 if (family != nullptr)
415 m_fid = m.mk_family_id(family);
416 else
417 m_fid = null_family_id;
418 }
operator ()num_consts_probe::proc419 void operator()(quantifier *) {}
operator ()num_consts_probe::proc420 void operator()(var *) {}
operator ()num_consts_probe::proc421 void operator()(app * n) {
422 if (n->get_num_args() == 0 && !m.is_value(n)) {
423 if (m_bool) {
424 if (m.is_bool(n))
425 m_counter++;
426 }
427 else {
428 if (m_fid == null_family_id) {
429 if (!m.is_bool(n))
430 m_counter++;
431 }
432 else {
433 if (m.get_sort(n)->get_family_id() == m_fid)
434 m_counter++;
435 }
436 }
437 }
438 }
439 };
440
441 public:
num_consts_probe(bool b,char const * f)442 num_consts_probe(bool b, char const * f):
443 m_bool(b), m_family(f) {
444 }
operator ()(goal const & g)445 result operator()(goal const & g) override {
446 proc p(g.m(), m_bool, m_family);
447 unsigned sz = g.size();
448 expr_fast_mark1 visited;
449 for (unsigned i = 0; i < sz; i++) {
450 for_each_expr_core<proc, expr_fast_mark1, true, true>(p, visited, g.form(i));
451 }
452 return result(p.m_counter);
453 }
454 };
455
mk_num_consts_probe()456 probe * mk_num_consts_probe() {
457 return alloc(num_consts_probe, false, nullptr);
458 }
459
mk_num_bool_consts_probe()460 probe * mk_num_bool_consts_probe() {
461 return alloc(num_consts_probe, true, nullptr);
462 }
463
mk_num_arith_consts_probe()464 probe * mk_num_arith_consts_probe() {
465 return alloc(num_consts_probe, false, "arith");
466 }
467
mk_num_bv_consts_probe()468 probe * mk_num_bv_consts_probe() {
469 return alloc(num_consts_probe, false, "bv");
470 }
471
472 class produce_proofs_probe : public probe {
473 public:
operator ()(goal const & g)474 result operator()(goal const & g) override {
475 return g.proofs_enabled();
476 }
477 };
478
479 class produce_models_probe : public probe {
480 public:
operator ()(goal const & g)481 result operator()(goal const & g) override {
482 return g.models_enabled();
483 }
484 };
485
486 class produce_unsat_cores_probe : public probe {
487 public:
operator ()(goal const & g)488 result operator()(goal const & g) override {
489 return g.unsat_core_enabled();
490 }
491 };
492
mk_produce_proofs_probe()493 probe * mk_produce_proofs_probe() {
494 return alloc(produce_proofs_probe);
495 }
496
mk_produce_models_probe()497 probe * mk_produce_models_probe() {
498 return alloc(produce_models_probe);
499 }
500
mk_produce_unsat_cores_probe()501 probe * mk_produce_unsat_cores_probe() {
502 return alloc(produce_unsat_cores_probe);
503 }
504
505 struct has_pattern_probe : public probe {
506 struct found {};
507
508 struct proc {
operator ()has_pattern_probe::proc509 void operator()(var * n) {}
operator ()has_pattern_probe::proc510 void operator()(app * n) {}
operator ()has_pattern_probe::proc511 void operator()(quantifier * n) {
512 if (n->get_num_patterns() > 0 || n->get_num_no_patterns() > 0)
513 throw found();
514 }
515 };
516 public:
operator ()has_pattern_probe517 result operator()(goal const & g) override {
518 try {
519 expr_fast_mark1 visited;
520 proc p;
521 unsigned sz = g.size();
522 for (unsigned i = 0; i < sz; i++) {
523 quick_for_each_expr(p, visited, g.form(i));
524 }
525 return false;
526 }
527 catch (const found &) {
528 return true;
529 }
530 }
531 };
532
mk_has_pattern_probe()533 probe * mk_has_pattern_probe() {
534 return alloc(has_pattern_probe);
535 }
536
537
538 struct has_quantifier_probe : public probe {
539 struct found {};
540
541 struct proc {
operator ()has_quantifier_probe::proc542 void operator()(var * n) {}
operator ()has_quantifier_probe::proc543 void operator()(app * n) {}
operator ()has_quantifier_probe::proc544 void operator()(quantifier * n) { throw found(); }
545 };
546 public:
operator ()has_quantifier_probe547 result operator()(goal const & g) override {
548 try {
549 expr_fast_mark1 visited;
550 proc p;
551 unsigned sz = g.size();
552 for (unsigned i = 0; i < sz; i++) {
553 quick_for_each_expr(p, visited, g.form(i));
554 }
555 return false;
556 }
557 catch (const found &) {
558 return true;
559 }
560 }
561 };
562
mk_has_quantifier_probe()563 probe * mk_has_quantifier_probe() {
564 return alloc(has_quantifier_probe);
565 }
566
567
568
569