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 <map>
18#include <set>
19#include <sstream>
20
21#if !HASH_CODE
23#endif
24
29
30#include "letify.h"
31
34class union_typet;
35
37{
38public:
39 enum class solvert
40 {
41 GENERIC,
45 CVC3,
46 CVC4,
47 CVC5,
48 MATHSAT,
49 YICES,
50 Z3
51 };
52
54 const namespacet &_ns,
55 const std::string &_benchmark,
56 const std::string &_notes,
57 const std::string &_logic,
58 solvert _solver,
59 std::ostream &_out);
60
61 ~smt2_convt() override = default;
62
70
71 exprt handle(const exprt &expr) override;
72 void set_to(const exprt &expr, bool value) override;
73 exprt get(const exprt &expr) const override;
74 std::string decision_procedure_text() const override;
75 void print_assignment(std::ostream &out) const override;
76
78 void push() override;
79
81 void push(const std::vector<exprt> &_assumptions) override;
82
84 void pop() override;
85
86 std::size_t get_number_of_solver_calls() const override;
87
88 static std::string convert_identifier(const irep_idt &identifier);
89
90 void set_converter(irep_idt id, std::function<void(const exprt &)> converter)
91 {
92 converters[id] = std::move(converter);
93 }
94
95protected:
96 const namespacet &ns;
97 std::ostream &out;
98 std::string benchmark, notes, logic;
100 using converterst = std::
101 unordered_map<irep_idt, std::function<void(const exprt &)>, irep_id_hash>;
103
104 std::vector<exprt> assumptions;
106
107 std::size_t number_of_solver_calls = 0;
108
109 resultt dec_solve() override;
110
111 void write_header();
121 void write_footer();
122
123 // tweaks for arrays
124 bool use_array_theory(const exprt &);
125 void flatten_array(const exprt &);
126
127 // specific expressions go here
128 void convert_typecast(const typecast_exprt &expr);
130 void convert_struct(const struct_exprt &expr);
131 void convert_union(const union_exprt &expr);
132 void convert_constant(const constant_exprt &expr);
135 void convert_plus(const plus_exprt &expr);
136 void convert_minus(const minus_exprt &expr);
137 void convert_div(const div_exprt &expr);
138 void convert_mult(const mult_exprt &expr);
139 void convert_rounding_mode_FPA(const exprt &expr);
144 void convert_floatbv_rem(const binary_exprt &expr);
145 void convert_mod(const mod_exprt &expr);
147 void convert_index(const index_exprt &expr);
148 void convert_member(const member_exprt &expr);
149
150 void convert_with(const with_exprt &expr);
151 void convert_update(const update_exprt &);
152
153 void convert_expr(const exprt &);
154 void convert_type(const typet &);
155 void convert_literal(const literalt);
156 void convert_string_literal(const std::string &);
157
158 literalt convert(const exprt &expr);
159 tvt l_get(literalt l) const;
160
161 // auxiliary methods
163 exprt lower_byte_operators(const exprt &expr);
164 void find_symbols(const exprt &expr);
165 void find_symbols(const typet &type);
166 void find_symbols_rec(const typet &type, std::set<irep_idt> &recstack);
167
168 // letification
170
171 // Parsing solver responses
172 constant_exprt parse_literal(const irept &, const typet &type);
173 struct_exprt parse_struct(const irept &s, const struct_typet &type);
174 exprt parse_union(const irept &s, const union_typet &type);
180 exprt parse_array(const irept &s, const array_typet &type);
181 exprt parse_rec(const irept &s, const typet &type);
188 void walk_array_tree(
189 std::unordered_map<int64_t, exprt> *operands_map,
190 const irept &src,
191 const array_typet &type);
192 std::unordered_map<irep_idt, irept> current_bindings;
193
194 // we use this to build a bit-vector encoding of the FPA theory
195 void convert_floatbv(const exprt &expr);
196 std::string type2id(const typet &) const;
197 std::string floatbv_suffix(const exprt &) const;
198 std::set<irep_idt> bvfp_set; // already converted
199
200 // conversion for ID_evaluate, ID_update_state,
201 // ID_object_address, ID_field_address, ID_element_address
202 std::set<irep_idt> state_fkt_declared;
203
205 {
206 public:
207 smt2_symbolt(const irep_idt &_identifier, const typet &_type)
208 : nullary_exprt(ID_smt2_symbol, _type)
209 { set(ID_identifier, _identifier); }
210
212 {
213 return get(ID_identifier);
214 }
215 };
216
218 {
219 PRECONDITION(expr.id() == ID_smt2_symbol && !expr.has_operands());
220 return static_cast<const smt2_symbolt&>(expr);
221 }
222
223 // flattens any non-bitvector type into a bitvector,
224 // e.g., booleans, vectors, structs, arrays but also
225 // floats when using the FPA theory.
226 // unflatten() does the opposite.
227 enum class wheret { BEGIN, END };
228 void flatten2bv(const exprt &);
229 void unflatten(wheret, const typet &, unsigned nesting=0);
230
231 // pointers
234 const exprt &expr, const pointer_typet &result_type);
235
236 void define_object_size(const irep_idt &id, const object_size_exprt &expr);
237
238 // keeps track of all non-Boolean symbols and their value
240 {
244
246 {
247 type.make_nil();
248 value.make_nil();
249 }
250 };
251
252 typedef std::unordered_map<irep_idt, identifiert> identifier_mapt;
253
255
256 // for modeling structs as SMT datatype when use_datatype is set
257 //
258 // it maintains a map of `struct_typet` or `struct_tag_typet`
259 // to datatype names declared in SMT
260 typedef std::map<typet, std::string> datatype_mapt;
262
263 // for replacing various defined expressions:
264 //
265 // ID_array_of
266 // ID_array
267 // ID_string_constant
268
269 typedef std::map<exprt, irep_idt> defined_expressionst;
274 std::unordered_map<irep_idt, bool> set_values;
275
276 std::map<object_size_exprt, irep_idt> object_sizes;
277
278 typedef std::set<std::string> smt2_identifierst;
280
281 // Boolean part
283 std::vector<bool> boolean_assignment;
284};
285
286#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:583
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
A constant literal expression.
Definition std_expr.h:2942
resultt
Result of running the decision procedure.
Division.
Definition std_expr.h:1097
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Boute's Euclidean definition of Modulo – to match SMT-LIB2.
Definition std_expr.h:1236
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:1410
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:372
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
void make_nil()
Definition irep.h:454
const irep_idt & id() const
Definition irep.h:396
Introduce LET for common subexpressions.
Definition letify.h:16
Extract member of struct or union.
Definition std_expr.h:2794
Binary minus.
Definition std_expr.h:1006
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1168
Binary multiplication Associativity is not specified.
Definition std_expr.h:1052
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
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:947
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:207
const irep_idt & get_identifier() const
Definition smt2_conv.h:211
void convert_relation(const binary_relation_exprt &)
bool use_lambda_for_array
Definition smt2_conv.h:68
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:269
std::size_t number_of_solver_calls
Definition smt2_conv.h:107
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:98
void convert_floatbv_rem(const binary_exprt &expr)
std::map< typet, std::string > datatype_mapt
Definition smt2_conv.h:260
std::unordered_map< irep_idt, irept > current_bindings
Definition smt2_conv.h:192
bool use_FPA_theory
Definition smt2_conv.h:63
std::set< irep_idt > bvfp_set
Definition smt2_conv.h:198
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:96
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
boolbv_widtht boolbv_width
Definition smt2_conv.h:105
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:252
void flatten2bv(const exprt &)
std::string notes
Definition smt2_conv.h:98
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:100
std::ostream & out
Definition smt2_conv.h:97
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:69
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:98
void convert_mult(const mult_exprt &expr)
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:66
std::map< object_size_exprt, irep_idt > object_sizes
Definition smt2_conv.h:276
void define_object_size(const irep_idt &id, const object_size_exprt &expr)
bool use_datatypes
Definition smt2_conv.h:67
datatype_mapt datatype_map
Definition smt2_conv.h:261
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:274
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:102
pointer_logict pointer_logic
Definition smt2_conv.h:232
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:278
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:65
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:90
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:283
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:169
bool use_array_of_bool
Definition smt2_conv.h:64
std::vector< exprt > assumptions
Definition smt2_conv.h:104
void convert_plus(const plus_exprt &expr)
defined_expressionst defined_expressions
Definition smt2_conv.h:270
void pop() override
Currently, only implements a single stack element (no nested contexts)
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:202
solvert solver
Definition smt2_conv.h:99
identifier_mapt identifier_map
Definition smt2_conv.h:254
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:217
std::size_t no_boolean_variables
Definition smt2_conv.h:282
smt2_identifierst smt2_identifiers
Definition smt2_conv.h:279
void convert_floatbv(const exprt &expr)
resultt dec_solve() override
Run the decision procedure to solve the problem.
literalt convert(const exprt &expr)
Struct constructor from list of elements.
Definition std_expr.h:1819
Structure type, corresponds to C style structs.
Definition std_types.h:231
Definition threeval.h:20
Semantic type conversion.
Definition std_expr.h:2017
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:314
Union constructor from single element.
Definition std_expr.h:1708
The union type.
Definition c_types.h:147
Operator to update elements in structs and arrays.
Definition std_expr.h:2608
Operator to update elements in structs and arrays.
Definition std_expr.h:2424
IREP Hash Container.
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.
dstringt irep_idt