cprover
Loading...
Searching...
No Matches
convert_expr_to_smt.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
4
8#include <util/arith_tools.h>
10#include <util/byte_operators.h>
11#include <util/expr.h>
12#include <util/expr_cast.h>
13#include <util/floatbv_expr.h>
15#include <util/pointer_expr.h>
17#include <util/range.h>
18#include <util/std_expr.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
47static 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
73static 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
80static 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
112static 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
127static 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
134static 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
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
179static 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
186static 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
205template <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
222static smt_termt convert_expr_to_smt(const and_exprt &and_expression)
223{
225 and_expression, smt_core_theoryt::make_and);
226}
227
228static smt_termt convert_expr_to_smt(const or_exprt &or_expression)
229{
231 or_expression, smt_core_theoryt::make_or);
232}
233
234static 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
246static smt_termt convert_expr_to_smt(const not_exprt &logical_not)
247{
249}
250
252{
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
270static smt_termt
272{
274 "Generation of SMT formula for floating point not equal expression: " +
275 float_not_equal.pretty());
276}
277
278template <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 {
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 {
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
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
411static 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
444static smt_termt
446{
448 "Generation of SMT formula for euclidean modulo expression: " +
449 euclidean_modulo.pretty());
450}
451
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
485static 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
518static 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
525static smt_termt
527{
529 "Generation of SMT formula for is dynamic object expression: " +
530 is_dynamic_object.pretty());
531}
532
533static smt_termt
535{
537 "Generation of SMT formula for is invalid pointer expression: " +
538 is_invalid_pointer.pretty());
539}
540
541static 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
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
583static 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
590static 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
597static 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
604static 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
611static 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
618static 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
650{
652 "Generation of SMT formula for byte swap expression: " +
653 byte_swap.pretty());
654}
655
656static 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
663static smt_termt
665{
667 "Generation of SMT formula for count leading zeros expression: " +
668 count_leading_zeros.pretty());
669}
670
671static 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 {
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 & lhs()
Definition: std_expr.h:580
exprt & rhs()
Definition: std_expr.h:590
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
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 & cond()
Definition: std_expr.h:2243
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
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 optionalt< smt_termt > try_relational_conversion(const exprt &expr)
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 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)