cprover
smt2_format.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "smt2_format.h"
10 
11 #include <util/arith_tools.h>
12 #include <util/bitvector_types.h>
13 
14 std::ostream &smt2_format_rec(std::ostream &out, const typet &type)
15 {
16  if(type.id() == ID_unsignedbv)
17  out << "(_ BitVec " << to_unsignedbv_type(type).get_width() << ')';
18  else if(type.id() == ID_bool)
19  out << "Bool";
20  else if(type.id() == ID_integer)
21  out << "Int";
22  else if(type.id() == ID_real)
23  out << "Real";
24  else if(type.id() == ID_array)
25  {
26  const auto &array_type = to_array_type(type);
27  out << "(Array " << smt2_format(array_type.size().type()) << ' '
28  << smt2_format(array_type.subtype()) << ')';
29  }
30  else if(type.id() == ID_floatbv)
31  {
32  const auto &floatbv_type = to_floatbv_type(type);
33  // the width of the mantissa needs to be increased by one to
34  // include the hidden bit
35  out << "(_ FloatingPoint " << floatbv_type.get_e() << ' '
36  << floatbv_type.get_f() + 1 << ')';
37  }
38  else
39  out << "? " << type.id();
40 
41  return out;
42 }
43 
44 std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
45 {
46  if(expr.id() == ID_constant)
47  {
48  const auto &constant_expr = to_constant_expr(expr);
49  const auto &value = constant_expr.get_value();
50  const typet &expr_type = expr.type();
51 
52  if(expr_type.id() == ID_unsignedbv)
53  {
54  const std::size_t width = to_unsignedbv_type(expr_type).get_width();
55 
56  const auto int_value = numeric_cast_v<mp_integer>(constant_expr);
57 
58  out << "(_ bv" << int_value << " " << width << ")";
59  }
60  else if(expr_type.id() == ID_bool)
61  {
62  if(expr.is_true())
63  out << "true";
64  else if(expr.is_false())
65  out << "false";
66  else
67  DATA_INVARIANT(false, "unknown Boolean constant");
68  }
69  else if(expr_type.id() == ID_integer)
70  {
71  // negative numbers need to be encoded using a unary minus expression
72  auto int_value = numeric_cast_v<mp_integer>(constant_expr);
73  if(int_value < 0)
74  out << "(- " << -int_value << ')';
75  else
76  out << int_value;
77  }
78  else if(expr_type.id() == ID_string)
79  {
80  out << '"';
81 
82  for(const auto &c : value)
83  {
84  // " is the only escape sequence
85  if(c == '"')
86  out << '"' << '"';
87  else
88  out << c;
89  }
90 
91  out << '"';
92  }
93  else if(expr_type.id() == ID_floatbv)
94  {
95  out << value;
96  }
97  else
98  DATA_INVARIANT(false, "unhandled constant: " + expr_type.id_string());
99  }
100  else if(expr.id() == ID_symbol)
101  {
102  const auto &identifier = to_symbol_expr(expr).get_identifier();
103  if(expr.get_bool("#quoted"))
104  {
105  out << '|';
106  out << identifier;
107  out << '|';
108  }
109  else
110  out << identifier;
111  }
112  else if(expr.id() == ID_with && expr.type().id() == ID_array)
113  {
114  const auto &with_expr = to_with_expr(expr);
115  out << "(store " << smt2_format(with_expr.old()) << ' '
116  << smt2_format(with_expr.where()) << ' '
117  << smt2_format(with_expr.new_value()) << ')';
118  }
119  else if(expr.id() == ID_array_list)
120  {
121  const auto &array_list_expr = to_multi_ary_expr(expr);
122 
123  for(std::size_t i = 0; i < array_list_expr.operands().size(); i += 2)
124  out << "(store ";
125 
126  out << "((as const " << smt2_format(expr.type()) << ")) "
127  << smt2_format(from_integer(0, expr.type().subtype())) << ')';
128 
129  for(std::size_t i = 0; i < array_list_expr.operands().size(); i += 2)
130  {
132  i < array_list_expr.operands().size() - 1,
133  "array_list has even number of operands");
134  out << ' ' << smt2_format(array_list_expr.operands()[i]) << ' '
135  << smt2_format(array_list_expr.operands()[i + 1]) << ')';
136  }
137  }
138  else
139  out << "? " << expr.id();
140 
141  return out;
142 }
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: bitvector_types.h:191
typet::subtype
const typet & subtype() const
Definition: type.h:47
arith_tools.h
typet
The type of an expression, extends irept.
Definition: type.h:28
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: bitvector_types.h:367
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:60
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:69
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
bitvector_types.h
Pre-defined bitvector types.
smt2_format
static smt2_format_containert< T > smt2_format(const T &_o)
Definition: smt2_format.h:25
smt2_format_rec
std::ostream & smt2_format_rec(std::ostream &out, const typet &type)
Definition: smt2_format.cpp:14
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2234
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
smt2_format.h
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:815
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700