cprover
convert_expr_to_smt.cpp
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
4 
8 #include <util/arith_tools.h>
9 #include <util/bitvector_expr.h>
10 #include <util/byte_operators.h>
11 #include <util/expr.h>
12 #include <util/expr_cast.h>
13 #include <util/floatbv_expr.h>
14 #include <util/mathematical_expr.h>
15 #include <util/pointer_expr.h>
17 #include <util/range.h>
18 #include <util/std_expr.h>
19 #include <util/string_constant.h>
20 
21 #include <functional>
22 #include <numeric>
23 
25 {
26  return smt_bool_sortt{};
27 }
28 
30 {
31  return smt_bit_vector_sortt{type.get_width()};
32 }
33 
35 {
36  if(const auto bool_type = type_try_dynamic_cast<bool_typet>(type))
37  {
38  return convert_type_to_smt_sort(*bool_type);
39  }
40  if(const auto bitvector_type = type_try_dynamic_cast<bitvector_typet>(type))
41  {
42  return convert_type_to_smt_sort(*bitvector_type);
43  }
44  UNIMPLEMENTED_FEATURE("Generation of SMT formula for type: " + type.pretty());
45 }
46 
47 static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
48 {
50  "Generation of SMT formula for symbol expression: " + symbol_expr.pretty());
51 }
52 
54 {
56  "Generation of SMT formula for nondet symbol expression: " +
57  nondet_symbol.pretty());
58 }
59 
61 {
63  "Generation of SMT formula for type cast expression: " + cast.pretty());
64 }
65 
67 {
69  "Generation of SMT formula for floating point type cast expression: " +
70  float_cast.pretty());
71 }
72 
73 static smt_termt convert_expr_to_smt(const struct_exprt &struct_construction)
74 {
76  "Generation of SMT formula for struct construction expression: " +
77  struct_construction.pretty());
78 }
79 
80 static smt_termt convert_expr_to_smt(const union_exprt &union_construction)
81 {
83  "Generation of SMT formula for union construction expression: " +
84  union_construction.pretty());
85 }
86 
88 {
91 
93  : member_input{input}
94  {
95  }
96 
97  void visit(const smt_bool_sortt &) override
98  {
100  }
101 
102  void visit(const smt_bit_vector_sortt &bit_vector_sort) override
103  {
104  const auto &width = bit_vector_sort.bit_width();
105  // We get the value using a non-signed interpretation, as smt bit vector
106  // terms do not carry signedness.
107  const auto value = bvrep2integer(member_input.get_value(), width, false);
108  result = smt_bit_vector_constant_termt{value, bit_vector_sort};
109  }
110 };
111 
112 static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal)
113 {
114  const auto sort = convert_type_to_smt_sort(constant_literal.type());
115  sort_based_literal_convertert converter(constant_literal);
116  sort.accept(converter);
117  return *converter.result;
118 }
119 
121 {
123  "Generation of SMT formula for concatenation expression: " +
124  concatenation.pretty());
125 }
126 
127 static smt_termt convert_expr_to_smt(const bitand_exprt &bitwise_and_expr)
128 {
130  "Generation of SMT formula for bitwise and expression: " +
131  bitwise_and_expr.pretty());
132 }
133 
134 static smt_termt convert_expr_to_smt(const bitor_exprt &bitwise_or_expr)
135 {
137  "Generation of SMT formula for bitwise or expression: " +
138  bitwise_or_expr.pretty());
139 }
140 
142 {
144  "Generation of SMT formula for bitwise xor expression: " +
145  bitwise_xor.pretty());
146 }
147 
148 static smt_termt convert_expr_to_smt(const bitnot_exprt &bitwise_not)
149 {
151  "Generation of SMT formula for bitwise not expression: " +
152  bitwise_not.pretty());
153 }
154 
156 {
158  "Generation of SMT formula for unary minus expression: " +
159  unary_minus.pretty());
160 }
161 
163 {
165  "Generation of SMT formula for unary plus expression: " +
166  unary_plus.pretty());
167 }
168 
169 static smt_termt convert_expr_to_smt(const sign_exprt &is_negative)
170 {
172  "Generation of SMT formula for \"is negative\" expression: " +
173  is_negative.pretty());
174 }
175 
176 static smt_termt convert_expr_to_smt(const if_exprt &if_expression)
177 {
179  convert_expr_to_smt(if_expression.cond()),
180  convert_expr_to_smt(if_expression.true_case()),
181  convert_expr_to_smt(if_expression.false_case()));
182 }
183 
195 template <typename factoryt>
197  const multi_ary_exprt &expr,
198  const factoryt &factory)
199 {
200  PRECONDITION(expr.operands().size() >= 2);
201  const auto operand_terms =
202  make_range(expr.operands()).map([](const exprt &expr) {
203  return convert_expr_to_smt(expr);
204  });
205  return std::accumulate(
206  ++operand_terms.begin(),
207  operand_terms.end(),
208  *operand_terms.begin(),
209  factory);
210 }
211 
212 static smt_termt convert_expr_to_smt(const and_exprt &and_expression)
213 {
215  and_expression, smt_core_theoryt::make_and);
216 }
217 
218 static smt_termt convert_expr_to_smt(const or_exprt &or_expression)
219 {
221  or_expression, smt_core_theoryt::make_or);
222 }
223 
224 static smt_termt convert_expr_to_smt(const xor_exprt &xor_expression)
225 {
227  xor_expression, smt_core_theoryt::make_xor);
228 }
229 
231 {
233  convert_expr_to_smt(implies.op0()), convert_expr_to_smt(implies.op1()));
234 }
235 
236 static smt_termt convert_expr_to_smt(const not_exprt &logical_not)
237 {
238  return smt_core_theoryt::make_not(convert_expr_to_smt(logical_not.op()));
239 }
240 
242 {
244  convert_expr_to_smt(equal.op0()), convert_expr_to_smt(equal.op1()));
245 }
246 
248 {
250  convert_expr_to_smt(not_equal.op0()), convert_expr_to_smt(not_equal.op1()));
251 }
252 
254 {
256  "Generation of SMT formula for floating point equality expression: " +
257  float_equal.pretty());
258 }
259 
260 static smt_termt
262 {
264  "Generation of SMT formula for floating point not equal expression: " +
265  float_not_equal.pretty());
266 }
267 
268 template <typename unsigned_factory_typet, typename signed_factory_typet>
270  const binary_relation_exprt &binary_relation,
271  const unsigned_factory_typet &unsigned_factory,
272  const signed_factory_typet &signed_factory)
273 {
274  PRECONDITION(binary_relation.lhs().type() == binary_relation.rhs().type());
275  const auto lhs = convert_expr_to_smt(binary_relation.lhs());
276  const auto rhs = convert_expr_to_smt(binary_relation.rhs());
277  const typet operand_type = binary_relation.lhs().type();
278  if(lhs.get_sort().cast<smt_bit_vector_sortt>())
279  {
280  if(can_cast_type<unsignedbv_typet>(operand_type))
281  return unsigned_factory(lhs, rhs);
282  if(can_cast_type<signedbv_typet>(operand_type))
283  return signed_factory(lhs, rhs);
284  }
286  "Generation of SMT formula for relational expression: " +
287  binary_relation.pretty());
288 }
289 
290 static smt_termt
292 {
293  if(can_cast_expr<greater_than_exprt>(binary_relation))
294  {
296  binary_relation,
297  smt_bit_vector_theoryt::unsigned_greater_than,
298  smt_bit_vector_theoryt::signed_greater_than);
299  }
300  if(can_cast_expr<greater_than_or_equal_exprt>(binary_relation))
301  {
303  binary_relation,
304  smt_bit_vector_theoryt::unsigned_greater_than_or_equal,
305  smt_bit_vector_theoryt::signed_greater_than_or_equal);
306  }
307  if(can_cast_expr<less_than_exprt>(binary_relation))
308  {
310  binary_relation,
311  smt_bit_vector_theoryt::unsigned_less_than,
312  smt_bit_vector_theoryt::signed_less_than);
313  }
314  if(can_cast_expr<less_than_or_equal_exprt>(binary_relation))
315  {
317  binary_relation,
318  smt_bit_vector_theoryt::unsigned_less_than_or_equal,
319  smt_bit_vector_theoryt::signed_less_than_or_equal);
320  }
322  "Generation of SMT formula for binary relation expression: " +
323  binary_relation.pretty());
324 }
325 
327 {
329  "Generation of SMT formula for plus expression: " + plus.pretty());
330 }
331 
333 {
335  "Generation of SMT formula for minus expression: " + minus.pretty());
336 }
337 
339 {
341  "Generation of SMT formula for divide expression: " + divide.pretty());
342 }
343 
344 static smt_termt convert_expr_to_smt(const ieee_float_op_exprt &float_operation)
345 {
346  // This case includes the floating point plus, minus, division and
347  // multiplication operations.
349  "Generation of SMT formula for floating point operation expression: " +
350  float_operation.pretty());
351 }
352 
353 static smt_termt convert_expr_to_smt(const mod_exprt &truncation_modulo)
354 {
356  "Generation of SMT formula for truncation modulo expression: " +
357  truncation_modulo.pretty());
358 }
359 
360 static smt_termt
361 convert_expr_to_smt(const euclidean_mod_exprt &euclidean_modulo)
362 {
364  "Generation of SMT formula for euclidean modulo expression: " +
365  euclidean_modulo.pretty());
366 }
367 
368 static smt_termt convert_expr_to_smt(const mult_exprt &multiply)
369 {
371  "Generation of SMT formula for multiply expression: " + multiply.pretty());
372 }
373 
375 {
377  "Generation of SMT formula for address of expression: " +
378  address_of.pretty());
379 }
380 
382 {
384  "Generation of SMT formula for array of expression: " + array_of.pretty());
385 }
386 
387 static smt_termt
389 {
391  "Generation of SMT formula for array comprehension expression: " +
392  array_comprehension.pretty());
393 }
394 
396 {
398  "Generation of SMT formula for index expression: " + index.pretty());
399 }
400 
402 {
403  // TODO: split into functions for separate types of shift including rotate.
405  "Generation of SMT formula for shift expression: " + shift.pretty());
406 }
407 
409 {
411  "Generation of SMT formula for with expression: " + with.pretty());
412 }
413 
415 {
417  "Generation of SMT formula for update expression: " + update.pretty());
418 }
419 
420 static smt_termt convert_expr_to_smt(const member_exprt &member_extraction)
421 {
423  "Generation of SMT formula for member extraction expression: " +
424  member_extraction.pretty());
425 }
426 
427 static smt_termt
429 {
431  "Generation of SMT formula for is dynamic object expression: " +
432  is_dynamic_object.pretty());
433 }
434 
435 static smt_termt
437 {
439  "Generation of SMT formula for is invalid pointer expression: " +
440  is_invalid_pointer.pretty());
441 }
442 
443 static smt_termt convert_expr_to_smt(const string_constantt &is_invalid_pointer)
444 {
446  "Generation of SMT formula for is invalid pointer expression: " +
447  is_invalid_pointer.pretty());
448 }
449 
451 {
453  "Generation of SMT formula for extract bit expression: " +
454  extract_bit.pretty());
455 }
456 
458 {
460  "Generation of SMT formula for extract bits expression: " +
461  extract_bits.pretty());
462 }
463 
465 {
467  "Generation of SMT formula for bit vector replication expression: " +
468  replication.pretty());
469 }
470 
471 static smt_termt convert_expr_to_smt(const byte_extract_exprt &byte_extraction)
472 {
474  "Generation of SMT formula for byte extract expression: " +
475  byte_extraction.pretty());
476 }
477 
479 {
481  "Generation of SMT formula for byte update expression: " +
482  byte_update.pretty());
483 }
484 
485 static smt_termt convert_expr_to_smt(const abs_exprt &absolute_value_of)
486 {
488  "Generation of SMT formula for absolute value of expression: " +
489  absolute_value_of.pretty());
490 }
491 
492 static smt_termt convert_expr_to_smt(const isnan_exprt &is_nan_expr)
493 {
495  "Generation of SMT formula for is not a number expression: " +
496  is_nan_expr.pretty());
497 }
498 
499 static smt_termt convert_expr_to_smt(const isfinite_exprt &is_finite_expr)
500 {
502  "Generation of SMT formula for is finite expression: " +
503  is_finite_expr.pretty());
504 }
505 
506 static smt_termt convert_expr_to_smt(const isinf_exprt &is_infinite_expr)
507 {
509  "Generation of SMT formula for is infinite expression: " +
510  is_infinite_expr.pretty());
511 }
512 
513 static smt_termt convert_expr_to_smt(const isnormal_exprt &is_normal_expr)
514 {
516  "Generation of SMT formula for is infinite expression: " +
517  is_normal_expr.pretty());
518 }
519 
520 static smt_termt convert_expr_to_smt(const array_exprt &array_construction)
521 {
523  "Generation of SMT formula for array construction expression: " +
524  array_construction.pretty());
525 }
526 
528 {
530  "Generation of SMT formula for literal expression: " + literal.pretty());
531 }
532 
534 {
536  "Generation of SMT formula for for all expression: " + for_all.pretty());
537 }
538 
540 {
542  "Generation of SMT formula for exists expression: " + exists.pretty());
543 }
544 
546 {
548  "Generation of SMT formula for vector expression: " + vector.pretty());
549 }
550 
551 static smt_termt convert_expr_to_smt(const bswap_exprt &byte_swap)
552 {
554  "Generation of SMT formula for byte swap expression: " +
555  byte_swap.pretty());
556 }
557 
558 static smt_termt convert_expr_to_smt(const popcount_exprt &population_count)
559 {
561  "Generation of SMT formula for population count expression: " +
562  population_count.pretty());
563 }
564 
565 static smt_termt
567 {
569  "Generation of SMT formula for count leading zeros expression: " +
570  count_leading_zeros.pretty());
571 }
572 
573 static smt_termt
575 {
577  "Generation of SMT formula for byte swap expression: " +
578  count_trailing_zeros.pretty());
579 }
580 
582 {
583  if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
584  {
585  return convert_expr_to_smt(*symbol);
586  }
587  if(const auto nondet = expr_try_dynamic_cast<nondet_symbol_exprt>(expr))
588  {
589  return convert_expr_to_smt(*nondet);
590  }
591  if(const auto cast = expr_try_dynamic_cast<typecast_exprt>(expr))
592  {
593  return convert_expr_to_smt(*cast);
594  }
595  if(
596  const auto float_cast = expr_try_dynamic_cast<floatbv_typecast_exprt>(expr))
597  {
598  return convert_expr_to_smt(*float_cast);
599  }
600  if(const auto struct_construction = expr_try_dynamic_cast<struct_exprt>(expr))
601  {
602  return convert_expr_to_smt(*struct_construction);
603  }
604  if(const auto union_construction = expr_try_dynamic_cast<union_exprt>(expr))
605  {
606  return convert_expr_to_smt(*union_construction);
607  }
608  if(const auto constant_literal = expr_try_dynamic_cast<constant_exprt>(expr))
609  {
610  return convert_expr_to_smt(*constant_literal);
611  }
612  if(
613  const auto concatenation = expr_try_dynamic_cast<concatenation_exprt>(expr))
614  {
615  return convert_expr_to_smt(*concatenation);
616  }
617  if(const auto bitwise_and_expr = expr_try_dynamic_cast<bitand_exprt>(expr))
618  {
619  return convert_expr_to_smt(*bitwise_and_expr);
620  }
621  if(const auto bitwise_or_expr = expr_try_dynamic_cast<bitor_exprt>(expr))
622  {
623  return convert_expr_to_smt(*bitwise_or_expr);
624  }
625  if(const auto bitwise_xor = expr_try_dynamic_cast<bitxor_exprt>(expr))
626  {
628  }
629  if(const auto bitwise_not = expr_try_dynamic_cast<bitnot_exprt>(expr))
630  {
631  return convert_expr_to_smt(*bitwise_not);
632  }
633  if(const auto unary_minus = expr_try_dynamic_cast<unary_minus_exprt>(expr))
634  {
635  return convert_expr_to_smt(*unary_minus);
636  }
637  if(const auto unary_plus = expr_try_dynamic_cast<unary_plus_exprt>(expr))
638  {
639  return convert_expr_to_smt(*unary_plus);
640  }
641  if(const auto is_negative = expr_try_dynamic_cast<sign_exprt>(expr))
642  {
643  return convert_expr_to_smt(*is_negative);
644  }
645  if(const auto if_expression = expr_try_dynamic_cast<if_exprt>(expr))
646  {
647  return convert_expr_to_smt(*if_expression);
648  }
649  if(const auto and_expression = expr_try_dynamic_cast<and_exprt>(expr))
650  {
651  return convert_expr_to_smt(*and_expression);
652  }
653  if(const auto or_expression = expr_try_dynamic_cast<or_exprt>(expr))
654  {
655  return convert_expr_to_smt(*or_expression);
656  }
657  if(const auto xor_expression = expr_try_dynamic_cast<xor_exprt>(expr))
658  {
659  return convert_expr_to_smt(*xor_expression);
660  }
661  if(const auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
662  {
663  return convert_expr_to_smt(*implies);
664  }
665  if(const auto logical_not = expr_try_dynamic_cast<not_exprt>(expr))
666  {
667  return convert_expr_to_smt(*logical_not);
668  }
669  if(const auto equal = expr_try_dynamic_cast<equal_exprt>(expr))
670  {
671  return convert_expr_to_smt(*equal);
672  }
673  if(const auto not_equal = expr_try_dynamic_cast<notequal_exprt>(expr))
674  {
675  return convert_expr_to_smt(*not_equal);
676  }
677  if(
678  const auto float_equal =
679  expr_try_dynamic_cast<ieee_float_equal_exprt>(expr))
680  {
681  return convert_expr_to_smt(*float_equal);
682  }
683  if(
684  const auto float_not_equal =
685  expr_try_dynamic_cast<ieee_float_notequal_exprt>(expr))
686  {
687  return convert_expr_to_smt(*float_not_equal);
688  }
689  if(
690  const auto binary_relation =
691  expr_try_dynamic_cast<binary_relation_exprt>(expr))
692  {
693  return convert_expr_to_smt(*binary_relation);
694  }
695  if(const auto plus = expr_try_dynamic_cast<plus_exprt>(expr))
696  {
697  return convert_expr_to_smt(*plus);
698  }
699  if(const auto minus = expr_try_dynamic_cast<minus_exprt>(expr))
700  {
701  return convert_expr_to_smt(*minus);
702  }
703  if(const auto divide = expr_try_dynamic_cast<div_exprt>(expr))
704  {
705  return convert_expr_to_smt(*divide);
706  }
707  if(
708  const auto float_operation =
709  expr_try_dynamic_cast<ieee_float_op_exprt>(expr))
710  {
711  return convert_expr_to_smt(*float_operation);
712  }
713  if(const auto truncation_modulo = expr_try_dynamic_cast<mod_exprt>(expr))
714  {
715  return convert_expr_to_smt(*truncation_modulo);
716  }
717  if(
718  const auto euclidean_modulo =
719  expr_try_dynamic_cast<euclidean_mod_exprt>(expr))
720  {
721  return convert_expr_to_smt(*euclidean_modulo);
722  }
723  if(const auto multiply = expr_try_dynamic_cast<mult_exprt>(expr))
724  {
725  return convert_expr_to_smt(*multiply);
726  }
727 #if 0
728  else if(expr.id() == ID_floatbv_rem)
729  {
730  convert_floatbv_rem(to_binary_expr(expr));
731  }
732 #endif
733  if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
734  {
735  return convert_expr_to_smt(*address_of);
736  }
737  if(const auto array_of = expr_try_dynamic_cast<array_of_exprt>(expr))
738  {
739  return convert_expr_to_smt(*array_of);
740  }
741  if(
742  const auto array_comprehension =
743  expr_try_dynamic_cast<array_comprehension_exprt>(expr))
744  {
745  return convert_expr_to_smt(*array_comprehension);
746  }
747  if(const auto index = expr_try_dynamic_cast<index_exprt>(expr))
748  {
749  return convert_expr_to_smt(*index);
750  }
751  if(const auto shift = expr_try_dynamic_cast<shift_exprt>(expr))
752  {
753  return convert_expr_to_smt(*shift);
754  }
755  if(const auto with = expr_try_dynamic_cast<with_exprt>(expr))
756  {
757  return convert_expr_to_smt(*with);
758  }
759  if(const auto update = expr_try_dynamic_cast<update_exprt>(expr))
760  {
761  return convert_expr_to_smt(*update);
762  }
763  if(const auto member_extraction = expr_try_dynamic_cast<member_exprt>(expr))
764  {
765  return convert_expr_to_smt(*member_extraction);
766  }
767 #if 0
768  else if(expr.id()==ID_pointer_offset)
769  {
770  }
771  else if(expr.id()==ID_pointer_object)
772  {
773  }
774 #endif
775  if(
776  const auto is_dynamic_object =
777  expr_try_dynamic_cast<is_dynamic_object_exprt>(expr))
778  {
779  return convert_expr_to_smt(*is_dynamic_object);
780  }
781  if(
782  const auto is_invalid_pointer =
783  expr_try_dynamic_cast<is_invalid_pointer_exprt>(expr))
784  {
785  return convert_expr_to_smt(*is_invalid_pointer);
786  }
787  if(const auto string_constant = expr_try_dynamic_cast<string_constantt>(expr))
788  {
789  return convert_expr_to_smt(*string_constant);
790  }
791  if(const auto extract_bit = expr_try_dynamic_cast<extractbit_exprt>(expr))
792  {
793  return convert_expr_to_smt(*extract_bit);
794  }
795  if(const auto extract_bits = expr_try_dynamic_cast<extractbits_exprt>(expr))
796  {
797  return convert_expr_to_smt(*extract_bits);
798  }
799  if(const auto replication = expr_try_dynamic_cast<replication_exprt>(expr))
800  {
801  return convert_expr_to_smt(*replication);
802  }
803  if(
804  const auto byte_extraction =
805  expr_try_dynamic_cast<byte_extract_exprt>(expr))
806  {
807  return convert_expr_to_smt(*byte_extraction);
808  }
809  if(const auto byte_update = expr_try_dynamic_cast<byte_update_exprt>(expr))
810  {
811  return convert_expr_to_smt(*byte_update);
812  }
813  if(const auto absolute_value_of = expr_try_dynamic_cast<abs_exprt>(expr))
814  {
815  return convert_expr_to_smt(*absolute_value_of);
816  }
817  if(const auto is_nan_expr = expr_try_dynamic_cast<isnan_exprt>(expr))
818  {
819  return convert_expr_to_smt(*is_nan_expr);
820  }
821  if(const auto is_finite_expr = expr_try_dynamic_cast<isfinite_exprt>(expr))
822  {
823  return convert_expr_to_smt(*is_finite_expr);
824  }
825  if(const auto is_infinite_expr = expr_try_dynamic_cast<isinf_exprt>(expr))
826  {
827  return convert_expr_to_smt(*is_infinite_expr);
828  }
829  if(const auto is_normal_expr = expr_try_dynamic_cast<isnormal_exprt>(expr))
830  {
831  return convert_expr_to_smt(*is_normal_expr);
832  }
833  if(const auto array_construction = expr_try_dynamic_cast<array_exprt>(expr))
834  {
835  return convert_expr_to_smt(*array_construction);
836  }
837  if(const auto literal = expr_try_dynamic_cast<literal_exprt>(expr))
838  {
839  return convert_expr_to_smt(*literal);
840  }
841  if(const auto for_all = expr_try_dynamic_cast<forall_exprt>(expr))
842  {
843  return convert_expr_to_smt(*for_all);
844  }
845  if(const auto exists = expr_try_dynamic_cast<exists_exprt>(expr))
846  {
847  return convert_expr_to_smt(*exists);
848  }
849  if(const auto vector = expr_try_dynamic_cast<vector_exprt>(expr))
850  {
851  return convert_expr_to_smt(*vector);
852  }
853 #if 0
854  else if(expr.id()==ID_object_size)
855  {
856  out << "|" << object_sizes[expr] << "|";
857  }
858 #endif
859  if(const auto let = expr_try_dynamic_cast<let_exprt>(expr))
860  {
861  return convert_expr_to_smt(*let);
862  }
863  INVARIANT(
864  expr.id() != ID_constraint_select_one,
865  "constraint_select_one is not expected in smt conversion: " +
866  expr.pretty());
867  if(const auto byte_swap = expr_try_dynamic_cast<bswap_exprt>(expr))
868  {
869  return convert_expr_to_smt(*byte_swap);
870  }
871  if(const auto population_count = expr_try_dynamic_cast<popcount_exprt>(expr))
872  {
873  return convert_expr_to_smt(*population_count);
874  }
875  if(
876  const auto count_leading_zeros =
877  expr_try_dynamic_cast<count_leading_zeros_exprt>(expr))
878  {
879  return convert_expr_to_smt(*count_leading_zeros);
880  }
881  if(
882  const auto count_trailing_zeros =
883  expr_try_dynamic_cast<count_trailing_zeros_exprt>(expr))
884  {
885  return convert_expr_to_smt(*count_trailing_zeros);
886  }
887 
889  "Generation of SMT formula for unknown kind of expression: " +
890  expr.pretty());
891 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
exists
mini_bddt exists(const mini_bddt &u, const unsigned var)
Definition: miniBDD.cpp:556
sort_based_literal_convertert
Definition: convert_expr_to_smt.cpp:88
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:590
byte_update_exprt
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Definition: byte_operators.h:78
count_trailing_zeros_exprt
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
Definition: bitvector_expr.h:924
arith_tools.h
nondet_symbol_exprt
Expression to hold a nondeterministic choice.
Definition: std_expr.h:209
UNIMPLEMENTED_FEATURE
#define UNIMPLEMENTED_FEATURE(FEATURE)
Definition: invariant.h:517
forall_exprt
A forall expression.
Definition: mathematical_expr.h:333
can_cast_expr< greater_than_or_equal_exprt >
bool can_cast_expr< greater_than_or_equal_exprt >(const exprt &base)
Definition: std_expr.h:749
typet
The type of an expression, extends irept.
Definition: type.h:28
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
smt_core_theoryt::distinct
static const smt_function_application_termt::factoryt< distinctt > distinct
Definition: smt_core_theory.h:65
smt_bit_vector_theory.h
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2172
convert_expr_to_smt
static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
Definition: convert_expr_to_smt.cpp:47
is_dynamic_object_exprt
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: pointer_expr.h:301
pointer_predicates.h
Various predicates over pointers in programs.
smt_termt
Definition: smt_terms.h:16
xor_exprt
Boolean XOR.
Definition: std_expr.h:2091
smt_core_theoryt::make_or
static const smt_function_application_termt::factoryt< ort > make_or
Definition: smt_core_theory.h:41
and_exprt
Boolean AND.
Definition: std_expr.h:1920
exists_exprt
An exists expression.
Definition: mathematical_expr.h:370
union_exprt
Union constructor from single element.
Definition: std_expr.h:1602
smt_core_theory.h
smt_core_theoryt::make_xor
static const smt_function_application_termt::factoryt< xort > make_xor
Definition: smt_core_theory.h:49
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:914
string_constant.h
smt_bit_vector_sortt
Definition: smt_sorts.h:84
exprt
Base class for all expressions.
Definition: expr.h:54
smt_core_theoryt::make_not
static const smt_function_application_termt::factoryt< nott > make_not
Definition: smt_core_theory.h:17
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:580
sign_exprt
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:506
can_cast_type< signedbv_typet >
bool can_cast_type< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
Definition: bitvector_types.h:228
bool_typet
The Boolean type.
Definition: std_types.h:36
concatenation_exprt
Concatenation of bit-vector operands.
Definition: bitvector_expr.h:590
vector_exprt
Vector constructor from list of elements.
Definition: std_expr.h:1566
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
div_exprt
Division.
Definition: std_expr.h:1064
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
string_constantt
Definition: string_constant.h:15
equal_exprt
Equality.
Definition: std_expr.h:1225
sort_based_literal_convertert::result
optionalt< smt_termt > result
Definition: convert_expr_to_smt.cpp:90
smt_core_theoryt::implies
static const smt_function_application_termt::factoryt< impliest > implies
Definition: smt_core_theory.h:25
replication_exprt
Bit-vector replication.
Definition: bitvector_expr.h:518
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2209
isfinite_exprt
Evaluates to true if the operand is finite.
Definition: floatbv_expr.h:176
notequal_exprt
Disequality.
Definition: std_expr.h:1283
smt_bit_vector_sortt::bit_width
std::size_t bit_width() const
Definition: smt_sorts.cpp:60
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
expr.h
euclidean_mod_exprt
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition: std_expr.h:1179
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1668
ieee_float_notequal_exprt
IEEE floating-point disequality.
Definition: floatbv_expr.h:312
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
byte_operators.h
Expression classes for byte-level operators.
bitxor_exprt
Bit-wise XOR.
Definition: bitvector_expr.h:160
bitor_exprt
Bit-wise OR.
Definition: bitvector_expr.h:125
or_exprt
Boolean OR.
Definition: std_expr.h:2028
convert_relational_to_smt
static smt_termt convert_relational_to_smt(const binary_relation_exprt &binary_relation, const unsigned_factory_typet &unsigned_factory, const signed_factory_typet &signed_factory)
Definition: convert_expr_to_smt.cpp:269
floatbv_typecast_exprt
Semantic type conversion from/to floating-point formats.
Definition: floatbv_expr.h:19
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
smt_sortt
Definition: smt_sorts.h:18
literal_exprt
Definition: literal_expr.h:18
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1402
smt_bool_sortt
Definition: smt_sorts.h:78
smt_sort_const_downcast_visitort
Definition: smt_sorts.h:91
pointer_expr.h
API to expression classes for Pointers.
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
sort_based_literal_convertert::visit
void visit(const smt_bool_sortt &) override
Definition: convert_expr_to_smt.cpp:97
smt_core_theoryt::if_then_else
static const smt_function_application_termt::factoryt< if_then_elset > if_then_else
Definition: smt_core_theory.h:80
can_cast_expr< less_than_or_equal_exprt >
bool can_cast_expr< less_than_or_equal_exprt >(const exprt &base)
Definition: std_expr.h:791
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:390
irept::id
const irep_idt & id() const
Definition: irep.h:407
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
convert_multiary_operator_to_terms
static smt_termt convert_multiary_operator_to_terms(const multi_ary_exprt &expr, const factoryt &factory)
Converts operator expressions with 2 or more operands to terms expressed as binary operator applicati...
Definition: convert_expr_to_smt.cpp:196
abs_exprt
Absolute value.
Definition: std_expr.h:346
floatbv_expr.h
API to expression classes for floating-point arithmetic.
unary_plus_exprt
The unary plus expression.
Definition: std_expr.h:439
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
bitand_exprt
Bit-wise AND.
Definition: bitvector_expr.h:195
can_cast_expr< less_than_exprt >
bool can_cast_expr< less_than_exprt >(const exprt &base)
Definition: std_expr.h:770
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
minus_exprt
Binary minus.
Definition: std_expr.h:973
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2442
smt_core_theoryt::make_and
static const smt_function_application_termt::factoryt< andt > make_and
Definition: smt_core_theory.h:33
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:843
bitnot_exprt
Bit-wise negation of bit-vectors.
Definition: bitvector_expr.h:82
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: bitvector_expr.h:363
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2613
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:401
bitwise_xor
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
bitwise 'xor' of two nonnegative integers
Definition: mp_arith.cpp:239
shift_exprt
A base class for shift and rotate operators.
Definition: bitvector_expr.h:230
can_cast_type< unsignedbv_typet >
bool can_cast_type< unsignedbv_typet >(const typet &type)
Check whether a reference to a typet is a unsignedbv_typet.
Definition: bitvector_types.h:178
sort_based_literal_convertert::member_input
const constant_exprt & member_input
Definition: convert_expr_to_smt.cpp:89
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2199
bitvector_typet
Base class of fixed-width bit-vector types.
Definition: std_types.h:832
isinf_exprt
Evaluates to true if the operand is infinite.
Definition: floatbv_expr.h:132
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2189
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
expr_cast.h
Templated functions to cast to specific exprt-derived classes.
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
smt_bool_literal_termt
Definition: smt_terms.h:72
sort_based_literal_convertert::visit
void visit(const smt_bit_vector_sortt &bit_vector_sort) override
Definition: convert_expr_to_smt.cpp:102
smt_core_theoryt::equal
static const smt_function_application_termt::factoryt< equalt > equal
Definition: smt_core_theory.h:57
ieee_float_op_exprt
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: floatbv_expr.h:364
bswap_exprt
The byte swap expression.
Definition: bitvector_expr.h:19
implies_exprt
Boolean implication.
Definition: std_expr.h:1983
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: bitvector_expr.h:430
exprt::operands
operandst & operands()
Definition: expr.h:92
index_exprt
Array index operator.
Definition: std_expr.h:1328
is_invalid_pointer_exprt
Definition: pointer_predicates.h:54
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition: bitvector_expr.h:633
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
smt_bit_vector_constant_termt
Definition: smt_terms.h:99
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3128
constant_exprt
A constant literal expression.
Definition: std_expr.h:2753
ieee_float_equal_exprt
IEEE-floating-point equality.
Definition: floatbv_expr.h:264
binary_exprt::op1
exprt & op1()
Definition: expr.h:102
can_cast_expr< greater_than_exprt >
bool can_cast_expr< greater_than_exprt >(const exprt &base)
Definition: std_expr.h:728
std_expr.h
API to expression classes.
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2761
sort_based_literal_convertert::sort_based_literal_convertert
sort_based_literal_convertert(const constant_exprt &input)
Definition: convert_expr_to_smt.cpp:92
convert_type_to_smt_sort
static smt_sortt convert_type_to_smt_sort(const bool_typet &type)
Definition: convert_expr_to_smt.cpp:24
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1467
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
isnormal_exprt
Evaluates to true if the operand is a normal number.
Definition: floatbv_expr.h:220
literal_expr.h
bitvector_expr.h
API to expression classes for bitvectors.
binary_exprt::op0
exprt & op0()
Definition: expr.h:99
mod_exprt
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
convert_expr_to_smt.h
count_leading_zeros_exprt
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
Definition: bitvector_expr.h:831
isnan_exprt
Evaluates to true if the operand is NaN.
Definition: floatbv_expr.h:88
mathematical_expr.h
API to expression classes for 'mathematical' expressions.
not_exprt
Boolean negation.
Definition: std_expr.h:2127