1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 check_logic.cpp
7
8 Abstract:
9
10 Check whether a given assertion is in the correct logic or not
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2011-08-11.
15
16 Revision History:
17
18 --*/
19 #include "solver/check_logic.h"
20 #include "solver/smt_logics.h"
21 #include "ast/arith_decl_plugin.h"
22 #include "ast/array_decl_plugin.h"
23 #include "ast/bv_decl_plugin.h"
24 #include "ast/seq_decl_plugin.h"
25 #include "ast/pb_decl_plugin.h"
26 #include "ast/datatype_decl_plugin.h"
27 #include "ast/ast_pp.h"
28 #include "ast/for_each_expr.h"
29 #include<sstream>
30
31 struct check_logic::imp {
32 ast_manager & m;
33 symbol m_logic;
34 arith_util m_a_util;
35 bv_util m_bv_util;
36 array_util m_ar_util;
37 seq_util m_seq_util;
38 datatype_util m_dt_util;
39 pb_util m_pb_util;
40 bool m_uf; // true if the logic supports uninterpreted functions
41 bool m_dt; // true if the lgoic supports dattypes
42 bool m_arrays; // true if the logic supports arbitrary arrays
43 bool m_bv_arrays; // true if the logic supports only bv arrays
44 bool m_reals; // true if the logic supports reals
45 bool m_ints; // true if the logic supports integers
46 bool m_diff; // true if the logic supports difference logic only
47 bool m_nonlinear; // true if the logic supports nonlinear arithmetic
48 bool m_bvs; // true if the logic supports bit-vectors
49 bool m_quantifiers; // true if the logic supports quantifiers
50 bool m_unknown_logic;
51
impcheck_logic::imp52 imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m), m_dt_util(m), m_pb_util(m) {
53 reset();
54 }
55
resetcheck_logic::imp56 void reset() {
57 m_uf = false;
58 m_dt = false;
59 m_arrays = false;
60 m_bv_arrays = false;
61 m_reals = false;
62 m_ints = false;
63 m_diff = false;
64 m_nonlinear = false;
65 m_bvs = false;
66 m_quantifiers = false;
67 m_unknown_logic = true;
68 }
69
set_logiccheck_logic::imp70 void set_logic(symbol const & logic) {
71 reset();
72 m_unknown_logic = false;
73 if (logic == "AUFLIA") {
74 m_uf = true;
75 m_arrays = true;
76 m_ints = true;
77 m_quantifiers = true;
78 }
79 else if (logic == "AUFLIRA") {
80 m_uf = true;
81 m_arrays = true;
82 m_reals = true;
83 m_ints = true;
84 m_quantifiers = true;
85 }
86 else if (logic == "AUFNIRA") {
87 m_uf = true;
88 m_arrays = true;
89 m_reals = true;
90 m_ints = true;
91 m_nonlinear = true;
92 m_quantifiers = true;
93 }
94 else if (logic == "LRA") {
95 m_reals = true;
96 m_quantifiers = true;
97 }
98 else if (logic == "QF_ABV") {
99 m_bv_arrays = true;
100 m_bvs = true;
101 }
102 else if (logic == "QF_AUFBV") {
103 m_uf = true;
104 m_bv_arrays = true;
105 m_bvs = true;
106 }
107 else if (logic == "QF_UFBV") {
108 m_uf = true;
109 m_bvs = true;
110 }
111 else if (logic == "QF_UFDT") {
112 m_uf = true;
113 m_dt = true;
114 }
115 else if (logic == "QF_DT") {
116 m_dt = true;
117 }
118 else if (logic == "QF_AUFLIA") {
119 m_uf = true;
120 m_arrays = true;
121 m_ints = true;
122 }
123 else if (logic == "QF_AX") {
124 m_arrays = true;
125 }
126 else if (logic == "QF_BV") {
127 m_bvs = true;
128 }
129 else if (logic == "QF_IDL") {
130 m_ints = true;
131 m_diff = true;
132 }
133 else if (logic == "QF_RDL") {
134 m_reals = true;
135 m_diff = true;
136 }
137 else if (logic == "QF_LIA") {
138 m_ints = true;
139 }
140 else if (logic == "QF_LRA") {
141 m_reals = true;
142 }
143 else if (logic == "QF_NIA") {
144 m_ints = true;
145 m_nonlinear = true;
146 }
147 else if (logic == "QF_NRA") {
148 m_reals = true;
149 m_nonlinear = true;
150 }
151 else if (logic == "QF_UF") {
152 m_uf = true;
153 }
154 else if (logic == "QF_UFIDL") {
155 m_uf = true;
156 m_ints = true;
157 m_diff = true;
158 }
159 else if (logic == "QF_UFLIA") {
160 m_uf = true;
161 m_ints = true;
162 }
163 else if (logic == "QF_UFLRA") {
164 m_uf = true;
165 m_reals = true;
166 }
167 else if (logic == "QF_UFNRA") {
168 m_uf = true;
169 m_reals = true;
170 m_nonlinear = true;
171 }
172 else if (logic == "UFLRA") {
173 m_uf = true;
174 m_reals = true;
175 m_quantifiers = true;
176 }
177 else if (logic == "UFNIA") {
178 m_uf = true;
179 m_ints = true;
180 m_quantifiers = true;
181 m_nonlinear = true;
182 }
183 else if (logic == "UFBV") {
184 m_uf = true;
185 m_bvs = true;
186 m_quantifiers = true;
187 }
188 else if (logic == "QF_S" || logic == "QF_SLIA") {
189 m_uf = true;
190 m_bvs = true;
191 m_ints = true;
192 m_arrays = true;
193 m_reals = true;
194 m_quantifiers = true; // some QF_SLIA benchmarks are miss-classified
195 }
196 else if (logic == "QF_FD") {
197 m_bvs = true;
198 m_uf = true;
199 m_ints = true;
200 m_dt = true;
201 m_nonlinear = true; // non-linear 0-1 variables may get eliminated
202 }
203 else if (logic == "SMTFD") {
204 m_bvs = true;
205 m_uf = true;
206 m_arrays = true;
207 m_ints = false;
208 m_dt = false;
209 m_nonlinear = false;
210 }
211 else {
212 m_unknown_logic = true;
213 }
214
215 m_logic = logic;
216 }
217
218 struct failed {};
219 std::string m_last_error;
220
failcheck_logic::imp221 void fail(std::string &&msg) {
222 m_last_error = std::move(msg);
223 throw failed();
224 }
225
failcheck_logic::imp226 void fail(char const * msg) {
227 m_last_error = msg;
228 throw failed();
229 }
230
check_sortcheck_logic::imp231 void check_sort(sort * s) {
232 if (s->get_family_id() == null_family_id) {
233 if (!m_uf)
234 fail("logic does not support uninterpreted sorts");
235 }
236 else if (m.is_bool(s)) {
237 return;
238 }
239 else if (m_a_util.is_int(s)) {
240 if (!m_ints)
241 fail("logic does not support integers");
242 }
243 else if (m_a_util.is_real(s)) {
244 if (!m_reals)
245 fail("logic does not support reals");
246 }
247 else if (m_bv_util.is_bv_sort(s)) {
248 if (!m_bvs)
249 fail("logic does not support bitvectors");
250 }
251 else if (m_dt_util.is_datatype(s)) {
252 if (!m_dt)
253 fail("logic does not support algebraic datatypes");
254 }
255 else if (m_ar_util.is_array(s)) {
256 if (m_arrays) {
257 return;
258 }
259 else if (m_bv_arrays) {
260 unsigned sz = get_array_arity(s);
261 for (unsigned i = 0; i < sz; ++i) {
262 if (!m_bv_util.is_bv_sort(get_array_domain(s, i)))
263 fail("logic supports only arrays from bitvectors to bitvectors");
264 }
265 check_sort(get_array_range(s));
266 }
267 else {
268 fail("logic does not support arrays");
269 }
270 }
271 }
272
operator ()check_logic::imp273 void operator()(var * n) {
274 if (!m_quantifiers)
275 fail("logic does not support quantifiers");
276 check_sort(n->get_sort());
277 }
278
is_intcheck_logic::imp279 bool is_int(expr * t) {
280 if (m_a_util.is_uminus(t))
281 t = to_app(t)->get_arg(0);
282 // Take care of coercions automatically added by Z3
283 if (m_a_util.is_to_real(t))
284 t = to_app(t)->get_arg(0);
285 return m_a_util.is_numeral(t);
286 }
287
is_numeralcheck_logic::imp288 bool is_numeral(expr * t) {
289 if (m_a_util.is_uminus(t))
290 t = to_app(t)->get_arg(0);
291 // c
292 if (is_int(t))
293 return true;
294 // c1/c2
295 if (m_a_util.is_div(t) && is_int(to_app(t)->get_arg(0)) && is_int(to_app(t)->get_arg(1)))
296 return true;
297 return false;
298 }
299
300 // check if n has at most one argument that is not numeral.
check_mulcheck_logic::imp301 void check_mul(app * n) {
302 if (m_nonlinear)
303 return; // nothing to check
304 unsigned num_args = n->get_num_args();
305 bool found_non_numeral = false;
306 for (unsigned i = 0; i < num_args; i++) {
307 if (!is_numeral(n->get_arg(i))) {
308 if (found_non_numeral)
309 fail("logic does not support nonlinear arithmetic");
310 else
311 found_non_numeral = true;
312 }
313 }
314 }
315
316 // check if the divisor is a numeral
check_divcheck_logic::imp317 void check_div(app * n) {
318 if (n->get_num_args() != 2 || (!m_nonlinear && !is_numeral(n->get_arg(1))))
319 fail("logic does not support nonlinear arithmetic");
320 }
321
is_diff_varcheck_logic::imp322 bool is_diff_var(expr * t) const {
323 if (is_app(t) && to_app(t)->get_decl()->get_family_id() == null_family_id)
324 return true;
325 if (m.is_ite(t))
326 return true;
327 return false;
328 }
329
fail_non_diffcheck_logic::imp330 void fail_non_diff(expr * t) {
331 TRACE("check_logic", tout << mk_pp(t, m) << "\n";);
332 fail("logic only supports difference arithmetic");
333 }
334
same_argscheck_logic::imp335 bool same_args(app * t) {
336 unsigned num_args = t->get_num_args();
337 if (num_args == 0)
338 return false;
339 expr * arg = t->get_arg(0);
340 for (unsigned i = 1; i < num_args; i++) {
341 if (t->get_arg(i) != arg)
342 return false;
343 }
344 return true;
345 }
346
is_arithcheck_logic::imp347 bool is_arith(expr * t) const {
348 return t->get_sort()->get_family_id() == m_a_util.get_family_id();
349 }
350
is_offsetcheck_logic::imp351 bool is_offset(app * t) {
352 while (true) {
353 expr * non_numeral = nullptr;
354 unsigned num_args = t->get_num_args();
355 for (unsigned i = 0; i < num_args; i++) {
356 expr * arg = t->get_arg(i);
357 if (is_numeral(arg))
358 continue;
359 if (non_numeral != nullptr)
360 return false;
361 non_numeral = arg;
362 }
363 if (non_numeral == nullptr)
364 return true;
365 if (is_diff_var(non_numeral))
366 return true;
367 if (!m_a_util.is_add(non_numeral) && !m_a_util.is_sub(non_numeral))
368 return false;
369 t = to_app(non_numeral);
370 }
371 return true;
372 }
373
is_diff_argcheck_logic::imp374 bool is_diff_arg(expr * t) {
375 if (is_diff_var(t))
376 return true;
377 if (is_numeral(t))
378 return true;
379 if (m_a_util.is_add(t) || m_a_util.is_sub(t))
380 return is_offset(to_app(t));
381 return false;
382 }
383
384 // Check if n is a diff logic predicate
check_diff_predicatecheck_logic::imp385 void check_diff_predicate(app * n) {
386 expr * lhs = n->get_arg(0);
387 expr * rhs = n->get_arg(1);
388 if (!is_arith(lhs))
389 return; // formula is not in arithmetic
390 if (is_diff_arg(lhs) && is_diff_arg(rhs))
391 return;
392 if (is_numeral(lhs))
393 std::swap(lhs, rhs);
394 if (!is_numeral(rhs))
395 fail_non_diff(n);
396 if (!m_a_util.is_sub(lhs) || to_app(lhs)->get_num_args() != 2)
397 fail_non_diff(n);
398 expr * t1 = to_app(lhs)->get_arg(0);
399 expr * t2 = to_app(lhs)->get_arg(1);
400 if (is_diff_var(t1) && is_diff_var(t2))
401 return;
402 if (m_a_util.is_add(t1) && m_a_util.is_add(t2)) {
403 // QF_RDL supports (<= (- (+ x ... x) (+ y ... y)) c)
404 if (to_app(t1)->get_num_args() != to_app(t2)->get_num_args())
405 fail_non_diff(n);
406 if (!same_args(to_app(t1)) || !same_args(to_app(t2)))
407 fail_non_diff(n);
408 return;
409 }
410 fail_non_diff(n);
411 }
412
check_diff_argcheck_logic::imp413 void check_diff_arg(expr * t) {
414 if (!is_diff_arg(t))
415 fail_non_diff(t);
416 }
417
418 // Check if the arith args of n are of the form (t + k) where k is a numeral.
check_diff_argscheck_logic::imp419 void check_diff_args(app * n) {
420 unsigned num_args = n->get_num_args();
421 for (unsigned i = 0; i < num_args; i++) {
422 if (is_arith(n))
423 check_diff_arg(n);
424 }
425 }
426
operator ()check_logic::imp427 void operator()(app * n) {
428 sort * s = n->get_sort();
429 check_sort(s);
430 func_decl * f = n->get_decl();
431 family_id fid = f->get_family_id();
432 if (fid == null_family_id) {
433 if (!m_uf && f->get_arity() > 0)
434 fail("logic does not support uninterpreted functions");
435 if (m_diff)
436 check_diff_args(n);
437 }
438 else if (fid == m_a_util.get_family_id()) {
439 if (m_a_util.is_mul(n))
440 check_mul(n);
441 else if (m_a_util.is_div(n) || m_a_util.is_idiv(n) || m_a_util.is_rem(n) || m_a_util.is_mod(n))
442 check_div(n);
443 if (m_diff) {
444 if (m_a_util.is_le(n) || m_a_util.is_lt(n) || m_a_util.is_ge(n) || m_a_util.is_gt(n))
445 check_diff_predicate(n);
446 }
447 if (!m_ints || !m_reals) {
448 if (m_a_util.is_to_real(n) || m_a_util.is_to_int(n))
449 fail("logic does not support casting operators");
450 }
451 }
452 else if (fid == m_bv_util.get_family_id()) {
453 // nothing to check...
454 }
455 else if (fid == m_ar_util.get_family_id()) {
456 // nothing to check...
457 if (m_diff)
458 check_diff_args(n);
459 }
460 else if (fid == m.get_basic_family_id()) {
461 // nothing to check...
462 if (m_diff) {
463 if (m.is_eq(n))
464 check_diff_predicate(n);
465 else if (m.is_distinct(n) || m.is_ite(n))
466 check_diff_args(n);
467 }
468 }
469 else if (m.is_builtin_family_id(fid)) {
470 // nothing to check
471 }
472 else if (fid == m_seq_util.get_family_id()) {
473 // nothing to check
474 }
475 else if (fid == m_dt_util.get_family_id() && m_dt) {
476 // nothing to check
477 }
478 else if (fid == m_pb_util.get_family_id() && smt_logics::logic_has_pb(m_logic)) {
479 // nothing to check
480 }
481 else {
482 std::stringstream strm;
483 strm << "logic does not support theory " << m.get_family_name(fid);
484 fail(strm.str());
485 }
486 }
487
operator ()check_logic::imp488 void operator()(quantifier * n) {
489 if (!m_quantifiers)
490 fail("logic does not support quantifiers");
491 }
492
operator ()check_logic::imp493 bool operator()(expr * n) {
494 if (m_unknown_logic)
495 return true;
496 try {
497 quick_for_each_expr(*this, n);
498 return true;
499 }
500 catch (const failed &) {
501 return false;
502 }
503 }
504
operator ()check_logic::imp505 bool operator()(func_decl * f) {
506 if (m_unknown_logic)
507 return true;
508 try {
509 unsigned arity = f->get_arity();
510 if (arity > 0) {
511 if (!m_uf && f->get_family_id() == null_family_id)
512 fail("logic does not support uninterpreted functions");
513 for (unsigned i = 0; i < arity; i++)
514 check_sort(f->get_domain(i));
515 }
516 check_sort(f->get_range());
517 return true;
518 }
519 catch (const failed &) {
520 return false;
521 }
522 }
523 };
524
check_logic()525 check_logic::check_logic() {
526 m_imp = nullptr;
527 }
528
~check_logic()529 check_logic::~check_logic() {
530 if (m_imp)
531 dealloc(m_imp);
532 }
533
reset()534 void check_logic::reset() {
535 if (m_imp)
536 dealloc(m_imp);
537 m_imp = nullptr;
538 }
539
set_logic(ast_manager & m,symbol const & logic)540 void check_logic::set_logic(ast_manager & m, symbol const & logic) {
541 reset();
542 m_imp = alloc(imp, m);
543 m_imp->set_logic(logic);
544 }
545
operator ()(expr * n)546 bool check_logic::operator()(expr * n) {
547 if (m_imp)
548 return m_imp->operator()(n);
549 return true;
550 }
551
operator ()(func_decl * f)552 bool check_logic::operator()(func_decl * f) {
553 if (m_imp)
554 return m_imp->operator()(f);
555 return true;
556 }
557
get_last_error() const558 char const * check_logic::get_last_error() const {
559 if (m_imp)
560 return m_imp->m_last_error.c_str();
561 return "";
562 }
563