cprover
smt2_conv.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_SMT2_SMT2_CONV_H
11 #define CPROVER_SOLVERS_SMT2_SMT2_CONV_H
12 
13 #include <sstream>
14 #include <set>
15 
16 #include <util/std_expr.h>
17 #include <util/byte_operators.h>
18 
19 #ifndef HASH_CODE
21 #endif
22 
23 #include <solvers/prop/prop_conv.h>
26 
27 class typecast_exprt;
28 class constant_exprt;
29 class index_exprt;
30 class member_exprt;
31 
32 class smt2_convt:public prop_convt
33 {
34 public:
35  enum class solvert
36  {
37  GENERIC,
38  BOOLECTOR,
39  CVC3,
40  CVC4,
41  MATHSAT,
42  YICES,
43  Z3
44  };
45 
47  const namespacet &_ns,
48  const std::string &_benchmark,
49  const std::string &_notes,
50  const std::string &_logic,
51  solvert _solver,
52  std::ostream &_out):
53  prop_convt(_ns),
54  use_FPA_theory(false),
55  use_datatypes(false),
56  use_array_of_bool(false),
57  emit_set_logic(true),
58  out(_out),
59  benchmark(_benchmark),
60  notes(_notes),
61  logic(_logic),
62  solver(_solver),
63  boolbv_width(_ns),
64  let_id_count(0),
65  pointer_logic(_ns),
67  {
68  // We set some defaults differently
69  // for some solvers.
70 
71  switch(solver)
72  {
73  case solvert::GENERIC:
74  break;
75 
76  case solvert::BOOLECTOR:
77  break;
78 
79  case solvert::CVC3:
80  break;
81 
82  case solvert::CVC4:
83  break;
84 
85  case solvert::MATHSAT:
86  break;
87 
88  case solvert::YICES:
89  break;
90 
91  case solvert::Z3:
92  use_array_of_bool=true;
93  emit_set_logic=false;
94  use_datatypes=true;
95  break;
96  }
97 
98  write_header();
99  }
100 
101  virtual ~smt2_convt() { }
102  virtual resultt dec_solve();
103 
108 
109  // overloading interfaces
110  virtual literalt convert(const exprt &expr);
111  virtual void set_frozen(literalt) { /* not needed */ }
112  virtual void set_to(const exprt &expr, bool value);
113  virtual exprt get(const exprt &expr) const;
114  virtual std::string decision_procedure_text() const { return "SMT2"; }
115  virtual void print_assignment(std::ostream &out) const;
116  virtual tvt l_get(literalt l) const;
117  virtual void set_assumptions(const bvt &bv) { assumptions=bv; }
118 
119  // new stuff
120  void convert_expr(const exprt &);
121  void convert_type(const typet &);
122  void convert_literal(const literalt);
123 
124 protected:
125  std::ostream &out;
126  std::string benchmark, notes, logic;
128 
131 
132  void write_header();
133  void write_footer(std::ostream &);
134 
135  // tweaks for arrays
136  bool use_array_theory(const exprt &);
137  void flatten_array(const exprt &);
138  void unflatten_array(const exprt &);
139 
140  // specific expressions go here
141  void convert_byte_update(const byte_update_exprt &expr);
142  void convert_byte_extract(const byte_extract_exprt &expr);
143  void convert_typecast(const typecast_exprt &expr);
145  void convert_struct(const struct_exprt &expr);
146  void convert_union(const union_exprt &expr);
147  void convert_constant(const constant_exprt &expr);
148  void convert_relation(const exprt &expr);
149  void convert_is_dynamic_object(const exprt &expr);
150  void convert_plus(const plus_exprt &expr);
151  void convert_minus(const minus_exprt &expr);
152  void convert_div(const div_exprt &expr);
153  void convert_mult(const mult_exprt &expr);
154  void convert_rounding_mode_FPA(const exprt &expr);
155  void convert_floatbv_plus(const ieee_float_op_exprt &expr);
156  void convert_floatbv_minus(const ieee_float_op_exprt &expr);
157  void convert_floatbv_div(const ieee_float_op_exprt &expr);
158  void convert_floatbv_mult(const ieee_float_op_exprt &expr);
159  void convert_mod(const mod_exprt &expr);
160  void convert_index(const index_exprt &expr);
161  void convert_member(const member_exprt &expr);
162  void convert_overflow(const exprt &expr);
163  void convert_with(const with_exprt &expr);
164  void convert_update(const exprt &expr);
165 
166  std::string convert_identifier(const irep_idt &identifier);
167 
168  // introduces a let-expression for operands
169  exprt convert_operands(const exprt &);
170 
171  // auxiliary methods
172  void find_symbols(const exprt &expr);
173  void find_symbols(const typet &type);
174  void find_symbols_rec(const typet &type, std::set<irep_idt> &recstack);
175 
176  // letification
178  {
179  let_count_idt(std::size_t _count, const symbol_exprt &_let_symbol)
180  : count(_count), let_symbol(_let_symbol)
181  {
182  }
183 
184  std::size_t count;
186  };
187 
188 #ifdef HASH_CODE
189  typedef std::unordered_map<exprt, let_count_idt, irep_hash> seen_expressionst;
190 #else
192 #endif
193 
194  std::size_t let_id_count;
195  static const std::size_t LET_COUNT = 2;
196 
198  {
200 
201  public:
202  explicit let_visitort(const seen_expressionst &map):let_map(map) { }
203 
204  void operator()(exprt &expr)
205  {
207  if(it != let_map.end() && it->second.count >= LET_COUNT)
208  {
209  const symbol_exprt &symb = it->second.let_symbol;
210  expr=symb;
211  }
212  }
213  };
214 
215  exprt letify(exprt &expr);
217  exprt &expr,
218  std::vector<exprt> &let_order,
219  const seen_expressionst &map,
220  std::size_t i);
221 
222  void collect_bindings(
223  exprt &expr,
224  seen_expressionst &map,
225  std::vector<exprt> &let_order);
226 
228  exprt &expr,
229  const seen_expressionst &map);
230 
231  // Parsing solver responses
232  constant_exprt parse_literal(const irept &, const typet &type);
233  exprt parse_struct(const irept &s, const struct_typet &type);
234  exprt parse_union(const irept &s, const union_typet &type);
235  exprt parse_array(const irept &s, const array_typet &type);
236  exprt parse_rec(const irept &s, const typet &type);
237 
238  // we use this to build a bit-vector encoding of the FPA theory
239  void convert_floatbv(const exprt &expr);
240  std::string type2id(const typet &) const;
241  std::string floatbv_suffix(const exprt &) const;
242  std::set<irep_idt> bvfp_set; // already converted
243 
244  class smt2_symbolt:public exprt
245  {
246  public:
247  smt2_symbolt(const irep_idt &_identifier, const typet &_type):
248  exprt(ID_smt2_symbol, _type)
249  { set(ID_identifier, _identifier); }
250 
251  const irep_idt &get_identifier() const
252  {
253  return get(ID_identifier);
254  }
255  };
256 
257  const smt2_symbolt &to_smt2_symbol(const exprt &expr)
258  {
259  assert(expr.id()==ID_smt2_symbol && !expr.has_operands());
260  return static_cast<const smt2_symbolt&>(expr);
261  }
262 
263  // flattens any non-bitvector type into a bitvector,
264  // e.g., booleans, vectors, structs, arrays but also
265  // floats when using the FPA theory.
266  // unflatten() does the opposite.
267  enum class wheret { BEGIN, END };
268  void flatten2bv(const exprt &);
269  void unflatten(wheret, const typet &, unsigned nesting=0);
270 
271  // pointers
274  const exprt &expr, const pointer_typet &result_type);
275 
276  void define_object_size(const irep_idt &id, const exprt &expr);
277 
278  // keeps track of all non-Boolean symbols and their value
279  struct identifiert
280  {
283 
285  {
286  type.make_nil();
287  value.make_nil();
288  }
289  };
290 
291  typedef std::unordered_map<irep_idt, identifiert> identifier_mapt;
292 
294 
295  // for modeling structs as Z3 datatype, enabled when
296  // use_datatype is set
297  typedef std::map<typet, std::string> datatype_mapt;
299 
300  // for replacing various defined expressions:
301  //
302  // ID_array_of
303  // ID_array
304  // ID_string_constant
305 
306  typedef std::map<exprt, irep_idt> defined_expressionst;
308 
310 
311  typedef std::set<std::string> smt2_identifierst;
313 
314  // Boolean part
315  std::size_t no_boolean_variables;
316  std::vector<bool> boolean_assignment;
317 };
318 
319 #endif // CPROVER_SOLVERS_SMT2_SMT2_CONV_H
void unflatten(wheret, const typet &, unsigned nesting=0)
Definition: smt2_conv.cpp:3957
The type of an expression.
Definition: type.h:22
smt2_symbolt(const irep_idt &_identifier, const typet &_type)
Definition: smt2_conv.h:247
exprt parse_union(const irept &s, const union_typet &type)
Definition: smt2_conv.cpp:369
exprt convert_operands(const exprt &)
IREP Hash Container.
datatype_mapt datatype_map
Definition: smt2_conv.h:298
virtual tvt l_get(literalt l) const
Definition: smt2_conv.cpp:61
semantic type conversion
Definition: std_expr.h:2111
void flatten2bv(const exprt &)
Definition: smt2_conv.cpp:3861
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
Definition: smt2_conv.cpp:2370
exprt parse_array(const irept &s, const array_typet &type)
Definition: smt2_conv.cpp:339
exprt letify(exprt &expr)
Definition: smt2_conv.cpp:4733
let_count_idt(std::size_t _count, const symbol_exprt &_let_symbol)
Definition: smt2_conv.h:179
virtual resultt dec_solve()
Definition: smt2_conv.cpp:172
void convert_literal(const literalt)
Definition: smt2_conv.cpp:742
void convert_typecast(const typecast_exprt &expr)
Definition: smt2_conv.cpp:1873
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3121
void convert_expr(const exprt &)
Definition: smt2_conv.cpp:866
void convert_constant(const constant_exprt &expr)
Definition: smt2_conv.cpp:2646
bool use_datatypes
Definition: smt2_conv.h:105
void convert_update(const exprt &expr)
Definition: smt2_conv.cpp:3687
const_iterator find(const Key &key) const
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
Definition: smt2_conv.h:257
void convert_floatbv(const exprt &expr)
Definition: smt2_conv.cpp:833
std::unordered_map< irep_idt, identifiert > identifier_mapt
Definition: smt2_conv.h:291
void convert_plus(const plus_exprt &expr)
Definition: smt2_conv.cpp:2927
std::string type2id(const typet &) const
Definition: smt2_conv.cpp:793
A constant literal expression.
Definition: std_expr.h:4422
std::string notes
Definition: smt2_conv.h:126
Structure type.
Definition: std_types.h:297
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
Definition: smt2_conv.cpp:2579
virtual void set_assumptions(const bvt &bv)
Definition: smt2_conv.h:117
identifier_mapt identifier_map
Definition: smt2_conv.h:293
void convert_type(const typet &)
Definition: smt2_conv.cpp:4380
std::size_t let_id_count
Definition: smt2_conv.h:194
bool use_array_theory(const exprt &)
Definition: smt2_conv.cpp:4358
Extract member of struct or union.
Definition: std_expr.h:3869
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3418
exprt substitute_let(exprt &expr, const seen_expressionst &map)
Definition: smt2_conv.cpp:4798
virtual literalt convert(const exprt &expr)
Definition: smt2_conv.cpp:710
void convert_mult(const mult_exprt &expr)
Definition: smt2_conv.cpp:3343
void convert_relation(const exprt &expr)
Definition: smt2_conv.cpp:2842
const irep_idt & id() const
Definition: irep.h:259
void define_object_size(const irep_idt &id, const exprt &expr)
Definition: smt2_conv.cpp:134
Expression classes for byte-level operators.
virtual void print_assignment(std::ostream &out) const
Definition: smt2_conv.cpp:51
defined_expressionst object_sizes
Definition: smt2_conv.h:309
division (integer and real)
Definition: std_expr.h:1075
void convert_mod(const mod_exprt &expr)
Definition: smt2_conv.cpp:2782
virtual std::string decision_procedure_text() const
Definition: smt2_conv.h:114
void operator()(exprt &expr)
Definition: smt2_conv.h:204
void convert_floatbv_div(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3324
void convert_struct(const struct_exprt &expr)
Definition: smt2_conv.cpp:2516
The pointer type.
Definition: std_types.h:1435
symbol_exprt let_symbol
Definition: smt2_conv.h:185
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
Definition: smt2_conv.cpp:3065
void convert_div(const div_exprt &expr)
Definition: smt2_conv.cpp:3278
union constructor from single element
Definition: std_expr.h:1730
API to expression classes.
void convert_index(const index_exprt &expr)
Definition: smt2_conv.cpp:3694
Definition: threeval.h:19
boolbv_widtht boolbv_width
Definition: smt2_conv.h:130
exprt letify_rec(exprt &expr, std::vector< exprt > &let_order, const seen_expressionst &map, std::size_t i)
Definition: smt2_conv.cpp:4743
virtual void set_frozen(literalt)
Definition: smt2_conv.h:111
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
Definition: smt2_conv.cpp:4537
Base class for tree-like data structures with sharing.
Definition: irep.h:156
std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:762
The plus expression.
Definition: std_expr.h:893
constant_exprt parse_literal(const irept &, const typet &type)
Definition: smt2_conv.cpp:211
void write_header()
Definition: smt2_conv.cpp:71
void convert_minus(const minus_exprt &expr)
Definition: smt2_conv.cpp:3157
const_iterator end() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
std::string floatbv_suffix(const exprt &) const
Definition: smt2_conv.cpp:827
const irep_idt & get_identifier() const
Definition: smt2_conv.h:251
bool has_operands() const
Definition: expr.h:63
smt2_convt(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)
Definition: smt2_conv.h:46
virtual ~smt2_convt()
Definition: smt2_conv.h:101
binary multiplication
Definition: std_expr.h:1017
std::map< typet, std::string > datatype_mapt
Definition: smt2_conv.h:297
bool use_array_of_bool
Definition: smt2_conv.h:106
typename mapt::const_iterator const_iterator
void convert_byte_update(const byte_update_exprt &expr)
Definition: smt2_conv.cpp:607
std::ostream & out
Definition: smt2_conv.h:125
std::string benchmark
Definition: smt2_conv.h:126
void convert_is_dynamic_object(const exprt &expr)
Definition: smt2_conv.cpp:2803
void unflatten_array(const exprt &)
semantic type conversion from/to floating-point formats
Definition: std_expr.h:2176
const seen_expressionst & let_map
Definition: smt2_conv.h:199
Base class for all expressions.
Definition: expr.h:42
std::set< irep_idt > bvfp_set
Definition: smt2_conv.h:242
The union type.
Definition: std_types.h:458
let_visitort(const seen_expressionst &map)
Definition: smt2_conv.h:202
Operator to update elements in structs and arrays.
Definition: std_expr.h:3459
void convert_overflow(const exprt &expr)
Definition: smt2_conv.cpp:4072
void find_symbols(const exprt &expr)
Definition: smt2_conv.cpp:4165
std::size_t no_boolean_variables
Definition: smt2_conv.h:315
void convert_member(const member_exprt &expr)
Definition: smt2_conv.cpp:3796
exprt parse_rec(const irept &s, const typet &type)
Definition: smt2_conv.cpp:445
void make_nil()
Definition: irep.h:315
arrays with given size
Definition: std_types.h:1013
void convert_union(const union_exprt &expr)
Definition: smt2_conv.cpp:2613
virtual void set_to(const exprt &expr, bool value)
Definition: smt2_conv.cpp:4077
static const std::size_t LET_COUNT
Definition: smt2_conv.h:195
binary minus
Definition: std_expr.h:959
TO_BE_DOCUMENTED.
void convert_with(const with_exprt &expr)
Definition: smt2_conv.cpp:3437
Expression to hold a symbol (variable)
Definition: std_expr.h:90
std::vector< bool > boolean_assignment
Definition: smt2_conv.h:316
solvert solver
Definition: smt2_conv.h:127
std::string logic
Definition: smt2_conv.h:126
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
Definition: smt2_conv.cpp:499
void convert_byte_extract(const byte_extract_exprt &expr)
Definition: smt2_conv.cpp:598
std::map< exprt, irep_idt > defined_expressionst
Definition: smt2_conv.h:306
Pointer Logic.
exprt parse_struct(const irept &s, const struct_typet &type)
Definition: smt2_conv.cpp:384
bool use_FPA_theory
Definition: smt2_conv.h:104
void write_footer(std::ostream &)
Definition: smt2_conv.cpp:97
TO_BE_DOCUMENTED.
struct constructor from list of elements
Definition: std_expr.h:1815
std::set< std::string > smt2_identifierst
Definition: smt2_conv.h:311
bool emit_set_logic
Definition: smt2_conv.h:107
bvt assumptions
Definition: smt2_conv.h:129
IEEE floating-point operations.
Definition: std_expr.h:4314
smt2_identifierst smt2_identifiers
Definition: smt2_conv.h:312
std::vector< literalt > bvt
Definition: literal.h:200
defined_expressionst defined_expressions
Definition: smt2_conv.h:307
binary modulo
Definition: std_expr.h:1133
pointer_logict pointer_logic
Definition: smt2_conv.h:272
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3259
void collect_bindings(exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)
Definition: smt2_conv.cpp:4767
irep_hash_mapt< exprt, let_count_idt > seen_expressionst
Definition: smt2_conv.h:191
array index operator
Definition: std_expr.h:1462