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