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 {
49  return smt_identifier_termt{symbol_expr.get_identifier(),
50  convert_type_to_smt_sort(symbol_expr.type())};
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 {
157  const bool operand_is_bitvector =
159  if(operand_is_bitvector)
160  {
162  convert_expr_to_smt(unary_minus.op()));
163  }
164  else
165  {
167  "Generation of SMT formula for unary minus expression: " +
168  unary_minus.pretty());
169  }
170 }
171 
173 {
175  "Generation of SMT formula for unary plus expression: " +
176  unary_plus.pretty());
177 }
178 
179 static smt_termt convert_expr_to_smt(const sign_exprt &is_negative)
180 {
182  "Generation of SMT formula for \"is negative\" expression: " +
183  is_negative.pretty());
184 }
185 
186 static smt_termt convert_expr_to_smt(const if_exprt &if_expression)
187 {
189  convert_expr_to_smt(if_expression.cond()),
190  convert_expr_to_smt(if_expression.true_case()),
191  convert_expr_to_smt(if_expression.false_case()));
192 }
193 
205 template <typename factoryt>
207  const multi_ary_exprt &expr,
208  const factoryt &factory)
209 {
210  PRECONDITION(expr.operands().size() >= 2);
211  const auto operand_terms =
212  make_range(expr.operands()).map([](const exprt &expr) {
213  return convert_expr_to_smt(expr);
214  });
215  return std::accumulate(
216  ++operand_terms.begin(),
217  operand_terms.end(),
218  *operand_terms.begin(),
219  factory);
220 }
221 
222 static smt_termt convert_expr_to_smt(const and_exprt &and_expression)
223 {
225  and_expression, smt_core_theoryt::make_and);
226 }
227 
228 static smt_termt convert_expr_to_smt(const or_exprt &or_expression)
229 {
231  or_expression, smt_core_theoryt::make_or);
232 }
233 
234 static smt_termt convert_expr_to_smt(const xor_exprt &xor_expression)
235 {
237  xor_expression, smt_core_theoryt::make_xor);
238 }
239 
241 {
243  convert_expr_to_smt(implies.op0()), convert_expr_to_smt(implies.op1()));
244 }
245 
246 static smt_termt convert_expr_to_smt(const not_exprt &logical_not)
247 {
248  return smt_core_theoryt::make_not(convert_expr_to_smt(logical_not.op()));
249 }
250 
252 {
254  convert_expr_to_smt(equal.op0()), convert_expr_to_smt(equal.op1()));
255 }
256 
258 {
260  convert_expr_to_smt(not_equal.op0()), convert_expr_to_smt(not_equal.op1()));
261 }
262 
264 {
266  "Generation of SMT formula for floating point equality expression: " +
267  float_equal.pretty());
268 }
269 
270 static smt_termt
272 {
274  "Generation of SMT formula for floating point not equal expression: " +
275  float_not_equal.pretty());
276 }
277 
278 template <typename unsigned_factory_typet, typename signed_factory_typet>
280  const binary_relation_exprt &binary_relation,
281  const unsigned_factory_typet &unsigned_factory,
282  const signed_factory_typet &signed_factory)
283 {
284  PRECONDITION(binary_relation.lhs().type() == binary_relation.rhs().type());
285  const auto lhs = convert_expr_to_smt(binary_relation.lhs());
286  const auto rhs = convert_expr_to_smt(binary_relation.rhs());
287  const typet operand_type = binary_relation.lhs().type();
288  if(lhs.get_sort().cast<smt_bit_vector_sortt>())
289  {
290  if(can_cast_type<unsignedbv_typet>(operand_type))
291  return unsigned_factory(lhs, rhs);
292  if(can_cast_type<signedbv_typet>(operand_type))
293  return signed_factory(lhs, rhs);
294  }
296  "Generation of SMT formula for relational expression: " +
297  binary_relation.pretty());
298 }
299 
301 {
302  if(const auto greater_than = expr_try_dynamic_cast<greater_than_exprt>(expr))
303  {
305  *greater_than,
308  }
309  if(
310  const auto greater_than_or_equal =
311  expr_try_dynamic_cast<greater_than_or_equal_exprt>(expr))
312  {
314  *greater_than_or_equal,
317  }
318  if(const auto less_than = expr_try_dynamic_cast<less_than_exprt>(expr))
319  {
321  *less_than,
324  }
325  if(
326  const auto less_than_or_equal =
327  expr_try_dynamic_cast<less_than_or_equal_exprt>(expr))
328  {
330  *less_than_or_equal,
333  }
334  return {};
335 }
336 
338 {
339  if(std::all_of(
340  plus.operands().cbegin(), plus.operands().cend(), [](exprt operand) {
341  return can_cast_type<integer_bitvector_typet>(operand.type());
342  }))
343  {
346  }
347  else
348  {
350  "Generation of SMT formula for plus expression: " + plus.pretty());
351  }
352 }
353 
355 {
356  const bool both_operands_bitvector =
359 
360  if(both_operands_bitvector)
361  {
363  convert_expr_to_smt(minus.lhs()), convert_expr_to_smt(minus.rhs()));
364  }
365  else
366  {
368  "Generation of SMT formula for minus expression: " + minus.pretty());
369  }
370 }
371 
373 {
374  const bool both_operands_bitvector =
377 
378  const bool both_operands_unsigned =
381 
382  if(both_operands_bitvector)
383  {
384  if(both_operands_unsigned)
385  {
387  convert_expr_to_smt(divide.lhs()), convert_expr_to_smt(divide.rhs()));
388  }
389  else
390  {
392  convert_expr_to_smt(divide.lhs()), convert_expr_to_smt(divide.rhs()));
393  }
394  }
395  else
396  {
398  "Generation of SMT formula for divide expression: " + divide.pretty());
399  }
400 }
401 
402 static smt_termt convert_expr_to_smt(const ieee_float_op_exprt &float_operation)
403 {
404  // This case includes the floating point plus, minus, division and
405  // multiplication operations.
407  "Generation of SMT formula for floating point operation expression: " +
408  float_operation.pretty());
409 }
410 
411 static smt_termt convert_expr_to_smt(const mod_exprt &truncation_modulo)
412 {
413  const bool both_operands_bitvector =
414  can_cast_type<integer_bitvector_typet>(truncation_modulo.lhs().type()) &&
415  can_cast_type<integer_bitvector_typet>(truncation_modulo.rhs().type());
416 
417  const bool both_operands_unsigned =
418  can_cast_type<unsignedbv_typet>(truncation_modulo.lhs().type()) &&
419  can_cast_type<unsignedbv_typet>(truncation_modulo.rhs().type());
420 
421  if(both_operands_bitvector)
422  {
423  if(both_operands_unsigned)
424  {
426  convert_expr_to_smt(truncation_modulo.lhs()),
427  convert_expr_to_smt(truncation_modulo.rhs()));
428  }
429  else
430  {
432  convert_expr_to_smt(truncation_modulo.lhs()),
433  convert_expr_to_smt(truncation_modulo.rhs()));
434  }
435  }
436  else
437  {
439  "Generation of SMT formula for remainder (modulus) expression: " +
440  truncation_modulo.pretty());
441  }
442 }
443 
444 static smt_termt
445 convert_expr_to_smt(const euclidean_mod_exprt &euclidean_modulo)
446 {
448  "Generation of SMT formula for euclidean modulo expression: " +
449  euclidean_modulo.pretty());
450 }
451 
452 static smt_termt convert_expr_to_smt(const mult_exprt &multiply)
453 {
454  if(std::all_of(
455  multiply.operands().cbegin(),
456  multiply.operands().cend(),
457  [](exprt operand) {
458  return can_cast_type<integer_bitvector_typet>(operand.type());
459  }))
460  {
463  }
464  else
465  {
467  "Generation of SMT formula for multiply expression: " +
468  multiply.pretty());
469  }
470 }
471 
473 {
475  "Generation of SMT formula for address of expression: " +
476  address_of.pretty());
477 }
478 
480 {
482  "Generation of SMT formula for array of expression: " + array_of.pretty());
483 }
484 
485 static smt_termt
487 {
489  "Generation of SMT formula for array comprehension expression: " +
490  array_comprehension.pretty());
491 }
492 
494 {
496  "Generation of SMT formula for index expression: " + index.pretty());
497 }
498 
500 {
501  // TODO: split into functions for separate types of shift including rotate.
503  "Generation of SMT formula for shift expression: " + shift.pretty());
504 }
505 
507 {
509  "Generation of SMT formula for with expression: " + with.pretty());
510 }
511 
513 {
515  "Generation of SMT formula for update expression: " + update.pretty());
516 }
517 
518 static smt_termt convert_expr_to_smt(const member_exprt &member_extraction)
519 {
521  "Generation of SMT formula for member extraction expression: " +
522  member_extraction.pretty());
523 }
524 
525 static smt_termt
527 {
529  "Generation of SMT formula for is dynamic object expression: " +
530  is_dynamic_object.pretty());
531 }
532 
533 static smt_termt
535 {
537  "Generation of SMT formula for is invalid pointer expression: " +
538  is_invalid_pointer.pretty());
539 }
540 
541 static smt_termt convert_expr_to_smt(const string_constantt &is_invalid_pointer)
542 {
544  "Generation of SMT formula for is invalid pointer expression: " +
545  is_invalid_pointer.pretty());
546 }
547 
549 {
551  "Generation of SMT formula for extract bit expression: " +
552  extract_bit.pretty());
553 }
554 
556 {
558  "Generation of SMT formula for extract bits expression: " +
559  extract_bits.pretty());
560 }
561 
563 {
565  "Generation of SMT formula for bit vector replication expression: " +
566  replication.pretty());
567 }
568 
569 static smt_termt convert_expr_to_smt(const byte_extract_exprt &byte_extraction)
570 {
572  "Generation of SMT formula for byte extract expression: " +
573  byte_extraction.pretty());
574 }
575 
577 {
579  "Generation of SMT formula for byte update expression: " +
580  byte_update.pretty());
581 }
582 
583 static smt_termt convert_expr_to_smt(const abs_exprt &absolute_value_of)
584 {
586  "Generation of SMT formula for absolute value of expression: " +
587  absolute_value_of.pretty());
588 }
589 
590 static smt_termt convert_expr_to_smt(const isnan_exprt &is_nan_expr)
591 {
593  "Generation of SMT formula for is not a number expression: " +
594  is_nan_expr.pretty());
595 }
596 
597 static smt_termt convert_expr_to_smt(const isfinite_exprt &is_finite_expr)
598 {
600  "Generation of SMT formula for is finite expression: " +
601  is_finite_expr.pretty());
602 }
603 
604 static smt_termt convert_expr_to_smt(const isinf_exprt &is_infinite_expr)
605 {
607  "Generation of SMT formula for is infinite expression: " +
608  is_infinite_expr.pretty());
609 }
610 
611 static smt_termt convert_expr_to_smt(const isnormal_exprt &is_normal_expr)
612 {
614  "Generation of SMT formula for is infinite expression: " +
615  is_normal_expr.pretty());
616 }
617 
618 static smt_termt convert_expr_to_smt(const array_exprt &array_construction)
619 {
621  "Generation of SMT formula for array construction expression: " +
622  array_construction.pretty());
623 }
624 
626 {
628  "Generation of SMT formula for literal expression: " + literal.pretty());
629 }
630 
632 {
634  "Generation of SMT formula for for all expression: " + for_all.pretty());
635 }
636 
638 {
640  "Generation of SMT formula for exists expression: " + exists.pretty());
641 }
642 
644 {
646  "Generation of SMT formula for vector expression: " + vector.pretty());
647 }
648 
649 static smt_termt convert_expr_to_smt(const bswap_exprt &byte_swap)
650 {
652  "Generation of SMT formula for byte swap expression: " +
653  byte_swap.pretty());
654 }
655 
656 static smt_termt convert_expr_to_smt(const popcount_exprt &population_count)
657 {
659  "Generation of SMT formula for population count expression: " +
660  population_count.pretty());
661 }
662 
663 static smt_termt
665 {
667  "Generation of SMT formula for count leading zeros expression: " +
668  count_leading_zeros.pretty());
669 }
670 
671 static smt_termt
673 {
675  "Generation of SMT formula for byte swap expression: " +
676  count_trailing_zeros.pretty());
677 }
678 
680 {
681  if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
682  {
683  return convert_expr_to_smt(*symbol);
684  }
685  if(const auto nondet = expr_try_dynamic_cast<nondet_symbol_exprt>(expr))
686  {
687  return convert_expr_to_smt(*nondet);
688  }
689  if(const auto cast = expr_try_dynamic_cast<typecast_exprt>(expr))
690  {
691  return convert_expr_to_smt(*cast);
692  }
693  if(
694  const auto float_cast = expr_try_dynamic_cast<floatbv_typecast_exprt>(expr))
695  {
696  return convert_expr_to_smt(*float_cast);
697  }
698  if(const auto struct_construction = expr_try_dynamic_cast<struct_exprt>(expr))
699  {
700  return convert_expr_to_smt(*struct_construction);
701  }
702  if(const auto union_construction = expr_try_dynamic_cast<union_exprt>(expr))
703  {
704  return convert_expr_to_smt(*union_construction);
705  }
706  if(const auto constant_literal = expr_try_dynamic_cast<constant_exprt>(expr))
707  {
708  return convert_expr_to_smt(*constant_literal);
709  }
710  if(
711  const auto concatenation = expr_try_dynamic_cast<concatenation_exprt>(expr))
712  {
713  return convert_expr_to_smt(*concatenation);
714  }
715  if(const auto bitwise_and_expr = expr_try_dynamic_cast<bitand_exprt>(expr))
716  {
717  return convert_expr_to_smt(*bitwise_and_expr);
718  }
719  if(const auto bitwise_or_expr = expr_try_dynamic_cast<bitor_exprt>(expr))
720  {
721  return convert_expr_to_smt(*bitwise_or_expr);
722  }
723  if(const auto bitwise_xor = expr_try_dynamic_cast<bitxor_exprt>(expr))
724  {
726  }
727  if(const auto bitwise_not = expr_try_dynamic_cast<bitnot_exprt>(expr))
728  {
729  return convert_expr_to_smt(*bitwise_not);
730  }
731  if(const auto unary_minus = expr_try_dynamic_cast<unary_minus_exprt>(expr))
732  {
733  return convert_expr_to_smt(*unary_minus);
734  }
735  if(const auto unary_plus = expr_try_dynamic_cast<unary_plus_exprt>(expr))
736  {
737  return convert_expr_to_smt(*unary_plus);
738  }
739  if(const auto is_negative = expr_try_dynamic_cast<sign_exprt>(expr))
740  {
741  return convert_expr_to_smt(*is_negative);
742  }
743  if(const auto if_expression = expr_try_dynamic_cast<if_exprt>(expr))
744  {
745  return convert_expr_to_smt(*if_expression);
746  }
747  if(const auto and_expression = expr_try_dynamic_cast<and_exprt>(expr))
748  {
749  return convert_expr_to_smt(*and_expression);
750  }
751  if(const auto or_expression = expr_try_dynamic_cast<or_exprt>(expr))
752  {
753  return convert_expr_to_smt(*or_expression);
754  }
755  if(const auto xor_expression = expr_try_dynamic_cast<xor_exprt>(expr))
756  {
757  return convert_expr_to_smt(*xor_expression);
758  }
759  if(const auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
760  {
761  return convert_expr_to_smt(*implies);
762  }
763  if(const auto logical_not = expr_try_dynamic_cast<not_exprt>(expr))
764  {
765  return convert_expr_to_smt(*logical_not);
766  }
767  if(const auto equal = expr_try_dynamic_cast<equal_exprt>(expr))
768  {
769  return convert_expr_to_smt(*equal);
770  }
771  if(const auto not_equal = expr_try_dynamic_cast<notequal_exprt>(expr))
772  {
773  return convert_expr_to_smt(*not_equal);
774  }
775  if(
776  const auto float_equal =
777  expr_try_dynamic_cast<ieee_float_equal_exprt>(expr))
778  {
779  return convert_expr_to_smt(*float_equal);
780  }
781  if(
782  const auto float_not_equal =
783  expr_try_dynamic_cast<ieee_float_notequal_exprt>(expr))
784  {
785  return convert_expr_to_smt(*float_not_equal);
786  }
787  if(const auto converted_relational = try_relational_conversion(expr))
788  {
789  return *converted_relational;
790  }
791  if(const auto plus = expr_try_dynamic_cast<plus_exprt>(expr))
792  {
793  return convert_expr_to_smt(*plus);
794  }
795  if(const auto minus = expr_try_dynamic_cast<minus_exprt>(expr))
796  {
797  return convert_expr_to_smt(*minus);
798  }
799  if(const auto divide = expr_try_dynamic_cast<div_exprt>(expr))
800  {
801  return convert_expr_to_smt(*divide);
802  }
803  if(
804  const auto float_operation =
805  expr_try_dynamic_cast<ieee_float_op_exprt>(expr))
806  {
807  return convert_expr_to_smt(*float_operation);
808  }
809  if(const auto truncation_modulo = expr_try_dynamic_cast<mod_exprt>(expr))
810  {
811  return convert_expr_to_smt(*truncation_modulo);
812  }
813  if(
814  const auto euclidean_modulo =
815  expr_try_dynamic_cast<euclidean_mod_exprt>(expr))
816  {
817  return convert_expr_to_smt(*euclidean_modulo);
818  }
819  if(const auto multiply = expr_try_dynamic_cast<mult_exprt>(expr))
820  {
821  return convert_expr_to_smt(*multiply);
822  }
823 #if 0
824  else if(expr.id() == ID_floatbv_rem)
825  {
826  convert_floatbv_rem(to_binary_expr(expr));
827  }
828 #endif
829  if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(expr))
830  {
831  return convert_expr_to_smt(*address_of);
832  }
833  if(const auto array_of = expr_try_dynamic_cast<array_of_exprt>(expr))
834  {
835  return convert_expr_to_smt(*array_of);
836  }
837  if(
838  const auto array_comprehension =
839  expr_try_dynamic_cast<array_comprehension_exprt>(expr))
840  {
841  return convert_expr_to_smt(*array_comprehension);
842  }
843  if(const auto index = expr_try_dynamic_cast<index_exprt>(expr))
844  {
845  return convert_expr_to_smt(*index);
846  }
847  if(const auto shift = expr_try_dynamic_cast<shift_exprt>(expr))
848  {
849  return convert_expr_to_smt(*shift);
850  }
851  if(const auto with = expr_try_dynamic_cast<with_exprt>(expr))
852  {
853  return convert_expr_to_smt(*with);
854  }
855  if(const auto update = expr_try_dynamic_cast<update_exprt>(expr))
856  {
857  return convert_expr_to_smt(*update);
858  }
859  if(const auto member_extraction = expr_try_dynamic_cast<member_exprt>(expr))
860  {
861  return convert_expr_to_smt(*member_extraction);
862  }
863 #if 0
864  else if(expr.id()==ID_pointer_offset)
865  {
866  }
867  else if(expr.id()==ID_pointer_object)
868  {
869  }
870 #endif
871  if(
872  const auto is_dynamic_object =
873  expr_try_dynamic_cast<is_dynamic_object_exprt>(expr))
874  {
875  return convert_expr_to_smt(*is_dynamic_object);
876  }
877  if(
878  const auto is_invalid_pointer =
879  expr_try_dynamic_cast<is_invalid_pointer_exprt>(expr))
880  {
881  return convert_expr_to_smt(*is_invalid_pointer);
882  }
883  if(const auto string_constant = expr_try_dynamic_cast<string_constantt>(expr))
884  {
885  return convert_expr_to_smt(*string_constant);
886  }
887  if(const auto extract_bit = expr_try_dynamic_cast<extractbit_exprt>(expr))
888  {
889  return convert_expr_to_smt(*extract_bit);
890  }
891  if(const auto extract_bits = expr_try_dynamic_cast<extractbits_exprt>(expr))
892  {
893  return convert_expr_to_smt(*extract_bits);
894  }
895  if(const auto replication = expr_try_dynamic_cast<replication_exprt>(expr))
896  {
897  return convert_expr_to_smt(*replication);
898  }
899  if(
900  const auto byte_extraction =
901  expr_try_dynamic_cast<byte_extract_exprt>(expr))
902  {
903  return convert_expr_to_smt(*byte_extraction);
904  }
905  if(const auto byte_update = expr_try_dynamic_cast<byte_update_exprt>(expr))
906  {
907  return convert_expr_to_smt(*byte_update);
908  }
909  if(const auto absolute_value_of = expr_try_dynamic_cast<abs_exprt>(expr))
910  {
911  return convert_expr_to_smt(*absolute_value_of);
912  }
913  if(const auto is_nan_expr = expr_try_dynamic_cast<isnan_exprt>(expr))
914  {
915  return convert_expr_to_smt(*is_nan_expr);
916  }
917  if(const auto is_finite_expr = expr_try_dynamic_cast<isfinite_exprt>(expr))
918  {
919  return convert_expr_to_smt(*is_finite_expr);
920  }
921  if(const auto is_infinite_expr = expr_try_dynamic_cast<isinf_exprt>(expr))
922  {
923  return convert_expr_to_smt(*is_infinite_expr);
924  }
925  if(const auto is_normal_expr = expr_try_dynamic_cast<isnormal_exprt>(expr))
926  {
927  return convert_expr_to_smt(*is_normal_expr);
928  }
929  if(const auto array_construction = expr_try_dynamic_cast<array_exprt>(expr))
930  {
931  return convert_expr_to_smt(*array_construction);
932  }
933  if(const auto literal = expr_try_dynamic_cast<literal_exprt>(expr))
934  {
935  return convert_expr_to_smt(*literal);
936  }
937  if(const auto for_all = expr_try_dynamic_cast<forall_exprt>(expr))
938  {
939  return convert_expr_to_smt(*for_all);
940  }
941  if(const auto exists = expr_try_dynamic_cast<exists_exprt>(expr))
942  {
943  return convert_expr_to_smt(*exists);
944  }
945  if(const auto vector = expr_try_dynamic_cast<vector_exprt>(expr))
946  {
947  return convert_expr_to_smt(*vector);
948  }
949 #if 0
950  else if(expr.id()==ID_object_size)
951  {
952  out << "|" << object_sizes[expr] << "|";
953  }
954 #endif
955  if(const auto let = expr_try_dynamic_cast<let_exprt>(expr))
956  {
957  return convert_expr_to_smt(*let);
958  }
959  INVARIANT(
960  expr.id() != ID_constraint_select_one,
961  "constraint_select_one is not expected in smt conversion: " +
962  expr.pretty());
963  if(const auto byte_swap = expr_try_dynamic_cast<bswap_exprt>(expr))
964  {
965  return convert_expr_to_smt(*byte_swap);
966  }
967  if(const auto population_count = expr_try_dynamic_cast<popcount_exprt>(expr))
968  {
969  return convert_expr_to_smt(*population_count);
970  }
971  if(
972  const auto count_leading_zeros =
973  expr_try_dynamic_cast<count_leading_zeros_exprt>(expr))
974  {
975  return convert_expr_to_smt(*count_leading_zeros);
976  }
977  if(
978  const auto count_trailing_zeros =
979  expr_try_dynamic_cast<count_trailing_zeros_exprt>(expr))
980  {
981  return convert_expr_to_smt(*count_trailing_zeros);
982  }
983 
985  "Generation of SMT formula for unknown kind of expression: " +
986  expr.pretty());
987 }
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
API to expression classes for bitvectors.
bool can_cast_type< signedbv_typet >(const typet &type)
Check whether a reference to a typet is a signedbv_typet.
bool can_cast_type< integer_bitvector_typet >(const typet &type)
Check whether a reference to a typet is an integer_bitvector_typet.
bool can_cast_type< unsignedbv_typet >(const typet &type)
Check whether a reference to a typet is a unsignedbv_typet.
Expression classes for byte-level operators.
Absolute value.
Definition: std_expr.h:346
Operator to return the address of an object.
Definition: pointer_expr.h:361
Boolean AND.
Definition: std_expr.h:1974
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3182
Array constructor from list of elements.
Definition: std_expr.h:1476
Array constructor from single element.
Definition: std_expr.h:1411
exprt & op1()
Definition: expr.h:102
exprt & lhs()
Definition: std_expr.h:580
exprt & op0()
Definition: expr.h:99
exprt & rhs()
Definition: std_expr.h:590
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
Bit-wise AND.
Bit-wise negation of bit-vectors.
Bit-wise OR.
Base class of fixed-width bit-vector types.
Definition: std_types.h:853
std::size_t get_width() const
Definition: std_types.h:864
Bit-wise XOR.
The Boolean type.
Definition: std_types.h:36
The byte swap expression.
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Concatenation of bit-vector operands.
A constant literal expression.
Definition: std_expr.h:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
Division.
Definition: std_expr.h:1064
Equality.
Definition: std_expr.h:1225
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition: std_expr.h:1179
An exists expression.
Base class for all expressions.
Definition: expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Extracts a single bit of a bit-vector operand.
Extracts a sub-range of a bit-vector operand.
Semantic type conversion from/to floating-point formats.
Definition: floatbv_expr.h:19
A forall expression.
IEEE-floating-point equality.
Definition: floatbv_expr.h:264
IEEE floating-point disequality.
Definition: floatbv_expr.h:312
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: floatbv_expr.h:364
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & true_case()
Definition: std_expr.h:2253
exprt & false_case()
Definition: std_expr.h:2263
exprt & cond()
Definition: std_expr.h:2243
Boolean implication.
Definition: std_expr.h:2037
Array index operator.
Definition: std_expr.h:1328
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irep_idt & id() const
Definition: irep.h:396
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: pointer_expr.h:321
Evaluates to true if the operand is finite.
Definition: floatbv_expr.h:176
Evaluates to true if the operand is infinite.
Definition: floatbv_expr.h:132
Evaluates to true if the operand is NaN.
Definition: floatbv_expr.h:88
Evaluates to true if the operand is a normal number.
Definition: floatbv_expr.h:220
Extract member of struct or union.
Definition: std_expr.h:2667
Binary minus.
Definition: std_expr.h:973
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
Expression to hold a nondeterministic choice.
Definition: std_expr.h:209
Boolean negation.
Definition: std_expr.h:2181
Disequality.
Definition: std_expr.h:1283
Boolean OR.
Definition: std_expr.h:2082
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The popcount (counting the number of bits set to 1) expression.
Bit-vector replication.
A base class for shift and rotate operators.
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:506
std::size_t bit_width() const
Definition: smt_sorts.cpp:60
static const smt_function_application_termt::factoryt< unsigned_less_than_or_equalt > unsigned_less_than_or_equal
static const smt_function_application_termt::factoryt< signed_less_than_or_equalt > signed_less_than_or_equal
static const smt_function_application_termt::factoryt< addt > add
static const smt_function_application_termt::factoryt< signed_greater_than_or_equalt > signed_greater_than_or_equal
static const smt_function_application_termt::factoryt< unsigned_greater_thant > unsigned_greater_than
static const smt_function_application_termt::factoryt< unsigned_remaindert > unsigned_remainder
static const smt_function_application_termt::factoryt< unsigned_greater_than_or_equalt > unsigned_greater_than_or_equal
static const smt_function_application_termt::factoryt< multiplyt > multiply
static const smt_function_application_termt::factoryt< signed_less_thant > signed_less_than
static const smt_function_application_termt::factoryt< signed_greater_thant > signed_greater_than
static const smt_function_application_termt::factoryt< negatet > negate
static const smt_function_application_termt::factoryt< unsigned_dividet > unsigned_divide
static const smt_function_application_termt::factoryt< unsigned_less_thant > unsigned_less_than
static const smt_function_application_termt::factoryt< signed_dividet > signed_divide
static const smt_function_application_termt::factoryt< signed_remaindert > signed_remainder
static const smt_function_application_termt::factoryt< subtractt > subtract
static const smt_function_application_termt::factoryt< distinctt > distinct
static const smt_function_application_termt::factoryt< if_then_elset > if_then_else
static const smt_function_application_termt::factoryt< impliest > implies
static const smt_function_application_termt::factoryt< ort > make_or
static const smt_function_application_termt::factoryt< equalt > equal
static const smt_function_application_termt::factoryt< andt > make_and
static const smt_function_application_termt::factoryt< xort > make_xor
static const smt_function_application_termt::factoryt< nott > make_not
Stores identifiers in unescaped and unquoted form.
Definition: smt_terms.h:81
Struct constructor from list of elements.
Definition: std_expr.h:1722
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
The unary minus expression.
Definition: std_expr.h:390
The unary plus expression.
Definition: std_expr.h:439
Union constructor from single element.
Definition: std_expr.h:1611
Operator to update elements in structs and arrays.
Definition: std_expr.h:2496
Vector constructor from list of elements.
Definition: std_expr.h:1575
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
Boolean XOR.
Definition: std_expr.h:2145
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)
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...
static smt_sortt convert_type_to_smt_sort(const bool_typet &type)
static optionalt< smt_termt > try_relational_conversion(const exprt &expr)
static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
Templated functions to cast to specific exprt-derived classes.
API to expression classes for floating-point arithmetic.
API to expression classes for 'mathematical' expressions.
mini_bddt exists(const mini_bddt &u, const unsigned var)
Definition: miniBDD.cpp:556
mp_integer bitwise_xor(const mp_integer &a, const mp_integer &b)
bitwise 'xor' of two nonnegative integers
Definition: mp_arith.cpp:239
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
#define UNIMPLEMENTED_FEATURE(FEATURE)
Definition: invariant.h:517
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
API to expression classes.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
binary_relation_exprt less_than(exprt lhs, exprt rhs)
Definition: string_expr.h:48
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
Definition: string_expr.h:25
void visit(const smt_bit_vector_sortt &bit_vector_sort) override
const constant_exprt & member_input
void visit(const smt_bool_sortt &) override
sort_based_literal_convertert(const constant_exprt &input)