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