cprover
Loading...
Searching...
No Matches
smt2_conv.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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 <util/pointer_expr.h>
14#include <util/std_expr.h>
15#include <util/threeval.h>
16
17#include <cstdint>
18#include <map>
19#include <set>
20#include <sstream>
21
22#if !HASH_CODE
24#endif
25
30
31#include "letify.h"
32
35class union_typet;
38
40{
41public:
55
57 const namespacet &_ns,
58 const std::string &_benchmark,
59 const std::string &_notes,
60 const std::string &_logic,
61 solvert _solver,
62 std::ostream &_out);
63
64 ~smt2_convt() override = default;
65
73
74 exprt handle(const exprt &expr) override;
75 void set_to(const exprt &expr, bool value) override;
76 exprt get(const exprt &expr) const override;
77 std::string decision_procedure_text() const override;
78 void print_assignment(std::ostream &out) const override;
79
81 void push() override;
82
84 void push(const std::vector<exprt> &_assumptions) override;
85
87 void pop() override;
88
89 std::size_t get_number_of_solver_calls() const override;
90
91 static std::string convert_identifier(const irep_idt &identifier);
92
93 void set_converter(irep_idt id, std::function<void(const exprt &)> converter)
94 {
95 converters[id] = std::move(converter);
96 }
97
98protected:
99 const namespacet &ns;
100 std::ostream &out;
101 std::string benchmark, notes, logic;
103 using converterst = std::
104 unordered_map<irep_idt, std::function<void(const exprt &)>, irep_id_hash>;
106
107 std::vector<literalt> assumptions;
109
110 std::size_t number_of_solver_calls = 0;
111
112 resultt dec_solve(const exprt &) override;
113
114 void write_header();
124 void write_footer();
125
126 // tweaks for arrays
127 bool use_array_theory(const exprt &);
128 void flatten_array(const exprt &);
129
130 // specific expressions go here
131 void convert_typecast(const typecast_exprt &expr);
133 void convert_struct(const struct_exprt &expr);
134 void convert_union(const union_exprt &expr);
135 void convert_constant(const constant_exprt &expr);
138 void convert_plus(const plus_exprt &expr);
139 void convert_minus(const minus_exprt &expr);
140 void convert_div(const div_exprt &expr);
141 void convert_mult(const mult_exprt &expr);
142 void convert_rounding_mode_FPA(const exprt &expr);
147 void convert_floatbv_rem(const binary_exprt &expr);
148 void convert_mod(const mod_exprt &expr);
150 void convert_index(const index_exprt &expr);
151 void convert_member(const member_exprt &expr);
152
153 void convert_with(const with_exprt &expr);
154 void convert_update(const update_exprt &);
157
158 void convert_expr(const exprt &);
159 void convert_type(const typet &);
160 void convert_literal(const literalt);
161 void convert_string_literal(const std::string &);
162
163 literalt convert(const exprt &expr);
164 tvt l_get(literalt l) const;
165
166 // auxiliary methods
168 exprt lower_byte_operators(const exprt &expr);
169 void find_symbols(const exprt &expr);
170 void find_symbols(const typet &type);
171 void find_symbols_rec(const typet &type, std::set<irep_idt> &recstack);
172
173 // letification
175
176 // Parsing solver responses
177 constant_exprt parse_literal(const irept &, const typet &type);
178 struct_exprt parse_struct(const irept &s, const struct_typet &type);
179 exprt parse_union(const irept &s, const union_typet &type);
185 exprt parse_array(const irept &s, const array_typet &type);
186 exprt parse_rec(const irept &s, const typet &type);
193 void walk_array_tree(
194 std::unordered_map<int64_t, exprt> *operands_map,
195 const irept &src,
196 const array_typet &type);
197 std::unordered_map<irep_idt, irept> current_bindings;
198
199 // we use this to build a bit-vector encoding of the FPA theory
200 void convert_floatbv(const exprt &expr);
201 std::string type2id(const typet &) const;
202 std::string floatbv_suffix(const exprt &) const;
203 std::set<irep_idt> bvfp_set; // already converted
204
205 // conversion for ID_evaluate, ID_update_state,
206 // ID_object_address, ID_field_address, ID_element_address
207 std::set<irep_idt> state_fkt_declared;
208
210 {
211 public:
212 smt2_symbolt(const irep_idt &_identifier, const typet &_type)
213 : nullary_exprt(ID_smt2_symbol, _type)
214 { set(ID_identifier, _identifier); }
215
217 {
218 return get(ID_identifier);
219 }
220 };
221
223 {
224 PRECONDITION(expr.id() == ID_smt2_symbol && !expr.has_operands());
225 return static_cast<const smt2_symbolt&>(expr);
226 }
227
228 // flattens any non-bitvector type into a bitvector,
229 // e.g., booleans, vectors, structs, arrays but also
230 // floats when using the FPA theory.
231 // unflatten() does the opposite.
232 enum class wheret { BEGIN, END };
233 void flatten2bv(const exprt &);
234 void unflatten(wheret, const typet &, unsigned nesting=0);
235
236 // pointers
239 const exprt &expr, const pointer_typet &result_type);
240
241 void define_object_size(const irep_idt &id, const object_size_exprt &expr);
242
243 // keeps track of all non-Boolean symbols and their value
245 {
246 // We do not currently read any of the following members, but might do so in
247 // future. At this time, we just care about (not) having an entry in
248 // `identifier_map`.
252
254 : is_bound(is_bound), type(std::move(type))
255 {
256 value.make_nil();
257 }
258 };
259
260 typedef std::unordered_map<irep_idt, identifiert> identifier_mapt;
261
263
264 // for modeling structs as SMT datatype when use_datatype is set
265 //
266 // it maintains a map of `struct_typet` or `struct_tag_typet`
267 // to datatype names declared in SMT
268 typedef std::map<typet, std::string> datatype_mapt;
270
271 // for replacing various defined expressions:
272 //
273 // ID_array_of
274 // ID_array
275 // ID_string_constant
276
277 typedef std::map<exprt, irep_idt> defined_expressionst;
282 std::unordered_map<irep_idt, bool> set_values;
283
284 std::map<object_size_exprt, irep_idt> object_sizes;
285
286 typedef std::set<std::string> smt2_identifierst;
288
289 // Boolean part
291 std::vector<bool> boolean_assignment;
292};
293
294#endif // CPROVER_SOLVERS_SMT2_SMT2_CONV_H
Arrays with given size.
Definition std_types.h:807
A base class for binary expressions.
Definition std_expr.h:638
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
A constant literal expression.
Definition std_expr.h:2995
resultt
Result of running the decision procedure.
Division.
Definition std_expr.h:1157
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition std_expr.h:1296
Base class for all expressions.
Definition expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:91
Semantic type conversion from/to floating-point formats.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Array index operator.
Definition std_expr.h:1470
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
const irep_idt & id() const
Definition irep.h:388
Introduce LET for common subexpressions.
Definition letify.h:16
Extract member of struct or union.
Definition std_expr.h:2849
Binary minus.
Definition std_expr.h:1061
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1228
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
nullary_exprt(const irep_idt &_id, typet _type)
Definition std_expr.h:24
Expression for finding the size (in bytes) of the object a pointer points to.
The plus expression Associativity is not specified.
Definition std_expr.h:1002
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
smt2_symbolt(const irep_idt &_identifier, const typet &_type)
Definition smt2_conv.h:212
const irep_idt & get_identifier() const
Definition smt2_conv.h:216
void convert_relation(const binary_relation_exprt &)
bool use_lambda_for_array
Definition smt2_conv.h:71
void convert_type(const typet &)
void unflatten(wheret, const typet &, unsigned nesting=0)
bool use_array_theory(const exprt &)
void find_symbols(const exprt &expr)
std::map< exprt, irep_idt > defined_expressionst
Definition smt2_conv.h:277
std::size_t number_of_solver_calls
Definition smt2_conv.h:110
void convert_typecast(const typecast_exprt &expr)
~smt2_convt() override=default
void write_footer()
Writes the end of the SMT file to the smt_convt::out stream.
tvt l_get(literalt l) const
std::string benchmark
Definition smt2_conv.h:101
void convert_floatbv_rem(const binary_exprt &expr)
std::map< typet, std::string > datatype_mapt
Definition smt2_conv.h:268
std::unordered_map< irep_idt, irept > current_bindings
Definition smt2_conv.h:197
bool use_FPA_theory
Definition smt2_conv.h:66
resultt dec_solve(const exprt &) override
Implementation of the decision procedure.
std::set< irep_idt > bvfp_set
Definition smt2_conv.h:203
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
void push() override
Unimplemented.
void convert_is_dynamic_object(const unary_exprt &)
void convert_literal(const literalt)
void convert_floatbv_div(const ieee_float_op_exprt &expr)
void convert_string_literal(const std::string &)
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
const namespacet & ns
Definition smt2_conv.h:99
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
boolbv_widtht boolbv_width
Definition smt2_conv.h:108
void convert_constant(const constant_exprt &expr)
std::string floatbv_suffix(const exprt &) const
std::unordered_map< irep_idt, identifiert > identifier_mapt
Definition smt2_conv.h:260
void flatten2bv(const exprt &)
std::string notes
Definition smt2_conv.h:101
void convert_div(const div_exprt &expr)
std:: unordered_map< irep_idt, std::function< void(const exprt &)>, irep_id_hash > converterst
Definition smt2_conv.h:103
std::ostream & out
Definition smt2_conv.h:100
exprt lower_byte_operators(const exprt &expr)
Lower byte_update and byte_extract operations within expr.
std::string type2id(const typet &) const
bool emit_set_logic
Definition smt2_conv.h:72
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
struct_exprt parse_struct(const irept &s, const struct_typet &type)
std::string logic
Definition smt2_conv.h:101
void convert_mult(const mult_exprt &expr)
void convert_update_bit(const update_bit_exprt &)
exprt prepare_for_convert_expr(const exprt &expr)
Perform steps necessary before an expression is passed to convert_expr.
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
bool use_check_sat_assuming
Definition smt2_conv.h:69
std::map< object_size_exprt, irep_idt > object_sizes
Definition smt2_conv.h:284
void define_object_size(const irep_idt &id, const object_size_exprt &expr)
bool use_datatypes
Definition smt2_conv.h:70
datatype_mapt datatype_map
Definition smt2_conv.h:269
void convert_mod(const mod_exprt &expr)
static std::string convert_identifier(const irep_idt &identifier)
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
void convert_struct(const struct_exprt &expr)
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:282
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:56
void convert_member(const member_exprt &expr)
void convert_euclidean_mod(const euclidean_mod_exprt &expr)
void convert_index(const index_exprt &expr)
converterst converters
Definition smt2_conv.h:105
pointer_logict pointer_logic
Definition smt2_conv.h:237
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...
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
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.
std::set< std::string > smt2_identifierst
Definition smt2_conv.h:286
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'.
bool use_as_const
Definition smt2_conv.h:68
exprt parse_rec(const irept &s, const typet &type)
void convert_union(const union_exprt &expr)
exprt parse_union(const irept &s, const union_typet &type)
void set_converter(irep_idt id, std::function< void(const exprt &)> converter)
Definition smt2_conv.h:93
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 ...
std::vector< bool > boolean_assignment
Definition smt2_conv.h:291
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
void convert_with(const with_exprt &expr)
letifyt letify
Definition smt2_conv.h:174
bool use_array_of_bool
Definition smt2_conv.h:67
std::vector< literalt > assumptions
Definition smt2_conv.h:107
void convert_plus(const plus_exprt &expr)
defined_expressionst defined_expressions
Definition smt2_conv.h:278
void pop() override
Currently, only implements a single stack element (no nested contexts)
void convert_update_bits(const update_bits_exprt &)
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
void convert_update(const update_exprt &)
void write_header()
std::set< irep_idt > state_fkt_declared
Definition smt2_conv.h:207
solvert solver
Definition smt2_conv.h:102
identifier_mapt identifier_map
Definition smt2_conv.h:262
void convert_minus(const minus_exprt &expr)
void convert_expr(const exprt &)
constant_exprt parse_literal(const irept &, const typet &type)
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
Definition smt2_conv.h:222
std::size_t no_boolean_variables
Definition smt2_conv.h:290
smt2_identifierst smt2_identifiers
Definition smt2_conv.h:287
void convert_floatbv(const exprt &expr)
literalt convert(const exprt &expr)
Struct constructor from list of elements.
Definition std_expr.h:1877
Structure type, corresponds to C style structs.
Definition std_types.h:231
Definition threeval.h:20
Semantic type conversion.
Definition std_expr.h:2073
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:361
Union constructor from single element.
Definition std_expr.h:1770
The union type.
Definition c_types.h:147
Replaces a sub-range of a bit-vector operand.
Replaces a sub-range of a bit-vector operand.
Operator to update elements in structs and arrays.
Definition std_expr.h:2660
Operator to update elements in structs and arrays.
Definition std_expr.h:2476
dstring_hash irep_id_hash
Definition irep.h:38
IREP Hash Container.
STL namespace.
API to expression classes for Pointers.
Pointer Logic.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Decision procedure with incremental solving with contexts and assumptions.
API to expression classes.
identifiert(typet type, bool is_bound)
Definition smt2_conv.h:253
dstringt irep_idt