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 }
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< 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:341
Boolean AND.
Definition: std_expr.h:1920
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3128
Array constructor from list of elements.
Definition: std_expr.h:1467
Array constructor from single element.
Definition: std_expr.h:1402
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:832
std::size_t get_width() const
Definition: std_types.h:843
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:2753
const irep_idt & get_value() const
Definition: std_expr.h:2761
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:2172
exprt & true_case()
Definition: std_expr.h:2199
exprt & false_case()
Definition: std_expr.h:2209
exprt & cond()
Definition: std_expr.h:2189
Boolean implication.
Definition: std_expr.h:1983
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:407
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: pointer_expr.h:301
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:2613
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:2127
Disequality.
Definition: std_expr.h:1283
Boolean OR.
Definition: std_expr.h:2028
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< 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
Struct constructor from list of elements.
Definition: std_expr.h:1668
Expression to hold a symbol (variable)
Definition: std_expr.h:80
Semantic type conversion.
Definition: std_expr.h:1866
The type of an expression, extends irept.
Definition: type.h:28
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:1602
Operator to update elements in structs and arrays.
Definition: std_expr.h:2442
Vector constructor from list of elements.
Definition: std_expr.h:1566
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
Boolean XOR.
Definition: std_expr.h:2091
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.
bool can_cast_expr< less_than_exprt >(const exprt &base)
Definition: std_expr.h:770
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
bool can_cast_expr< greater_than_exprt >(const exprt &base)
Definition: std_expr.h:728
bool can_cast_expr< greater_than_or_equal_exprt >(const exprt &base)
Definition: std_expr.h:749
bool can_cast_expr< less_than_or_equal_exprt >(const exprt &base)
Definition: std_expr.h:791
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)