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  out << value;
73  }
74  else if(expr_type.id() == ID_string)
75  {
76  out << '"';
77 
78  for(const auto &c : value)
79  {
80  // " is the only escape sequence
81  if(c == '"')
82  out << '"' << '"';
83  else
84  out << c;
85  }
86 
87  out << '"';
88  }
89  else if(expr_type.id() == ID_floatbv)
90  {
91  out << value;
92  }
93  else
94  DATA_INVARIANT(false, "unhandled constant: " + expr_type.id_string());
95  }
96  else if(expr.id() == ID_symbol)
97  {
98  const auto &identifier = to_symbol_expr(expr).get_identifier();
99  if(expr.get_bool("#quoted"))
100  {
101  out << '|';
102  out << identifier;
103  out << '|';
104  }
105  else
106  out << identifier;
107  }
108  else if(expr.id() == ID_with && expr.type().id() == ID_array)
109  {
110  const auto &with_expr = to_with_expr(expr);
111  out << "(store " << smt2_format(with_expr.old()) << ' '
112  << smt2_format(with_expr.where()) << ' '
113  << smt2_format(with_expr.new_value()) << ')';
114  }
115  else if(expr.id() == ID_array_list)
116  {
117  const auto &array_list_expr = to_multi_ary_expr(expr);
118 
119  for(std::size_t i = 0; i < array_list_expr.operands().size(); i += 2)
120  out << "(store ";
121 
122  out << "((as const " << smt2_format(expr.type()) << ")) "
123  << smt2_format(from_integer(0, expr.type().subtype())) << ')';
124 
125  for(std::size_t i = 0; i < array_list_expr.operands().size(); i += 2)
126  {
128  i < array_list_expr.operands().size() - 1,
129  "array_list has even number of operands");
130  out << ' ' << smt2_format(array_list_expr.operands()[i]) << ' '
131  << smt2_format(array_list_expr.operands()[i + 1]) << ')';
132  }
133  }
134  else
135  out << "? " << expr.id();
136 
137  return out;
138 }
typet::subtype
const typet & subtype() const
Definition: type.h:47
arith_tools.h
typet
The type of an expression, extends irept.
Definition: type.h:29
exprt
Base class for all expressions.
Definition: expr.h:53
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1248
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:111
smt2_format
static smt2_format_containert< T > smt2_format(const T &_o)
Definition: smt2_format.h:25
std_types.h
Pre-defined types.
smt2_format_rec
std::ostream & smt2_format_rec(std::ostream &out, const typet &type)
Definition: smt2_format.cpp:15
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3112
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
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:866
std_expr.h
API to expression classes.
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939