cprover
Loading...
Searching...
No Matches
boolbv.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_FLATTENING_BOOLBV_H
11#define CPROVER_SOLVERS_FLATTENING_BOOLBV_H
12
13//
14// convert expression to boolean formula
15//
16
17#include <util/endianness_map.h>
18#include <util/expr.h>
19#include <util/mp_arith.h>
20
22
23#include "arrays.h"
24#include "boolbv_map.h"
25#include "boolbv_width.h"
26#include "bv_utils.h" // IWYU pragma: keep
27
30class bswap_exprt;
41class union_typet;
44
45class boolbvt:public arrayst
46{
47public:
49 const namespacet &_ns,
50 propt &_prop,
52 bool get_array_constraints = false)
55 bv_width(_ns),
56 bv_utils(_prop),
57 functions(*this),
58 map(_prop)
59 {
60 }
61
62 virtual const bvt &convert_bv( // check cache
63 const exprt &expr,
64 const std::optional<std::size_t> expected_width = {});
65
66 virtual bvt convert_bitvector(const exprt &expr); // no cache
67
68 // overloading
69 exprt get(const exprt &expr) const override;
70 void set_to(const exprt &expr, bool value) override;
71 void print_assignment(std::ostream &out) const override;
72 exprt handle(const exprt &) override;
73
74 void clear_cache() override
75 {
77 bv_cache.clear();
78 }
79
81 {
83 functions.finish_eager_conversion();
85 }
86
89
91 {
92 return get_value(bv, 0, bv.size());
93 }
94
95 mp_integer get_value(const bvt &bv, std::size_t offset, std::size_t width);
96
97 const boolbv_mapt &get_map() const
98 {
99 return map;
100 }
101
102 virtual std::size_t boolbv_width(const typet &type) const
103 {
104 return bv_width(type);
105 }
106
107 virtual endianness_mapt
108 endianness_map(const typet &type, bool little_endian) const
109 {
110 return endianness_mapt{type, little_endian, ns};
111 }
112
113 virtual endianness_mapt endianness_map(const typet &type) const;
114
115protected:
118
119 // uninterpreted functions
121
122 // the mapping from identifiers to literals
124
125 // overloading
126 literalt convert_rest(const exprt &expr) override;
127 virtual bool boolbv_set_equality_to_true(const equal_exprt &expr);
128
129 // NOLINTNEXTLINE(readability/identifiers)
130 typedef arrayst SUB;
131
132 bvt conversion_failed(const exprt &expr);
133
134 typedef std::unordered_map<const exprt, bvt, irep_hash> bv_cachet;
136
137 bool type_conversion(
138 const typet &src_type, const bvt &src,
139 const typet &dest_type, bvt &dest);
140
142 virtual literalt convert_typecast(const typecast_exprt &expr);
143 virtual literalt convert_reduction(const unary_exprt &expr);
144 virtual literalt convert_onehot(const unary_exprt &expr);
145 virtual literalt convert_extractbit(const extractbit_exprt &expr);
148 virtual literalt convert_equality(const equal_exprt &expr);
150 const binary_relation_exprt &expr);
152 virtual literalt convert_quantifier(const quantifier_exprt &expr);
153
154 virtual bvt convert_index(const exprt &array, const mp_integer &index);
155 virtual bvt convert_index(const index_exprt &expr);
156 virtual bvt convert_bswap(const bswap_exprt &expr);
157 virtual bvt convert_byte_extract(const byte_extract_exprt &expr);
158 virtual bvt convert_byte_update(const byte_update_exprt &expr);
159 virtual bvt convert_constraint_select_one(const exprt &expr);
160 virtual bvt convert_if(const if_exprt &expr);
161 virtual bvt convert_struct(const struct_exprt &expr);
162 virtual bvt convert_array(const exprt &expr);
163 virtual bvt convert_complex(const complex_exprt &expr);
164 virtual bvt convert_complex_real(const complex_real_exprt &expr);
165 virtual bvt convert_complex_imag(const complex_imag_exprt &expr);
167 virtual bvt convert_let(const let_exprt &);
168 virtual bvt convert_array_of(const array_of_exprt &expr);
169 virtual bvt convert_union(const union_exprt &expr);
170 virtual bvt convert_empty_union(const empty_union_exprt &expr);
171 virtual bvt convert_bv_typecast(const typecast_exprt &expr);
172 virtual bvt convert_add_sub(const exprt &expr);
173 virtual bvt convert_mult(const mult_exprt &expr);
174 virtual bvt convert_div(const div_exprt &expr);
175 virtual bvt convert_mod(const mod_exprt &expr);
179 virtual bvt convert_member(const member_exprt &expr);
180 virtual bvt convert_with(const with_exprt &expr);
181 virtual bvt convert_update(const update_exprt &);
182 virtual bvt convert_update_bit(const update_bit_exprt &);
184 virtual bvt convert_case(const exprt &expr);
185 virtual bvt convert_cond(const cond_exprt &);
186 virtual bvt convert_shift(const binary_exprt &expr);
187 virtual bvt convert_bitwise(const exprt &expr);
188 virtual bvt convert_unary_minus(const unary_minus_exprt &expr);
189 virtual bvt convert_abs(const abs_exprt &expr);
190 virtual bvt convert_concatenation(const concatenation_exprt &expr);
191 virtual bvt convert_replication(const replication_exprt &expr);
192 virtual bvt convert_constant(const constant_exprt &expr);
193 virtual bvt convert_extractbits(const extractbits_exprt &expr);
194 virtual bvt convert_symbol(const exprt &expr);
195 virtual bvt convert_bv_reduction(const unary_exprt &expr);
196 virtual bvt convert_not(const not_exprt &expr);
197 virtual bvt convert_power(const binary_exprt &expr);
199 const function_application_exprt &expr);
200 virtual bvt convert_bitreverse(const bitreverse_exprt &expr);
201 virtual bvt convert_saturating_add_sub(const binary_exprt &expr);
203
204 bvt convert_update_bits(bvt src, const exprt &index, const bvt &new_value);
205
206 void convert_with(
207 const typet &type,
208 const exprt &where,
209 const exprt &new_value,
210 const bvt &prev_bv,
211 bvt &next_bv);
212
214 const exprt &index,
215 const exprt &new_value,
216 const bvt &prev_bv,
217 bvt &next_bv);
218
220 const array_typet &type,
221 const exprt &index,
222 const exprt &new_value,
223 const bvt &prev_bv,
224 bvt &next_bv);
225
227 const union_typet &type,
228 const exprt &new_value,
229 const bvt &prev_bv,
230 bvt &next_bv);
231
233 const struct_typet &type,
234 const exprt &where,
235 const exprt &new_value,
236 const bvt &prev_bv,
237 bvt &next_bv);
238
240 const exprt::operandst &designator,
241 std::size_t d,
242 const typet &type,
243 std::size_t offset,
244 const exprt &new_value,
245 bvt &bv);
246
247 virtual exprt bv_get_unbounded_array(const exprt &) const;
248
249 virtual exprt
250 bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset) const;
251
252 exprt bv_get(const bvt &bv, const typet &type) const;
253 exprt bv_get_cache(const exprt &expr) const;
254
255 // unbounded arrays
256 bool is_unbounded_array(const typet &type) const override;
257
258 // quantifier instantiations
260 {
261 public:
263 : expr(std::move(_expr)), l(std::move(_l))
264 {
265 }
266
269 };
270
271 typedef std::list<quantifiert> quantifier_listt;
273
275
276 typedef std::vector<std::size_t> offset_mapt;
278
279 // strings
281
282 // scopes
283 std::size_t scope_counter = 0;
284
287};
288
289#endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H
Theory of Arrays with Extensionality.
Absolute value.
Definition std_expr.h:442
Expression to define a mapping from an argument (index) to elements.
Definition std_expr.h:3418
Array constructor from single element.
Definition std_expr.h:1558
Arrays with given size.
Definition std_types.h:807
const namespacet & ns
Definition arrays.h:56
message_handlert & message_handler
Definition arrays.h:58
arrayst(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
Definition arrays.cpp:29
void finish_eager_conversion() override
Definition arrays.h:41
bool get_array_constraints
Definition arrays.h:114
A base class for binary expressions.
Definition std_expr.h:638
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
A base class for variable bindings (quantifiers, let, lambda)
Definition std_expr.h:3112
std::vector< symbol_exprt > variablest
Definition std_expr.h:3114
Reverse the order of bits in a bit-vector.
quantifiert(exprt _expr, literalt _l)
Definition boolbv.h:262
virtual bvt convert_with(const with_exprt &expr)
virtual bvt convert_array(const exprt &expr)
Flatten array.
virtual literalt convert_bv_rel(const binary_relation_exprt &)
Flatten <, >, <= and >= expressions.
bv_cachet bv_cache
Definition boolbv.h:135
virtual literalt convert_onehot(const unary_exprt &expr)
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition boolbv.cpp:39
std::size_t scope_counter
Definition boolbv.h:283
virtual bvt convert_constraint_select_one(const exprt &expr)
void convert_update_rec(const exprt::operandst &designator, std::size_t d, const typet &type, std::size_t offset, const exprt &new_value, bvt &bv)
virtual bvt convert_complex_imag(const complex_imag_exprt &expr)
virtual literalt convert_reduction(const unary_exprt &expr)
virtual literalt convert_ieee_float_rel(const binary_relation_exprt &)
std::unordered_map< const exprt, bvt, irep_hash > bv_cachet
Definition boolbv.h:134
virtual bvt convert_complex_real(const complex_real_exprt &expr)
virtual bvt convert_complex(const complex_exprt &expr)
virtual bvt convert_let(const let_exprt &)
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
offset_mapt build_offset_map(const struct_typet &src)
Definition boolbv.cpp:581
void convert_with_array(const array_typet &type, const exprt &index, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)
virtual bvt convert_bitvector(const exprt &expr)
Converts an expression into its gate-level representation and returns a vector of literals correspond...
Definition boolbv.cpp:108
unbounded_arrayt
Definition boolbv.h:87
binding_exprt::variablest fresh_binding(const binding_exprt &)
create new, unique variables for the given binding
Definition boolbv.cpp:552
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
virtual bvt convert_bswap(const bswap_exprt &expr)
bool is_unbounded_array(const typet &type) const override
Definition boolbv.cpp:533
bvt convert_update_bits(bvt src, const exprt &index, const bvt &new_value)
void finish_eager_conversion_quantifiers()
exprt bv_get(const bvt &bv, const typet &type) const
virtual bvt convert_mod(const mod_exprt &expr)
virtual bvt convert_add_sub(const exprt &expr)
virtual bvt convert_constant(const constant_exprt &expr)
numberingt< irep_idt > string_numbering
Definition boolbv.h:280
virtual literalt convert_quantifier(const quantifier_exprt &expr)
void convert_with_union(const union_typet &type, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)
boolbvt(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
Definition boolbv.h:48
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
Definition boolbv.cpp:492
virtual exprt bv_get_unbounded_array(const exprt &) const
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset) const
virtual bvt convert_update_bits(const update_bits_exprt &)
void clear_cache() override
Definition boolbv.h:74
virtual bvt convert_mult(const mult_exprt &expr)
exprt handle(const exprt &) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
Definition boolbv.cpp:83
virtual bvt convert_member(const member_exprt &expr)
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
virtual bvt convert_function_application(const function_application_exprt &expr)
Definition boolbv.cpp:323
virtual bvt convert_cond(const cond_exprt &)
virtual bvt convert_empty_union(const empty_union_exprt &expr)
virtual bvt convert_if(const if_exprt &expr)
Definition boolbv_if.cpp:12
virtual bvt convert_union(const union_exprt &expr)
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 boolbv.cpp:523
virtual bvt convert_byte_update(const byte_update_exprt &expr)
boolbv_widtht bv_width
Definition boolbv.h:116
virtual literalt convert_extractbit(const extractbit_exprt &expr)
const boolbv_mapt & get_map() const
Definition boolbv.h:97
std::list< quantifiert > quantifier_listt
Definition boolbv.h:271
unbounded_arrayt unbounded_array
Definition boolbv.h:88
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
virtual bvt convert_floatbv_op(const ieee_float_op_exprt &)
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition boolbv.cpp:575
virtual bvt convert_not(const not_exprt &expr)
exprt bv_get_cache(const exprt &expr) const
virtual bvt convert_extractbits(const extractbits_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
virtual bvt convert_update(const update_exprt &)
void finish_eager_conversion() override
Definition boolbv.h:80
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
virtual bvt convert_div(const div_exprt &expr)
virtual literalt convert_binary_overflow(const binary_overflow_exprt &expr)
virtual bvt convert_array_of(const array_of_exprt &expr)
Flatten arrays constructed from a single element.
bv_utilst bv_utils
Definition boolbv.h:117
virtual bvt convert_floatbv_mod_rem(const binary_exprt &)
virtual bvt convert_saturating_add_sub(const binary_exprt &expr)
virtual bvt convert_overflow_result(const overflow_result_exprt &expr)
virtual bvt convert_bitwise(const exprt &expr)
virtual bvt convert_array_comprehension(const array_comprehension_exprt &)
Definition boolbv.cpp:264
virtual bvt convert_bv_reduction(const unary_exprt &expr)
virtual literalt convert_equality(const equal_exprt &expr)
functionst functions
Definition boolbv.h:120
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition boolbv.cpp:94
quantifier_listt quantifier_list
Definition boolbv.h:272
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
Definition boolbv.h:108
virtual literalt convert_unary_overflow(const unary_overflow_exprt &expr)
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:102
virtual bvt convert_case(const exprt &expr)
virtual bvt convert_symbol(const exprt &expr)
Definition boolbv.cpp:299
virtual bvt convert_update_bit(const update_bit_exprt &)
void convert_with_bv(const exprt &index, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
arrayst SUB
Definition boolbv.h:130
virtual bvt convert_power(const binary_exprt &expr)
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
mp_integer get_value(const bvt &bv)
Definition boolbv.h:90
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
virtual bvt convert_concatenation(const concatenation_exprt &expr)
virtual bvt convert_struct(const struct_exprt &expr)
void convert_with_struct(const struct_typet &type, const exprt &where, const exprt &new_value, const bvt &prev_bv, bvt &next_bv)
virtual bvt convert_bitreverse(const bitreverse_exprt &expr)
virtual bvt convert_replication(const replication_exprt &expr)
literalt convert_rest(const exprt &expr) override
Definition boolbv.cpp:334
std::vector< std::size_t > offset_mapt
Definition boolbv.h:276
virtual bvt convert_abs(const abs_exprt &expr)
boolbv_mapt map
Definition boolbv.h:123
The byte swap expression.
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Complex constructor from a pair of numbers.
Definition std_expr.h:1916
Imaginary part of the expression describing a complex number.
Definition std_expr.h:2027
Real part of the expression describing a complex number.
Definition std_expr.h:1984
Concatenation of bit-vector operands.
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition std_expr.h:3355
A constant literal expression.
Definition std_expr.h:2995
Division.
Definition std_expr.h:1157
Union constructor to support unions without any member (a GCC/Clang feature).
Definition std_expr.h:1834
Maps a big-endian offset to a little-endian offset.
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
Extracts a single bit of a bit-vector operand.
Extracts a sub-range of a bit-vector operand.
Semantic type conversion from/to floating-point formats.
Application of (mathematical) function.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
The trinary if-then-else operator.
Definition std_expr.h:2375
Array index operator.
Definition std_expr.h:1470
A let expression.
Definition std_expr.h:3209
Extract member of struct or union.
Definition std_expr.h:2849
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
Boolean negation.
Definition std_expr.h:2332
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
virtual void clear_cache()
TO_BE_DOCUMENTED.
Definition prop.h:25
A base class for quantifier expressions.
Bit-vector replication.
Struct constructor from list of elements.
Definition std_expr.h:1877
Structure type, corresponds to C style structs.
Definition std_types.h:231
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
The unary minus expression.
Definition std_expr.h:484
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
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
Uninterpreted Functions.
std::vector< literalt > bvt
Definition literal.h:201
STL namespace.
BigInt mp_integer
Definition smt_terms.h:17