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 <map>
14 #include <set>
15 #include <sstream>
16 
17 #include <util/std_expr.h>
18 #include <util/threeval.h>
19 
20 #if !HASH_CODE
22 #endif
23 
26 #include <solvers/prop/literal.h>
28 
29 #include "letify.h"
30 
33 class union_typet;
34 
36 {
37 public:
38  enum class solvert
39  {
40  GENERIC,
41  BOOLECTOR,
43  CVC3,
44  CVC4,
45  MATHSAT,
46  YICES,
47  Z3
48  };
49 
50  smt2_convt(
51  const namespacet &_ns,
52  const std::string &_benchmark,
53  const std::string &_notes,
54  const std::string &_logic,
55  solvert _solver,
56  std::ostream &_out);
57 
58  ~smt2_convt() override = default;
59 
67 
68  exprt handle(const exprt &expr) override;
69  void set_to(const exprt &expr, bool value) override;
70  exprt get(const exprt &expr) const override;
71  std::string decision_procedure_text() const override;
72  void print_assignment(std::ostream &out) const override;
73 
75  void push() override;
76 
78  void push(const std::vector<exprt> &_assumptions) override;
79 
81  void pop() override;
82 
83  std::size_t get_number_of_solver_calls() const override;
84 
85  static std::string convert_identifier(const irep_idt &identifier);
86 
87 protected:
88  const namespacet &ns;
89  std::ostream &out;
90  std::string benchmark, notes, logic;
92 
93  std::vector<exprt> assumptions;
95 
96  std::size_t number_of_solver_calls = 0;
97 
98  resultt dec_solve() override;
99 
100  void write_header();
110  void write_footer();
111 
112  // tweaks for arrays
113  bool use_array_theory(const exprt &);
114  void flatten_array(const exprt &);
115 
116  // specific expressions go here
117  void convert_typecast(const typecast_exprt &expr);
119  void convert_struct(const struct_exprt &expr);
120  void convert_union(const union_exprt &expr);
121  void convert_constant(const constant_exprt &expr);
124  void convert_plus(const plus_exprt &expr);
125  void convert_minus(const minus_exprt &expr);
126  void convert_div(const div_exprt &expr);
127  void convert_mult(const mult_exprt &expr);
128  void convert_rounding_mode_FPA(const exprt &expr);
129  void convert_floatbv_plus(const ieee_float_op_exprt &expr);
130  void convert_floatbv_minus(const ieee_float_op_exprt &expr);
131  void convert_floatbv_div(const ieee_float_op_exprt &expr);
132  void convert_floatbv_mult(const ieee_float_op_exprt &expr);
133  void convert_floatbv_rem(const binary_exprt &expr);
134  void convert_mod(const mod_exprt &expr);
135  void convert_euclidean_mod(const euclidean_mod_exprt &expr);
136  void convert_index(const index_exprt &expr);
137  void convert_member(const member_exprt &expr);
138 
139  void convert_with(const with_exprt &expr);
140  void convert_update(const exprt &expr);
141 
142  void convert_expr(const exprt &);
143  void convert_type(const typet &);
144  void convert_literal(const literalt);
145 
146  literalt convert(const exprt &expr);
147  tvt l_get(literalt l) const;
148 
149  // auxiliary methods
150  exprt prepare_for_convert_expr(const exprt &expr);
151  exprt lower_byte_operators(const exprt &expr);
152  void find_symbols(const exprt &expr);
153  void find_symbols(const typet &type);
154  void find_symbols_rec(const typet &type, std::set<irep_idt> &recstack);
155 
156  // letification
158 
159  // Parsing solver responses
160  constant_exprt parse_literal(const irept &, const typet &type);
161  struct_exprt parse_struct(const irept &s, const struct_typet &type);
162  exprt parse_union(const irept &s, const union_typet &type);
168  exprt parse_array(const irept &s, const array_typet &type);
169  exprt parse_rec(const irept &s, const typet &type);
176  void walk_array_tree(
177  std::unordered_map<int64_t, exprt> *operands_map,
178  const irept &src,
179  const array_typet &type);
180 
181  // we use this to build a bit-vector encoding of the FPA theory
182  void convert_floatbv(const exprt &expr);
183  std::string type2id(const typet &) const;
184  std::string floatbv_suffix(const exprt &) const;
185  std::set<irep_idt> bvfp_set; // already converted
186 
188  {
189  public:
190  smt2_symbolt(const irep_idt &_identifier, const typet &_type)
191  : nullary_exprt(ID_smt2_symbol, _type)
192  { set(ID_identifier, _identifier); }
193 
194  const irep_idt &get_identifier() const
195  {
196  return get(ID_identifier);
197  }
198  };
199 
200  const smt2_symbolt &to_smt2_symbol(const exprt &expr)
201  {
202  assert(expr.id()==ID_smt2_symbol && !expr.has_operands());
203  return static_cast<const smt2_symbolt&>(expr);
204  }
205 
206  // flattens any non-bitvector type into a bitvector,
207  // e.g., booleans, vectors, structs, arrays but also
208  // floats when using the FPA theory.
209  // unflatten() does the opposite.
210  enum class wheret { BEGIN, END };
211  void flatten2bv(const exprt &);
212  void unflatten(wheret, const typet &, unsigned nesting=0);
213 
214  // pointers
217  const exprt &expr, const pointer_typet &result_type);
218 
219  void define_object_size(const irep_idt &id, const exprt &expr);
220 
221  // keeps track of all non-Boolean symbols and their value
222  struct identifiert
223  {
224  bool is_bound;
227 
229  {
230  type.make_nil();
231  value.make_nil();
232  }
233  };
234 
235  typedef std::unordered_map<irep_idt, identifiert> identifier_mapt;
236 
238 
239  // for modeling structs as SMT datatype when use_datatype is set
240  //
241  // it maintains a map of `struct_typet` or `struct_tag_typet`
242  // to datatype names declared in SMT
243  typedef std::map<typet, std::string> datatype_mapt;
245 
246  // for replacing various defined expressions:
247  //
248  // ID_array_of
249  // ID_array
250  // ID_string_constant
251 
252  typedef std::map<exprt, irep_idt> defined_expressionst;
257  std::unordered_map<irep_idt, bool> set_values;
258 
260 
261  typedef std::set<std::string> smt2_identifierst;
263 
264  // Boolean part
265  std::size_t no_boolean_variables;
266  std::vector<bool> boolean_assignment;
267 };
268 
269 #endif // CPROVER_SOLVERS_SMT2_SMT2_CONV_H
Arrays with given size.
Definition: std_types.h:763
A base class for binary expressions.
Definition: std_expr.h:550
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
A constant literal expression.
Definition: std_expr.h:2753
resultt
Result of running the decision procedure.
Division.
Definition: std_expr.h:1064
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition: std_expr.h:1179
Base class for all expressions.
Definition: expr.h:54
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
Semantic type conversion from/to floating-point formats.
Definition: floatbv_expr.h:19
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: floatbv_expr.h:364
Array index operator.
Definition: std_expr.h:1328
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const irep_idt & id() const
Definition: irep.h:407
void make_nil()
Definition: irep.h:465
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
Introduce LET for common subexpressions.
Definition: letify.h:16
Extract member of struct or union.
Definition: std_expr.h:2613
Binary minus.
Definition: std_expr.h:973
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
An expression without operands.
Definition: std_expr.h:22
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
smt2_symbolt(const irep_idt &_identifier, const typet &_type)
Definition: smt2_conv.h:190
const irep_idt & get_identifier() const
Definition: smt2_conv.h:194
void convert_relation(const binary_relation_exprt &)
Definition: smt2_conv.cpp:3158
bool use_lambda_for_array
Definition: smt2_conv.h:65
void convert_type(const typet &)
Definition: smt2_conv.cpp:4828
void unflatten(wheret, const typet &, unsigned nesting=0)
Definition: smt2_conv.cpp:4270
bool use_array_theory(const exprt &)
Definition: smt2_conv.cpp:4807
void find_symbols(const exprt &expr)
Definition: smt2_conv.cpp:4527
std::map< exprt, irep_idt > defined_expressionst
Definition: smt2_conv.h:252
std::size_t number_of_solver_calls
Definition: smt2_conv.h:96
void convert_typecast(const typecast_exprt &expr)
Definition: smt2_conv.cpp:2135
~smt2_convt() override=default
void write_footer()
Writes the end of the SMT file to the smt_convt::out stream.
Definition: smt2_conv.cpp:181
tvt l_get(literalt l) const
Definition: smt2_conv.cpp:138
std::string benchmark
Definition: smt2_conv.h:90
void convert_floatbv_rem(const binary_exprt &expr)
Definition: smt2_conv.cpp:3745
std::map< typet, std::string > datatype_mapt
Definition: smt2_conv.h:243
void convert_update(const exprt &expr)
Definition: smt2_conv.cpp:4015
bool use_FPA_theory
Definition: smt2_conv.h:60
std::set< irep_idt > bvfp_set
Definition: smt2_conv.h:185
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
Definition: smt2_conv.cpp:698
void push() override
Unimplemented.
Definition: smt2_conv.cpp:859
void convert_is_dynamic_object(const unary_exprt &)
Definition: smt2_conv.cpp:3121
void convert_literal(const literalt)
Definition: smt2_conv.cpp:839
void convert_floatbv_div(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3630
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
Definition: smt2_conv.cpp:5175
const namespacet & ns
Definition: smt2_conv.h:88
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3725
boolbv_widtht boolbv_width
Definition: smt2_conv.h:94
void convert_constant(const constant_exprt &expr)
Definition: smt2_conv.cpp:2942
std::string floatbv_suffix(const exprt &) const
Definition: smt2_conv.cpp:944
std::unordered_map< irep_idt, identifiert > identifier_mapt
Definition: smt2_conv.h:235
void flatten2bv(const exprt &)
Definition: smt2_conv.cpp:4181
std::string notes
Definition: smt2_conv.h:90
void convert_div(const div_exprt &expr)
Definition: smt2_conv.cpp:3586
std::ostream & out
Definition: smt2_conv.h:89
exprt lower_byte_operators(const exprt &expr)
Lower byte_update and byte_extract operations within expr.
Definition: smt2_conv.cpp:4480
std::string type2id(const typet &) const
Definition: smt2_conv.cpp:907
bool emit_set_logic
Definition: smt2_conv.h:66
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
Definition: smt2_conv.cpp:3373
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
Definition: smt2_conv.cpp:2668
struct_exprt parse_struct(const irept &s, const struct_typet &type)
Definition: smt2_conv.cpp:575
std::string logic
Definition: smt2_conv.h:90
void convert_mult(const mult_exprt &expr)
Definition: smt2_conv.cpp:3650
exprt prepare_for_convert_expr(const exprt &expr)
Perform steps necessary before an expression is passed to convert_expr.
Definition: smt2_conv.cpp:4512
void define_object_size(const irep_idt &id, const exprt &expr)
Definition: smt2_conv.cpp:232
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: smt2_conv.cpp:277
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Definition: smt2_conv.cpp:123
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3566
bool use_check_sat_assuming
Definition: smt2_conv.h:63
bool use_datatypes
Definition: smt2_conv.h:64
datatype_mapt datatype_map
Definition: smt2_conv.h:244
void convert_mod(const mod_exprt &expr)
Definition: smt2_conv.cpp:3102
static std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:876
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3430
void convert_struct(const struct_exprt &expr)
Definition: smt2_conv.cpp:2814
std::unordered_map< irep_idt, bool > set_values
The values which boolean identifiers have been smt2_convt::set_to or in other words those which are a...
Definition: smt2_conv.h:257
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.cpp:53
void convert_member(const member_exprt &expr)
Definition: smt2_conv.cpp:4120
void convert_euclidean_mod(const euclidean_mod_exprt &expr)
Definition: smt2_conv.cpp:3087
void convert_index(const index_exprt &expr)
Definition: smt2_conv.cpp:4022
pointer_logict pointer_logic
Definition: smt2_conv.h:215
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
Definition: smt2_conv.cpp:830
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: smt2_conv.cpp:128
void walk_array_tree(std::unordered_map< int64_t, exprt > *operands_map, const irept &src, const array_typet &type)
This function walks the SMT output and populates a map with index/value pairs for the array.
Definition: smt2_conv.cpp:519
std::set< std::string > smt2_identifierst
Definition: smt2_conv.h:261
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
Definition: smt2_conv.cpp:4374
defined_expressionst object_sizes
Definition: smt2_conv.h:259
bool use_as_const
Definition: smt2_conv.h:62
exprt parse_rec(const irept &s, const typet &type)
Definition: smt2_conv.cpp:634
void convert_union(const union_exprt &expr)
Definition: smt2_conv.cpp:2909
exprt parse_union(const irept &s, const union_typet &type)
Definition: smt2_conv.cpp:559
exprt parse_array(const irept &s, const array_typet &type)
This function is for parsing array output from SMT solvers when "(get-value |???|)" returns an array ...
Definition: smt2_conv.cpp:475
std::vector< bool > boolean_assignment
Definition: smt2_conv.h:266
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
Definition: smt2_conv.cpp:2878
void convert_with(const with_exprt &expr)
Definition: smt2_conv.cpp:3768
letifyt letify
Definition: smt2_conv.h:157
bool use_array_of_bool
Definition: smt2_conv.h:61
std::vector< exprt > assumptions
Definition: smt2_conv.h:93
void convert_plus(const plus_exprt &expr)
Definition: smt2_conv.cpp:3241
defined_expressionst defined_expressions
Definition: smt2_conv.h:253
void pop() override
Currently, only implements a single stack element (no nested contexts)
Definition: smt2_conv.cpp:871
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
Definition: smt2_conv.cpp:4969
void write_header()
Definition: smt2_conv.cpp:151
solvert solver
Definition: smt2_conv.h:91
identifier_mapt identifier_map
Definition: smt2_conv.h:237
void convert_minus(const minus_exprt &expr)
Definition: smt2_conv.cpp:3469
void convert_expr(const exprt &)
Definition: smt2_conv.cpp:985
constant_exprt parse_literal(const irept &, const typet &type)
Definition: smt2_conv.cpp:337
std::size_t no_boolean_variables
Definition: smt2_conv.h:265
smt2_identifierst smt2_identifiers
Definition: smt2_conv.h:262
void convert_floatbv(const exprt &expr)
Definition: smt2_conv.cpp:951
resultt dec_solve() override
Run the decision procedure to solve the problem.
Definition: smt2_conv.cpp:270
literalt convert(const exprt &expr)
Definition: smt2_conv.cpp:790
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
Definition: smt2_conv.h:200
Struct constructor from list of elements.
Definition: std_expr.h:1668
Structure type, corresponds to C style structs.
Definition: std_types.h:231
Definition: threeval.h:20
Semantic type conversion.
Definition: std_expr.h:1866
The type of an expression, extends irept.
Definition: type.h:28
Generic base class for unary expressions.
Definition: std_expr.h:281
Union constructor from single element.
Definition: std_expr.h:1602
The union type.
Definition: c_types.h:112
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
IREP Hash Container.
Pointer Logic.
Decision procedure with incremental solving with contexts and assumptions.
API to expression classes.