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 #include <solvers/prop/prop_conv.h>
22 
23 class typecast_exprt;
24 class constant_exprt;
25 class index_exprt;
26 class member_exprt;
27 
28 class smt2_convt:public prop_convt
29 {
30 public:
31  enum class solvert
32  {
33  GENERIC,
34  BOOLECTOR,
35  CVC3,
36  CVC4,
37  MATHSAT,
38  OPENSMT,
39  YICES,
40  Z3
41  };
42 
44  const namespacet &_ns,
45  const std::string &_benchmark,
46  const std::string &_notes,
47  const std::string &_logic,
48  solvert _solver,
49  std::ostream &_out):
50  prop_convt(_ns),
51  use_FPA_theory(false),
52  use_datatypes(false),
53  use_array_of_bool(false),
54  emit_set_logic(true),
55  out(_out),
56  benchmark(_benchmark),
57  notes(_notes),
58  logic(_logic),
59  solver(_solver),
60  boolbv_width(_ns),
61  let_id_count(0),
62  pointer_logic(_ns),
64  {
65  // We set some defaults differently
66  // for some solvers.
67 
68  switch(solver)
69  {
70  case solvert::GENERIC:
71  break;
72 
73  case solvert::BOOLECTOR:
74  break;
75 
76  case solvert::CVC3:
77  break;
78 
79  case solvert::CVC4:
80  break;
81 
82  case solvert::MATHSAT:
83  break;
84 
85  case solvert::OPENSMT:
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 a) { /* 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
177  typedef std::pair<unsigned, symbol_exprt> let_count_idt;
178  typedef std::unordered_map<exprt, let_count_idt, irep_hash> seen_expressionst;
179  unsigned let_id_count;
180  static const unsigned LET_COUNT=2;
181 
183  {
185 
186  public:
187  explicit let_visitort(const seen_expressionst &map):let_map(map) { }
188 
189  void operator()(exprt &expr)
190  {
191  seen_expressionst::const_iterator it=let_map.find(expr);
192  if(it!=let_map.end() &&
193  it->second.first>=LET_COUNT)
194  {
195  symbol_exprt symb=it->second.second;
196  expr=symb;
197  }
198  }
199  };
200 
201  exprt letify(exprt &expr);
203  exprt &expr,
204  std::vector<exprt> &let_order,
205  const seen_expressionst &map,
206  unsigned i);
207 
208  void collect_bindings(
209  exprt &expr,
210  seen_expressionst &map,
211  std::vector<exprt> &let_order);
212 
214  exprt &expr,
215  const seen_expressionst &map);
216 
217  // Parsing solver responses
218  constant_exprt parse_literal(const irept &, const typet &type);
219  exprt parse_struct(const irept &s, const struct_typet &type);
220  exprt parse_union(const irept &s, const union_typet &type);
221  exprt parse_array(const irept &s, const array_typet &type);
222  exprt parse_rec(const irept &s, const typet &type);
223 
224  // we use this to build a bit-vector encoding of the FPA theory
225  void convert_floatbv(const exprt &expr);
226  std::string type2id(const typet &) const;
227  std::string floatbv_suffix(const exprt &) const;
228  std::set<irep_idt> bvfp_set; // already converted
229 
230  class smt2_symbolt:public exprt
231  {
232  public:
233  smt2_symbolt(const irep_idt &_identifier, const typet &_type):
234  exprt(ID_smt2_symbol, _type)
235  { set(ID_identifier, _identifier); }
236 
237  const irep_idt &get_identifier() const
238  {
239  return get(ID_identifier);
240  }
241  };
242 
243  const smt2_symbolt &to_smt2_symbol(const exprt &expr)
244  {
245  assert(expr.id()==ID_smt2_symbol && !expr.has_operands());
246  return static_cast<const smt2_symbolt&>(expr);
247  }
248 
249  // flattens any non-bitvector type into a bitvector,
250  // e.g., booleans, vectors, structs, arrays but also
251  // floats when using the FPA theory.
252  // unflatten() does the opposite.
253  enum class wheret { BEGIN, END };
254  void flatten2bv(const exprt &);
255  void unflatten(wheret, const typet &, unsigned nesting=0);
256 
257  // pointers
260  const exprt &expr, const pointer_typet &result_type);
261 
262  void define_object_size(const irep_idt &id, const exprt &expr);
263 
264  // keeps track of all non-Boolean symbols and their value
265  struct identifiert
266  {
269 
271  {
272  type.make_nil();
273  value.make_nil();
274  }
275  };
276 
277  typedef std::unordered_map<irep_idt, identifiert, irep_id_hash>
279 
281 
282  // for modeling structs as Z3 datatype, enabled when
283  // use_datatype is set
284  typedef std::map<typet, std::string> datatype_mapt;
286 
287  // for replacing various defined expressions:
288  //
289  // ID_array_of
290  // ID_array
291  // ID_string_constant
292 
293  typedef std::map<exprt, irep_idt> defined_expressionst;
295 
297 
298  typedef std::set<std::string> smt2_identifierst;
300 
301  // Boolean part
303  std::vector<bool> boolean_assignment;
304 };
305 
306 #endif // CPROVER_SOLVERS_SMT2_SMT2_CONV_H
void unflatten(wheret, const typet &, unsigned nesting=0)
Definition: smt2_conv.cpp:3837
The type of an expression.
Definition: type.h:20
smt2_symbolt(const irep_idt &_identifier, const typet &_type)
Definition: smt2_conv.h:233
exprt parse_union(const irept &s, const union_typet &type)
Definition: smt2_conv.cpp:352
exprt convert_operands(const exprt &)
datatype_mapt datatype_map
Definition: smt2_conv.h:285
virtual tvt l_get(literalt l) const
Definition: smt2_conv.cpp:61
semantic type conversion
Definition: std_expr.h:1725
void flatten2bv(const exprt &)
Definition: smt2_conv.cpp:3741
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
Definition: smt2_conv.cpp:2280
exprt parse_array(const irept &s, const array_typet &type)
Definition: smt2_conv.cpp:322
exprt letify(exprt &expr)
Definition: smt2_conv.cpp:4613
unsigned let_id_count
Definition: smt2_conv.h:179
virtual resultt dec_solve()
Definition: smt2_conv.cpp:172
void convert_literal(const literalt)
Definition: smt2_conv.cpp:722
void convert_typecast(const typecast_exprt &expr)
Definition: smt2_conv.cpp:1796
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3014
void convert_expr(const exprt &)
Definition: smt2_conv.cpp:846
void convert_constant(const constant_exprt &expr)
Definition: smt2_conv.cpp:2556
bool use_datatypes
Definition: smt2_conv.h:105
void convert_update(const exprt &expr)
Definition: smt2_conv.cpp:3567
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
Definition: smt2_conv.h:243
void convert_floatbv(const exprt &expr)
Definition: smt2_conv.cpp:813
std::unordered_map< exprt, let_count_idt, irep_hash > seen_expressionst
Definition: smt2_conv.h:178
void convert_plus(const plus_exprt &expr)
Definition: smt2_conv.cpp:2837
std::string type2id(const typet &) const
Definition: smt2_conv.cpp:773
A constant literal expression.
Definition: std_expr.h:3685
exprt letify_rec(exprt &expr, std::vector< exprt > &let_order, const seen_expressionst &map, unsigned i)
Definition: smt2_conv.cpp:4623
std::string notes
Definition: smt2_conv.h:126
Structure type.
Definition: std_types.h:296
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
Definition: smt2_conv.cpp:2489
virtual void set_assumptions(const bvt &bv)
Definition: smt2_conv.h:117
identifier_mapt identifier_map
Definition: smt2_conv.h:280
void convert_type(const typet &)
Definition: smt2_conv.cpp:4260
bool use_array_theory(const exprt &)
Definition: smt2_conv.cpp:4238
static const unsigned LET_COUNT
Definition: smt2_conv.h:180
Extract member of struct or union.
Definition: std_expr.h:3214
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3301
exprt substitute_let(exprt &expr, const seen_expressionst &map)
Definition: smt2_conv.cpp:4678
virtual literalt convert(const exprt &expr)
Definition: smt2_conv.cpp:690
void convert_mult(const mult_exprt &expr)
Definition: smt2_conv.cpp:3228
void convert_relation(const exprt &expr)
Definition: smt2_conv.cpp:2752
const irep_idt & id() const
Definition: irep.h:189
void define_object_size(const irep_idt &id, const exprt &expr)
Definition: smt2_conv.cpp:135
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:296
division (integer and real)
Definition: std_expr.h:854
void convert_mod(const mod_exprt &expr)
Definition: smt2_conv.cpp:2692
virtual std::string decision_procedure_text() const
Definition: smt2_conv.h:114
void operator()(exprt &expr)
Definition: smt2_conv.h:189
void convert_floatbv_div(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3209
void convert_struct(const struct_exprt &expr)
Definition: smt2_conv.cpp:2426
The pointer type.
Definition: std_types.h:1343
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
Definition: smt2_conv.cpp:2958
void convert_div(const div_exprt &expr)
Definition: smt2_conv.cpp:3163
std::pair< unsigned, symbol_exprt > let_count_idt
Definition: smt2_conv.h:177
union constructor from single element
Definition: std_expr.h:1389
API to expression classes.
void convert_index(const index_exprt &expr)
Definition: smt2_conv.cpp:3574
Definition: threeval.h:19
boolbv_widtht boolbv_width
Definition: smt2_conv.h:130
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
Definition: smt2_conv.cpp:4417
Base class for tree-like data structures with sharing.
Definition: irep.h:87
std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:742
The plus expression.
Definition: std_expr.h:702
constant_exprt parse_literal(const irept &, const typet &type)
Definition: smt2_conv.cpp:202
void write_header()
Definition: smt2_conv.cpp:71
void convert_minus(const minus_exprt &expr)
Definition: smt2_conv.cpp:3050
std::string floatbv_suffix(const exprt &) const
Definition: smt2_conv.cpp:807
const irep_idt & get_identifier() const
Definition: smt2_conv.h:237
bool has_operands() const
Definition: expr.h:67
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:43
virtual ~smt2_convt()
Definition: smt2_conv.h:101
binary multiplication
Definition: std_expr.h:806
unsigned no_boolean_variables
Definition: smt2_conv.h:302
std::map< typet, std::string > datatype_mapt
Definition: smt2_conv.h:284
bool use_array_of_bool
Definition: smt2_conv.h:106
void convert_byte_update(const byte_update_exprt &expr)
Definition: smt2_conv.cpp:586
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:2713
void unflatten_array(const exprt &)
semantic type conversion from/to floating-point formats
Definition: std_expr.h:1783
const seen_expressionst & let_map
Definition: smt2_conv.h:184
Base class for all expressions.
Definition: expr.h:46
std::set< irep_idt > bvfp_set
Definition: smt2_conv.h:228
The union type.
Definition: std_types.h:424
let_visitort(const seen_expressionst &map)
Definition: smt2_conv.h:187
Operator to update elements in structs and arrays.
Definition: std_expr.h:2861
void convert_overflow(const exprt &expr)
Definition: smt2_conv.cpp:3952
void find_symbols(const exprt &expr)
Definition: smt2_conv.cpp:4045
void convert_member(const member_exprt &expr)
Definition: smt2_conv.cpp:3676
exprt parse_rec(const irept &s, const typet &type)
Definition: smt2_conv.cpp:428
void make_nil()
Definition: irep.h:243
arrays with given size
Definition: std_types.h:901
void convert_union(const union_exprt &expr)
Definition: smt2_conv.cpp:2523
virtual void set_to(const exprt &expr, bool value)
Definition: smt2_conv.cpp:3957
binary minus
Definition: std_expr.h:758
TO_BE_DOCUMENTED.
void convert_with(const with_exprt &expr)
Definition: smt2_conv.cpp:3320
Expression to hold a symbol (variable)
Definition: std_expr.h:82
std::vector< bool > boolean_assignment
Definition: smt2_conv.h:303
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:479
void convert_byte_extract(const byte_extract_exprt &expr)
Definition: smt2_conv.cpp:577
std::map< exprt, irep_idt > defined_expressionst
Definition: smt2_conv.h:293
Pointer Logic.
exprt parse_struct(const irept &s, const struct_typet &type)
Definition: smt2_conv.cpp:367
bool use_FPA_theory
Definition: smt2_conv.h:104
void write_footer(std::ostream &)
Definition: smt2_conv.cpp:98
TO_BE_DOCUMENTED.
struct constructor from list of elements
Definition: std_expr.h:1464
std::set< std::string > smt2_identifierst
Definition: smt2_conv.h:298
bool emit_set_logic
Definition: smt2_conv.h:107
bvt assumptions
Definition: smt2_conv.h:129
IEEE floating-point operations.
Definition: std_expr.h:3591
std::unordered_map< irep_idt, identifiert, irep_id_hash > identifier_mapt
Definition: smt2_conv.h:278
smt2_identifierst smt2_identifiers
Definition: smt2_conv.h:299
std::vector< literalt > bvt
Definition: literal.h:197
defined_expressionst defined_expressions
Definition: smt2_conv.h:294
binary modulo
Definition: std_expr.h:902
pointer_logict pointer_logic
Definition: smt2_conv.h:258
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3144
void collect_bindings(exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)
Definition: smt2_conv.cpp:4647
array index operator
Definition: std_expr.h:1170
virtual void set_frozen(literalt a)
Definition: smt2_conv.h:111