cprover
smt2_conv.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: SMT Backend
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "smt2_conv.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/bitvector_expr.h>
16 #include <util/byte_operators.h>
17 #include <util/c_types.h>
18 #include <util/config.h>
19 #include <util/expr_iterator.h>
20 #include <util/expr_util.h>
21 #include <util/fixedbv.h>
22 #include <util/floatbv_expr.h>
23 #include <util/format_expr.h>
24 #include <util/ieee_float.h>
25 #include <util/invariant.h>
26 #include <util/mathematical_expr.h>
27 #include <util/namespace.h>
28 #include <util/pointer_expr.h>
30 #include <util/prefix.h>
31 #include <util/range.h>
32 #include <util/simplify_expr.h>
33 #include <util/std_expr.h>
34 #include <util/string2int.h>
35 #include <util/string_constant.h>
36 #include <util/threeval.h>
37 
43 
44 // Mark different kinds of error conditions
45 
46 // Unexpected types and other combinations not implemented and not
47 // expected to be needed
48 #define UNEXPECTEDCASE(S) PRECONDITION_WITH_DIAGNOSTICS(false, S);
49 
50 // General todos
51 #define SMT2_TODO(S) PRECONDITION_WITH_DIAGNOSTICS(false, "TODO: " S)
52 
54  const namespacet &_ns,
55  const std::string &_benchmark,
56  const std::string &_notes,
57  const std::string &_logic,
58  solvert _solver,
59  std::ostream &_out)
60  : use_FPA_theory(false),
61  use_array_of_bool(false),
62  use_as_const(false),
63  use_check_sat_assuming(false),
64  use_datatypes(false),
65  use_lambda_for_array(false),
66  emit_set_logic(true),
67  ns(_ns),
68  out(_out),
69  benchmark(_benchmark),
70  notes(_notes),
71  logic(_logic),
72  solver(_solver),
73  boolbv_width(_ns),
74  pointer_logic(_ns),
75  no_boolean_variables(0)
76 {
77  // We set some defaults differently
78  // for some solvers.
79 
80  switch(solver)
81  {
82  case solvert::GENERIC:
83  break;
84 
85  case solvert::BOOLECTOR:
86  break;
87 
89  use_FPA_theory = true;
90  use_array_of_bool = true;
91  use_as_const = true;
93  emit_set_logic = false;
94  break;
95 
96  case solvert::CVC3:
97  break;
98 
99  case solvert::CVC4:
100  use_array_of_bool = true;
101  use_as_const = true;
102  break;
103 
104  case solvert::MATHSAT:
105  break;
106 
107  case solvert::YICES:
108  break;
109 
110  case solvert::Z3:
111  use_array_of_bool = true;
112  use_as_const = true;
113  use_check_sat_assuming = true;
114  use_lambda_for_array = true;
115  emit_set_logic = false;
116  use_datatypes = true;
117  break;
118  }
119 
120  write_header();
121 }
122 
124 {
125  return "SMT2";
126 }
127 
128 void smt2_convt::print_assignment(std::ostream &os) const
129 {
130  // Boolean stuff
131 
132  for(std::size_t v=0; v<boolean_assignment.size(); v++)
133  os << "b" << v << "=" << boolean_assignment[v] << "\n";
134 
135  // others
136 }
137 
139 {
140  if(l.is_true())
141  return tvt(true);
142  if(l.is_false())
143  return tvt(false);
144 
145  INVARIANT(
146  l.var_no() < boolean_assignment.size(),
147  "variable number shall be within bounds");
148  return tvt(boolean_assignment[l.var_no()]^l.sign());
149 }
150 
152 {
153  out << "; SMT 2" << "\n";
154 
155  switch(solver)
156  {
157  // clang-format off
158  case solvert::GENERIC: break;
159  case solvert::BOOLECTOR: out << "; Generated for Boolector\n"; break;
161  out << "; Generated for the CPROVER SMT2 solver\n"; break;
162  case solvert::CVC3: out << "; Generated for CVC 3\n"; break;
163  case solvert::CVC4: out << "; Generated for CVC 4\n"; break;
164  case solvert::MATHSAT: out << "; Generated for MathSAT\n"; break;
165  case solvert::YICES: out << "; Generated for Yices\n"; break;
166  case solvert::Z3: out << "; Generated for Z3\n"; break;
167  // clang-format on
168  }
169 
170  out << "(set-info :source \"" << notes << "\")" << "\n";
171 
172  out << "(set-option :produce-models true)" << "\n";
173 
174  // We use a broad mixture of logics, so on some solvers
175  // its better not to declare here.
176  // set-logic should come after setting options
177  if(emit_set_logic && !logic.empty())
178  out << "(set-logic " << logic << ")" << "\n";
179 }
180 
182 {
183  out << "\n";
184 
185  // fix up the object sizes
186  for(const auto &object : object_sizes)
187  define_object_size(object.second, object.first);
188 
189  if(use_check_sat_assuming && !assumptions.empty())
190  {
191  out << "(check-sat-assuming (";
192  for(const auto &assumption : assumptions)
193  convert_literal(to_literal_expr(assumption).get_literal());
194  out << "))\n";
195  }
196  else
197  {
198  // add the assumptions, if any
199  if(!assumptions.empty())
200  {
201  out << "; assumptions\n";
202 
203  for(const auto &assumption : assumptions)
204  {
205  out << "(assert ";
206  convert_literal(to_literal_expr(assumption).get_literal());
207  out << ")"
208  << "\n";
209  }
210  }
211 
212  out << "(check-sat)\n";
213  }
214 
215  out << "\n";
216 
218  {
219  for(const auto &id : smt2_identifiers)
220  out << "(get-value (|" << id << "|))"
221  << "\n";
222  }
223 
224  out << "\n";
225 
226  out << "(exit)\n";
227 
228  out << "; end of SMT2 file"
229  << "\n";
230 }
231 
233  const irep_idt &id,
234  const exprt &expr)
235 {
236  PRECONDITION(expr.id() == ID_object_size);
237  const exprt &ptr = to_unary_expr(expr).op();
238  std::size_t size_width = boolbv_width(expr.type());
239  std::size_t pointer_width = boolbv_width(ptr.type());
240  std::size_t number = 0;
241  std::size_t h=pointer_width-1;
242  std::size_t l=pointer_width-config.bv_encoding.object_bits;
243 
244  for(const auto &o : pointer_logic.objects)
245  {
246  const typet &type = o.type();
247  auto size_expr = size_of_expr(type, ns);
248  const auto object_size =
249  numeric_cast<mp_integer>(size_expr.value_or(nil_exprt()));
250 
251  if(
252  (o.id() != ID_symbol && o.id() != ID_string_constant) ||
253  !size_expr.has_value() || !object_size.has_value())
254  {
255  ++number;
256  continue;
257  }
258 
259  out << "(assert (=> (= "
260  << "((_ extract " << h << " " << l << ") ";
261  convert_expr(ptr);
262  out << ") (_ bv" << number << " " << config.bv_encoding.object_bits << "))"
263  << "(= |" << id << "| (_ bv" << *object_size << " " << size_width
264  << "))))\n";
265 
266  ++number;
267  }
268 }
269 
271 {
272  write_footer();
273  out.flush();
275 }
276 
277 exprt smt2_convt::get(const exprt &expr) const
278 {
279  if(expr.id()==ID_symbol)
280  {
281  const irep_idt &id=to_symbol_expr(expr).get_identifier();
282 
283  identifier_mapt::const_iterator it=identifier_map.find(id);
284 
285  if(it!=identifier_map.end())
286  return it->second.value;
287  return expr;
288  }
289  else if(expr.id()==ID_nondet_symbol)
290  {
292 
293  identifier_mapt::const_iterator it=identifier_map.find(id);
294 
295  if(it!=identifier_map.end())
296  return it->second.value;
297  }
298  else if(expr.id()==ID_member)
299  {
300  const member_exprt &member_expr=to_member_expr(expr);
301  exprt tmp=get(member_expr.struct_op());
302  if(tmp.is_nil())
303  return nil_exprt();
304  return member_exprt(tmp, member_expr.get_component_name(), expr.type());
305  }
306  else if(expr.id() == ID_literal)
307  {
308  auto l = to_literal_expr(expr).get_literal();
309  if(l_get(l).is_true())
310  return true_exprt();
311  else
312  return false_exprt();
313  }
314  else if(expr.id() == ID_not)
315  {
316  auto op = get(to_not_expr(expr).op());
317  if(op.is_true())
318  return false_exprt();
319  else if(op.is_false())
320  return true_exprt();
321  }
322  else if(expr.is_constant())
323  return expr;
324  else if(const auto &array = expr_try_dynamic_cast<array_exprt>(expr))
325  {
326  exprt array_copy = *array;
327  for(auto &element : array_copy.operands())
328  {
329  element = get(element);
330  }
331  return array_copy;
332  }
333 
334  return nil_exprt();
335 }
336 
338  const irept &src,
339  const typet &type)
340 {
341  // See http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf for the
342  // syntax of SMTlib2 literals.
343  //
344  // A literal expression is one of the following forms:
345  //
346  // * Numeral -- this is a natural number in decimal and is of the form:
347  // 0|([1-9][0-9]*)
348  // * Decimal -- this is a decimal expansion of a real number of the form:
349  // (0|[1-9][0-9]*)[.]([0-9]+)
350  // * Binary -- this is a natural number in binary and is of the form:
351  // #b[01]+
352  // * Hex -- this is a natural number in hexadecimal and is of the form:
353  // #x[0-9a-fA-F]+
354  //
355  // Right now I'm not parsing decimals. It'd be nice if we had a real YACC
356  // parser here, but whatever.
357 
358  mp_integer value;
359 
360  if(!src.id().empty())
361  {
362  const std::string &s=src.id_string();
363 
364  if(s.size()>=2 && s[0]=='#' && s[1]=='b')
365  {
366  // Binary #b010101
367  value=string2integer(s.substr(2), 2);
368  }
369  else if(s.size()>=2 && s[0]=='#' && s[1]=='x')
370  {
371  // Hex #x012345
372  value=string2integer(s.substr(2), 16);
373  }
374  else
375  {
376  // Numeral
377  value=string2integer(s);
378  }
379  }
380  else if(src.get_sub().size()==2 &&
381  src.get_sub()[0].id()=="-") // (- 100)
382  {
383  value=-string2integer(src.get_sub()[1].id_string());
384  }
385  else if(src.get_sub().size()==3 &&
386  src.get_sub()[0].id()=="_" &&
387  // (_ bvDECIMAL_VALUE SIZE)
388  src.get_sub()[1].id_string().substr(0, 2)=="bv")
389  {
390  value=string2integer(src.get_sub()[1].id_string().substr(2));
391  }
392  else if(src.get_sub().size()==4 &&
393  src.get_sub()[0].id()=="fp") // (fp signbv exponentbv significandbv)
394  {
395  if(type.id()==ID_floatbv)
396  {
397  const floatbv_typet &floatbv_type=to_floatbv_type(type);
400  parse_literal(src.get_sub()[2], unsignedbv_typet(floatbv_type.get_e()));
401  constant_exprt s3 =
402  parse_literal(src.get_sub()[3], unsignedbv_typet(floatbv_type.get_f()));
403 
404  const auto s1_int = numeric_cast_v<mp_integer>(s1);
405  const auto s2_int = numeric_cast_v<mp_integer>(s2);
406  const auto s3_int = numeric_cast_v<mp_integer>(s3);
407 
408  // stitch the bits together
409  value = bitwise_or(
410  s1_int << (floatbv_type.get_e() + floatbv_type.get_f()),
411  bitwise_or((s2_int << floatbv_type.get_f()), s3_int));
412  }
413  else
414  value=0;
415  }
416  else if(src.get_sub().size()==4 &&
417  src.get_sub()[0].id()=="_" &&
418  src.get_sub()[1].id()=="+oo") // (_ +oo e s)
419  {
420  std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
421  std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
423  }
424  else if(src.get_sub().size()==4 &&
425  src.get_sub()[0].id()=="_" &&
426  src.get_sub()[1].id()=="-oo") // (_ -oo e s)
427  {
428  std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
429  std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
431  }
432  else if(src.get_sub().size()==4 &&
433  src.get_sub()[0].id()=="_" &&
434  src.get_sub()[1].id()=="NaN") // (_ NaN e s)
435  {
436  std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
437  std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
438  return ieee_floatt::NaN(ieee_float_spect(s - 1, e)).to_expr();
439  }
440 
441  if(type.id()==ID_signedbv ||
442  type.id()==ID_unsignedbv ||
443  type.id()==ID_c_enum ||
444  type.id()==ID_c_bool)
445  {
446  return from_integer(value, type);
447  }
448  else if(type.id()==ID_c_enum_tag)
449  {
450  constant_exprt result =
452 
453  // restore the c_enum_tag type
454  result.type() = type;
455  return result;
456  }
457  else if(type.id()==ID_fixedbv ||
458  type.id()==ID_floatbv)
459  {
460  std::size_t width=boolbv_width(type);
461  return constant_exprt(integer2bvrep(value, width), type);
462  }
463  else if(type.id()==ID_integer ||
464  type.id()==ID_range)
465  {
466  return from_integer(value, type);
467  }
468  else
469  INVARIANT(
470  false,
471  "smt2_convt::parse_literal should not be of unsupported type " +
472  type.id_string());
473 }
474 
476  const irept &src,
477  const array_typet &type)
478 {
479  std::unordered_map<int64_t, exprt> operands_map;
480  walk_array_tree(&operands_map, src, type);
481  exprt::operandst operands;
482  // Try to find the default value, if there is none then set it
483  auto maybe_default_op = operands_map.find(-1);
484  exprt default_op;
485  if(maybe_default_op == operands_map.end())
486  default_op = nil_exprt();
487  else
488  default_op = maybe_default_op->second;
489  int64_t i = 0;
490  auto maybe_size = numeric_cast<std::int64_t>(type.size());
491  if(maybe_size.has_value())
492  {
493  while(i < maybe_size.value())
494  {
495  auto found_op = operands_map.find(i);
496  if(found_op != operands_map.end())
497  operands.emplace_back(found_op->second);
498  else
499  operands.emplace_back(default_op);
500  i++;
501  }
502  }
503  else
504  {
505  // Array size is unknown, keep adding with known indexes in order
506  // until we fail to find one.
507  auto found_op = operands_map.find(i);
508  while(found_op != operands_map.end())
509  {
510  operands.emplace_back(found_op->second);
511  i++;
512  found_op = operands_map.find(i);
513  }
514  operands.emplace_back(default_op);
515  }
516  return array_exprt(operands, type);
517 }
518 
520  std::unordered_map<int64_t, exprt> *operands_map,
521  const irept &src,
522  const array_typet &type)
523 {
524  if(src.get_sub().size()==4 && src.get_sub()[0].id()=="store")
525  {
526  // This is the SMT syntax being parsed here
527  // (store array index value)
528  // Recurse
529  walk_array_tree(operands_map, src.get_sub()[1], type);
530  const auto index_expr = parse_rec(src.get_sub()[2], type.size().type());
531  const constant_exprt index_constant = to_constant_expr(index_expr);
532  mp_integer tempint;
533  bool failure = to_integer(index_constant, tempint);
534  if(failure)
535  return;
536  long index = tempint.to_long();
537  exprt value = parse_rec(src.get_sub()[3], type.subtype());
538  operands_map->emplace(index, value);
539  }
540  else if(src.get_sub().size() == 3 && src.get_sub()[0].id() == "let")
541  {
542  // This is produced by Z3
543  // (let (....) (....))
545  operands_map, src.get_sub()[1].get_sub()[0].get_sub()[1], type);
546  walk_array_tree(operands_map, src.get_sub()[2], type);
547  }
548  else if(src.get_sub().size()==2 &&
549  src.get_sub()[0].get_sub().size()==3 &&
550  src.get_sub()[0].get_sub()[0].id()=="as" &&
551  src.get_sub()[0].get_sub()[1].id()=="const")
552  {
553  // (as const type_info default_value)
554  exprt default_value = parse_rec(src.get_sub()[1], type.subtype());
555  operands_map->emplace(-1, default_value);
556  }
557 }
558 
560  const irept &src,
561  const union_typet &type)
562 {
563  // these are always flat
564  PRECONDITION(!type.components().empty());
565  const union_typet::componentt &first=type.components().front();
566  std::size_t width=boolbv_width(type);
567  exprt value = parse_rec(src, unsignedbv_typet(width));
568  if(value.is_nil())
569  return nil_exprt();
570  const typecast_exprt converted(value, first.type());
571  return union_exprt(first.get_name(), converted, type);
572 }
573 
576 {
577  const struct_typet::componentst &components =
578  type.components();
579 
580  struct_exprt result(exprt::operandst(components.size(), nil_exprt()), type);
581 
582  if(components.empty())
583  return result;
584 
585  if(use_datatypes)
586  {
587  // Structs look like:
588  // (mk-struct.1 <component0> <component1> ... <componentN>)
589 
590  if(src.get_sub().size()!=components.size()+1)
591  return result; // give up
592 
593  for(std::size_t i=0; i<components.size(); i++)
594  {
595  const struct_typet::componentt &c=components[i];
596  result.operands()[i]=parse_rec(src.get_sub()[i+1], c.type());
597  }
598  }
599  else
600  {
601  // These are just flattened, i.e., we expect to see a monster bit vector.
602  std::size_t total_width=boolbv_width(type);
603  const auto l = parse_literal(src, unsignedbv_typet(total_width));
604 
605  const irep_idt binary =
606  integer2binary(numeric_cast_v<mp_integer>(l), total_width);
607 
608  CHECK_RETURN(binary.size() == total_width);
609 
610  std::size_t offset=0;
611 
612  for(std::size_t i=0; i<components.size(); i++)
613  {
614  std::size_t component_width=boolbv_width(components[i].type());
615 
616  INVARIANT(
617  offset + component_width <= total_width,
618  "struct component bits shall be within struct bit vector");
619 
620  std::string component_binary=
621  "#b"+id2string(binary).substr(
622  total_width-offset-component_width, component_width);
623 
624  result.operands()[i]=
625  parse_rec(irept(component_binary), components[i].type());
626 
627  offset+=component_width;
628  }
629  }
630 
631  return result;
632 }
633 
634 exprt smt2_convt::parse_rec(const irept &src, const typet &type)
635 {
636  if(
637  type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
638  type.id() == ID_integer || type.id() == ID_rational ||
639  type.id() == ID_real || type.id() == ID_c_enum ||
640  type.id() == ID_c_enum_tag || type.id() == ID_fixedbv ||
641  type.id() == ID_floatbv)
642  {
643  return parse_literal(src, type);
644  }
645  else if(type.id()==ID_bool)
646  {
647  if(src.id()==ID_1 || src.id()==ID_true)
648  return true_exprt();
649  else if(src.id()==ID_0 || src.id()==ID_false)
650  return false_exprt();
651  }
652  else if(type.id()==ID_pointer)
653  {
654  // these come in as bit-vector literals
655  std::size_t width=boolbv_width(type);
656  constant_exprt bv_expr = parse_literal(src, unsignedbv_typet(width));
657 
658  mp_integer v = numeric_cast_v<mp_integer>(bv_expr);
659 
660  // split into object and offset
663  ptr.object = numeric_cast_v<std::size_t>(v / pow);
664  ptr.offset=v%pow;
665  return pointer_logic.pointer_expr(ptr, to_pointer_type(type));
666  }
667  else if(type.id()==ID_struct)
668  {
669  return parse_struct(src, to_struct_type(type));
670  }
671  else if(type.id() == ID_struct_tag)
672  {
673  auto struct_expr =
675  // restore the tag type
676  struct_expr.type() = type;
677  return std::move(struct_expr);
678  }
679  else if(type.id()==ID_union)
680  {
681  return parse_union(src, to_union_type(type));
682  }
683  else if(type.id() == ID_union_tag)
684  {
685  auto union_expr = parse_union(src, ns.follow_tag(to_union_tag_type(type)));
686  // restore the tag type
687  union_expr.type() = type;
688  return union_expr;
689  }
690  else if(type.id()==ID_array)
691  {
692  return parse_array(src, to_array_type(type));
693  }
694 
695  return nil_exprt();
696 }
697 
699  const exprt &expr,
700  const pointer_typet &result_type)
701 {
702  if(expr.id()==ID_symbol ||
703  expr.id()==ID_constant ||
704  expr.id()==ID_string_constant ||
705  expr.id()==ID_label)
706  {
707  out
708  << "(concat (_ bv"
709  << pointer_logic.add_object(expr) << " "
710  << config.bv_encoding.object_bits << ")"
711  << " (_ bv0 "
712  << boolbv_width(result_type)-config.bv_encoding.object_bits << "))";
713  }
714  else if(expr.id()==ID_index)
715  {
716  const index_exprt &index_expr = to_index_expr(expr);
717 
718  const exprt &array = index_expr.array();
719  const exprt &index = index_expr.index();
720 
721  if(index.is_zero())
722  {
723  if(array.type().id()==ID_pointer)
724  convert_expr(array);
725  else if(array.type().id()==ID_array)
726  convert_address_of_rec(array, result_type);
727  else
728  UNREACHABLE;
729  }
730  else
731  {
732  // this is really pointer arithmetic
733  index_exprt new_index_expr = index_expr;
734  new_index_expr.index() = from_integer(0, index.type());
735 
736  address_of_exprt address_of_expr(
737  new_index_expr,
738  pointer_type(array.type().subtype()));
739 
740  plus_exprt plus_expr{address_of_expr, index};
741 
742  convert_expr(plus_expr);
743  }
744  }
745  else if(expr.id()==ID_member)
746  {
747  const member_exprt &member_expr=to_member_expr(expr);
748 
749  const exprt &struct_op=member_expr.struct_op();
750  const typet &struct_op_type = struct_op.type();
751 
753  struct_op_type.id() == ID_struct || struct_op_type.id() == ID_struct_tag,
754  "member expression operand shall have struct type");
755 
756  const struct_typet &struct_type = to_struct_type(ns.follow(struct_op_type));
757 
758  const irep_idt &component_name = member_expr.get_component_name();
759 
760  const auto offset = member_offset(struct_type, component_name, ns);
761  CHECK_RETURN(offset.has_value() && *offset >= 0);
762 
764 
765  // pointer arithmetic
766  out << "(bvadd ";
767  convert_address_of_rec(struct_op, result_type);
769  out << ")"; // bvadd
770  }
771  else if(expr.id()==ID_if)
772  {
773  const if_exprt &if_expr = to_if_expr(expr);
774 
775  out << "(ite ";
776  convert_expr(if_expr.cond());
777  out << " ";
778  convert_address_of_rec(if_expr.true_case(), result_type);
779  out << " ";
780  convert_address_of_rec(if_expr.false_case(), result_type);
781  out << ")";
782  }
783  else
784  INVARIANT(
785  false,
786  "operand of address of expression should not be of kind " +
787  expr.id_string());
788 }
789 
791 {
792  PRECONDITION(expr.type().id() == ID_bool);
793 
794  // Three cases where no new handle is needed.
795 
796  if(expr.is_true())
797  return const_literal(true);
798  else if(expr.is_false())
799  return const_literal(false);
800  else if(expr.id()==ID_literal)
801  return to_literal_expr(expr).get_literal();
802 
803  // Need a new handle
804 
805  out << "\n";
806 
807  exprt prepared_expr = prepare_for_convert_expr(expr);
808 
809  literalt l(no_boolean_variables, false);
811 
812  out << "; convert\n";
813  out << "; Converting var_no " << l.var_no() << " with expr ID of "
814  << expr.id_string() << "\n";
815  // We're converting the expression, so store it in the defined_expressions
816  // store and in future we use the literal instead of the whole expression
817  // Note that here we are always converting, so we do not need to consider
818  // other literal kinds, only "|B###|"
819  defined_expressions[expr] =
820  std::string{"|B"} + std::to_string(l.var_no()) + "|";
821  out << "(define-fun ";
822  convert_literal(l);
823  out << " () Bool ";
824  convert_expr(prepared_expr);
825  out << ")" << "\n";
826 
827  return l;
828 }
829 
831 {
832  // We can only improve Booleans.
833  if(expr.type().id() != ID_bool)
834  return expr;
835 
836  return literal_exprt(convert(expr));
837 }
838 
840 {
841  if(l==const_literal(false))
842  out << "false";
843  else if(l==const_literal(true))
844  out << "true";
845  else
846  {
847  if(l.sign())
848  out << "(not ";
849 
850  out << "|B" << l.var_no() << "|";
851 
852  if(l.sign())
853  out << ")";
854 
855  smt2_identifiers.insert("B"+std::to_string(l.var_no()));
856  }
857 }
858 
860 {
862 }
863 
864 void smt2_convt::push(const std::vector<exprt> &_assumptions)
865 {
866  INVARIANT(assumptions.empty(), "nested contexts are not supported");
867 
868  assumptions = _assumptions;
869 }
870 
872 {
873  assumptions.clear();
874 }
875 
876 std::string smt2_convt::convert_identifier(const irep_idt &identifier)
877 {
878  // Backslashes are disallowed in quoted symbols just for simplicity.
879  // Otherwise, for Common Lisp compatibility they would have to be treated
880  // as escaping symbols.
881 
882  std::string result;
883 
884  for(std::size_t i=0; i<identifier.size(); i++)
885  {
886  char ch=identifier[i];
887 
888  switch(ch)
889  {
890  case '|':
891  case '\\':
892  case '&': // we use the & for escaping
893  result+='&';
894  result+=std::to_string(ch);
895  result+=';';
896  break;
897 
898  case '$': // $ _is_ allowed
899  default:
900  result+=ch;
901  }
902  }
903 
904  return result;
905 }
906 
907 std::string smt2_convt::type2id(const typet &type) const
908 {
909  if(type.id()==ID_floatbv)
910  {
911  ieee_float_spect spec(to_floatbv_type(type));
912  return "f"+std::to_string(spec.width())+"_"+std::to_string(spec.f);
913  }
914  else if(type.id()==ID_unsignedbv)
915  {
916  return "u"+std::to_string(to_unsignedbv_type(type).get_width());
917  }
918  else if(type.id()==ID_c_bool)
919  {
920  return "u"+std::to_string(to_c_bool_type(type).get_width());
921  }
922  else if(type.id()==ID_signedbv)
923  {
924  return "s"+std::to_string(to_signedbv_type(type).get_width());
925  }
926  else if(type.id()==ID_bool)
927  {
928  return "b";
929  }
930  else if(type.id()==ID_c_enum_tag)
931  {
932  return type2id(ns.follow_tag(to_c_enum_tag_type(type)).subtype());
933  }
934  else if(type.id() == ID_pointer)
935  {
936  return "p" + std::to_string(to_pointer_type(type).get_width());
937  }
938  else
939  {
940  UNREACHABLE;
941  }
942 }
943 
944 std::string smt2_convt::floatbv_suffix(const exprt &expr) const
945 {
946  PRECONDITION(!expr.operands().empty());
947  return "_" + type2id(to_multi_ary_expr(expr).op0().type()) + "->" +
948  type2id(expr.type());
949 }
950 
952 {
954 
955  if(expr.id()==ID_symbol)
956  {
957  const irep_idt &id = to_symbol_expr(expr).get_identifier();
958  out << '|' << convert_identifier(id) << '|';
959  return;
960  }
961 
962  if(expr.id()==ID_smt2_symbol)
963  {
964  const irep_idt &id = to_smt2_symbol(expr).get_identifier();
965  out << id;
966  return;
967  }
968 
969  INVARIANT(
970  !expr.operands().empty(), "non-symbol expressions shall have operands");
971 
972  out << "(|float_bv." << expr.id()
973  << floatbv_suffix(expr)
974  << '|';
975 
976  forall_operands(it, expr)
977  {
978  out << ' ';
979  convert_expr(*it);
980  }
981 
982  out << ')';
983 }
984 
986 {
987  // huge monster case split over expression id
988  if(expr.id()==ID_symbol)
989  {
990  const irep_idt &id = to_symbol_expr(expr).get_identifier();
991  DATA_INVARIANT(!id.empty(), "symbol must have identifier");
992  out << '|' << convert_identifier(id) << '|';
993  }
994  else if(expr.id()==ID_nondet_symbol)
995  {
996  const irep_idt &id = to_nondet_symbol_expr(expr).get_identifier();
997  DATA_INVARIANT(!id.empty(), "nondet symbol must have identifier");
998  out << '|' << convert_identifier("nondet_"+id2string(id)) << '|';
999  }
1000  else if(expr.id()==ID_smt2_symbol)
1001  {
1002  const irep_idt &id = to_smt2_symbol(expr).get_identifier();
1003  DATA_INVARIANT(!id.empty(), "smt2 symbol must have identifier");
1004  out << id;
1005  }
1006  else if(expr.id()==ID_typecast)
1007  {
1009  }
1010  else if(expr.id()==ID_floatbv_typecast)
1011  {
1013  }
1014  else if(expr.id()==ID_struct)
1015  {
1017  }
1018  else if(expr.id()==ID_union)
1019  {
1021  }
1022  else if(expr.id()==ID_constant)
1023  {
1025  }
1026  else if(expr.id() == ID_concatenation && expr.operands().size() == 1)
1027  {
1029  expr.type() == expr.operands().front().type(),
1030  "concatenation over a single operand should have matching types",
1031  expr.pretty());
1032 
1033  convert_expr(expr.operands().front());
1034  }
1035  else if(expr.id()==ID_concatenation ||
1036  expr.id()==ID_bitand ||
1037  expr.id()==ID_bitor ||
1038  expr.id()==ID_bitxor ||
1039  expr.id()==ID_bitnand ||
1040  expr.id()==ID_bitnor)
1041  {
1043  expr.operands().size() >= 2,
1044  "given expression should have at least two operands",
1045  expr.id_string());
1046 
1047  out << "(";
1048 
1049  if(expr.id()==ID_concatenation)
1050  out << "concat";
1051  else if(expr.id()==ID_bitand)
1052  out << "bvand";
1053  else if(expr.id()==ID_bitor)
1054  out << "bvor";
1055  else if(expr.id()==ID_bitxor)
1056  out << "bvxor";
1057  else if(expr.id()==ID_bitnand)
1058  out << "bvnand";
1059  else if(expr.id()==ID_bitnor)
1060  out << "bvnor";
1061 
1062  forall_operands(it, expr)
1063  {
1064  out << " ";
1065  flatten2bv(*it);
1066  }
1067 
1068  out << ")";
1069  }
1070  else if(expr.id()==ID_bitnot)
1071  {
1072  const bitnot_exprt &bitnot_expr = to_bitnot_expr(expr);
1073 
1074  if(bitnot_expr.type().id() == ID_vector)
1075  {
1076  if(use_datatypes)
1077  {
1078  const std::string &smt_typename = datatype_map.at(bitnot_expr.type());
1079 
1080  // extract elements
1081  const vector_typet &vector_type = to_vector_type(bitnot_expr.type());
1082 
1083  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
1084 
1085  out << "(let ((?vectorop ";
1086  convert_expr(bitnot_expr.op());
1087  out << ")) ";
1088 
1089  out << "(mk-" << smt_typename;
1090 
1091  typet index_type=vector_type.size().type();
1092 
1093  // do bitnot component-by-component
1094  for(mp_integer i=0; i!=size; ++i)
1095  {
1096  out << " (bvnot (" << smt_typename << "." << (size-i-1)
1097  << " ?vectorop))";
1098  }
1099 
1100  out << "))"; // mk-, let
1101  }
1102  else
1103  SMT2_TODO("bitnot for vectors");
1104  }
1105  else
1106  {
1107  out << "(bvnot ";
1108  convert_expr(bitnot_expr.op());
1109  out << ")";
1110  }
1111  }
1112  else if(expr.id()==ID_unary_minus)
1113  {
1114  const unary_minus_exprt &unary_minus_expr = to_unary_minus_expr(expr);
1115 
1116  if(
1117  unary_minus_expr.type().id() == ID_rational ||
1118  unary_minus_expr.type().id() == ID_integer ||
1119  unary_minus_expr.type().id() == ID_real)
1120  {
1121  out << "(- ";
1122  convert_expr(unary_minus_expr.op());
1123  out << ")";
1124  }
1125  else if(unary_minus_expr.type().id() == ID_floatbv)
1126  {
1127  // this has no rounding mode
1128  if(use_FPA_theory)
1129  {
1130  out << "(fp.neg ";
1131  convert_expr(unary_minus_expr.op());
1132  out << ")";
1133  }
1134  else
1135  convert_floatbv(unary_minus_expr);
1136  }
1137  else if(unary_minus_expr.type().id() == ID_vector)
1138  {
1139  if(use_datatypes)
1140  {
1141  const std::string &smt_typename =
1142  datatype_map.at(unary_minus_expr.type());
1143 
1144  // extract elements
1145  const vector_typet &vector_type =
1146  to_vector_type(unary_minus_expr.type());
1147 
1148  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
1149 
1150  out << "(let ((?vectorop ";
1151  convert_expr(unary_minus_expr.op());
1152  out << ")) ";
1153 
1154  out << "(mk-" << smt_typename;
1155 
1156  typet index_type=vector_type.size().type();
1157 
1158  // negate component-by-component
1159  for(mp_integer i=0; i!=size; ++i)
1160  {
1161  out << " (bvneg (" << smt_typename << "." << (size-i-1)
1162  << " ?vectorop))";
1163  }
1164 
1165  out << "))"; // mk-, let
1166  }
1167  else
1168  SMT2_TODO("unary minus for vector");
1169  }
1170  else
1171  {
1172  out << "(bvneg ";
1173  convert_expr(unary_minus_expr.op());
1174  out << ")";
1175  }
1176  }
1177  else if(expr.id()==ID_unary_plus)
1178  {
1179  // A no-op (apart from type promotion)
1180  convert_expr(to_unary_plus_expr(expr).op());
1181  }
1182  else if(expr.id()==ID_sign)
1183  {
1184  const sign_exprt &sign_expr = to_sign_expr(expr);
1185 
1186  const typet &op_type = sign_expr.op().type();
1187 
1188  if(op_type.id()==ID_floatbv)
1189  {
1190  if(use_FPA_theory)
1191  {
1192  out << "(fp.isNegative ";
1193  convert_expr(sign_expr.op());
1194  out << ")";
1195  }
1196  else
1197  convert_floatbv(sign_expr);
1198  }
1199  else if(op_type.id()==ID_signedbv)
1200  {
1201  std::size_t op_width=to_signedbv_type(op_type).get_width();
1202 
1203  out << "(bvslt ";
1204  convert_expr(sign_expr.op());
1205  out << " (_ bv0 " << op_width << "))";
1206  }
1207  else
1209  false,
1210  "sign should not be applied to unsupported type",
1211  sign_expr.type().id_string());
1212  }
1213  else if(expr.id()==ID_if)
1214  {
1215  const if_exprt &if_expr = to_if_expr(expr);
1216 
1217  out << "(ite ";
1218  convert_expr(if_expr.cond());
1219  out << " ";
1220  convert_expr(if_expr.true_case());
1221  out << " ";
1222  convert_expr(if_expr.false_case());
1223  out << ")";
1224  }
1225  else if(expr.id()==ID_and ||
1226  expr.id()==ID_or ||
1227  expr.id()==ID_xor)
1228  {
1230  expr.type().id() == ID_bool,
1231  "logical and, or, and xor expressions should have Boolean type");
1233  expr.operands().size() >= 2,
1234  "logical and, or, and xor expressions should have at least two operands");
1235 
1236  out << "(" << expr.id();
1237  forall_operands(it, expr)
1238  {
1239  out << " ";
1240  convert_expr(*it);
1241  }
1242  out << ")";
1243  }
1244  else if(expr.id()==ID_implies)
1245  {
1246  const implies_exprt &implies_expr = to_implies_expr(expr);
1247 
1249  implies_expr.type().id() == ID_bool,
1250  "implies expression should have Boolean type");
1251 
1252  out << "(=> ";
1253  convert_expr(implies_expr.op0());
1254  out << " ";
1255  convert_expr(implies_expr.op1());
1256  out << ")";
1257  }
1258  else if(expr.id()==ID_not)
1259  {
1260  const not_exprt &not_expr = to_not_expr(expr);
1261 
1263  not_expr.type().id() == ID_bool,
1264  "not expression should have Boolean type");
1265 
1266  out << "(not ";
1267  convert_expr(not_expr.op());
1268  out << ")";
1269  }
1270  else if(expr.id() == ID_equal)
1271  {
1272  const equal_exprt &equal_expr = to_equal_expr(expr);
1273 
1275  equal_expr.op0().type() == equal_expr.op1().type(),
1276  "operands of equal expression shall have same type");
1277 
1278  out << "(= ";
1279  convert_expr(equal_expr.op0());
1280  out << " ";
1281  convert_expr(equal_expr.op1());
1282  out << ")";
1283  }
1284  else if(expr.id() == ID_notequal)
1285  {
1286  const notequal_exprt &notequal_expr = to_notequal_expr(expr);
1287 
1289  notequal_expr.op0().type() == notequal_expr.op1().type(),
1290  "operands of not equal expression shall have same type");
1291 
1292  out << "(not (= ";
1293  convert_expr(notequal_expr.op0());
1294  out << " ";
1295  convert_expr(notequal_expr.op1());
1296  out << "))";
1297  }
1298  else if(expr.id()==ID_ieee_float_equal ||
1299  expr.id()==ID_ieee_float_notequal)
1300  {
1301  // These are not the same as (= A B)
1302  // because of NaN and negative zero.
1303  const auto &rel_expr = to_binary_relation_expr(expr);
1304 
1306  rel_expr.lhs().type() == rel_expr.rhs().type(),
1307  "operands of float equal and not equal expressions shall have same type");
1308 
1309  // The FPA theory properly treats NaN and negative zero.
1310  if(use_FPA_theory)
1311  {
1312  if(rel_expr.id() == ID_ieee_float_notequal)
1313  out << "(not ";
1314 
1315  out << "(fp.eq ";
1316  convert_expr(rel_expr.lhs());
1317  out << " ";
1318  convert_expr(rel_expr.rhs());
1319  out << ")";
1320 
1321  if(rel_expr.id() == ID_ieee_float_notequal)
1322  out << ")";
1323  }
1324  else
1325  convert_floatbv(expr);
1326  }
1327  else if(expr.id()==ID_le ||
1328  expr.id()==ID_lt ||
1329  expr.id()==ID_ge ||
1330  expr.id()==ID_gt)
1331  {
1333  }
1334  else if(expr.id()==ID_plus)
1335  {
1336  convert_plus(to_plus_expr(expr));
1337  }
1338  else if(expr.id()==ID_floatbv_plus)
1339  {
1341  }
1342  else if(expr.id()==ID_minus)
1343  {
1345  }
1346  else if(expr.id()==ID_floatbv_minus)
1347  {
1349  }
1350  else if(expr.id()==ID_div)
1351  {
1352  convert_div(to_div_expr(expr));
1353  }
1354  else if(expr.id()==ID_floatbv_div)
1355  {
1357  }
1358  else if(expr.id()==ID_mod)
1359  {
1360  convert_mod(to_mod_expr(expr));
1361  }
1362  else if(expr.id() == ID_euclidean_mod)
1363  {
1365  }
1366  else if(expr.id()==ID_mult)
1367  {
1368  convert_mult(to_mult_expr(expr));
1369  }
1370  else if(expr.id()==ID_floatbv_mult)
1371  {
1373  }
1374  else if(expr.id() == ID_floatbv_rem)
1375  {
1377  }
1378  else if(expr.id()==ID_address_of)
1379  {
1380  const address_of_exprt &address_of_expr = to_address_of_expr(expr);
1382  address_of_expr.object(), to_pointer_type(address_of_expr.type()));
1383  }
1384  else if(expr.id() == ID_array_of)
1385  {
1386  const auto &array_of_expr = to_array_of_expr(expr);
1387 
1389  array_of_expr.type().id() == ID_array,
1390  "array of expression shall have array type");
1391 
1392  if(use_as_const)
1393  {
1394  out << "((as const ";
1395  convert_type(array_of_expr.type());
1396  out << ") ";
1397  convert_expr(array_of_expr.what());
1398  out << ")";
1399  }
1400  else
1401  {
1402  defined_expressionst::const_iterator it =
1403  defined_expressions.find(array_of_expr);
1404  CHECK_RETURN(it != defined_expressions.end());
1405  out << it->second;
1406  }
1407  }
1408  else if(expr.id() == ID_array_comprehension)
1409  {
1410  const auto &array_comprehension = to_array_comprehension_expr(expr);
1411 
1413  array_comprehension.type().id() == ID_array,
1414  "array_comprehension expression shall have array type");
1415 
1417  {
1418  out << "(lambda ((";
1419  convert_expr(array_comprehension.arg());
1420  out << " ";
1421  convert_type(array_comprehension.type().size().type());
1422  out << ")) ";
1423  convert_expr(array_comprehension.body());
1424  out << ")";
1425  }
1426  else
1427  {
1428  const auto &it = defined_expressions.find(array_comprehension);
1429  CHECK_RETURN(it != defined_expressions.end());
1430  out << it->second;
1431  }
1432  }
1433  else if(expr.id()==ID_index)
1434  {
1436  }
1437  else if(expr.id()==ID_ashr ||
1438  expr.id()==ID_lshr ||
1439  expr.id()==ID_shl)
1440  {
1441  const shift_exprt &shift_expr = to_shift_expr(expr);
1442  const typet &type = shift_expr.type();
1443 
1444  if(type.id()==ID_unsignedbv ||
1445  type.id()==ID_signedbv ||
1446  type.id()==ID_bv)
1447  {
1448  if(shift_expr.id() == ID_ashr)
1449  out << "(bvashr ";
1450  else if(shift_expr.id() == ID_lshr)
1451  out << "(bvlshr ";
1452  else if(shift_expr.id() == ID_shl)
1453  out << "(bvshl ";
1454  else
1455  UNREACHABLE;
1456 
1457  convert_expr(shift_expr.op());
1458  out << " ";
1459 
1460  // SMT2 requires the shift distance to have the same width as
1461  // the value that is shifted -- odd!
1462 
1463  if(shift_expr.distance().type().id() == ID_integer)
1464  {
1465  const mp_integer i =
1466  numeric_cast_v<mp_integer>(to_constant_expr(shift_expr.distance()));
1467 
1468  // shift distance must be bit vector
1469  std::size_t width_op0 = boolbv_width(shift_expr.op().type());
1470  exprt tmp=from_integer(i, unsignedbv_typet(width_op0));
1471  convert_expr(tmp);
1472  }
1473  else if(
1474  shift_expr.distance().type().id() == ID_signedbv ||
1475  shift_expr.distance().type().id() == ID_unsignedbv ||
1476  shift_expr.distance().type().id() == ID_c_enum ||
1477  shift_expr.distance().type().id() == ID_c_bool)
1478  {
1479  std::size_t width_op0 = boolbv_width(shift_expr.op().type());
1480  std::size_t width_op1 = boolbv_width(shift_expr.distance().type());
1481 
1482  if(width_op0==width_op1)
1483  convert_expr(shift_expr.distance());
1484  else if(width_op0>width_op1)
1485  {
1486  out << "((_ zero_extend " << width_op0-width_op1 << ") ";
1487  convert_expr(shift_expr.distance());
1488  out << ")"; // zero_extend
1489  }
1490  else // width_op0<width_op1
1491  {
1492  out << "((_ extract " << width_op0-1 << " 0) ";
1493  convert_expr(shift_expr.distance());
1494  out << ")"; // extract
1495  }
1496  }
1497  else
1499  "unsupported distance type for " + shift_expr.id_string() + ": " +
1500  type.id_string());
1501 
1502  out << ")"; // bv*sh
1503  }
1504  else
1506  "unsupported type for " + shift_expr.id_string() + ": " +
1507  type.id_string());
1508  }
1509  else if(expr.id() == ID_rol || expr.id() == ID_ror)
1510  {
1511  const shift_exprt &shift_expr = to_shift_expr(expr);
1512  const typet &type = shift_expr.type();
1513 
1514  if(
1515  type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
1516  type.id() == ID_bv)
1517  {
1518  // SMT-LIB offers rotate_left and rotate_right, but these require a
1519  // constant distance.
1520  if(shift_expr.id() == ID_rol)
1521  out << "((_ rotate_left";
1522  else if(shift_expr.id() == ID_ror)
1523  out << "((_ rotate_right";
1524  else
1525  UNREACHABLE;
1526 
1527  out << ' ';
1528 
1529  auto distance_int_op = numeric_cast<mp_integer>(shift_expr.distance());
1530 
1531  if(distance_int_op.has_value())
1532  {
1533  out << distance_int_op.value();
1534  }
1535  else
1537  "distance type for " + shift_expr.id_string() + "must be constant");
1538 
1539  out << ") ";
1540  convert_expr(shift_expr.op());
1541 
1542  out << ")"; // rotate_*
1543  }
1544  else
1546  "unsupported type for " + shift_expr.id_string() + ": " +
1547  type.id_string());
1548  }
1549  else if(expr.id()==ID_with)
1550  {
1551  convert_with(to_with_expr(expr));
1552  }
1553  else if(expr.id()==ID_update)
1554  {
1555  convert_update(expr);
1556  }
1557  else if(expr.id()==ID_member)
1558  {
1560  }
1561  else if(expr.id()==ID_pointer_offset)
1562  {
1563  const auto &op = to_unary_expr(expr).op();
1564 
1566  op.type().id() == ID_pointer,
1567  "operand of pointer offset expression shall be of pointer type");
1568 
1569  std::size_t offset_bits =
1571  std::size_t result_width=boolbv_width(expr.type());
1572 
1573  // max extract width
1574  if(offset_bits>result_width)
1575  offset_bits=result_width;
1576 
1577  // too few bits?
1578  if(result_width>offset_bits)
1579  out << "((_ zero_extend " << result_width-offset_bits << ") ";
1580 
1581  out << "((_ extract " << offset_bits-1 << " 0) ";
1582  convert_expr(op);
1583  out << ")";
1584 
1585  if(result_width>offset_bits)
1586  out << ")"; // zero_extend
1587  }
1588  else if(expr.id()==ID_pointer_object)
1589  {
1590  const auto &op = to_unary_expr(expr).op();
1591 
1593  op.type().id() == ID_pointer,
1594  "pointer object expressions should be of pointer type");
1595 
1596  std::size_t ext=boolbv_width(expr.type())-config.bv_encoding.object_bits;
1597  std::size_t pointer_width = boolbv_width(op.type());
1598 
1599  if(ext>0)
1600  out << "((_ zero_extend " << ext << ") ";
1601 
1602  out << "((_ extract "
1603  << pointer_width-1 << " "
1604  << pointer_width-config.bv_encoding.object_bits << ") ";
1605  convert_expr(op);
1606  out << ")";
1607 
1608  if(ext>0)
1609  out << ")"; // zero_extend
1610  }
1611  else if(expr.id() == ID_is_dynamic_object)
1612  {
1614  }
1615  else if(expr.id() == ID_is_invalid_pointer)
1616  {
1617  const auto &op = to_unary_expr(expr).op();
1618  std::size_t pointer_width = boolbv_width(op.type());
1619  out << "(= ((_ extract "
1620  << pointer_width-1 << " "
1621  << pointer_width-config.bv_encoding.object_bits << ") ";
1622  convert_expr(op);
1623  out << ") (_ bv" << pointer_logic.get_invalid_object()
1624  << " " << config.bv_encoding.object_bits << "))";
1625  }
1626  else if(expr.id()==ID_string_constant)
1627  {
1628  defined_expressionst::const_iterator it=defined_expressions.find(expr);
1629  CHECK_RETURN(it != defined_expressions.end());
1630  out << it->second;
1631  }
1632  else if(expr.id()==ID_extractbit)
1633  {
1634  const extractbit_exprt &extractbit_expr = to_extractbit_expr(expr);
1635 
1636  if(extractbit_expr.index().is_constant())
1637  {
1638  const mp_integer i =
1639  numeric_cast_v<mp_integer>(to_constant_expr(extractbit_expr.index()));
1640 
1641  out << "(= ((_ extract " << i << " " << i << ") ";
1642  flatten2bv(extractbit_expr.src());
1643  out << ") #b1)";
1644  }
1645  else
1646  {
1647  out << "(= ((_ extract 0 0) ";
1648  // the arguments of the shift need to have the same width
1649  out << "(bvlshr ";
1650  flatten2bv(extractbit_expr.src());
1651  typecast_exprt tmp(extractbit_expr.index(), extractbit_expr.src().type());
1652  convert_expr(tmp);
1653  out << ")) bin1)"; // bvlshr, extract, =
1654  }
1655  }
1656  else if(expr.id()==ID_extractbits)
1657  {
1658  const extractbits_exprt &extractbits_expr = to_extractbits_expr(expr);
1659 
1660  if(
1661  extractbits_expr.upper().is_constant() &&
1662  extractbits_expr.lower().is_constant())
1663  {
1664  mp_integer op1_i =
1665  numeric_cast_v<mp_integer>(to_constant_expr(extractbits_expr.upper()));
1666  mp_integer op2_i =
1667  numeric_cast_v<mp_integer>(to_constant_expr(extractbits_expr.lower()));
1668 
1669  if(op2_i>op1_i)
1670  std::swap(op1_i, op2_i);
1671 
1672  // now op1_i>=op2_i
1673 
1674  out << "((_ extract " << op1_i << " " << op2_i << ") ";
1675  flatten2bv(extractbits_expr.src());
1676  out << ")";
1677  }
1678  else
1679  {
1680  #if 0
1681  out << "(= ((_ extract 0 0) ";
1682  // the arguments of the shift need to have the same width
1683  out << "(bvlshr ";
1684  convert_expr(expr.op0());
1685  typecast_exprt tmp(expr.op0().type());
1686  tmp.op0()=expr.op1();
1687  convert_expr(tmp);
1688  out << ")) bin1)"; // bvlshr, extract, =
1689  #endif
1690  SMT2_TODO("smt2: extractbits with non-constant index");
1691  }
1692  }
1693  else if(expr.id()==ID_replication)
1694  {
1695  const replication_exprt &replication_expr = to_replication_expr(expr);
1696 
1697  mp_integer times = numeric_cast_v<mp_integer>(replication_expr.times());
1698 
1699  out << "((_ repeat " << times << ") ";
1700  flatten2bv(replication_expr.op());
1701  out << ")";
1702  }
1703  else if(expr.id()==ID_byte_extract_little_endian ||
1704  expr.id()==ID_byte_extract_big_endian)
1705  {
1706  INVARIANT(
1707  false, "byte_extract ops should be lowered in prepare_for_convert_expr");
1708  }
1709  else if(expr.id()==ID_byte_update_little_endian ||
1710  expr.id()==ID_byte_update_big_endian)
1711  {
1712  INVARIANT(
1713  false, "byte_update ops should be lowered in prepare_for_convert_expr");
1714  }
1715  else if(expr.id()==ID_abs)
1716  {
1717  const abs_exprt &abs_expr = to_abs_expr(expr);
1718 
1719  const typet &type = abs_expr.type();
1720 
1721  if(type.id()==ID_signedbv)
1722  {
1723  std::size_t result_width = to_signedbv_type(type).get_width();
1724 
1725  out << "(ite (bvslt ";
1726  convert_expr(abs_expr.op());
1727  out << " (_ bv0 " << result_width << ")) ";
1728  out << "(bvneg ";
1729  convert_expr(abs_expr.op());
1730  out << ") ";
1731  convert_expr(abs_expr.op());
1732  out << ")";
1733  }
1734  else if(type.id()==ID_fixedbv)
1735  {
1736  std::size_t result_width=to_fixedbv_type(type).get_width();
1737 
1738  out << "(ite (bvslt ";
1739  convert_expr(abs_expr.op());
1740  out << " (_ bv0 " << result_width << ")) ";
1741  out << "(bvneg ";
1742  convert_expr(abs_expr.op());
1743  out << ") ";
1744  convert_expr(abs_expr.op());
1745  out << ")";
1746  }
1747  else if(type.id()==ID_floatbv)
1748  {
1749  if(use_FPA_theory)
1750  {
1751  out << "(fp.abs ";
1752  convert_expr(abs_expr.op());
1753  out << ")";
1754  }
1755  else
1756  convert_floatbv(abs_expr);
1757  }
1758  else
1759  UNREACHABLE;
1760  }
1761  else if(expr.id()==ID_isnan)
1762  {
1763  const isnan_exprt &isnan_expr = to_isnan_expr(expr);
1764 
1765  const typet &op_type = isnan_expr.op().type();
1766 
1767  if(op_type.id()==ID_fixedbv)
1768  out << "false";
1769  else if(op_type.id()==ID_floatbv)
1770  {
1771  if(use_FPA_theory)
1772  {
1773  out << "(fp.isNaN ";
1774  convert_expr(isnan_expr.op());
1775  out << ")";
1776  }
1777  else
1778  convert_floatbv(isnan_expr);
1779  }
1780  else
1781  UNREACHABLE;
1782  }
1783  else if(expr.id()==ID_isfinite)
1784  {
1785  const isfinite_exprt &isfinite_expr = to_isfinite_expr(expr);
1786 
1787  const typet &op_type = isfinite_expr.op().type();
1788 
1789  if(op_type.id()==ID_fixedbv)
1790  out << "true";
1791  else if(op_type.id()==ID_floatbv)
1792  {
1793  if(use_FPA_theory)
1794  {
1795  out << "(and ";
1796 
1797  out << "(not (fp.isNaN ";
1798  convert_expr(isfinite_expr.op());
1799  out << "))";
1800 
1801  out << "(not (fp.isInf ";
1802  convert_expr(isfinite_expr.op());
1803  out << "))";
1804 
1805  out << ")";
1806  }
1807  else
1808  convert_floatbv(isfinite_expr);
1809  }
1810  else
1811  UNREACHABLE;
1812  }
1813  else if(expr.id()==ID_isinf)
1814  {
1815  const isinf_exprt &isinf_expr = to_isinf_expr(expr);
1816 
1817  const typet &op_type = isinf_expr.op().type();
1818 
1819  if(op_type.id()==ID_fixedbv)
1820  out << "false";
1821  else if(op_type.id()==ID_floatbv)
1822  {
1823  if(use_FPA_theory)
1824  {
1825  out << "(fp.isInfinite ";
1826  convert_expr(isinf_expr.op());
1827  out << ")";
1828  }
1829  else
1830  convert_floatbv(isinf_expr);
1831  }
1832  else
1833  UNREACHABLE;
1834  }
1835  else if(expr.id()==ID_isnormal)
1836  {
1837  const isnormal_exprt &isnormal_expr = to_isnormal_expr(expr);
1838 
1839  const typet &op_type = isnormal_expr.op().type();
1840 
1841  if(op_type.id()==ID_fixedbv)
1842  out << "true";
1843  else if(op_type.id()==ID_floatbv)
1844  {
1845  if(use_FPA_theory)
1846  {
1847  out << "(fp.isNormal ";
1848  convert_expr(isnormal_expr.op());
1849  out << ")";
1850  }
1851  else
1852  convert_floatbv(isnormal_expr);
1853  }
1854  else
1855  UNREACHABLE;
1856  }
1857  else if(expr.id()==ID_overflow_plus ||
1858  expr.id()==ID_overflow_minus)
1859  {
1860  const auto &op0 = to_binary_expr(expr).op0();
1861  const auto &op1 = to_binary_expr(expr).op1();
1862 
1864  expr.type().id() == ID_bool,
1865  "overflow plus and overflow minus expressions shall be of Boolean type");
1866 
1867  bool subtract=expr.id()==ID_overflow_minus;
1868  const typet &op_type = op0.type();
1869  std::size_t width=boolbv_width(op_type);
1870 
1871  if(op_type.id()==ID_signedbv)
1872  {
1873  // an overflow occurs if the top two bits of the extended sum differ
1874  out << "(let ((?sum (";
1875  out << (subtract?"bvsub":"bvadd");
1876  out << " ((_ sign_extend 1) ";
1877  convert_expr(op0);
1878  out << ")";
1879  out << " ((_ sign_extend 1) ";
1880  convert_expr(op1);
1881  out << ")))) "; // sign_extend, bvadd/sub let2
1882  out << "(not (= "
1883  "((_ extract " << width << " " << width << ") ?sum) "
1884  "((_ extract " << (width-1) << " " << (width-1) << ") ?sum)";
1885  out << ")))"; // =, not, let
1886  }
1887  else if(op_type.id()==ID_unsignedbv ||
1888  op_type.id()==ID_pointer)
1889  {
1890  // overflow is simply carry-out
1891  out << "(= ";
1892  out << "((_ extract " << width << " " << width << ") ";
1893  out << "(" << (subtract?"bvsub":"bvadd");
1894  out << " ((_ zero_extend 1) ";
1895  convert_expr(op0);
1896  out << ")";
1897  out << " ((_ zero_extend 1) ";
1898  convert_expr(op1);
1899  out << ")))"; // zero_extend, bvsub/bvadd, extract
1900  out << " #b1)"; // =
1901  }
1902  else
1904  false,
1905  "overflow check should not be performed on unsupported type",
1906  op_type.id_string());
1907  }
1908  else if(expr.id()==ID_overflow_mult)
1909  {
1910  const auto &op0 = to_binary_expr(expr).op0();
1911  const auto &op1 = to_binary_expr(expr).op1();
1912 
1914  expr.type().id() == ID_bool,
1915  "overflow mult expression shall be of Boolean type");
1916 
1917  // No better idea than to multiply with double the bits and then compare
1918  // with max value.
1919 
1920  const typet &op_type = op0.type();
1921  std::size_t width=boolbv_width(op_type);
1922 
1923  if(op_type.id()==ID_signedbv)
1924  {
1925  out << "(let ( (prod (bvmul ((_ sign_extend " << width << ") ";
1926  convert_expr(op0);
1927  out << ") ((_ sign_extend " << width << ") ";
1928  convert_expr(op1);
1929  out << ")) )) ";
1930  out << "(or (bvsge prod (_ bv" << power(2, width-1) << " "
1931  << width*2 << "))";
1932  out << " (bvslt prod (bvneg (_ bv" << power(2, width-1) << " "
1933  << width*2 << ")))))";
1934  }
1935  else if(op_type.id()==ID_unsignedbv)
1936  {
1937  out << "(bvuge (bvmul ((_ zero_extend " << width << ") ";
1938  convert_expr(op0);
1939  out << ") ((_ zero_extend " << width << ") ";
1940  convert_expr(op1);
1941  out << ")) (_ bv" << power(2, width) << " " << width*2 << "))";
1942  }
1943  else
1945  false,
1946  "overflow check should not be performed on unsupported type",
1947  op_type.id_string());
1948  }
1949  else if(expr.id()==ID_array)
1950  {
1951  defined_expressionst::const_iterator it=defined_expressions.find(expr);
1952  CHECK_RETURN(it != defined_expressions.end());
1953  out << it->second;
1954  }
1955  else if(expr.id()==ID_literal)
1956  {
1957  convert_literal(to_literal_expr(expr).get_literal());
1958  }
1959  else if(expr.id()==ID_forall ||
1960  expr.id()==ID_exists)
1961  {
1962  const quantifier_exprt &quantifier_expr = to_quantifier_expr(expr);
1963 
1965  // NOLINTNEXTLINE(readability/throw)
1966  throw "MathSAT does not support quantifiers";
1967 
1968  if(quantifier_expr.id() == ID_forall)
1969  out << "(forall ";
1970  else if(quantifier_expr.id() == ID_exists)
1971  out << "(exists ";
1972 
1973  exprt bound = quantifier_expr.symbol();
1974 
1975  out << "((";
1976  convert_expr(bound);
1977  out << " ";
1978  convert_type(bound.type());
1979  out << ")) ";
1980 
1981  convert_expr(quantifier_expr.where());
1982 
1983  out << ")";
1984  }
1985  else if(expr.id()==ID_vector)
1986  {
1987  const vector_exprt &vector_expr = to_vector_expr(expr);
1988  const vector_typet &vector_type = to_vector_type(vector_expr.type());
1989 
1990  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
1991 
1993  size == vector_expr.operands().size(),
1994  "size indicated by type shall be equal to the number of operands");
1995 
1996  if(use_datatypes)
1997  {
1998  const std::string &smt_typename = datatype_map.at(vector_type);
1999 
2000  out << "(mk-" << smt_typename;
2001  }
2002  else
2003  out << "(concat";
2004 
2005  // build component-by-component
2006  forall_operands(it, vector_expr)
2007  {
2008  out << " ";
2009  convert_expr(*it);
2010  }
2011 
2012  out << ")"; // mk-... or concat
2013  }
2014  else if(expr.id()==ID_object_size)
2015  {
2016  out << "|" << object_sizes[expr] << "|";
2017  }
2018  else if(expr.id()==ID_let)
2019  {
2020  const let_exprt &let_expr=to_let_expr(expr);
2021  const auto &variables = let_expr.variables();
2022  const auto &values = let_expr.values();
2023 
2024  out << "(let (";
2025  bool first = true;
2026 
2027  for(auto &binding : make_range(variables).zip(values))
2028  {
2029  if(first)
2030  first = false;
2031  else
2032  out << ' ';
2033 
2034  out << '(';
2035  convert_expr(binding.first);
2036  out << ' ';
2037  convert_expr(binding.second);
2038  out << ')';
2039  }
2040 
2041  out << ") "; // bindings
2042 
2043  convert_expr(let_expr.where());
2044  out << ')'; // let
2045  }
2046  else if(expr.id()==ID_constraint_select_one)
2047  {
2049  "smt2_convt::convert_expr: '" + expr.id_string() +
2050  "' is not yet supported");
2051  }
2052  else if(expr.id() == ID_bswap)
2053  {
2054  const bswap_exprt &bswap_expr = to_bswap_expr(expr);
2055 
2057  bswap_expr.op().type() == bswap_expr.type(),
2058  "operand of byte swap expression shall have same type as the expression");
2059 
2060  // first 'let' the operand
2061  out << "(let ((bswap_op ";
2062  convert_expr(bswap_expr.op());
2063  out << ")) ";
2064 
2065  if(
2066  bswap_expr.type().id() == ID_signedbv ||
2067  bswap_expr.type().id() == ID_unsignedbv)
2068  {
2069  const std::size_t width =
2070  to_bitvector_type(bswap_expr.type()).get_width();
2071 
2072  const std::size_t bits_per_byte = bswap_expr.get_bits_per_byte();
2073 
2074  // width must be multiple of bytes
2076  width % bits_per_byte == 0,
2077  "bit width indicated by type of bswap expression should be a multiple "
2078  "of the number of bits per byte");
2079 
2080  const std::size_t bytes = width / bits_per_byte;
2081 
2082  if(bytes <= 1)
2083  out << "bswap_op";
2084  else
2085  {
2086  // do a parallel 'let' for each byte
2087  out << "(let (";
2088 
2089  for(std::size_t byte = 0; byte < bytes; byte++)
2090  {
2091  if(byte != 0)
2092  out << ' ';
2093  out << "(bswap_byte_" << byte << ' ';
2094  out << "((_ extract " << (byte * bits_per_byte + (bits_per_byte - 1))
2095  << " " << (byte * bits_per_byte) << ") bswap_op)";
2096  out << ')';
2097  }
2098 
2099  out << ") ";
2100 
2101  // now stitch back together with 'concat'
2102  out << "(concat";
2103 
2104  for(std::size_t byte = 0; byte < bytes; byte++)
2105  out << " bswap_byte_" << byte;
2106 
2107  out << ')'; // concat
2108  out << ')'; // let bswap_byte_*
2109  }
2110  }
2111  else
2112  UNEXPECTEDCASE("bswap must get bitvector operand");
2113 
2114  out << ')'; // let bswap_op
2115  }
2116  else if(expr.id() == ID_popcount)
2117  {
2118  convert_expr(simplify_expr(to_popcount_expr(expr).lower(), ns));
2119  }
2120  else if(expr.id() == ID_count_leading_zeros)
2121  {
2123  }
2124  else if(expr.id() == ID_count_trailing_zeros)
2125  {
2127  }
2128  else
2130  false,
2131  "smt2_convt::convert_expr should not be applied to unsupported type",
2132  expr.id_string());
2133 }
2134 
2136 {
2137  const exprt &src = expr.op();
2138 
2139  typet dest_type = expr.type();
2140  if(dest_type.id()==ID_c_enum_tag)
2141  dest_type=ns.follow_tag(to_c_enum_tag_type(dest_type));
2142 
2143  typet src_type = src.type();
2144  if(src_type.id()==ID_c_enum_tag)
2145  src_type=ns.follow_tag(to_c_enum_tag_type(src_type));
2146 
2147  if(dest_type.id()==ID_bool)
2148  {
2149  // this is comparison with zero
2150  if(src_type.id()==ID_signedbv ||
2151  src_type.id()==ID_unsignedbv ||
2152  src_type.id()==ID_c_bool ||
2153  src_type.id()==ID_fixedbv ||
2154  src_type.id()==ID_pointer ||
2155  src_type.id()==ID_integer)
2156  {
2157  out << "(not (= ";
2158  convert_expr(src);
2159  out << " ";
2160  convert_expr(from_integer(0, src_type));
2161  out << "))";
2162  }
2163  else if(src_type.id()==ID_floatbv)
2164  {
2165  if(use_FPA_theory)
2166  {
2167  out << "(not (fp.isZero ";
2168  convert_expr(src);
2169  out << "))";
2170  }
2171  else
2172  convert_floatbv(expr);
2173  }
2174  else
2175  {
2176  UNEXPECTEDCASE("TODO typecast1 "+src_type.id_string()+" -> bool");
2177  }
2178  }
2179  else if(dest_type.id()==ID_c_bool)
2180  {
2181  std::size_t to_width=boolbv_width(dest_type);
2182  out << "(ite ";
2183  out << "(not (= ";
2184  convert_expr(src);
2185  out << " ";
2186  convert_expr(from_integer(0, src_type));
2187  out << ")) "; // not, =
2188  out << " (_ bv1 " << to_width << ")";
2189  out << " (_ bv0 " << to_width << ")";
2190  out << ")"; // ite
2191  }
2192  else if(dest_type.id()==ID_signedbv ||
2193  dest_type.id()==ID_unsignedbv ||
2194  dest_type.id()==ID_c_enum ||
2195  dest_type.id()==ID_bv)
2196  {
2197  std::size_t to_width=boolbv_width(dest_type);
2198 
2199  if(src_type.id()==ID_signedbv || // from signedbv
2200  src_type.id()==ID_unsignedbv || // from unsigedbv
2201  src_type.id()==ID_c_bool ||
2202  src_type.id()==ID_c_enum ||
2203  src_type.id()==ID_bv)
2204  {
2205  std::size_t from_width=boolbv_width(src_type);
2206 
2207  if(from_width==to_width)
2208  convert_expr(src); // ignore
2209  else if(from_width<to_width) // extend
2210  {
2211  if(src_type.id()==ID_signedbv)
2212  out << "((_ sign_extend ";
2213  else
2214  out << "((_ zero_extend ";
2215 
2216  out << (to_width-from_width)
2217  << ") "; // ind
2218  convert_expr(src);
2219  out << ")";
2220  }
2221  else // chop off extra bits
2222  {
2223  out << "((_ extract " << (to_width-1) << " 0) ";
2224  convert_expr(src);
2225  out << ")";
2226  }
2227  }
2228  else if(src_type.id()==ID_fixedbv) // from fixedbv to int
2229  {
2230  const fixedbv_typet &fixedbv_type=to_fixedbv_type(src_type);
2231 
2232  std::size_t from_width=fixedbv_type.get_width();
2233  std::size_t from_integer_bits=fixedbv_type.get_integer_bits();
2234  std::size_t from_fraction_bits=fixedbv_type.get_fraction_bits();
2235 
2236  // we might need to round up in case of negative numbers
2237  // e.g., (int)(-1.00001)==1
2238 
2239  out << "(let ((?tcop ";
2240  convert_expr(src);
2241  out << ")) ";
2242 
2243  out << "(bvadd ";
2244 
2245  if(to_width>from_integer_bits)
2246  {
2247  out << "((_ sign_extend "
2248  << (to_width-from_integer_bits) << ") ";
2249  out << "((_ extract " << (from_width-1) << " "
2250  << from_fraction_bits << ") ";
2251  convert_expr(src);
2252  out << "))";
2253  }
2254  else
2255  {
2256  out << "((_ extract " << (from_fraction_bits+to_width-1)
2257  << " " << from_fraction_bits << ") ";
2258  convert_expr(src);
2259  out << ")";
2260  }
2261 
2262  out << " (ite (and ";
2263 
2264  // some fraction bit is not zero
2265  out << "(not (= ((_ extract " << (from_fraction_bits-1) << " 0) ?tcop) "
2266  "(_ bv0 " << from_fraction_bits << ")))";
2267 
2268  // number negative
2269  out << " (= ((_ extract " << (from_width-1) << " " << (from_width-1)
2270  << ") ?tcop) #b1)";
2271 
2272  out << ")"; // and
2273 
2274  out << " (_ bv1 " << to_width << ") (_ bv0 " << to_width << "))"; // ite
2275  out << ")"; // bvadd
2276  out << ")"; // let
2277  }
2278  else if(src_type.id()==ID_floatbv) // from floatbv to int
2279  {
2280  if(dest_type.id()==ID_bv)
2281  {
2282  // this is _NOT_ a semantic conversion, but bit-wise
2283 
2284  if(use_FPA_theory)
2285  {
2286  // This conversion is non-trivial as it requires creating a
2287  // new bit-vector variable and then asserting that it converts
2288  // to the required floating-point number.
2289  SMT2_TODO("bit-wise floatbv to bv");
2290  }
2291  else
2292  {
2293  // straight-forward if width matches
2294  convert_expr(src);
2295  }
2296  }
2297  else if(dest_type.id()==ID_signedbv)
2298  {
2299  // this should be floatbv_typecast, not typecast
2301  "typecast unexpected "+src_type.id_string()+" -> "+
2302  dest_type.id_string());
2303  }
2304  else if(dest_type.id()==ID_unsignedbv)
2305  {
2306  // this should be floatbv_typecast, not typecast
2308  "typecast unexpected "+src_type.id_string()+" -> "+
2309  dest_type.id_string());
2310  }
2311  }
2312  else if(src_type.id()==ID_bool) // from boolean to int
2313  {
2314  out << "(ite ";
2315  convert_expr(src);
2316 
2317  if(dest_type.id()==ID_fixedbv)
2318  {
2319  fixedbv_spect spec(to_fixedbv_type(dest_type));
2320  out << " (concat (_ bv1 "
2321  << spec.integer_bits << ") " <<
2322  "(_ bv0 " << spec.get_fraction_bits() << ")) " <<
2323  "(_ bv0 " << spec.width << ")";
2324  }
2325  else
2326  {
2327  out << " (_ bv1 " << to_width << ")";
2328  out << " (_ bv0 " << to_width << ")";
2329  }
2330 
2331  out << ")";
2332  }
2333  else if(src_type.id()==ID_pointer) // from pointer to int
2334  {
2335  std::size_t from_width=boolbv_width(src_type);
2336 
2337  if(from_width<to_width) // extend
2338  {
2339  out << "((_ sign_extend ";
2340  out << (to_width-from_width)
2341  << ") ";
2342  convert_expr(src);
2343  out << ")";
2344  }
2345  else // chop off extra bits
2346  {
2347  out << "((_ extract " << (to_width-1) << " 0) ";
2348  convert_expr(src);
2349  out << ")";
2350  }
2351  }
2352  else if(src_type.id()==ID_integer) // from integer to bit-vector
2353  {
2354  // must be constant
2355  if(src.is_constant())
2356  {
2357  mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(src));
2358  out << "(_ bv" << i << " " << to_width << ")";
2359  }
2360  else
2361  SMT2_TODO("can't convert non-constant integer to bitvector");
2362  }
2363  else if(
2364  src_type.id() == ID_struct ||
2365  src_type.id() == ID_struct_tag) // flatten a struct to a bit-vector
2366  {
2367  if(use_datatypes)
2368  {
2369  INVARIANT(
2370  boolbv_width(src_type) == boolbv_width(dest_type),
2371  "bit vector with of source and destination type shall be equal");
2372  flatten2bv(src);
2373  }
2374  else
2375  {
2376  INVARIANT(
2377  boolbv_width(src_type) == boolbv_width(dest_type),
2378  "bit vector with of source and destination type shall be equal");
2379  convert_expr(src); // nothing else to do!
2380  }
2381  }
2382  else if(
2383  src_type.id() == ID_union ||
2384  src_type.id() == ID_union_tag) // flatten a union
2385  {
2386  INVARIANT(
2387  boolbv_width(src_type) == boolbv_width(dest_type),
2388  "bit vector with of source and destination type shall be equal");
2389  convert_expr(src); // nothing else to do!
2390  }
2391  else if(src_type.id()==ID_c_bit_field)
2392  {
2393  std::size_t from_width=boolbv_width(src_type);
2394 
2395  if(from_width==to_width)
2396  convert_expr(src); // ignore
2397  else
2398  {
2400  typecast_exprt tmp(typecast_exprt(src, t), dest_type);
2401  convert_typecast(tmp);
2402  }
2403  }
2404  else
2405  {
2406  std::ostringstream e_str;
2407  e_str << src_type.id() << " -> " << dest_type.id()
2408  << " src == " << format(src);
2409  UNEXPECTEDCASE("TODO typecast2 " + e_str.str());
2410  }
2411  }
2412  else if(dest_type.id()==ID_fixedbv) // to fixedbv
2413  {
2414  const fixedbv_typet &fixedbv_type=to_fixedbv_type(dest_type);
2415  std::size_t to_fraction_bits=fixedbv_type.get_fraction_bits();
2416  std::size_t to_integer_bits=fixedbv_type.get_integer_bits();
2417 
2418  if(src_type.id()==ID_unsignedbv ||
2419  src_type.id()==ID_signedbv ||
2420  src_type.id()==ID_c_enum)
2421  {
2422  // integer to fixedbv
2423 
2424  std::size_t from_width=to_bitvector_type(src_type).get_width();
2425  out << "(concat ";
2426 
2427  if(from_width==to_integer_bits)
2428  convert_expr(src);
2429  else if(from_width>to_integer_bits)
2430  {
2431  // too many integer bits
2432  out << "((_ extract " << (to_integer_bits-1) << " 0) ";
2433  convert_expr(src);
2434  out << ")";
2435  }
2436  else
2437  {
2438  // too few integer bits
2439  INVARIANT(
2440  from_width < to_integer_bits,
2441  "from_width should be smaller than to_integer_bits as other case "
2442  "have been handled above");
2443  if(dest_type.id()==ID_unsignedbv)
2444  {
2445  out << "(_ zero_extend "
2446  << (to_integer_bits-from_width) << ") ";
2447  convert_expr(src);
2448  out << ")";
2449  }
2450  else
2451  {
2452  out << "((_ sign_extend "
2453  << (to_integer_bits-from_width) << ") ";
2454  convert_expr(src);
2455  out << ")";
2456  }
2457  }
2458 
2459  out << "(_ bv0 " << to_fraction_bits << ")";
2460  out << ")"; // concat
2461  }
2462  else if(src_type.id()==ID_bool) // bool to fixedbv
2463  {
2464  out << "(concat (concat"
2465  << " (_ bv0 " << (to_integer_bits-1) << ") ";
2466  flatten2bv(src); // produces #b0 or #b1
2467  out << ") (_ bv0 "
2468  << to_fraction_bits
2469  << "))";
2470  }
2471  else if(src_type.id()==ID_fixedbv) // fixedbv to fixedbv
2472  {
2473  const fixedbv_typet &from_fixedbv_type=to_fixedbv_type(src_type);
2474  std::size_t from_fraction_bits=from_fixedbv_type.get_fraction_bits();
2475  std::size_t from_integer_bits=from_fixedbv_type.get_integer_bits();
2476  std::size_t from_width=from_fixedbv_type.get_width();
2477 
2478  out << "(let ((?tcop ";
2479  convert_expr(src);
2480  out << ")) ";
2481 
2482  out << "(concat ";
2483 
2484  if(to_integer_bits<=from_integer_bits)
2485  {
2486  out << "((_ extract "
2487  << (from_fraction_bits+to_integer_bits-1) << " "
2488  << from_fraction_bits
2489  << ") ?tcop)";
2490  }
2491  else
2492  {
2493  INVARIANT(
2494  to_integer_bits > from_integer_bits,
2495  "to_integer_bits should be greater than from_integer_bits as the"
2496  "other case has been handled above");
2497  out << "((_ sign_extend "
2498  << (to_integer_bits-from_integer_bits)
2499  << ") ((_ extract "
2500  << (from_width-1) << " "
2501  << from_fraction_bits
2502  << ") ?tcop))";
2503  }
2504 
2505  out << " ";
2506 
2507  if(to_fraction_bits<=from_fraction_bits)
2508  {
2509  out << "((_ extract "
2510  << (from_fraction_bits-1) << " "
2511  << (from_fraction_bits-to_fraction_bits)
2512  << ") ?tcop)";
2513  }
2514  else
2515  {
2516  INVARIANT(
2517  to_fraction_bits > from_fraction_bits,
2518  "to_fraction_bits should be greater than from_fraction_bits as the"
2519  "other case has been handled above");
2520  out << "(concat ((_ extract "
2521  << (from_fraction_bits-1) << " 0) ";
2522  convert_expr(src);
2523  out << ")"
2524  << " (_ bv0 " << to_fraction_bits-from_fraction_bits
2525  << "))";
2526  }
2527 
2528  out << "))"; // concat, let
2529  }
2530  else
2531  UNEXPECTEDCASE("unexpected typecast to fixedbv");
2532  }
2533  else if(dest_type.id()==ID_pointer)
2534  {
2535  std::size_t to_width=boolbv_width(dest_type);
2536 
2537  if(src_type.id()==ID_pointer) // pointer to pointer
2538  {
2539  // this just passes through
2540  convert_expr(src);
2541  }
2542  else if(
2543  src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv ||
2544  src_type.id() == ID_bv)
2545  {
2546  // integer to pointer
2547 
2548  std::size_t from_width=boolbv_width(src_type);
2549 
2550  if(from_width==to_width)
2551  convert_expr(src);
2552  else if(from_width<to_width)
2553  {
2554  out << "((_ sign_extend "
2555  << (to_width-from_width)
2556  << ") ";
2557  convert_expr(src);
2558  out << ")"; // sign_extend
2559  }
2560  else // from_width>to_width
2561  {
2562  out << "((_ extract " << to_width << " 0) ";
2563  convert_expr(src);
2564  out << ")"; // extract
2565  }
2566  }
2567  else
2568  UNEXPECTEDCASE("TODO typecast3 "+src_type.id_string()+" -> pointer");
2569  }
2570  else if(dest_type.id()==ID_range)
2571  {
2572  SMT2_TODO("range typecast");
2573  }
2574  else if(dest_type.id()==ID_floatbv)
2575  {
2576  // Typecast from integer to floating-point should have be been
2577  // converted to ID_floatbv_typecast during symbolic execution,
2578  // adding the rounding mode. See
2579  // smt2_convt::convert_floatbv_typecast.
2580  // The exception is bool and c_bool to float.
2581  const auto &dest_floatbv_type = to_floatbv_type(dest_type);
2582 
2583  if(src_type.id()==ID_bool)
2584  {
2585  constant_exprt val(irep_idt(), dest_type);
2586 
2587  ieee_floatt a(dest_floatbv_type);
2588 
2589  mp_integer significand;
2590  mp_integer exponent;
2591 
2592  out << "(ite ";
2593  convert_expr(src);
2594  out << " ";
2595 
2596  significand = 1;
2597  exponent = 0;
2598  a.build(significand, exponent);
2599  val.set_value(integer2bvrep(a.pack(), a.spec.width()));
2600 
2601  convert_constant(val);
2602  out << " ";
2603 
2604  significand = 0;
2605  exponent = 0;
2606  a.build(significand, exponent);
2607  val.set_value(integer2bvrep(a.pack(), a.spec.width()));
2608 
2609  convert_constant(val);
2610  out << ")";
2611  }
2612  else if(src_type.id()==ID_c_bool)
2613  {
2614  // turn into proper bool
2615  const typecast_exprt tmp(src, bool_typet());
2616  convert_typecast(typecast_exprt(tmp, dest_type));
2617  }
2618  else if(src_type.id() == ID_bv)
2619  {
2620  if(to_bv_type(src_type).get_width() != dest_floatbv_type.get_width())
2621  {
2622  UNEXPECTEDCASE("Typecast bv -> float with wrong width");
2623  }
2624 
2625  if(use_FPA_theory)
2626  {
2627  out << "((_ to_fp " << dest_floatbv_type.get_e() << " "
2628  << dest_floatbv_type.get_f() + 1 << ") ";
2629  convert_expr(src);
2630  out << ')';
2631  }
2632  else
2633  convert_expr(src);
2634  }
2635  else
2636  UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float");
2637  }
2638  else if(dest_type.id()==ID_integer)
2639  {
2640  if(src_type.id()==ID_bool)
2641  {
2642  out << "(ite ";
2643  convert_expr(src);
2644  out <<" 1 0)";
2645  }
2646  else
2647  UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> integer");
2648  }
2649  else if(dest_type.id()==ID_c_bit_field)
2650  {
2651  std::size_t from_width=boolbv_width(src_type);
2652  std::size_t to_width=boolbv_width(dest_type);
2653 
2654  if(from_width==to_width)
2655  convert_expr(src); // ignore
2656  else
2657  {
2659  typecast_exprt tmp(typecast_exprt(src, t), dest_type);
2660  convert_typecast(tmp);
2661  }
2662  }
2663  else
2665  "TODO typecast8 "+src_type.id_string()+" -> "+dest_type.id_string());
2666 }
2667 
2669 {
2670  const exprt &src=expr.op();
2671  // const exprt &rounding_mode=expr.rounding_mode();
2672  const typet &src_type=src.type();
2673  const typet &dest_type=expr.type();
2674 
2675  if(dest_type.id()==ID_floatbv)
2676  {
2677  if(src_type.id()==ID_floatbv)
2678  {
2679  // float to float
2680 
2681  /* ISO 9899:1999
2682  * 6.3.1.5 Real floating types
2683  * 1 When a float is promoted to double or long double, or a
2684  * double is promoted to long double, its value is unchanged.
2685  *
2686  * 2 When a double is demoted to float, a long double is
2687  * demoted to double or float, or a value being represented in
2688  * greater precision and range than required by its semantic
2689  * type (see 6.3.1.8) is explicitly converted to its semantic
2690  * type, if the value being converted can be represented
2691  * exactly in the new type, it is unchanged. If the value
2692  * being converted is in the range of values that can be
2693  * represented but cannot be represented exactly, the result
2694  * is either the nearest higher or nearest lower representable
2695  * value, chosen in an implementation-defined manner. If the
2696  * value being converted is outside the range of values that
2697  * can be represented, the behavior is undefined.
2698  */
2699 
2700  const floatbv_typet &dst=to_floatbv_type(dest_type);
2701 
2702  if(use_FPA_theory)
2703  {
2704  out << "((_ to_fp " << dst.get_e() << " "
2705  << dst.get_f() + 1 << ") ";
2707  out << " ";
2708  convert_expr(src);
2709  out << ")";
2710  }
2711  else
2712  convert_floatbv(expr);
2713  }
2714  else if(src_type.id()==ID_unsignedbv)
2715  {
2716  // unsigned to float
2717 
2718  /* ISO 9899:1999
2719  * 6.3.1.4 Real floating and integer
2720  * 2 When a value of integer type is converted to a real
2721  * floating type, if the value being converted can be
2722  * represented exactly in the new type, it is unchanged. If the
2723  * value being converted is in the range of values that can be
2724  * represented but cannot be represented exactly, the result is
2725  * either the nearest higher or nearest lower representable
2726  * value, chosen in an implementation-defined manner. If the
2727  * value being converted is outside the range of values that can
2728  * be represented, the behavior is undefined.
2729  */
2730 
2731  const floatbv_typet &dst=to_floatbv_type(dest_type);
2732 
2733  if(use_FPA_theory)
2734  {
2735  out << "((_ to_fp_unsigned " << dst.get_e() << " "
2736  << dst.get_f() + 1 << ") ";
2738  out << " ";
2739  convert_expr(src);
2740  out << ")";
2741  }
2742  else
2743  convert_floatbv(expr);
2744  }
2745  else if(src_type.id()==ID_signedbv)
2746  {
2747  // signed to float
2748 
2749  const floatbv_typet &dst=to_floatbv_type(dest_type);
2750 
2751  if(use_FPA_theory)
2752  {
2753  out << "((_ to_fp " << dst.get_e() << " "
2754  << dst.get_f() + 1 << ") ";
2756  out << " ";
2757  convert_expr(src);
2758  out << ")";
2759  }
2760  else
2761  convert_floatbv(expr);
2762  }
2763  else if(src_type.id()==ID_c_enum_tag)
2764  {
2765  // enum to float
2766 
2767  // We first convert to 'underlying type'
2768  floatbv_typecast_exprt tmp=expr;
2769  tmp.op()=
2771  src,
2772  ns.follow_tag(to_c_enum_tag_type(src_type)).subtype());
2774  }
2775  else
2777  "TODO typecast11 "+src_type.id_string()+" -> "+dest_type.id_string());
2778  }
2779  else if(dest_type.id()==ID_signedbv)
2780  {
2781  if(use_FPA_theory)
2782  {
2783  std::size_t dest_width=to_signedbv_type(dest_type).get_width();
2784  out << "((_ fp.to_sbv " << dest_width << ") ";
2786  out << " ";
2787  convert_expr(src);
2788  out << ")";
2789  }
2790  else
2791  convert_floatbv(expr);
2792  }
2793  else if(dest_type.id()==ID_unsignedbv)
2794  {
2795  if(use_FPA_theory)
2796  {
2797  std::size_t dest_width=to_unsignedbv_type(dest_type).get_width();
2798  out << "((_ fp.to_ubv " << dest_width << ") ";
2800  out << " ";
2801  convert_expr(src);
2802  out << ")";
2803  }
2804  else
2805  convert_floatbv(expr);
2806  }
2807  else
2808  {
2810  "TODO typecast12 "+src_type.id_string()+" -> "+dest_type.id_string());
2811  }
2812 }
2813 
2815 {
2816  const struct_typet &struct_type = to_struct_type(ns.follow(expr.type()));
2817 
2818  const struct_typet::componentst &components=
2819  struct_type.components();
2820 
2822  components.size() == expr.operands().size(),
2823  "number of struct components as indicated by the struct type shall be equal"
2824  "to the number of operands of the struct expression");
2825 
2826  DATA_INVARIANT(!components.empty(), "struct shall have struct components");
2827 
2828  if(use_datatypes)
2829  {
2830  const std::string &smt_typename = datatype_map.at(struct_type);
2831 
2832  // use the constructor for the Z3 datatype
2833  out << "(mk-" << smt_typename;
2834 
2835  std::size_t i=0;
2836  for(struct_typet::componentst::const_iterator
2837  it=components.begin();
2838  it!=components.end();
2839  it++, i++)
2840  {
2841  out << " ";
2842  convert_expr(expr.operands()[i]);
2843  }
2844 
2845  out << ")";
2846  }
2847  else
2848  {
2849  if(components.size()==1)
2850  convert_expr(expr.op0());
2851  else
2852  {
2853  // SMT-LIB 2 concat is binary only
2854  for(std::size_t i=components.size(); i>1; i--)
2855  {
2856  out << "(concat ";
2857 
2858  exprt op=expr.operands()[i-1];
2859 
2860  // may need to flatten array-theory arrays in there
2861  if(op.type().id() == ID_array)
2862  flatten_array(op);
2863  else
2864  convert_expr(op);
2865 
2866  out << " ";
2867  }
2868 
2869  convert_expr(expr.op0());
2870 
2871  for(std::size_t i=1; i<components.size(); i++)
2872  out << ")";
2873  }
2874  }
2875 }
2876 
2879 {
2880  const array_typet &array_type = to_array_type(expr.type());
2881  const auto &size_expr = array_type.size();
2882  PRECONDITION(size_expr.id() == ID_constant);
2883 
2884  mp_integer size = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
2885  CHECK_RETURN_WITH_DIAGNOSTICS(size != 0, "can't convert zero-sized array");
2886 
2887  out << "(let ((?far ";
2888  convert_expr(expr);
2889  out << ")) ";
2890 
2891  for(mp_integer i=size; i!=0; --i)
2892  {
2893  if(i!=1)
2894  out << "(concat ";
2895  out << "(select ?far ";
2896  convert_expr(from_integer(i-1, array_type.size().type()));
2897  out << ")";
2898  if(i!=1)
2899  out << " ";
2900  }
2901 
2902  // close the many parentheses
2903  for(mp_integer i=size; i>1; --i)
2904  out << ")";
2905 
2906  out << ")"; // let
2907 }
2908 
2910 {
2911  const union_typet &union_type = to_union_type(ns.follow(expr.type()));
2912  const exprt &op=expr.op();
2913 
2914  std::size_t total_width=boolbv_width(union_type);
2916  total_width != 0, "failed to get union width for union");
2917 
2918  std::size_t member_width=boolbv_width(op.type());
2920  member_width != 0, "failed to get union member width for union");
2921 
2922  if(total_width==member_width)
2923  {
2924  flatten2bv(op);
2925  }
2926  else
2927  {
2928  // we will pad with zeros, but non-det would be better
2929  INVARIANT(
2930  total_width > member_width,
2931  "total_width should be greater than member_width as member_width can be"
2932  "at most as large as total_width and the other case has been handled "
2933  "above");
2934  out << "(concat ";
2935  out << "(_ bv0 "
2936  << (total_width-member_width) << ") ";
2937  flatten2bv(op);
2938  out << ")";
2939  }
2940 }
2941 
2943 {
2944  const typet &expr_type=expr.type();
2945 
2946  if(expr_type.id()==ID_unsignedbv ||
2947  expr_type.id()==ID_signedbv ||
2948  expr_type.id()==ID_bv ||
2949  expr_type.id()==ID_c_enum ||
2950  expr_type.id()==ID_c_enum_tag ||
2951  expr_type.id()==ID_c_bool ||
2952  expr_type.id()==ID_c_bit_field)
2953  {
2954  const std::size_t width = boolbv_width(expr_type);
2955 
2956  const mp_integer value = bvrep2integer(expr.get_value(), width, false);
2957 
2958  out << "(_ bv" << value
2959  << " " << width << ")";
2960  }
2961  else if(expr_type.id()==ID_fixedbv)
2962  {
2963  const fixedbv_spect spec(to_fixedbv_type(expr_type));
2964 
2965  const mp_integer v = bvrep2integer(expr.get_value(), spec.width, false);
2966 
2967  out << "(_ bv" << v << " " << spec.width << ")";
2968  }
2969  else if(expr_type.id()==ID_floatbv)
2970  {
2971  const floatbv_typet &floatbv_type=
2972  to_floatbv_type(expr_type);
2973 
2974  if(use_FPA_theory)
2975  {
2976  /* CBMC stores floating point literals in the most
2977  computationally useful form; biased exponents and
2978  significands including the hidden bit. Thus some encoding
2979  is needed to get to IEEE-754 style representations. */
2980 
2981  ieee_floatt v=ieee_floatt(expr);
2982  size_t e=floatbv_type.get_e();
2983  size_t f=floatbv_type.get_f()+1;
2984 
2985  /* Should be sufficient, but not currently supported by mathsat */
2986  #if 0
2987  mp_integer binary = v.pack();
2988 
2989  out << "((_ to_fp " << e << " " << f << ")"
2990  << " #b" << integer2binary(v.pack(), v.spec.width()) << ")";
2991  #endif
2992 
2993  if(v.is_NaN())
2994  {
2995  out << "(_ NaN " << e << " " << f << ")";
2996  }
2997  else if(v.is_infinity())
2998  {
2999  if(v.get_sign())
3000  out << "(_ -oo " << e << " " << f << ")";
3001  else
3002  out << "(_ +oo " << e << " " << f << ")";
3003  }
3004  else
3005  {
3006  // Zero, normal or subnormal
3007 
3008  mp_integer binary = v.pack();
3009  std::string binaryString(integer2binary(v.pack(), v.spec.width()));
3010 
3011  out << "(fp "
3012  << "#b" << binaryString.substr(0, 1) << " "
3013  << "#b" << binaryString.substr(1, e) << " "
3014  << "#b" << binaryString.substr(1+e, f-1) << ")";
3015  }
3016  }
3017  else
3018  {
3019  // produce corresponding bit-vector
3020  const ieee_float_spect spec(floatbv_type);
3021  const mp_integer v = bvrep2integer(expr.get_value(), spec.width(), false);
3022  out << "(_ bv" << v << " " << spec.width() << ")";
3023  }
3024  }
3025  else if(expr_type.id()==ID_pointer)
3026  {
3027  const irep_idt &value = expr.get_value();
3028 
3029  if(value==ID_NULL)
3030  {
3031  out << "(_ bv0 " << boolbv_width(expr_type)
3032  << ")";
3033  }
3034  else
3035  UNEXPECTEDCASE("unknown pointer constant: "+id2string(value));
3036  }
3037  else if(expr_type.id()==ID_bool)
3038  {
3039  if(expr.is_true())
3040  out << "true";
3041  else if(expr.is_false())
3042  out << "false";
3043  else
3044  UNEXPECTEDCASE("unknown Boolean constant");
3045  }
3046  else if(expr_type.id()==ID_array)
3047  {
3048  defined_expressionst::const_iterator it=defined_expressions.find(expr);
3049  CHECK_RETURN(it != defined_expressions.end());
3050  out << it->second;
3051  }
3052  else if(expr_type.id()==ID_rational)
3053  {
3054  std::string value=id2string(expr.get_value());
3055  const bool negative = has_prefix(value, "-");
3056 
3057  if(negative)
3058  out << "(- ";
3059 
3060  size_t pos=value.find("/");
3061 
3062  if(pos==std::string::npos)
3063  out << value << ".0";
3064  else
3065  {
3066  out << "(/ " << value.substr(0, pos) << ".0 "
3067  << value.substr(pos+1) << ".0)";
3068  }
3069 
3070  if(negative)
3071  out << ')';
3072  }
3073  else if(expr_type.id()==ID_integer)
3074  {
3075  const auto value = id2string(expr.get_value());
3076 
3077  // SMT2 has no negative integer literals
3078  if(has_prefix(value, "-"))
3079  out << "(- " << value.substr(1, std::string::npos) << ')';
3080  else
3081  out << value;
3082  }
3083  else
3084  UNEXPECTEDCASE("unknown constant: "+expr_type.id_string());
3085 }
3086 
3088 {
3089  if(expr.type().id() == ID_integer)
3090  {
3091  out << "(mod ";
3092  convert_expr(expr.op0());
3093  out << ' ';
3094  convert_expr(expr.op1());
3095  out << ')';
3096  }
3097  else
3099  "unsupported type for euclidean_mod: " + expr.type().id_string());
3100 }
3101 
3103 {
3104  if(expr.type().id()==ID_unsignedbv ||
3105  expr.type().id()==ID_signedbv)
3106  {
3107  if(expr.type().id()==ID_unsignedbv)
3108  out << "(bvurem ";
3109  else
3110  out << "(bvsrem ";
3111 
3112  convert_expr(expr.op0());
3113  out << " ";
3114  convert_expr(expr.op1());
3115  out << ")";
3116  }
3117  else
3118  UNEXPECTEDCASE("unsupported type for mod: "+expr.type().id_string());
3119 }
3120 
3122 {
3123  std::vector<std::size_t> dynamic_objects;
3124  pointer_logic.get_dynamic_objects(dynamic_objects);
3125 
3126  if(dynamic_objects.empty())
3127  out << "false";
3128  else
3129  {
3130  std::size_t pointer_width = boolbv_width(expr.op().type());
3131 
3132  out << "(let ((?obj ((_ extract "
3133  << pointer_width-1 << " "
3134  << pointer_width-config.bv_encoding.object_bits << ") ";
3135  convert_expr(expr.op());
3136  out << "))) ";
3137 
3138  if(dynamic_objects.size()==1)
3139  {
3140  out << "(= (_ bv" << dynamic_objects.front()
3141  << " " << config.bv_encoding.object_bits << ") ?obj)";
3142  }
3143  else
3144  {
3145  out << "(or";
3146 
3147  for(const auto &object : dynamic_objects)
3148  out << " (= (_ bv" << object
3149  << " " << config.bv_encoding.object_bits << ") ?obj)";
3150 
3151  out << ")"; // or
3152  }
3153 
3154  out << ")"; // let
3155  }
3156 }
3157 
3159 {
3160  const typet &op_type=expr.op0().type();
3161 
3162  if(op_type.id()==ID_unsignedbv ||
3163  op_type.id()==ID_pointer ||
3164  op_type.id()==ID_bv)
3165  {
3166  out << "(";
3167  if(expr.id()==ID_le)
3168  out << "bvule";
3169  else if(expr.id()==ID_lt)
3170  out << "bvult";
3171  else if(expr.id()==ID_ge)
3172  out << "bvuge";
3173  else if(expr.id()==ID_gt)
3174  out << "bvugt";
3175 
3176  out << " ";
3177  convert_expr(expr.op0());
3178  out << " ";
3179  convert_expr(expr.op1());
3180  out << ")";
3181  }
3182  else if(op_type.id()==ID_signedbv ||
3183  op_type.id()==ID_fixedbv)
3184  {
3185  out << "(";
3186  if(expr.id()==ID_le)
3187  out << "bvsle";
3188  else if(expr.id()==ID_lt)
3189  out << "bvslt";
3190  else if(expr.id()==ID_ge)
3191  out << "bvsge";
3192  else if(expr.id()==ID_gt)
3193  out << "bvsgt";
3194 
3195  out << " ";
3196  convert_expr(expr.op0());
3197  out << " ";
3198  convert_expr(expr.op1());
3199  out << ")";
3200  }
3201  else if(op_type.id()==ID_floatbv)
3202  {
3203  if(use_FPA_theory)
3204  {
3205  out << "(";
3206  if(expr.id()==ID_le)
3207  out << "fp.leq";
3208  else if(expr.id()==ID_lt)
3209  out << "fp.lt";
3210  else if(expr.id()==ID_ge)
3211  out << "fp.geq";
3212  else if(expr.id()==ID_gt)
3213  out << "fp.gt";
3214 
3215  out << " ";
3216  convert_expr(expr.op0());
3217  out << " ";
3218  convert_expr(expr.op1());
3219  out << ")";
3220  }
3221  else
3222  convert_floatbv(expr);
3223  }
3224  else if(op_type.id()==ID_rational ||
3225  op_type.id()==ID_integer)
3226  {
3227  out << "(";
3228  out << expr.id();
3229 
3230  out << " ";
3231  convert_expr(expr.op0());
3232  out << " ";
3233  convert_expr(expr.op1());
3234  out << ")";
3235  }
3236  else
3238  "unsupported type for "+expr.id_string()+": "+op_type.id_string());
3239 }
3240 
3242 {
3243  if(
3244  expr.type().id() == ID_rational || expr.type().id() == ID_integer ||
3245  expr.type().id() == ID_real)
3246  {
3247  // these are multi-ary in SMT-LIB2
3248  out << "(+";
3249 
3250  for(const auto &op : expr.operands())
3251  {
3252  out << ' ';
3253  convert_expr(op);
3254  }
3255 
3256  out << ')';
3257  }
3258  else if(
3259  expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv ||
3260  expr.type().id() == ID_fixedbv)
3261  {
3262  // These could be chained, i.e., need not be binary,
3263  // but at least MathSat doesn't like that.
3264  if(expr.operands().size() == 2)
3265  {
3266  out << "(bvadd ";
3267  convert_expr(expr.op0());
3268  out << " ";
3269  convert_expr(expr.op1());
3270  out << ")";
3271  }
3272  else
3273  {
3275  }
3276  }
3277  else if(expr.type().id() == ID_floatbv)
3278  {
3279  // Floating-point additions should have be been converted
3280  // to ID_floatbv_plus during symbolic execution, adding
3281  // the rounding mode. See smt2_convt::convert_floatbv_plus.
3282  UNREACHABLE;
3283  }
3284  else if(expr.type().id() == ID_pointer)
3285  {
3286  if(expr.operands().size() == 2)
3287  {
3288  exprt p = expr.op0(), i = expr.op1();
3289 
3290  if(p.type().id() != ID_pointer)
3291  p.swap(i);
3292 
3294  p.type().id() == ID_pointer,
3295  "one of the operands should have pointer type");
3296 
3297  mp_integer element_size;
3298  if(expr.type().subtype().id() == ID_empty)
3299  {
3300  // This is a gcc extension.
3301  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
3302  element_size = 1;
3303  }
3304  else
3305  {
3306  auto element_size_opt = pointer_offset_size(expr.type().subtype(), ns);
3307  CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
3308  element_size = *element_size_opt;
3309  }
3310 
3311  out << "(bvadd ";
3312  convert_expr(p);
3313  out << " ";
3314 
3315  if(element_size >= 2)
3316  {
3317  out << "(bvmul ";
3318  convert_expr(i);
3319  out << " (_ bv" << element_size << " " << boolbv_width(expr.type())
3320  << "))";
3321  }
3322  else
3323  convert_expr(i);
3324 
3325  out << ')';
3326  }
3327  else
3328  {
3330  }
3331  }
3332  else if(expr.type().id() == ID_vector)
3333  {
3334  const vector_typet &vector_type = to_vector_type(expr.type());
3335 
3336  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
3337 
3338  typet index_type = vector_type.size().type();
3339 
3340  if(use_datatypes)
3341  {
3342  const std::string &smt_typename = datatype_map.at(vector_type);
3343 
3344  out << "(mk-" << smt_typename;
3345  }
3346  else
3347  out << "(concat";
3348 
3349  // add component-by-component
3350  for(mp_integer i = 0; i != size; ++i)
3351  {
3352  exprt::operandst summands;
3353  summands.reserve(expr.operands().size());
3354  for(const auto &op : expr.operands())
3355  summands.push_back(index_exprt(
3356  op, from_integer(size - i - 1, index_type), vector_type.subtype()));
3357 
3358  plus_exprt tmp(std::move(summands), vector_type.subtype());
3359 
3360  out << " ";
3361  convert_expr(tmp);
3362  }
3363 
3364  out << ")"; // mk-... or concat
3365  }
3366  else
3367  UNEXPECTEDCASE("unsupported type for +: " + expr.type().id_string());
3368 }
3369 
3374 {
3376 
3377  /* CProver uses the x86 numbering of the rounding-mode
3378  * 0 == FE_TONEAREST
3379  * 1 == FE_DOWNWARD
3380  * 2 == FE_UPWARD
3381  * 3 == FE_TOWARDZERO
3382  * These literal values must be used rather than the macros
3383  * the macros from fenv.h to avoid portability problems.
3384  */
3385 
3386  if(expr.id()==ID_constant)
3387  {
3388  const constant_exprt &cexpr=to_constant_expr(expr);
3389 
3390  mp_integer value = numeric_cast_v<mp_integer>(cexpr);
3391 
3392  if(value==0)
3393  out << "roundNearestTiesToEven";
3394  else if(value==1)
3395  out << "roundTowardNegative";
3396  else if(value==2)
3397  out << "roundTowardPositive";
3398  else if(value==3)
3399  out << "roundTowardZero";
3400  else
3402  false,
3403  "Rounding mode should have value 0, 1, 2, or 3",
3404  id2string(cexpr.get_value()));
3405  }
3406  else
3407  {
3408  std::size_t width=to_bitvector_type(expr.type()).get_width();
3409 
3410  // Need to make the choice above part of the model
3411  out << "(ite (= (_ bv0 " << width << ") ";
3412  convert_expr(expr);
3413  out << ") roundNearestTiesToEven ";
3414 
3415  out << "(ite (= (_ bv1 " << width << ") ";
3416  convert_expr(expr);
3417  out << ") roundTowardNegative ";
3418 
3419  out << "(ite (= (_ bv2 " << width << ") ";
3420  convert_expr(expr);
3421  out << ") roundTowardPositive ";
3422 
3423  // TODO: add some kind of error checking here
3424  out << "roundTowardZero";
3425 
3426  out << ")))";
3427  }
3428 }
3429 
3431 {
3432  const typet &type=expr.type();
3433 
3434  PRECONDITION(
3435  type.id() == ID_floatbv ||
3436  (type.id() == ID_complex && type.subtype().id() == ID_floatbv) ||
3437  (type.id() == ID_vector && type.subtype().id() == ID_floatbv));
3438 
3439  if(use_FPA_theory)
3440  {
3441  if(type.id()==ID_floatbv)
3442  {
3443  out << "(fp.add ";
3445  out << " ";
3446  convert_expr(expr.lhs());
3447  out << " ";
3448  convert_expr(expr.rhs());
3449  out << ")";
3450  }
3451  else if(type.id()==ID_complex)
3452  {
3453  SMT2_TODO("+ for floatbv complex");
3454  }
3455  else if(type.id()==ID_vector)
3456  {
3457  SMT2_TODO("+ for floatbv vector");
3458  }
3459  else
3461  false,
3462  "type should not be one of the unsupported types",
3463  type.id_string());
3464  }
3465  else
3466  convert_floatbv(expr);
3467 }
3468 
3470 {
3471  if(expr.type().id()==ID_integer)
3472  {
3473  out << "(- ";
3474  convert_expr(expr.op0());
3475  out << " ";
3476  convert_expr(expr.op1());
3477  out << ")";
3478  }
3479  else if(expr.type().id()==ID_unsignedbv ||
3480  expr.type().id()==ID_signedbv ||
3481  expr.type().id()==ID_fixedbv)
3482  {
3483  if(expr.op0().type().id()==ID_pointer &&
3484  expr.op1().type().id()==ID_pointer)
3485  {
3486  // Pointer difference
3487  auto element_size = pointer_offset_size(expr.op0().type().subtype(), ns);
3488  CHECK_RETURN(element_size.has_value() && *element_size >= 1);
3489 
3490  if(*element_size >= 2)
3491  out << "(bvsdiv ";
3492 
3493  INVARIANT(
3494  boolbv_width(expr.op0().type()) == boolbv_width(expr.type()),
3495  "bitvector width of operand shall be equal to the bitvector width of "
3496  "the expression");
3497 
3498  out << "(bvsub ";
3499  convert_expr(expr.op0());
3500  out << " ";
3501  convert_expr(expr.op1());
3502  out << ")";
3503 
3504  if(*element_size >= 2)
3505  out << " (_ bv" << *element_size << " " << boolbv_width(expr.type())
3506  << "))";
3507  }
3508  else
3509  {
3510  out << "(bvsub ";
3511  convert_expr(expr.op0());
3512  out << " ";
3513  convert_expr(expr.op1());
3514  out << ")";
3515  }
3516  }
3517  else if(expr.type().id()==ID_floatbv)
3518  {
3519  // Floating-point subtraction should have be been converted
3520  // to ID_floatbv_minus during symbolic execution, adding
3521  // the rounding mode. See smt2_convt::convert_floatbv_minus.
3522  UNREACHABLE;
3523  }
3524  else if(expr.type().id()==ID_pointer)
3525  {
3526  SMT2_TODO("pointer subtraction");
3527  }
3528  else if(expr.type().id()==ID_vector)
3529  {
3530  const vector_typet &vector_type=to_vector_type(expr.type());
3531 
3532  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
3533 
3534  typet index_type=vector_type.size().type();
3535 
3536  if(use_datatypes)
3537  {
3538  const std::string &smt_typename = datatype_map.at(vector_type);
3539 
3540  out << "(mk-" << smt_typename;
3541  }
3542  else
3543  out << "(concat";
3544 
3545  // subtract component-by-component
3546  for(mp_integer i=0; i!=size; ++i)
3547  {
3548  exprt tmp(ID_minus, vector_type.subtype());
3549  forall_operands(it, expr)
3550  tmp.copy_to_operands(
3551  index_exprt(
3552  *it,
3553  from_integer(size-i-1, index_type),
3554  vector_type.subtype()));
3555 
3556  out << " ";
3557  convert_expr(tmp);
3558  }
3559 
3560  out << ")"; // mk-... or concat
3561  }
3562  else
3563  UNEXPECTEDCASE("unsupported type for -: "+expr.type().id_string());
3564 }
3565 
3567 {
3569  expr.type().id() == ID_floatbv,
3570  "type of ieee floating point expression shall be floatbv");
3571 
3572  if(use_FPA_theory)
3573  {
3574  out << "(fp.sub ";
3576  out << " ";
3577  convert_expr(expr.lhs());
3578  out << " ";
3579  convert_expr(expr.rhs());
3580  out << ")";
3581  }
3582  else
3583  convert_floatbv(expr);
3584 }
3585 
3587 {
3588  if(expr.type().id()==ID_unsignedbv ||
3589  expr.type().id()==ID_signedbv)
3590  {
3591  if(expr.type().id()==ID_unsignedbv)
3592  out << "(bvudiv ";
3593  else
3594  out << "(bvsdiv ";
3595 
3596  convert_expr(expr.op0());
3597  out << " ";
3598  convert_expr(expr.op1());
3599  out << ")";
3600  }
3601  else if(expr.type().id()==ID_fixedbv)
3602  {
3603  fixedbv_spect spec(to_fixedbv_type(expr.type()));
3604  std::size_t fraction_bits=spec.get_fraction_bits();
3605 
3606  out << "((_ extract " << spec.width-1 << " 0) ";
3607  out << "(bvsdiv ";
3608 
3609  out << "(concat ";
3610  convert_expr(expr.op0());
3611  out << " (_ bv0 " << fraction_bits << ")) ";
3612 
3613  out << "((_ sign_extend " << fraction_bits << ") ";
3614  convert_expr(expr.op1());
3615  out << ")";
3616 
3617  out << "))";
3618  }
3619  else if(expr.type().id()==ID_floatbv)
3620  {
3621  // Floating-point division should have be been converted
3622  // to ID_floatbv_div during symbolic execution, adding
3623  // the rounding mode. See smt2_convt::convert_floatbv_div.
3624  UNREACHABLE;
3625  }
3626  else
3627  UNEXPECTEDCASE("unsupported type for /: "+expr.type().id_string());
3628 }
3629 
3631 {
3633  expr.type().id() == ID_floatbv,
3634  "type of ieee floating point expression shall be floatbv");
3635 
3636  if(use_FPA_theory)
3637  {
3638  out << "(fp.div ";
3640  out << " ";
3641  convert_expr(expr.lhs());
3642  out << " ";
3643  convert_expr(expr.rhs());
3644  out << ")";
3645  }
3646  else
3647  convert_floatbv(expr);
3648 }
3649 
3651 {
3652  // re-write to binary if needed
3653  if(expr.operands().size()>2)
3654  {
3655  // strip last operand
3656  exprt tmp=expr;
3657  tmp.operands().pop_back();
3658 
3659  // recursive call
3660  return convert_mult(mult_exprt(tmp, expr.operands().back()));
3661  }
3662 
3663  INVARIANT(
3664  expr.operands().size() == 2,
3665  "expression should have been converted to a variant with two operands");
3666 
3667  if(expr.type().id()==ID_unsignedbv ||
3668  expr.type().id()==ID_signedbv)
3669  {
3670  // Note that bvmul is really unsigned,
3671  // but this is irrelevant as we chop-off any extra result
3672  // bits.
3673  out << "(bvmul ";
3674  convert_expr(expr.op0());
3675  out << " ";
3676  convert_expr(expr.op1());
3677  out << ")";
3678  }
3679  else if(expr.type().id()==ID_floatbv)
3680  {
3681  // Floating-point multiplication should have be been converted
3682  // to ID_floatbv_mult during symbolic execution, adding
3683  // the rounding mode. See smt2_convt::convert_floatbv_mult.
3684  UNREACHABLE;
3685  }
3686  else if(expr.type().id()==ID_fixedbv)
3687  {
3688  fixedbv_spect spec(to_fixedbv_type(expr.type()));
3689  std::size_t fraction_bits=spec.get_fraction_bits();
3690 
3691  out << "((_ extract "
3692  << spec.width+fraction_bits-1 << " "
3693  << fraction_bits << ") ";
3694 
3695  out << "(bvmul ";
3696 
3697  out << "((_ sign_extend " << fraction_bits << ") ";
3698  convert_expr(expr.op0());
3699  out << ") ";
3700 
3701  out << "((_ sign_extend " << fraction_bits << ") ";
3702  convert_expr(expr.op1());
3703  out << ")";
3704 
3705  out << "))"; // bvmul, extract
3706  }
3707  else if(expr.type().id()==ID_rational ||
3708  expr.type().id()==ID_integer ||
3709  expr.type().id()==ID_real)
3710  {
3711  out << "(*";
3712 
3713  forall_operands(it, expr)
3714  {
3715  out << " ";
3716  convert_expr(*it);
3717  }
3718 
3719  out << ")";
3720  }
3721  else
3722  UNEXPECTEDCASE("unsupported type for *: "+expr.type().id_string());
3723 }
3724 
3726 {
3728  expr.type().id() == ID_floatbv,
3729  "type of ieee floating point expression shall be floatbv");
3730 
3731  if(use_FPA_theory)
3732  {
3733  out << "(fp.mul ";
3735  out << " ";
3736  convert_expr(expr.lhs());
3737  out << " ";
3738  convert_expr(expr.rhs());
3739  out << ")";
3740  }
3741  else
3742  convert_floatbv(expr);
3743 }
3744 
3746 {
3748  expr.type().id() == ID_floatbv,
3749  "type of ieee floating point expression shall be floatbv");
3750 
3751  if(use_FPA_theory)
3752  {
3753  // Note that these do not have a rounding mode
3754  out << "(fp.rem ";
3755  convert_expr(expr.lhs());
3756  out << " ";
3757  convert_expr(expr.rhs());
3758  out << ")";
3759  }
3760  else
3761  {
3762  SMT2_TODO(
3763  "smt2_convt::convert_floatbv_rem to be implemented when not using "
3764  "FPA_theory");
3765  }
3766 }
3767 
3769 {
3770  // get rid of "with" that has more than three operands
3771 
3772  if(expr.operands().size()>3)
3773  {
3774  std::size_t s=expr.operands().size();
3775 
3776  // strip off the trailing two operands
3777  with_exprt tmp = expr;
3778  tmp.operands().resize(s-2);
3779 
3780  with_exprt new_with_expr(
3781  tmp, expr.operands()[s - 2], expr.operands().back());
3782 
3783  // recursive call
3784  return convert_with(new_with_expr);
3785  }
3786 
3787  INVARIANT(
3788  expr.operands().size() == 3,
3789  "with expression should have been converted to a version with three "
3790  "operands above");
3791 
3792  const typet &expr_type = expr.type();
3793 
3794  if(expr_type.id()==ID_array)
3795  {
3796  const array_typet &array_type=to_array_type(expr_type);
3797 
3798  if(use_array_theory(expr))
3799  {
3800  out << "(store ";
3801  convert_expr(expr.old());
3802  out << " ";
3803  convert_expr(typecast_exprt(expr.where(), array_type.size().type()));
3804  out << " ";
3805  convert_expr(expr.new_value());
3806  out << ")";
3807  }
3808  else
3809  {
3810  // fixed-width
3811  std::size_t array_width=boolbv_width(array_type);
3812  std::size_t sub_width=boolbv_width(array_type.subtype());
3813  std::size_t index_width=boolbv_width(expr.where().type());
3814 
3815  // We mask out the updated bits with AND,
3816  // and then OR-in the shifted new value.
3817 
3818  out << "(let ((distance? ";
3819  out << "(bvmul (_ bv" << sub_width << " " << array_width << ") ";
3820 
3821  // SMT2 says that the shift distance needs to be as wide
3822  // as the stuff we are shifting.
3823  if(array_width>index_width)
3824  {
3825  out << "((_ zero_extend " << array_width-index_width << ") ";
3826  convert_expr(expr.where());
3827  out << ")";
3828  }
3829  else
3830  {
3831  out << "((_ extract " << array_width-1 << " 0) ";
3832  convert_expr(expr.where());
3833  out << ")";
3834  }
3835 
3836  out << "))) "; // bvmul, distance?
3837 
3838  out << "(bvor ";
3839  out << "(bvand ";
3840  out << "(bvnot ";
3841  out << "(bvshl (_ bv" << power(2, sub_width) - 1 << " " << array_width
3842  << ") ";
3843  out << "distance?)) "; // bvnot, bvlshl
3844  convert_expr(expr.old());
3845  out << ") "; // bvand
3846  out << "(bvshl ";
3847  out << "((_ zero_extend " << array_width-sub_width << ") ";
3848  convert_expr(expr.new_value());
3849  out << ") distance?)))"; // zero_extend, bvshl, bvor, let
3850  }
3851  }
3852  else if(expr_type.id() == ID_struct || expr_type.id() == ID_struct_tag)
3853  {
3854  const struct_typet &struct_type = to_struct_type(ns.follow(expr_type));
3855 
3856  const exprt &index = expr.where();
3857  const exprt &value = expr.new_value();
3858 
3859  const irep_idt &component_name=index.get(ID_component_name);
3860 
3861  INVARIANT(
3862  struct_type.has_component(component_name),
3863  "struct should have accessed component");
3864 
3865  if(use_datatypes)
3866  {
3867  const std::string &smt_typename = datatype_map.at(expr_type);
3868 
3869  out << "(update-" << smt_typename << "." << component_name << " ";
3870  convert_expr(expr.old());
3871  out << " ";
3872  convert_expr(value);
3873  out << ")";
3874  }
3875  else
3876  {
3877  std::size_t struct_width=boolbv_width(struct_type);
3878 
3879  // figure out the offset and width of the member
3881  boolbv_width.get_member(struct_type, component_name);
3882 
3883  out << "(let ((?withop ";
3884  convert_expr(expr.old());
3885  out << ")) ";
3886 
3887  if(m.width==struct_width)
3888  {
3889  // the struct is the same as the member, no concat needed,
3890  // ?withop won't be used
3891  convert_expr(value);
3892  }
3893  else if(m.offset==0)
3894  {
3895  // the member is at the beginning
3896  out << "(concat "
3897  << "((_ extract " << (struct_width-1) << " "
3898  << m.width << ") ?withop) ";
3899  convert_expr(value);
3900  out << ")"; // concat
3901  }
3902  else if(m.offset+m.width==struct_width)
3903  {
3904  // the member is at the end
3905  out << "(concat ";
3906  convert_expr(value);
3907  out << " ((_ extract " << (m.offset - 1) << " 0) ?withop))";
3908  }
3909  else
3910  {
3911  // most general case, need two concat-s
3912  out << "(concat (concat "
3913  << "((_ extract " << (struct_width-1) << " "
3914  << (m.offset+m.width) << ") ?withop) ";
3915  convert_expr(value);
3916  out << ") ((_ extract " << (m.offset-1) << " 0) ?withop)";
3917  out << ")"; // concat
3918  }
3919 
3920  out << ")"; // let ?withop
3921  }
3922  }
3923  else if(expr_type.id() == ID_union || expr_type.id() == ID_union_tag)
3924  {
3925  const union_typet &union_type = to_union_type(ns.follow(expr_type));
3926 
3927  const exprt &value = expr.new_value();
3928 
3929  std::size_t total_width=boolbv_width(union_type);
3931  total_width != 0, "failed to get union width for with");
3932 
3933  std::size_t member_width=boolbv_width(value.type());
3935  member_width != 0, "failed to get union member width for with");
3936 
3937  if(total_width==member_width)
3938  {
3939  flatten2bv(value);
3940  }
3941  else
3942  {
3943  INVARIANT(
3944  total_width > member_width,
3945  "total width should be greater than member_width as member_width is at "
3946  "most as large as total_width and the other case has been handled "
3947  "above");
3948  out << "(concat ";
3949  out << "((_ extract "
3950  << (total_width-1)
3951  << " " << member_width << ") ";
3952  convert_expr(expr.old());
3953  out << ") ";
3954  flatten2bv(value);
3955  out << ")";
3956  }
3957  }
3958  else if(expr_type.id()==ID_bv ||
3959  expr_type.id()==ID_unsignedbv ||
3960  expr_type.id()==ID_signedbv)
3961  {
3962  // Update bits in a bit-vector. We will use masking and shifts.
3963 
3964  std::size_t total_width=boolbv_width(expr_type);
3966  total_width != 0, "failed to get total width");
3967 
3968  const exprt &index=expr.operands()[1];
3969  const exprt &value=expr.operands()[2];
3970 
3971  std::size_t value_width=boolbv_width(value.type());
3973  value_width != 0, "failed to get value width");
3974 
3975  typecast_exprt index_tc(index, expr_type);
3976 
3977  // TODO: SMT2-ify
3978  SMT2_TODO("SMT2-ify");
3979 
3980 #if 0
3981  out << "(bvor ";
3982  out << "(band ";
3983 
3984  // the mask to get rid of the old bits
3985  out << " (bvnot (bvshl";
3986 
3987  out << " (concat";
3988  out << " (repeat[" << total_width-value_width << "] bv0[1])";
3989  out << " (repeat[" << value_width << "] bv1[1])";
3990  out << ")"; // concat
3991 
3992  // shift it to the index
3993  convert_expr(index_tc);
3994  out << "))"; // bvshl, bvot
3995 
3996  out << ")"; // bvand
3997 
3998  // the new value
3999  out << " (bvshl ";
4000  convert_expr(value);
4001 
4002  // shift it to the index
4003  convert_expr(index_tc);
4004  out << ")"; // bvshl
4005 
4006  out << ")"; // bvor
4007 #endif
4008  }
4009  else
4011  "with expects struct, union, or array type, but got "+
4012  expr.type().id_string());
4013 }
4014 
4016 {
4017  PRECONDITION(expr.operands().size() == 3);
4018 
4019  SMT2_TODO("smt2_convt::convert_update to be implemented");
4020 }
4021 
4023 {
4024  const typet &array_op_type = expr.array().type();
4025 
4026  if(array_op_type.id()==ID_array)
4027  {
4028  const array_typet &array_type=to_array_type(array_op_type);
4029 
4030  if(use_array_theory(expr.array()))
4031  {
4032  if(expr.type().id() == ID_bool && !use_array_of_bool)
4033  {
4034  out << "(= ";
4035  out << "(select ";
4036  convert_expr(expr.array());
4037  out << " ";
4038  convert_expr(typecast_exprt(expr.index(), array_type.size().type()));
4039  out << ")";
4040  out << " #b1)";
4041  }
4042  else
4043  {
4044  out << "(select ";
4045  convert_expr(expr.array());
4046  out << " ";
4047  convert_expr(typecast_exprt(expr.index(), array_type.size().type()));
4048  out << ")";
4049  }
4050  }
4051  else
4052  {
4053  // fixed size
4054  std::size_t array_width=boolbv_width(array_type);
4055  CHECK_RETURN(array_width != 0);
4056 
4057  unflatten(wheret::BEGIN, array_type.subtype());
4058 
4059  std::size_t sub_width=boolbv_width(array_type.subtype());
4060  std::size_t index_width=boolbv_width(expr.index().type());
4061 
4062  out << "((_ extract " << sub_width-1 << " 0) ";
4063  out << "(bvlshr ";
4064  convert_expr(expr.array());
4065  out << " ";
4066  out << "(bvmul (_ bv" << sub_width << " " << array_width << ") ";
4067 
4068  // SMT2 says that the shift distance must be the same as
4069  // the width of what we shift.
4070  if(array_width>index_width)
4071  {
4072  out << "((_ zero_extend " << array_width-index_width << ") ";
4073  convert_expr(expr.index());
4074  out << ")"; // zero_extend
4075  }
4076  else
4077  {
4078  out << "((_ extract " << array_width-1 << " 0) ";
4079  convert_expr(expr.index());
4080  out << ")"; // extract
4081  }
4082 
4083  out << ")))"; // mult, bvlshr, extract
4084 
4085  unflatten(wheret::END, array_type.subtype());
4086  }
4087  }
4088  else if(array_op_type.id()==ID_vector)
4089  {
4090  const vector_typet &vector_type=to_vector_type(array_op_type);
4091 
4092  if(use_datatypes)
4093  {
4094  const std::string &smt_typename = datatype_map.at(vector_type);
4095 
4096  // this is easy for constant indicies
4097 
4098  const auto index_int = numeric_cast<mp_integer>(expr.index());
4099  if(!index_int.has_value())
4100  {
4101  SMT2_TODO("non-constant index on vectors");
4102  }
4103  else
4104  {
4105  out << "(" << smt_typename << "." << *index_int << " ";
4106  convert_expr(expr.array());
4107  out << ")";
4108  }
4109  }
4110  else
4111  {
4112  SMT2_TODO("index on vectors");
4113  }
4114  }
4115  else
4116  INVARIANT(
4117  false, "index with unsupported array type: " + array_op_type.id_string());
4118 }
4119 
4121 {
4122  const member_exprt &member_expr=to_member_expr(expr);
4123  const exprt &struct_op=member_expr.struct_op();
4124  const typet &struct_op_type = struct_op.type();
4125  const irep_idt &name=member_expr.get_component_name();
4126 
4127  if(struct_op_type.id() == ID_struct || struct_op_type.id() == ID_struct_tag)
4128  {
4129  const struct_typet &struct_type = to_struct_type(ns.follow(struct_op_type));
4130 
4131  INVARIANT(
4132  struct_type.has_component(name), "struct should have accessed component");
4133 
4134  if(use_datatypes)
4135  {
4136  const std::string &smt_typename = datatype_map.at(struct_type);
4137 
4138  out << "(" << smt_typename << "."
4139  << struct_type.get_component(name).get_name()
4140  << " ";
4141  convert_expr(struct_op);
4142  out << ")";
4143  }
4144  else
4145  {
4146  // we extract
4147  const std::size_t member_width = boolbv_width(expr.type());
4148  const auto member_offset = member_offset_bits(struct_type, name, ns);
4149 
4151  member_offset.has_value(), "failed to get struct member offset");
4152 
4153  out << "((_ extract " << (member_offset.value() + member_width - 1) << " "
4154  << member_offset.value() << ") ";
4155  convert_expr(struct_op);
4156  out << ")";
4157  }
4158  }
4159  else if(
4160  struct_op_type.id() == ID_union || struct_op_type.id() == ID_union_tag)
4161  {
4162  std::size_t width=boolbv_width(expr.type());
4164  width != 0, "failed to get union member width");
4165 
4166  unflatten(wheret::BEGIN, expr.type());
4167 
4168  out << "((_ extract "
4169  << (width-1)
4170  << " 0) ";
4171  convert_expr(struct_op);
4172  out << ")";
4173 
4174  unflatten(wheret::END, expr.type());
4175  }
4176  else
4178  "convert_member on an unexpected type "+struct_op_type.id_string());
4179 }
4180 
4182 {
4183  const typet &type = expr.type();
4184 
4185  if(type.id()==ID_bool)
4186  {
4187  out << "(ite ";
4188  convert_expr(expr); // this returns a Bool
4189  out << " #b1 #b0)"; // this is a one-bit bit-vector
4190  }
4191  else if(type.id()==ID_vector)
4192  {
4193  if(use_datatypes)
4194  {
4195  const std::string &smt_typename = datatype_map.at(type);
4196 
4197  // concatenate elements
4198  const vector_typet &vector_type=to_vector_type(type);
4199 
4200  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
4201 
4202  out << "(let ((?vflop ";
4203  convert_expr(expr);
4204  out << ")) ";
4205 
4206  out << "(concat";
4207 
4208  for(mp_integer i=0; i!=size; ++i)
4209  {
4210  out << " (" << smt_typename << "." << i << " ?vflop)";
4211  }
4212 
4213  out << "))"; // concat, let
4214  }
4215  else
4216  convert_expr(expr); // already a bv
4217  }
4218  else if(type.id()==ID_array)
4219  {
4220  convert_expr(expr);
4221  }
4222  else if(type.id() == ID_struct || type.id() == ID_struct_tag)
4223  {
4224  if(use_datatypes)
4225  {
4226  const std::string &smt_typename = datatype_map.at(type);
4227 
4228  // concatenate elements
4229  const struct_typet &struct_type = to_struct_type(ns.follow(type));
4230 
4231  out << "(let ((?sflop ";
4232  convert_expr(expr);
4233  out << ")) ";
4234 
4235  const struct_typet::componentst &components=
4236  struct_type.components();
4237 
4238  // SMT-LIB 2 concat is binary only
4239  for(std::size_t i=components.size(); i>1; i--)
4240  {
4241  out << "(concat (" << smt_typename << "."
4242  << components[i-1].get_name() << " ?sflop)";
4243 
4244  out << " ";
4245  }
4246 
4247  out << "(" << smt_typename << "."
4248  << components[0].get_name() << " ?sflop)";
4249 
4250  for(std::size_t i=1; i<components.size(); i++)
4251  out << ")"; // concat
4252 
4253  out << ")"; // let
4254  }
4255  else
4256  convert_expr(expr);
4257  }
4258  else if(type.id()==ID_floatbv)
4259  {
4260  INVARIANT(
4261  !use_FPA_theory,
4262  "floatbv expressions should be flattened when using FPA theory");
4263 
4264  convert_expr(expr);
4265  }
4266  else
4267  convert_expr(expr);
4268 }
4269 
4271  wheret where,
4272  const typet &type,
4273  unsigned nesting)
4274 {
4275  if(type.id()==ID_bool)
4276  {
4277  if(where==wheret::BEGIN)
4278  out << "(= "; // produces a bool
4279  else
4280  out << " #b1)";
4281  }
4282  else if(type.id()==ID_vector)
4283  {
4284  if(use_datatypes)
4285  {
4286  const std::string &smt_typename = datatype_map.at(type);
4287 
4288  // extract elements
4289  const vector_typet &vector_type=to_vector_type(type);
4290 
4291  std::size_t subtype_width=boolbv_width(vector_type.subtype());
4292 
4293  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
4294 
4295  if(where==wheret::BEGIN)
4296  out << "(let ((?ufop" << nesting << " ";
4297  else
4298  {
4299  out << ")) ";
4300 
4301  out << "(mk-" << smt_typename;
4302 
4303  std::size_t offset=0;
4304 
4305  for(mp_integer i=0; i!=size; ++i, offset+=subtype_width)
4306  {
4307  out << " ";
4308  unflatten(wheret::BEGIN, vector_type.subtype(), nesting+1);
4309  out << "((_ extract " << offset+subtype_width-1 << " "
4310  << offset << ") ?ufop" << nesting << ")";
4311  unflatten(wheret::END, vector_type.subtype(), nesting+1);
4312  }
4313 
4314  out << "))"; // mk-, let
4315  }
4316  }
4317  else
4318  {
4319  // nop, already a bv
4320  }
4321  }
4322  else if(type.id() == ID_struct || type.id() == ID_struct_tag)
4323  {
4324  if(use_datatypes)
4325  {
4326  // extract members
4327  if(where==wheret::BEGIN)
4328  out << "(let ((?ufop" << nesting << " ";
4329  else
4330  {
4331  out << ")) ";
4332 
4333  const std::string &smt_typename = datatype_map.at(type);
4334 
4335  out << "(mk-" << smt_typename;
4336 
4337  const struct_typet &struct_type = to_struct_type(ns.follow(type));
4338 
4339  const struct_typet::componentst &components=
4340  struct_type.components();
4341 
4342  std::size_t offset=0;
4343 
4344  std::size_t i=0;
4345  for(struct_typet::componentst::const_iterator
4346  it=components.begin();
4347  it!=components.end();
4348  it++, i++)
4349  {
4350  std::size_t member_width=boolbv_width(it->type());
4351 
4352  out << " ";
4353  unflatten(wheret::BEGIN, it->type(), nesting+1);
4354  out << "((_ extract " << offset+member_width-1 << " "
4355  << offset << ") ?ufop" << nesting << ")";
4356  unflatten(wheret::END, it->type(), nesting+1);
4357  offset+=member_width;
4358  }
4359 
4360  out << "))"; // mk-, let
4361  }
4362  }
4363  else
4364  {
4365  // nop, already a bv
4366  }
4367  }
4368  else
4369  {
4370  // nop
4371  }
4372 }
4373 
4374 void smt2_convt::set_to(const exprt &expr, bool value)
4375 {
4376  PRECONDITION(expr.type().id() == ID_bool);
4377 
4378  if(expr.id()==ID_and && value)
4379  {
4380  forall_operands(it, expr)
4381  set_to(*it, true);
4382  return;
4383  }
4384 
4385  if(expr.id()==ID_or && !value)
4386  {
4387  forall_operands(it, expr)
4388  set_to(*it, false);
4389  return;
4390  }
4391 
4392  if(expr.id()==ID_not)
4393  {
4394  return set_to(to_not_expr(expr).op(), !value);
4395  }
4396 
4397  out << "\n";
4398 
4399  // special treatment for "set_to(a=b, true)" where
4400  // a is a new symbol
4401 
4402  if(expr.id() == ID_equal && value)
4403  {
4404  const equal_exprt &equal_expr=to_equal_expr(expr);
4405  if(equal_expr.lhs().type().id() == ID_empty)
4406  {
4407  // ignore equality checking over expressions with empty (void) type
4408  return;
4409  }
4410 
4411  if(equal_expr.lhs().id()==ID_symbol)
4412  {
4413  const irep_idt &identifier=
4414  to_symbol_expr(equal_expr.lhs()).get_identifier();
4415 
4416  if(identifier_map.find(identifier)==identifier_map.end())
4417  {
4418  identifiert &id=identifier_map[identifier];
4419  CHECK_RETURN(id.type.is_nil());
4420 
4421  id.type=equal_expr.lhs().type();
4422  find_symbols(id.type);
4423  exprt prepared_rhs = prepare_for_convert_expr(equal_expr.rhs());
4424 
4425  std::string smt2_identifier=convert_identifier(identifier);
4426  smt2_identifiers.insert(smt2_identifier);
4427 
4428  out << "; set_to true (equal)\n";
4429  out << "(define-fun |" << smt2_identifier << "| () ";
4430 
4431  convert_type(equal_expr.lhs().type());
4432  out << " ";
4433  convert_expr(prepared_rhs);
4434 
4435  out << ")" << "\n";
4436  return; // done
4437  }
4438  }
4439  }
4440 
4441  exprt prepared_expr = prepare_for_convert_expr(expr);
4442 
4443 #if 0
4444  out << "; CONV: "
4445  << format(expr) << "\n";
4446 #endif
4447 
4448  out << "; set_to " << (value?"true":"false") << "\n"
4449  << "(assert ";
4450  if(!value)
4451  {
4452  out << "(not ";
4453  }
4454  const auto found_literal = defined_expressions.find(expr);
4455  if(!(found_literal == defined_expressions.end()))
4456  {
4457  // This is a converted expression, we can just assert the literal name
4458  // since the expression is already defined
4459  out << found_literal->second;
4460  set_values[found_literal->second] = value;
4461  }
4462  else
4463  {
4464  convert_expr(prepared_expr);
4465  }
4466  if(!value)
4467  {
4468  out << ")";
4469  }
4470  out << ")\n";
4471  return;
4472 }
4473 
4481 {
4482  exprt lowered_expr = expr;
4483 
4484  for(auto it = lowered_expr.depth_begin(), itend = lowered_expr.depth_end();
4485  it != itend;
4486  ++it)
4487  {
4488  if(
4489  it->id() == ID_byte_extract_little_endian ||
4490  it->id() == ID_byte_extract_big_endian)
4491  {
4492  it.mutate() = lower_byte_extract(to_byte_extract_expr(*it), ns);
4493  }
4494  else if(
4495  it->id() == ID_byte_update_little_endian ||
4496  it->id() == ID_byte_update_big_endian)
4497  {
4498  it.mutate() = lower_byte_update(to_byte_update_expr(*it), ns);
4499  }
4500  }
4501 
4502  return lowered_expr;
4503 }
4504 
4513 {
4514  // First, replace byte operators, because they may introduce new array
4515  // expressions that must be seen by find_symbols:
4516  exprt lowered_expr = lower_byte_operators(expr);
4517  INVARIANT(
4518  !has_byte_operator(lowered_expr),
4519  "lower_byte_operators should remove all byte operators");
4520 
4521  // Now create symbols for all composite expressions present in lowered_expr:
4522  find_symbols(lowered_expr);
4523 
4524  return lowered_expr;
4525 }
4526 
4528 {
4529  // recursive call on type
4530  find_symbols(expr.type());
4531 
4532  if(expr.id() == ID_exists || expr.id() == ID_forall)
4533  {
4534  // do not declare the quantified symbol, but record
4535  // as 'bound symbol'
4536  const auto &q_expr = to_quantifier_expr(expr);
4537  const auto identifier = q_expr.symbol().get_identifier();
4538  identifiert &id = identifier_map[identifier];
4539  id.type = q_expr.symbol().type();
4540  id.is_bound = true;
4541  find_symbols(q_expr.where());
4542  return;
4543  }
4544 
4545  // recursive call on operands
4546  forall_operands(it, expr)
4547  find_symbols(*it);
4548 
4549  if(expr.id()==ID_symbol ||
4550  expr.id()==ID_nondet_symbol)
4551  {
4552  // we don't track function-typed symbols
4553  if(expr.type().id()==ID_code)
4554  return;
4555 
4556  irep_idt identifier;
4557 
4558  if(expr.id()==ID_symbol)
4559  identifier=to_symbol_expr(expr).get_identifier();
4560  else
4561  identifier="nondet_"+
4562  id2string(to_nondet_symbol_expr(expr).get_identifier());
4563 
4564  identifiert &id=identifier_map[identifier];
4565 
4566  if(id.type.is_nil())
4567  {
4568  id.type=expr.type();
4569 
4570  std::string smt2_identifier=convert_identifier(identifier);
4571  smt2_identifiers.insert(smt2_identifier);
4572 
4573  out << "; find_symbols\n";
4574  out << "(declare-fun |"
4575  << smt2_identifier
4576  << "| () ";
4577  convert_type(expr.type());
4578  out << ")" << "\n";
4579  }
4580  }
4581  else if(expr.id() == ID_array_of)
4582  {
4583  if(!use_as_const)
4584  {
4585  if(defined_expressions.find(expr) == defined_expressions.end())
4586  {
4587  const auto &array_of = to_array_of_expr(expr);
4588  const auto &array_type = array_of.type();
4589 
4590  const irep_idt id =
4591  "array_of." + std::to_string(defined_expressions.size());
4592  out << "; the following is a substitute for lambda i. x\n";
4593  out << "(declare-fun " << id << " () ";
4594  convert_type(array_type);
4595  out << ")\n";
4596 
4597  // use a quantifier-based initialization instead of lambda
4598  out << "(assert (forall ((i ";
4599  convert_type(array_type.size().type());
4600  out << ")) (= (select " << id << " i) ";
4601  if(array_type.subtype().id() == ID_bool && !use_array_of_bool)
4602  {
4603  out << "(ite ";
4604  convert_expr(array_of.what());
4605  out << " #b1 #b0)";
4606  }
4607  else
4608  {
4609  convert_expr(array_of.what());
4610  }
4611  out << ")))\n";
4612 
4613  defined_expressions[expr] = id;
4614  }
4615  }
4616  }
4617  else if(expr.id() == ID_array_comprehension)
4618  {
4620  {
4621  if(defined_expressions.find(expr) == defined_expressions.end())
4622  {
4623  const auto &array_comprehension = to_array_comprehension_expr(expr);
4624  const auto &array_type = array_comprehension.type();
4625  const auto &array_size = array_type.size();
4626 
4627  const irep_idt id =
4628  "array_comprehension." + std::to_string(defined_expressions.size());
4629  out << "(declare-fun " << id << " () ";
4630  convert_type(array_type);
4631  out << ")\n";
4632 
4633  out << "; the following is a substitute for lambda i . x(i)\n";
4634  out << "; universally quantified initialization of the array\n";
4635  out << "(assert (forall ((";
4636  convert_expr(array_comprehension.arg());
4637  out << " ";
4638  convert_type(array_size.type());
4639  out << ")) (=> (and (bvule (_ bv0 " << boolbv_width(array_size.type())
4640  << ") ";
4641  convert_expr(array_comprehension.arg());
4642  out << ") (bvult ";
4643  convert_expr(array_comprehension.arg());
4644  out << " ";
4645  convert_expr(array_size);
4646  out << ")) (= (select " << id << " ";
4647  convert_expr(array_comprehension.arg());
4648  out << ") ";
4649  if(array_type.subtype().id() == ID_bool && !use_array_of_bool)
4650  {
4651  out << "(ite ";
4652  convert_expr(array_comprehension.body());
4653  out << " #b1 #b0)";
4654  }
4655  else
4656  {
4657  convert_expr(array_comprehension.body());
4658  }
4659  out << "))))\n";
4660 
4661  defined_expressions[expr] = id;
4662  }
4663  }
4664  }
4665  else if(expr.id()==ID_array)
4666  {
4667  if(defined_expressions.find(expr)==defined_expressions.end())
4668  {
4669  const array_typet &array_type=to_array_type(expr.type());
4670 
4671  const irep_idt id = "array." + std::to_string(defined_expressions.size());
4672  out << "; the following is a substitute for an array constructor" << "\n";
4673  out << "(declare-fun " << id << " () ";
4674  convert_type(array_type);
4675  out << ")" << "\n";
4676 
4677  for(std::size_t i=0; i<expr.operands().size(); i++)
4678  {
4679  out << "(assert (= (select " << id << " ";
4680  convert_expr(from_integer(i, array_type.size().type()));
4681  out << ") "; // select
4682  if(array_type.subtype().id() == ID_bool && !use_array_of_bool)
4683  {
4684  out << "(ite ";
4685  convert_expr(expr.operands()[i]);
4686  out << " #b1 #b0)";
4687  }
4688  else
4689  {
4690  convert_expr(expr.operands()[i]);
4691  }
4692  out << "))" << "\n"; // =, assert
4693  }
4694 
4695  defined_expressions[expr]=id;
4696  }
4697  }
4698  else if(expr.id()==ID_string_constant)
4699  {
4700  if(defined_expressions.find(expr)==defined_expressions.end())
4701  {
4702  // introduce a temporary array.
4704  const array_typet &array_type=to_array_type(tmp.type());
4705 
4706  const irep_idt id =
4707  "string." + std::to_string(defined_expressions.size());
4708  out << "; the following is a substitute for a string" << "\n";
4709  out << "(declare-fun " << id << " () ";
4710  convert_type(array_type);
4711  out << ")" << "\n";
4712 
4713  for(std::size_t i=0; i<tmp.operands().size(); i++)
4714  {
4715  out << "(assert (= (select " << id;
4716  convert_expr(from_integer(i, array_type.size().type()));
4717  out << ") "; // select
4718  convert_expr(tmp.operands()[i]);
4719  out << "))" << "\n";
4720  }
4721 
4722  defined_expressions[expr]=id;
4723  }
4724  }
4725  else if(expr.id() == ID_object_size)
4726  {
4727  const exprt &op = to_unary_expr(expr).op();
4728 
4729  if(op.type().id()==ID_pointer)
4730  {
4731  if(object_sizes.find(expr)==object_sizes.end())
4732  {
4733  const irep_idt id =
4734  "object_size." + std::to_string(object_sizes.size());
4735  out << "(declare-fun |" << id << "| () ";
4736  convert_type(expr.type());
4737  out << ")" << "\n";
4738 
4739  object_sizes[expr]=id;
4740  }
4741  }
4742  }
4743  // clang-format off
4744  else if(!use_FPA_theory &&
4745  expr.operands().size() >= 1 &&
4746  (expr.id() == ID_floatbv_plus ||
4747  expr.id() == ID_floatbv_minus ||
4748  expr.id() == ID_floatbv_mult ||
4749  expr.id() == ID_floatbv_div ||
4750  expr.id() == ID_floatbv_typecast ||
4751  expr.id() == ID_ieee_float_equal ||
4752  expr.id() == ID_ieee_float_notequal ||
4753  ((expr.id() == ID_lt ||
4754  expr.id() == ID_gt ||
4755  expr.id() == ID_le ||
4756  expr.id() == ID_ge ||
4757  expr.id() == ID_isnan ||
4758  expr.id() == ID_isnormal ||
4759  expr.id() == ID_isfinite ||
4760  expr.id() == ID_isinf ||
4761  expr.id() == ID_sign ||
4762  expr.id() == ID_unary_minus ||
4763  expr.id() == ID_typecast ||
4764  expr.id() == ID_abs) &&
4765  to_multi_ary_expr(expr).op0().type().id() == ID_floatbv)))
4766  // clang-format on
4767  {
4768  irep_idt function=
4769  "|float_bv."+expr.id_string()+floatbv_suffix(expr)+"|";
4770 
4771  if(bvfp_set.insert(function).second)
4772  {
4773  out << "; this is a model for " << expr.id() << " : "
4774  << type2id(to_multi_ary_expr(expr).op0().type()) << " -> "
4775  << type2id(expr.type()) << "\n"
4776  << "(define-fun " << function << " (";
4777 
4778  for(std::size_t i = 0; i < expr.operands().size(); i++)
4779  {
4780  if(i!=0)
4781  out << " ";
4782  out << "(op" << i << ' ';
4783  convert_type(expr.operands()[i].type());
4784  out << ')';
4785  }
4786 
4787  out << ") ";
4788  convert_type(expr.type()); // return type
4789  out << ' ';
4790 
4791  exprt tmp1=expr;
4792  for(std::size_t i = 0; i < tmp1.operands().size(); i++)
4793  tmp1.operands()[i]=
4794  smt2_symbolt("op"+std::to_string(i), tmp1.operands()[i].type());
4795 
4796  exprt tmp2=float_bv(tmp1);
4797  tmp2=letify(tmp2);
4798  CHECK_RETURN(!tmp2.is_nil());
4799 
4800  convert_expr(tmp2);
4801 
4802  out << ")\n"; // define-fun
4803  }
4804  }
4805 }
4806 
4808 {
4809  const typet &type = expr.type();
4810  PRECONDITION(type.id()==ID_array);
4811 
4812  if(use_datatypes)
4813  {
4814  return true; // always use array theory when we have datatypes
4815  }
4816  else
4817  {
4818  // arrays inside structs get flattened
4819  if(expr.id()==ID_with)
4820  return use_array_theory(to_with_expr(expr).old());
4821  else if(expr.id()==ID_member)
4822  return false;
4823  else
4824  return true;
4825  }
4826 }
4827 
4829 {
4830  if(type.id()==ID_array)
4831  {
4832  const array_typet &array_type=to_array_type(type);
4833  CHECK_RETURN(array_type.size().is_not_nil());
4834 
4835  // we always use array theory for top-level arrays
4836  const typet &subtype = array_type.subtype();
4837 
4838  out << "(Array ";
4839  convert_type(array_type.size().type());
4840  out << " ";
4841 
4842  if(subtype.id()==ID_bool && !use_array_of_bool)
4843  out << "(_ BitVec 1)";
4844  else
4845  convert_type(array_type.subtype());
4846 
4847  out << ")";
4848  }
4849  else if(type.id()==ID_bool)
4850  {
4851  out << "Bool";
4852  }
4853  else if(type.id() == ID_struct || type.id() == ID_struct_tag)
4854  {
4855  if(use_datatypes)
4856  {
4857  out << datatype_map.at(type);
4858  }
4859  else
4860  {
4861  std::size_t width=boolbv_width(type);
4863  width != 0, "failed to get width of struct");
4864 
4865  out << "(_ BitVec " << width << ")";
4866  }
4867  }
4868  else if(type.id()==ID_vector)
4869  {
4870  if(use_datatypes)
4871  {
4872  out << datatype_map.at(type);
4873  }
4874  else
4875  {
4876  std::size_t width=boolbv_width(type);
4878  width != 0, "failed to get width of vector");
4879 
4880  out << "(_ BitVec " << width << ")";
4881  }
4882  }
4883  else if(type.id()==ID_code)
4884  {
4885  // These may appear in structs.
4886  // We replace this by "Bool" in order to keep the same
4887  // member count.
4888  out << "Bool";
4889  }
4890  else if(type.id() == ID_union || type.id() == ID_union_tag)
4891  {
4892  std::size_t width=boolbv_width(type);
4893  CHECK_RETURN_WITH_DIAGNOSTICS(width != 0, "failed to get width of union");
4894 
4895  out << "(_ BitVec " << width << ")";
4896  }
4897  else if(type.id()==ID_pointer)
4898  {
4899  out << "(_ BitVec "
4900  << boolbv_width(type) << ")";
4901  }
4902  else if(type.id()==ID_bv ||
4903  type.id()==ID_fixedbv ||
4904  type.id()==ID_unsignedbv ||
4905  type.id()==ID_signedbv ||
4906  type.id()==ID_c_bool)
4907  {
4908  out << "(_ BitVec "
4909  << to_bitvector_type(type).get_width() << ")";
4910  }
4911  else if(type.id()==ID_c_enum)
4912  {
4913  // these have a subtype
4914  out << "(_ BitVec "
4915  << to_bitvector_type(type.subtype()).get_width() << ")";
4916  }
4917  else if(type.id()==ID_c_enum_tag)
4918  {
4920  }
4921  else if(type.id()==ID_floatbv)
4922  {
4923  const floatbv_typet &floatbv_type=to_floatbv_type(type);
4924 
4925  if(use_FPA_theory)
4926  out << "(_ FloatingPoint "
4927  << floatbv_type.get_e() << " "
4928  << floatbv_type.get_f() + 1 << ")";
4929  else
4930  out << "(_ BitVec "
4931  << floatbv_type.get_width() << ")";
4932  }
4933  else if(type.id()==ID_rational ||
4934  type.id()==ID_real)
4935  out << "Real";
4936  else if(type.id()==ID_integer)
4937  out << "Int";
4938  else if(type.id()==ID_complex)
4939  {
4940  if(use_datatypes)
4941  {
4942  out << datatype_map.at(type);
4943  }
4944  else
4945  {
4946  std::size_t width=boolbv_width(type);
4948  width != 0, "failed to get width of complex");
4949 
4950  out << "(_ BitVec " << width << ")";
4951  }
4952  }
4953  else if(type.id()==ID_c_bit_field)
4954  {
4956  }
4957  else
4958  {
4959  UNEXPECTEDCASE("unsupported type: "+type.id_string());
4960  }
4961 }
4962 
4964 {
4965  std::set<irep_idt> recstack;
4966  find_symbols_rec(type, recstack);
4967 }
4968 
4970  const typet &type,
4971  std::set<irep_idt> &recstack)
4972 {
4973  if(type.id()==ID_array)
4974  {
4975  const array_typet &array_type=to_array_type(type);
4976  find_symbols(array_type.size());
4977  find_symbols_rec(array_type.subtype(), recstack);
4978  }
4979  else if(type.id()==ID_complex)
4980  {
4981  find_symbols_rec(type.subtype(), recstack);
4982 
4983  if(use_datatypes &&
4984  datatype_map.find(type)==datatype_map.end())
4985  {
4986  const std::string smt_typename =
4987  "complex." + std::to_string(datatype_map.size());
4988  datatype_map[type] = smt_typename;
4989 
4990  out << "(declare-datatypes () ((" << smt_typename << " "
4991  << "(mk-" << smt_typename;
4992 
4993  out << " (" << smt_typename << ".imag ";
4994  convert_type(type.subtype());
4995  out << ")";
4996 
4997  out << " (" << smt_typename << ".real ";
4998  convert_type(type.subtype());
4999  out << ")";
5000 
5001  out << "))))\n";
5002  }
5003  }
5004  else if(type.id()==ID_vector)
5005  {
5006  find_symbols_rec(type.subtype(), recstack);
5007 
5008  if(use_datatypes &&
5009  datatype_map.find(type)==datatype_map.end())
5010  {
5011  const vector_typet &vector_type=to_vector_type(type);
5012 
5013  mp_integer size = numeric_cast_v<mp_integer>(vector_type.size());
5014 
5015  const std::string smt_typename =
5016  "vector." + std::to_string(datatype_map.size());
5017  datatype_map[type] = smt_typename;
5018 
5019  out << "(declare-datatypes () ((" << smt_typename << " "
5020  << "(mk-" << smt_typename;
5021 
5022  for(mp_integer i=0; i!=size; ++i)
5023  {
5024  out << " (" << smt_typename << "." << i << " ";
5025  convert_type(type.subtype());
5026  out << ")";
5027  }
5028 
5029  out << "))))\n";
5030  }
5031  }
5032  else if(type.id() == ID_struct)
5033  {
5034  // Cater for mutually recursive struct types
5035  bool need_decl=false;
5036  if(use_datatypes &&
5037  datatype_map.find(type)==datatype_map.end())
5038  {
5039  const std::string smt_typename =
5040  "struct." + std::to_string(datatype_map.size());
5041  datatype_map[type] = smt_typename;
5042  need_decl=true;
5043  }
5044 
5045  const struct_typet::componentst &components =
5046  to_struct_type(type).components();
5047 
5048  for(const auto &component : components)
5049  find_symbols_rec(component.type(), recstack);
5050 
5051  // Declare the corresponding SMT type if we haven't already.
5052  if(need_decl)
5053  {
5054  const std::string &smt_typename = datatype_map.at(type);
5055 
5056  // We're going to create a datatype named something like `struct.0'.
5057  // It's going to have a single constructor named `mk-struct.0' with an
5058  // argument for each member of the struct. The declaration that
5059  // creates this type looks like:
5060  //
5061  // (declare-datatypes () ((struct.0 (mk-struct.0
5062  // (struct.0.component1 type1)
5063  // ...
5064  // (struct.0.componentN typeN)))))
5065  out << "(declare-datatypes () ((" << smt_typename << " "
5066  << "(mk-" << smt_typename << " ";
5067 
5068  for(const auto &component : components)
5069  {
5070  out << "(" << smt_typename << "." << component.get_name()
5071  << " ";
5072  convert_type(component.type());
5073  out << ") ";
5074  }
5075 
5076  out << "))))" << "\n";
5077 
5078  // Let's also declare convenience functions to update individual
5079  // members of the struct whil we're at it. The functions are
5080  // named like `update-struct.0.component1'. Their declarations
5081  // look like:
5082  //
5083  // (declare-fun update-struct.0.component1
5084  // ((s struct.0) ; first arg -- the struct to update
5085  // (v type1)) ; second arg -- the value to update
5086  // struct.0 ; the output type
5087  // (mk-struct.0 ; build the new struct...
5088  // v ; the updated value
5089  // (struct.0.component2 s) ; retain the other members
5090  // ...
5091  // (struct.0.componentN s)))
5092 
5093  for(struct_union_typet::componentst::const_iterator
5094  it=components.begin();
5095  it!=components.end();
5096  ++it)
5097  {
5099  out << "(define-fun update-" << smt_typename << "."
5100  << component.get_name() << " "
5101  << "((s " << smt_typename << ") "
5102  << "(v ";
5103  convert_type(component.type());
5104  out << ")) " << smt_typename << " "
5105  << "(mk-" << smt_typename
5106  << " ";
5107 
5108  for(struct_union_typet::componentst::const_iterator
5109  it2=components.begin();
5110  it2!=components.end();
5111  ++it2)
5112  {
5113  if(it==it2)
5114  out << "v ";
5115  else
5116  {
5117  out << "(" << smt_typename << "."
5118  << it2->get_name() << " s) ";
5119  }
5120  }
5121 
5122  out << "))" << "\n";
5123  }
5124 
5125  out << "\n";
5126  }
5127  }
5128  else if(type.id() == ID_union)
5129  {
5130  const union_typet::componentst &components =
5131  to_union_type(type).components();
5132 
5133  for(const auto &component : components)
5134  find_symbols_rec(component.type(), recstack);
5135  }
5136  else if(type.id()==ID_code)
5137  {
5138  const code_typet::parameterst &parameters=
5139  to_code_type(type).parameters();
5140  for(const auto &param : parameters)
5141  find_symbols_rec(param.type(), recstack);
5142 
5143  find_symbols_rec(to_code_type(type).return_type(), recstack);
5144  }
5145  else if(type.id()==ID_pointer)
5146  {
5147  find_symbols_rec(type.subtype(), recstack);
5148  }
5149  else if(type.id() == ID_struct_tag)
5150  {
5151  const auto &struct_tag = to_struct_tag_type(type);
5152  const irep_idt &id = struct_tag.get_identifier();
5153 
5154  if(recstack.find(id) == recstack.end())
5155  {
5156  const auto &base_struct = ns.follow_tag(struct_tag);
5157  recstack.insert(id);
5158  find_symbols_rec(base_struct, recstack);
5159  datatype_map[type] = datatype_map[base_struct];
5160  }
5161  }
5162  else if(type.id() == ID_union_tag)
5163  {
5164  const auto &union_tag = to_union_tag_type(type);
5165  const irep_idt &id = union_tag.get_identifier();
5166 
5167  if(recstack.find(id) == recstack.end())
5168  {
5169  recstack.insert(id);
5170  find_symbols_rec(ns.follow_tag(union_tag), recstack);
5171  }
5172  }
5173 }
5174 
5176 {
5177  return number_of_solver_calls;
5178 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
smt2_convt::set_to
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
Definition: smt2_conv.cpp:4374
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
smt2_convt::convert_typecast
void convert_typecast(const typecast_exprt &expr)
Definition: smt2_conv.cpp:2135
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
smt2_convt::solvert::CVC4
@ CVC4
smt2_convt::convert_euclidean_mod
void convert_euclidean_mod(const euclidean_mod_exprt &expr)
Definition: smt2_conv.cpp:3087
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:147
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
UNEXPECTEDCASE
#define UNEXPECTEDCASE(S)
Definition: smt2_conv.cpp:48
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
smt2_convt::solver
solvert solver
Definition: smt2_conv.h:91
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: bitvector_types.h:191
to_array_comprehension_expr
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:3195
configt::bv_encodingt::object_bits
std::size_t object_bits
Definition: config.h:255
to_vector_expr
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1586
ieee_floatt
Definition: ieee_float.h:117
format
static format_containert< T > format(const T &o)
Definition: format.h:37
pointer_logict::get_dynamic_objects
void get_dynamic_objects(std::vector< std::size_t > &objects) const
Definition: pointer_logic.cpp:34
to_extractbit_expr
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: bitvector_expr.h:411
smt2_convt::walk_array_tree
void walk_array_tree(std::unordered_map< int64_t, exprt > *operands_map, const irept &src, const array_typet &type)
This function walks the SMT output and populates a map with index/value pairs for the array.
Definition: smt2_conv.cpp:519
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
smt2_conv.h
literal_exprt::get_literal
literalt get_literal() const
Definition: literal_expr.h:26
typet::subtype
const typet & subtype() const
Definition: type.h:47
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition: invariant.h:525
to_c_bool_type
const c_bool_typet & to_c_bool_type(const typet &type)
Cast a typet to a c_bool_typet.
Definition: c_types.h:93
extractbits_exprt::lower
exprt & lower()
Definition: bitvector_expr.h:461
boolbv_widtht::membert
Definition: boolbv_width.h:30
smt2_convt::solvert::CPROVER_SMT2
@ CPROVER_SMT2
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
smt2_convt::print_assignment
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: smt2_conv.cpp:128
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1113
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:590
configt::bv_encoding
struct configt::bv_encodingt bv_encoding
arith_tools.h
struct_union_typet::get_component
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:49
smt2_convt::wheret
wheret
Definition: smt2_conv.h:210
smt2_convt::get_number_of_solver_calls
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
Definition: smt2_conv.cpp:5175
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:350
smt2_convt::wheret::END
@ END
smt2_convt::letify
letifyt letify
Definition: smt2_conv.h:157
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:265
float_bv
exprt float_bv(const exprt &src)
Definition: float_bv.h:187
smt2_convt::convert_type
void convert_type(const typet &)
Definition: smt2_conv.cpp:4828
nondet_symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:237
pos
literalt pos(literalt a)
Definition: literal.h:194
to_euclidean_mod_expr
const euclidean_mod_exprt & to_euclidean_mod_expr(const exprt &expr)
Cast an exprt to a euclidean_mod_exprt.
Definition: std_expr.h:1204
c_bit_field_replacement_type.h
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
member_offset_bits
optionalt< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:65
floatbv_typecast_exprt::op
exprt & op()
Definition: floatbv_expr.h:30
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:541
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
smt2_convt::pop
void pop() override
Currently, only implements a single stack element (no nested contexts)
Definition: smt2_conv.cpp:871
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
smt2_convt::datatype_map
datatype_mapt datatype_map
Definition: smt2_conv.h:244
threeval.h
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: bitvector_types.h:367
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
smt2_convt::parse_array
exprt parse_array(const irept &s, const array_typet &type)
This function is for parsing array output from SMT solvers when "(get-value |???|)" returns an array ...
Definition: smt2_conv.cpp:475
smt2_convt::use_array_theory
bool use_array_theory(const exprt &)
Definition: smt2_conv.cpp:4807
smt2_convt::convert_floatbv
void convert_floatbv(const exprt &expr)
Definition: smt2_conv.cpp:951
floatbv_typet::get_f
std::size_t get_f() const
Definition: bitvector_types.cpp:26
smt2_convt::use_datatypes
bool use_datatypes
Definition: smt2_conv.h:64
smt2_convt::convert
literalt convert(const exprt &expr)
Definition: smt2_conv.cpp:790
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2172
to_isinf_expr
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
Definition: floatbv_expr.h:157
has_byte_operator
bool has_byte_operator(const exprt &src)
Definition: byte_operators.cpp:2302
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: bitvector_types.h:322
boolbv_widtht::membert::offset
std::size_t offset
Definition: boolbv_width.h:31
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
replication_exprt::times
constant_exprt & times()
Definition: bitvector_expr.h:529
pointer_logict::add_object
std::size_t add_object(const exprt &expr)
Definition: pointer_logic.cpp:44
lower_byte_update
static exprt lower_byte_update(const byte_update_exprt &src, const exprt &value_as_byte_array, const optionalt< exprt > &non_const_update_bound, const namespacet &ns)
Apply a byte update src using the byte array value_as_byte_array as update value.
Definition: byte_operators.cpp:2045
fixedbv_spect::get_fraction_bits
std::size_t get_fraction_bits() const
Definition: fixedbv.h:35
prefix.h
with_exprt::new_value
exprt & new_value()
Definition: std_expr.h:2288
fixedbv.h
invariant.h
smt2_convt::solvert::MATHSAT
@ MATHSAT
smt2_convt::convert_update
void convert_update(const exprt &expr)
Definition: smt2_conv.cpp:4015
s1
int8_t s1
Definition: bytecode_info.h:59
union_exprt
Union constructor from single element.
Definition: std_expr.h:1602
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:41
to_array_of_expr
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1447
smt2_convt::convert_plus
void convert_plus(const plus_exprt &expr)
Definition: smt2_conv.cpp:3241
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:914
smt2_convt::convert_floatbv_plus
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3430
lower_byte_extract
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
Definition: byte_operators.cpp:986
fixedbv_spect::integer_bits
std::size_t integer_bits
Definition: fixedbv.h:22
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:54
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:580
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:140
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
smt2_convt::convert_expr
void convert_expr(const exprt &)
Definition: smt2_conv.cpp:985
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:550
to_bv_type
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: bitvector_types.h:82
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1648
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
bswap_exprt::get_bits_per_byte
std::size_t get_bits_per_byte() const
Definition: bitvector_expr.h:33
smt2_convt::convert_constant
void convert_constant(const constant_exprt &expr)
Definition: smt2_conv.cpp:2942
sign_exprt
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:506
exprt::op0
exprt & op0()
Definition: expr.h:99
smt2_convt::convert_literal
void convert_literal(const literalt)
Definition: smt2_conv.cpp:839
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
smt2_convt::handle
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
Definition: smt2_conv.cpp:830
irep_idt
dstringt irep_idt
Definition: irep.h:37
vector_typet
The vector type.
Definition: std_types.h:975
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
bool_typet
The Boolean type.
Definition: std_types.h:36
quantifier_exprt
A base class for quantifier expressions.
Definition: mathematical_expr.h:263
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
to_bitnot_expr
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Definition: bitvector_expr.h:106
vector_exprt
Vector constructor from list of elements.
Definition: std_expr.h:1566
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
literalt::var_no
var_not var_no() const
Definition: literal.h:83
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
make_binary
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:34
div_exprt
Division.
Definition: std_expr.h:1064
shift_exprt::op
exprt & op()
Definition: bitvector_expr.h:239
namespace.h
smt2_convt::solvert::CVC3
@ CVC3
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1225
CHECK_RETURN_WITH_DIAGNOSTICS
#define CHECK_RETURN_WITH_DIAGNOSTICS(CONDITION,...)
Definition: invariant.h:496
smt2_convt::type2id
std::string type2id(const typet &) const
Definition: smt2_conv.cpp:907
to_popcount_expr
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: bitvector_expr.h:667
smt2_convt::flatten_array
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
Definition: smt2_conv.cpp:2878
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:998
replication_exprt
Bit-vector replication.
Definition: bitvector_expr.h:518
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2209
smt2_convt::solvert::BOOLECTOR
@ BOOLECTOR
isfinite_exprt
Evaluates to true if the operand is finite.
Definition: floatbv_expr.h:176
notequal_exprt
Disequality.
Definition: std_expr.h:1283
smt2_convt::convert_is_dynamic_object
void convert_is_dynamic_object(const unary_exprt &)
Definition: smt2_conv.cpp:3121
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: bitvector_types.h:159
smt2_convt::convert_index
void convert_index(const index_exprt &expr)
Definition: smt2_conv.cpp:4022
replication_exprt::op
exprt & op()
Definition: bitvector_expr.h:539
to_floatbv_typecast_expr
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: floatbv_expr.h:68
extractbits_exprt::upper
exprt & upper()
Definition: bitvector_expr.h:456
to_literal_expr
const literal_exprt & to_literal_expr(const exprt &expr)
Cast a generic exprt to a literal_exprt.
Definition: literal_expr.h:56
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: bitvector_types.h:305
ieee_float_spect
Definition: ieee_float.h:23
expr_lowering.h
to_unary_plus_expr
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:464
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
INVARIANT_WITH_DIAGNOSTICS
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition: invariant.h:437
to_bswap_expr
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Definition: bitvector_expr.h:63
euclidean_mod_exprt
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition: std_expr.h:1179
pointer_logict::pointert::object
std::size_t object
Definition: pointer_logic.h:30
smt2_convt::convert_rounding_mode_FPA
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
Definition: smt2_conv.cpp:3373
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1668
array_typet::size
const exprt & size() const
Definition: std_types.h:771
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
to_nondet_symbol_expr
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:260
let_exprt::variables
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition: std_expr.h:3000
string2int.h
smt2_convt::notes
std::string notes
Definition: smt2_conv.h:90
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
literalt::is_true
bool is_true() const
Definition: literal.h:156
smt2_convt::to_smt2_symbol
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
Definition: smt2_conv.h:200
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
smt2_convt::number_of_solver_calls
std::size_t number_of_solver_calls
Definition: smt2_conv.h:96
with_exprt::old
exprt & old()
Definition: std_expr.h:2268
smt2_convt::convert_mult
void convert_mult(const mult_exprt &expr)
Definition: smt2_conv.cpp:3650
expr_protectedt::op0
exprt & op0()
Definition: expr.h:99
byte_operators.h
Expression classes for byte-level operators.
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
smt2_convt::convert_identifier
static std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:876
smt2_convt::convert_floatbv_div
void convert_floatbv_div(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3630
smt2_convt::prepare_for_convert_expr
exprt prepare_for_convert_expr(const exprt &expr)
Perform steps necessary before an expression is passed to convert_expr.
Definition: smt2_conv.cpp:4512
smt2_convt::push
void push() override
Unimplemented.
Definition: smt2_conv.cpp:859
smt2_convt::set_values
std::unordered_map< irep_idt, bool > set_values
The values which boolean identifiers have been smt2_convt::set_to or in other words those which are a...
Definition: smt2_conv.h:257
smt2_convt::parse_literal
constant_exprt parse_literal(const irept &, const typet &type)
Definition: smt2_conv.cpp:337
DATA_INVARIANT_WITH_DIAGNOSTICS
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:511
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
integer2bvrep
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
Definition: arith_tools.cpp:379
to_mod_expr
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1160
ieee_float_spect::width
std::size_t width() const
Definition: ieee_float.h:51
smt2_convt::solvert::YICES
@ YICES
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1044
smt2_convt::write_footer
void write_footer()
Writes the end of the SMT file to the smt_convt::out stream.
Definition: smt2_conv.cpp:181
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
struct_union_typet::componentt::get_name
const irep_idt & get_name() const
Definition: std_types.h:79
smt2_convt::convert_relation
void convert_relation(const binary_relation_exprt &)
Definition: smt2_conv.cpp:3158
floatbv_typecast_exprt
Semantic type conversion from/to floating-point formats.
Definition: floatbv_expr.h:19
smt2_convt::identifier_map
identifier_mapt identifier_map
Definition: smt2_conv.h:237
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:317
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:117
pointer_logict::pointert::offset
mp_integer offset
Definition: pointer_logic.h:31
smt2_convt::convert_mod
void convert_mod(const mod_exprt &expr)
Definition: smt2_conv.cpp:3102
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:2643
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:850
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
quantifier_exprt::symbol
symbol_exprt & symbol()
Definition: mathematical_expr.h:278
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
literal_exprt
Definition: literal_expr.h:18
nil_exprt
The NIL expression.
Definition: std_expr.h:2820
to_isfinite_expr
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
Definition: floatbv_expr.h:201
smt2_convt::smt2_symbolt::get_identifier
const irep_idt & get_identifier() const
Definition: smt2_conv.h:194
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3043
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:953
pointer_expr.h
API to expression classes for Pointers.
smt2_convt::convert_floatbv_mult
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3725
fixedbv_spect::width
std::size_t width
Definition: fixedbv.h:22
extractbits_exprt::src
exprt & src()
Definition: bitvector_expr.h:451
smt2_convt::use_check_sat_assuming
bool use_check_sat_assuming
Definition: smt2_conv.h:63
literalt::is_false
bool is_false() const
Definition: literal.h:161
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
exprt::op1
exprt & op1()
Definition: expr.h:102
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
to_notequal_expr
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1308
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
floatbv_typet::get_e
std::size_t get_e() const
Definition: bitvector_types.h:328
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2659
index_exprt::index
exprt & index()
Definition: std_expr.h:1354
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
ieee_floatt::pack
mp_integer pack() const
Definition: ieee_float.cpp:374
smt2_convt::convert_struct
void convert_struct(const struct_exprt &expr)
Definition: smt2_conv.cpp:2814
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:390
index_exprt::array
exprt & array()
Definition: std_expr.h:1344
irept::swap
void swap(irept &irep)
Definition: irep.h:453
extractbit_exprt::index
exprt & index()
Definition: bitvector_expr.h:378
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
smt2_convt::use_lambda_for_array
bool use_lambda_for_array
Definition: smt2_conv.h:65
struct_union_typet::has_component
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:157
smt2_convt::out
std::ostream & out
Definition: smt2_conv.h:89
object_size
exprt object_size(const exprt &pointer)
Definition: pointer_predicates.cpp:33
decision_proceduret::resultt::D_ERROR
@ D_ERROR
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
smt2_convt::define_object_size
void define_object_size(const irep_idt &id, const exprt &expr)
Definition: smt2_conv.cpp:232
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
smt2_convt::object_sizes
defined_expressionst object_sizes
Definition: smt2_conv.h:259
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
dstringt::empty
bool empty() const
Definition: dstring.h:88
smt2_convt::bvfp_set
std::set< irep_idt > bvfp_set
Definition: smt2_conv.h:185
abs_exprt
Absolute value.
Definition: std_expr.h:346
to_count_trailing_zeros_expr
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
Definition: bitvector_expr.h:992
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
floatbv_expr.h
API to expression classes for floating-point arithmetic.
union_typet
The union type.
Definition: c_types.h:112
smt2_convt::convert_div
void convert_div(const div_exprt &expr)
Definition: smt2_conv.cpp:3586
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
smt2_convt::use_array_of_bool
bool use_array_of_bool
Definition: smt2_conv.h:61
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:655
ieee_floatt::is_infinity
bool is_infinity() const
Definition: ieee_float.h:250
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:239
smt2_convt::convert_minus
void convert_minus(const minus_exprt &expr)
Definition: smt2_conv.cpp:3469
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: bitvector_expr.h:278
fixedbv_spect
Definition: fixedbv.h:20
tvt
Definition: threeval.h:20
literalt::sign
bool sign() const
Definition: literal.h:88
pointer_logict::objects
numberingt< exprt, irep_hash > objects
Definition: pointer_logic.h:26
decision_proceduret::resultt
resultt
Result of running the decision procedure.
Definition: decision_procedure.h:44
minus_exprt
Binary minus.
Definition: std_expr.h:973
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2320
ieee_floatt::plus_infinity
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:212
config
configt config
Definition: config.cpp:25
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: bitvector_types.h:241
smt2_convt::boolbv_width
boolbv_widtht boolbv_width
Definition: smt2_conv.h:94
ieee_floatt::spec
ieee_float_spect spec
Definition: ieee_float.h:135
fixedbv_typet
Fixed-width bit-vector with signed fixed-point interpretation.
Definition: bitvector_types.h:261
smt2_convt::find_symbols_rec
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
Definition: smt2_conv.cpp:4969
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:843
to_ieee_float_op_expr
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: floatbv_expr.h:425
bitnot_exprt
Bit-wise negation of bit-vectors.
Definition: bitvector_expr.h:82
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: bitvector_expr.h:363
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
smt2_convt::convert_with
void convert_with(const with_exprt &expr)
Definition: smt2_conv.cpp:3768
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2613
struct_union_typet::componentt
Definition: std_types.h:69
to_c_bit_field_type
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:47
expr_util.h
Deprecated expression utility functions.
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:401
shift_exprt
A base class for shift and rotate operators.
Definition: bitvector_expr.h:230
format_expr.h
string_constantt::to_array_expr
array_exprt to_array_expr() const
convert string into array constant
Definition: string_constant.cpp:29
smt2_convt::use_FPA_theory
bool use_FPA_theory
Definition: smt2_conv.h:60
smt2_convt::write_header
void write_header()
Definition: smt2_conv.cpp:151
ieee_float_op_exprt::rounding_mode
exprt & rounding_mode()
Definition: floatbv_expr.h:395
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:231
smt2_convt::logic
std::string logic
Definition: smt2_conv.h:90
pointer_offset_size
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Definition: pointer_offset_size.cpp:90
array_typet
Arrays with given size.
Definition: std_types.h:763
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2199
binding_exprt::where
exprt & where()
Definition: std_expr.h:2877
fixedbv_typet::get_fraction_bits
std::size_t get_fraction_bits() const
Definition: bitvector_types.h:267
smt2_convt::smt2_symbolt
Definition: smt2_conv.h:188
to_quantifier_expr
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: mathematical_expr.h:314
boolbv_width.h
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
to_sign_expr
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:531
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2152
shift_exprt::distance
exprt & distance()
Definition: bitvector_expr.h:249
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
smt2_convt::parse_rec
exprt parse_rec(const irept &s, const typet &type)
Definition: smt2_conv.cpp:634
isinf_exprt
Evaluates to true if the operand is infinite.
Definition: floatbv_expr.h:132
smt2_convt::dec_solve
resultt dec_solve() override
Run the decision procedure to solve the problem.
Definition: smt2_conv.cpp:270
to_implies_expr
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2008
smt2_convt::floatbv_suffix
std::string floatbv_suffix(const exprt &) const
Definition: smt2_conv.cpp:944
smt2_convt::smt2_convt
smt2_convt(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)
Definition: smt2_conv.cpp:53
extractbit_exprt::src
exprt & src()
Definition: bitvector_expr.h:373
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:407
ieee_float.h
smt2_convt::assumptions
std::vector< exprt > assumptions
Definition: smt2_conv.h:93
fixedbv_typet::get_integer_bits
std::size_t get_integer_bits() const
Definition: bitvector_types.cpp:19
smt2_convt::lower_byte_operators
exprt lower_byte_operators(const exprt &expr)
Lower byte_update and byte_extract operations within expr.
Definition: smt2_conv.cpp:4480
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2189
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
smt2_convt::convert_floatbv_rem
void convert_floatbv_rem(const binary_exprt &expr)
Definition: smt2_conv.cpp:3745
smt2_convt::parse_struct
struct_exprt parse_struct(const irept &s, const struct_typet &type)
Definition: smt2_conv.cpp:575
to_isnormal_expr
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
Definition: floatbv_expr.h:245
smt2_convt::no_boolean_variables
std::size_t no_boolean_variables
Definition: smt2_conv.h:265
literalt
Definition: literal.h:26
smt2_convt::convert_union
void convert_union(const union_exprt &expr)
Definition: smt2_conv.cpp:2909
ieee_float_op_exprt::lhs
exprt & lhs()
Definition: floatbv_expr.h:375
irept::get_sub
subt & get_sub()
Definition: irep.h:467
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:205
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
smt2_convt::ns
const namespacet & ns
Definition: smt2_conv.h:88
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:194
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
c_bit_field_replacement_type
typet c_bit_field_replacement_type(const c_bit_field_typet &src, const namespacet &ns)
Definition: c_bit_field_replacement_type.cpp:15
pointer_logict::get_invalid_object
std::size_t get_invalid_object() const
Definition: pointer_logic.h:64
smt2_convt::solvert::GENERIC
@ GENERIC
smt2_convt::emit_set_logic
bool emit_set_logic
Definition: smt2_conv.h:66
smt2_convt::pointer_logic
pointer_logict pointer_logic
Definition: smt2_conv.h:215
unsafe_string2size_t
std::size_t unsafe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:40
smt2_convt::convert_address_of_rec
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
Definition: smt2_conv.cpp:698
config.h
smt2_convt::get
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: smt2_conv.cpp:277
to_extractbits_expr
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: bitvector_expr.h:499
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1000
ieee_float_op_exprt
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: floatbv_expr.h:364
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:279
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
smt2_convt::solvert::Z3
@ Z3
bswap_exprt
The byte swap expression.
Definition: bitvector_expr.h:19
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2627
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
smt2_convt::l_get
tvt l_get(literalt l) const
Definition: smt2_conv.cpp:138
implies_exprt
Boolean implication.
Definition: std_expr.h:1983
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:702
ieee_floatt::get_sign
bool get_sign() const
Definition: ieee_float.h:248
smt2_convt::identifiert
Definition: smt2_conv.h:223
boolbv_widtht::membert::width
std::size_t width
Definition: boolbv_width.h:31
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
smt2_convt::find_symbols
void find_symbols(const exprt &expr)
Definition: smt2_conv.cpp:4527
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: bitvector_expr.h:430
exprt::operands
operandst & operands()
Definition: expr.h:92
smt2_convt::solvert
solvert
Definition: smt2_conv.h:39
float_bv.h
let_exprt::values
operandst & values()
Definition: std_expr.h:2989
integer2binary
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:64
index_exprt
Array index operator.
Definition: std_expr.h:1328
smt2_convt::boolean_assignment
std::vector< bool > boolean_assignment
Definition: smt2_conv.h:266
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
s2
int16_t s2
Definition: bytecode_info.h:60
smt2_convt::use_as_const
bool use_as_const
Definition: smt2_conv.h:62
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
ieee_floatt::NaN
static ieee_floatt NaN(const ieee_float_spect &_spec)
Definition: ieee_float.h:209
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
constant_exprt
A constant literal expression.
Definition: std_expr.h:2753
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:267
is_true
bool is_true(const literalt &l)
Definition: literal.h:198
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:844
binary_exprt::op1
exprt & op1()
Definition: expr.h:102
to_isnan_expr
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
Definition: floatbv_expr.h:113
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
let_exprt::where
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:3012
std_expr.h
API to expression classes.
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
constant_exprt::set_value
void set_value(const irep_idt &value)
Definition: std_expr.h:2766
smt2_convt::unflatten
void unflatten(wheret, const typet &, unsigned nesting=0)
Definition: smt2_conv.cpp:4270
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2761
with_exprt::where
exprt & where()
Definition: std_expr.h:2278
member_offset
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:24
boolbv_widtht::get_member
const membert & get_member(const struct_typet &type, const irep_idt &member) const
Definition: boolbv_width.cpp:202
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1467
smt2_convt::parse_union
exprt parse_union(const irept &s, const union_typet &type)
Definition: smt2_conv.cpp:559
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
ieee_float_op_exprt::rhs
exprt & rhs()
Definition: floatbv_expr.h:385
smt2_convt::convert_floatbv_minus
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3566
c_types.h
smt2_convt::flatten2bv
void flatten2bv(const exprt &)
Definition: smt2_conv.cpp:4181
isnormal_exprt
Evaluates to true if the operand is a normal number.
Definition: floatbv_expr.h:220
smt2_convt::smt2_identifiers
smt2_identifierst smt2_identifiers
Definition: smt2_conv.h:262
ieee_floatt::minus_infinity
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:215
let_exprt
A let expression.
Definition: std_expr.h:2919
pointer_logict::pointert
Definition: pointer_logic.h:29
bitwise_or
mp_integer bitwise_or(const mp_integer &a, const mp_integer &b)
bitwise 'or' of two nonnegative integers
Definition: mp_arith.cpp:215
literal_expr.h
to_count_leading_zeros_expr
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
Definition: bitvector_expr.h:899
bitvector_expr.h
API to expression classes for bitvectors.
smt2_convt::convert_floatbv_typecast
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
Definition: smt2_conv.cpp:2668
to_replication_expr
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
Definition: bitvector_expr.h:567
dstringt::size
size_t size() const
Definition: dstring.h:104
binary_exprt::op0
exprt & op0()
Definition: expr.h:99
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1691
to_abs_expr
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:370
mod_exprt
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
smt2_convt::wheret::BEGIN
@ BEGIN
ieee_float_spect::f
std::size_t f
Definition: ieee_float.h:27
SMT2_TODO
#define SMT2_TODO(S)
Definition: smt2_conv.cpp:51
pointer_logict::pointer_expr
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
Definition: pointer_logic.cpp:68
isnan_exprt
Evaluates to true if the operand is NaN.
Definition: floatbv_expr.h:88
smt2_convt::decision_procedure_text
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Definition: smt2_conv.cpp:123
mathematical_expr.h
API to expression classes for 'mathematical' expressions.
not_exprt
Boolean negation.
Definition: std_expr.h:2127
ieee_floatt::is_NaN
bool is_NaN() const
Definition: ieee_float.h:249
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
ieee_floatt::build
void build(const mp_integer &exp, const mp_integer &frac)
Definition: ieee_float.cpp:472
smt2_convt::convert_member
void convert_member(const member_exprt &expr)
Definition: smt2_conv.cpp:4120
smt2_convt::defined_expressions
defined_expressionst defined_expressions
Definition: smt2_conv.h:253