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