cprover
boolbv.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_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 #include <util/optional.h>
21 
23 
24 #include "bv_utils.h"
25 #include "boolbv_width.h"
26 #include "boolbv_map.h"
27 #include "arrays.h"
28 
30 class bswap_exprt;
31 class byte_extract_exprt;
32 class byte_update_exprt;
34 class extractbit_exprt;
35 class extractbits_exprt;
38 class member_exprt;
39 class replication_exprt;
40 
41 class boolbvt:public arrayst
42 {
43 public:
45  const namespacet &_ns,
46  propt &_prop,
48  bool get_array_constraints = false)
51  bv_width(_ns),
52  bv_utils(_prop),
53  functions(*this),
54  map(_prop)
55  {
56  }
57 
58  virtual const bvt &convert_bv( // check cache
59  const exprt &expr,
60  const optionalt<std::size_t> expected_width = nullopt);
61 
62  virtual bvt convert_bitvector(const exprt &expr); // no cache
63 
64  // overloading
65  exprt get(const exprt &expr) const override;
66  void set_to(const exprt &expr, bool value) override;
67  void print_assignment(std::ostream &out) const override;
68 
69  void clear_cache() override
70  {
72  bv_cache.clear();
73  }
74 
75  void post_process() override
76  {
80  }
81 
82  enum class unbounded_arrayt { U_NONE, U_ALL, U_AUTO };
84 
86  {
87  return get_value(bv, 0, bv.size());
88  }
89 
90  mp_integer get_value(const bvt &bv, std::size_t offset, std::size_t width);
91 
92  const boolbv_mapt &get_map() const
93  {
94  return map;
95  }
96 
97  virtual std::size_t boolbv_width(const typet &type) const
98  {
99  return bv_width(type);
100  }
101 
102  virtual endianness_mapt
103  endianness_map(const typet &type, bool little_endian) const
104  {
105  return endianness_mapt{type, little_endian, ns};
106  }
107 
108  virtual endianness_mapt endianness_map(const typet &type) const;
109 
110 protected:
113 
114  // uninterpreted functions
116 
117  // the mapping from identifiers to literals
119 
120  // overloading
121  literalt convert_rest(const exprt &expr) override;
122  virtual bool boolbv_set_equality_to_true(const equal_exprt &expr);
123 
124  // NOLINTNEXTLINE(readability/identifiers)
125  typedef arrayst SUB;
126 
127  bvt conversion_failed(const exprt &expr);
128 
129  typedef std::unordered_map<const exprt, bvt, irep_hash> bv_cachet;
131 
132  bool type_conversion(
133  const typet &src_type, const bvt &src,
134  const typet &dest_type, bvt &dest);
135 
137  virtual literalt convert_typecast(const typecast_exprt &expr);
138  virtual literalt convert_reduction(const unary_exprt &expr);
139  virtual literalt convert_onehot(const unary_exprt &expr);
140  virtual literalt convert_extractbit(const extractbit_exprt &expr);
141  virtual literalt convert_overflow(const exprt &expr);
142  virtual literalt convert_equality(const equal_exprt &expr);
144  const binary_relation_exprt &expr);
146  virtual literalt convert_quantifier(const quantifier_exprt &expr);
147 
148  virtual bvt convert_index(const exprt &array, const mp_integer &index);
149  virtual bvt convert_index(const index_exprt &expr);
150  virtual bvt convert_bswap(const bswap_exprt &expr);
151  virtual bvt convert_byte_extract(const byte_extract_exprt &expr);
152  virtual bvt convert_byte_update(const byte_update_exprt &expr);
153  virtual bvt convert_constraint_select_one(const exprt &expr);
154  virtual bvt convert_if(const if_exprt &expr);
155  virtual bvt convert_struct(const struct_exprt &expr);
156  virtual bvt convert_array(const exprt &expr);
157  virtual bvt convert_vector(const vector_exprt &expr);
158  virtual bvt convert_complex(const complex_exprt &expr);
159  virtual bvt convert_complex_real(const complex_real_exprt &expr);
160  virtual bvt convert_complex_imag(const complex_imag_exprt &expr);
162  virtual bvt convert_let(const let_exprt &);
163  virtual bvt convert_array_of(const array_of_exprt &expr);
164  virtual bvt convert_union(const union_exprt &expr);
165  virtual bvt convert_bv_typecast(const typecast_exprt &expr);
166  virtual bvt convert_add_sub(const exprt &expr);
167  virtual bvt convert_mult(const mult_exprt &expr);
168  virtual bvt convert_div(const div_exprt &expr);
169  virtual bvt convert_mod(const mod_exprt &expr);
170  virtual bvt convert_floatbv_op(const ieee_float_op_exprt &);
171  virtual bvt convert_floatbv_mod_rem(const binary_exprt &);
173  virtual bvt convert_member(const member_exprt &expr);
174  virtual bvt convert_with(const with_exprt &expr);
175  virtual bvt convert_update(const update_exprt &);
176  virtual bvt convert_case(const exprt &expr);
177  virtual bvt convert_cond(const cond_exprt &);
178  virtual bvt convert_shift(const binary_exprt &expr);
179  virtual bvt convert_bitwise(const exprt &expr);
180  virtual bvt convert_unary_minus(const unary_minus_exprt &expr);
181  virtual bvt convert_abs(const abs_exprt &expr);
182  virtual bvt convert_concatenation(const concatenation_exprt &expr);
183  virtual bvt convert_replication(const replication_exprt &expr);
184  virtual bvt convert_bv_literals(const exprt &expr);
185  virtual bvt convert_constant(const constant_exprt &expr);
186  virtual bvt convert_extractbits(const extractbits_exprt &expr);
187  virtual bvt convert_symbol(const exprt &expr);
188  virtual bvt convert_bv_reduction(const unary_exprt &expr);
189  virtual bvt convert_not(const not_exprt &expr);
190  virtual bvt convert_power(const binary_exprt &expr);
192  const function_application_exprt &expr);
193 
194  virtual exprt make_bv_expr(const typet &type, const bvt &bv);
195  virtual exprt make_free_bv_expr(const typet &type);
196 
197  void convert_with(
198  const typet &type,
199  const exprt &op1,
200  const exprt &op2,
201  const bvt &prev_bv,
202  bvt &next_bv);
203 
204  void convert_with_bv(
205  const exprt &op1,
206  const exprt &op2,
207  const bvt &prev_bv,
208  bvt &next_bv);
209 
210  void convert_with_array(
211  const array_typet &type,
212  const exprt &op1,
213  const exprt &op2,
214  const bvt &prev_bv,
215  bvt &next_bv);
216 
217  void convert_with_union(
218  const union_typet &type,
219  const exprt &op2,
220  const bvt &prev_bv,
221  bvt &next_bv);
222 
223  void convert_with_struct(
224  const struct_typet &type,
225  const exprt &op1,
226  const exprt &op2,
227  const bvt &prev_bv,
228  bvt &next_bv);
229 
230  void convert_update_rec(
231  const exprt::operandst &designator,
232  std::size_t d,
233  const typet &type,
234  std::size_t offset,
235  const exprt &new_value,
236  bvt &bv);
237 
238  virtual exprt bv_get_unbounded_array(const exprt &) const;
239 
240  virtual exprt bv_get_rec(
241  const exprt &expr,
242  const bvt &bv,
243  std::size_t offset,
244  const typet &type) const;
245 
246  exprt bv_get(const bvt &bv, const typet &type) const;
247  exprt bv_get_cache(const exprt &expr) const;
248 
249  // unbounded arrays
250  bool is_unbounded_array(const typet &type) const override;
251 
252  // quantifier instantiations
254  {
255  public:
257  : expr(std::move(_expr)), l(std::move(_l))
258  {
259  }
260 
263  };
264 
265  typedef std::list<quantifiert> quantifier_listt;
267 
269 
270  typedef std::vector<std::size_t> offset_mapt;
272 
273  // strings
275 
276  // scopes
277  std::size_t scope_counter = 0;
278 
281 };
282 
283 #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
boolbvt::convert_bv_typecast
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
Definition: boolbv_typecast.cpp:19
boolbvt::convert_overflow
virtual literalt convert_overflow(const exprt &expr)
Definition: boolbv_overflow.cpp:13
boolbvt::bv_width
boolbv_widtht bv_width
Definition: boolbv.h:111
boolbvt::unbounded_array
unbounded_arrayt unbounded_array
Definition: boolbv.h:83
boolbvt::convert_with_array
void convert_with_array(const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
Definition: boolbv_with.cpp:83
boolbvt::map
boolbv_mapt map
Definition: boolbv.h:118
boolbvt::convert_member
virtual bvt convert_member(const member_exprt &expr)
Definition: boolbv_member.cpp:91
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
boolbvt::bv_cachet
std::unordered_map< const exprt, bvt, irep_hash > bv_cachet
Definition: boolbv.h:129
boolbvt::convert_bv_rel
virtual literalt convert_bv_rel(const binary_relation_exprt &)
Flatten <, >, <= and >= expressions.
Definition: boolbv_bv_rel.cpp:18
boolbvt::convert_byte_update
virtual bvt convert_byte_update(const byte_update_exprt &expr)
Definition: boolbv_byte_update.cpp:17
byte_update_exprt
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Definition: byte_operators.h:78
boolbvt::post_process_quantifiers
void post_process_quantifiers()
Definition: boolbv_quantifier.cpp:231
mp_arith.h
boolbvt::convert_array_of
virtual bvt convert_array_of(const array_of_exprt &expr)
Flatten arrays constructed from a single element.
Definition: boolbv_array_of.cpp:16
boolbvt::convert_reduction
virtual literalt convert_reduction(const unary_exprt &expr)
Definition: boolbv_reduction.cpp:13
functionst::post_process
virtual void post_process()
Definition: functions.h:36
boolbvt::type_conversion
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
Definition: boolbv_typecast.cpp:32
boolbvt::convert_cond
virtual bvt convert_cond(const cond_exprt &)
Definition: boolbv_cond.cpp:13
boolbvt::convert_bitvector
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:98
boolbvt::is_unbounded_array
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:543
typet
The type of an expression, extends irept.
Definition: type.h:28
bvt
std::vector< literalt > bvt
Definition: literal.h:201
boolbvt::fresh_binding
binding_exprt::variablest fresh_binding(const binding_exprt &)
create new, unique variables for the given binding
Definition: boolbv.cpp:562
boolbvt::quantifier_listt
std::list< quantifiert > quantifier_listt
Definition: boolbv.h:265
optional.h
boolbvt::set_to
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:514
boolbvt::convert_complex
virtual bvt convert_complex(const complex_exprt &expr)
Definition: boolbv_complex.cpp:13
numberingt< irep_idt >
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2172
boolbvt::boolbvt
boolbvt(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
Definition: boolbv.h:44
boolbvt::convert_with_struct
void convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
Definition: boolbv_with.cpp:176
boolbvt::bv_get_rec
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset, const typet &type) const
Definition: boolbv_get.cpp:44
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1775
boolbvt::convert_mod
virtual bvt convert_mod(const mod_exprt &expr)
Definition: boolbv_mod.cpp:12
union_exprt
Union constructor from single element.
Definition: std_expr.h:1602
bv_utils.h
boolbvt::convert_vector
virtual bvt convert_vector(const vector_exprt &expr)
Definition: boolbv_vector.cpp:12
boolbvt::convert_symbol
virtual bvt convert_symbol(const exprt &expr)
Definition: boolbv.cpp:295
boolbvt::convert_index
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
Definition: boolbv_index.cpp:285
exprt
Base class for all expressions.
Definition: expr.h:54
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:550
boolbvt::convert_onehot
virtual literalt convert_onehot(const unary_exprt &expr)
Definition: boolbv_onehot.cpp:12
boolbvt::convert_abs
virtual bvt convert_abs(const abs_exprt &expr)
Definition: boolbv_abs.cpp:17
concatenation_exprt
Concatenation of bit-vector operands.
Definition: bitvector_expr.h:590
quantifier_exprt
A base class for quantifier expressions.
Definition: mathematical_expr.h:263
boolbvt::convert_union
virtual bvt convert_union(const union_exprt &expr)
Definition: boolbv_union.cpp:11
vector_exprt
Vector constructor from list of elements.
Definition: std_expr.h:1566
functions.h
Uninterpreted Functions.
div_exprt
Division.
Definition: std_expr.h:1064
boolbvt::convert_case
virtual bvt convert_case(const exprt &expr)
Definition: boolbv_case.cpp:13
equal_exprt
Equality.
Definition: std_expr.h:1225
boolbvt::functions
functionst functions
Definition: boolbv.h:115
boolbvt::convert_add_sub
virtual bvt convert_add_sub(const exprt &expr)
Definition: boolbv_add_sub.cpp:16
boolbvt::unbounded_arrayt::U_AUTO
@ U_AUTO
replication_exprt
Bit-vector replication.
Definition: bitvector_expr.h:518
boolbvt::convert_constant
virtual bvt convert_constant(const constant_exprt &expr)
Definition: boolbv_constant.cpp:13
boolbvt::convert_extractbit
virtual literalt convert_extractbit(const extractbit_exprt &expr)
Definition: boolbv_extractbit.cpp:19
boolbvt::convert_concatenation
virtual bvt convert_concatenation(const concatenation_exprt &expr)
Definition: boolbv_concatenation.cpp:14
functionst
Definition: functions.h:23
boolbvt::quantifiert::quantifiert
quantifiert(exprt _expr, literalt _l)
Definition: boolbv.h:256
expr.h
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1668
bv_utilst
Definition: bv_utils.h:24
boolbvt::convert_mult
virtual bvt convert_mult(const mult_exprt &expr)
Definition: boolbv_mult.cpp:13
boolbvt::convert_shift
virtual bvt convert_shift(const binary_exprt &expr)
Definition: boolbv_shift.cpp:15
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
arrayst::post_process
void post_process() override
Definition: arrays.h:39
boolbvt::convert_byte_extract
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
Definition: boolbv_byte_extract.cpp:35
boolbvt::boolbv_set_equality_to_true
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
Definition: boolbv.cpp:483
boolbvt::convert_array
virtual bvt convert_array(const exprt &expr)
Flatten array.
Definition: boolbv_array.cpp:16
boolbvt::unbounded_arrayt
unbounded_arrayt
Definition: boolbv.h:82
boolbvt::bv_cache
bv_cachet bv_cache
Definition: boolbv.h:130
boolbvt::convert_bv_literals
virtual bvt convert_bv_literals(const exprt &expr)
Definition: boolbv.cpp:274
prop_conv_solvert::clear_cache
virtual void clear_cache()
Definition: prop_conv_solver.h:74
boolbvt::convert_extractbits
virtual bvt convert_extractbits(const extractbits_exprt &expr)
Definition: boolbv_extractbits.cpp:14
boolbvt::boolbv_width
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:97
floatbv_typecast_exprt
Semantic type conversion from/to floating-point formats.
Definition: floatbv_expr.h:19
boolbvt::convert_floatbv_typecast
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
Definition: boolbv_floatbv_op.cpp:19
boolbvt::convert_verilog_case_equality
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
Definition: boolbv_equality.cpp:60
arrayst::ns
const namespacet & ns
Definition: arrays.h:54
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1402
boolbvt::convert_if
virtual bvt convert_if(const if_exprt &expr)
Definition: boolbv_if.cpp:12
boolbvt::convert_complex_real
virtual bvt convert_complex_real(const complex_real_exprt &expr)
Definition: boolbv_complex.cpp:40
boolbvt::make_bv_expr
virtual exprt make_bv_expr(const typet &type, const bvt &bv)
Definition: boolbv.cpp:524
boolbvt::convert_ieee_float_rel
virtual literalt convert_ieee_float_rel(const binary_relation_exprt &)
Definition: boolbv_ieee_float_rel.cpp:17
boolbvt::scope_counter
std::size_t scope_counter
Definition: boolbv.h:277
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:192
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
binding_exprt::variablest
std::vector< symbol_exprt > variablest
Definition: std_expr.h:2848
boolbvt::convert_update_rec
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)
Definition: boolbv_update.cpp:35
boolbvt::post_process
void post_process() override
Definition: boolbv.h:75
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:390
boolbvt::bv_get_cache
exprt bv_get_cache(const exprt &expr) const
Definition: boolbv_get.cpp:267
boolbvt::convert_bv_reduction
virtual bvt convert_bv_reduction(const unary_exprt &expr)
Definition: boolbv_reduction.cpp:54
boolbvt::convert_with_union
void convert_with_union(const union_typet &type, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
Definition: boolbv_with.cpp:223
message_handlert
Definition: message.h:28
binding_exprt
A base class for variable bindings (quantifiers, let, lambda)
Definition: std_expr.h:2846
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1707
abs_exprt
Absolute value.
Definition: std_expr.h:346
union_typet
The union type.
Definition: c_types.h:112
boolbvt::convert_constraint_select_one
virtual bvt convert_constraint_select_one(const exprt &expr)
Definition: boolbv_constraint_select_one.cpp:12
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:40
boolbvt::clear_cache
void clear_cache() override
Definition: boolbv.h:69
boolbvt::convert_bswap
virtual bvt convert_bswap(const bswap_exprt &expr)
Definition: boolbv_bswap.cpp:13
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
boolbvt::get_value
mp_integer get_value(const bvt &bv)
Definition: boolbv.h:85
boolbvt::make_free_bv_expr
virtual exprt make_free_bv_expr(const typet &type)
Definition: boolbv.cpp:535
boolbvt::unbounded_arrayt::U_NONE
@ U_NONE
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2442
boolbvt::quantifier_list
quantifier_listt quantifier_list
Definition: boolbv.h:266
boolbvt::bv_get_unbounded_array
virtual exprt bv_get_unbounded_array(const exprt &) const
Definition: boolbv_get.cpp:279
boolbvt::quantifiert::expr
exprt expr
Definition: boolbv.h:261
endianness_map.h
boolbvt::quantifiert::l
literalt l
Definition: boolbv.h:262
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: bitvector_expr.h:363
boolbvt::SUB
arrayst SUB
Definition: boolbv.h:125
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2613
boolbvt::convert_let
virtual bvt convert_let(const let_exprt &)
Definition: boolbv_let.cpp:15
boolbv_widtht
Definition: boolbv_width.h:19
boolbvt::convert_bitwise
virtual bvt convert_bitwise(const exprt &expr)
Definition: boolbv_bitwise.cpp:13
boolbvt::get_map
const boolbv_mapt & get_map() const
Definition: boolbv.h:92
boolbvt::convert_floatbv_op
virtual bvt convert_floatbv_op(const ieee_float_op_exprt &)
Definition: boolbv_floatbv_op.cpp:83
arrays.h
Theory of Arrays with Extensionality.
propt
TO_BE_DOCUMENTED.
Definition: prop.h:23
cond_exprt
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition: std_expr.h:3065
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:231
array_typet
Arrays with given size.
Definition: std_types.h:763
boolbvt::convert_struct
virtual bvt convert_struct(const struct_exprt &expr)
Definition: boolbv_struct.cpp:11
boolbvt::quantifiert
Definition: boolbv.h:254
boolbv_width.h
boolbvt::bv_get
exprt bv_get(const bvt &bv, const typet &type) const
Definition: boolbv_get.cpp:262
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:112
boolbvt::string_numbering
numberingt< irep_idt > string_numbering
Definition: boolbv.h:274
boolbvt::convert_with_bv
void convert_with_bv(const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
Definition: boolbv_with.cpp:146
boolbvt::unbounded_arrayt::U_ALL
@ U_ALL
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
complex_imag_exprt
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1820
literalt
Definition: literal.h:26
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
endianness_mapt
Maps a big-endian offset to a little-endian offset.
Definition: endianness_map.h:31
boolbvt
Definition: boolbv.h:42
boolbvt::convert_equality
virtual literalt convert_equality(const equal_exprt &expr)
Definition: boolbv_equality.cpp:16
boolbv_mapt
Definition: boolbv_map.h:22
ieee_float_op_exprt
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: floatbv_expr.h:364
boolbvt::convert_unary_minus
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
Definition: boolbv_unary_minus.cpp:20
boolbvt::conversion_failed
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:84
bswap_exprt
The byte swap expression.
Definition: bitvector_expr.h:19
boolbvt::convert_replication
virtual bvt convert_replication(const replication_exprt &expr)
Definition: boolbv_replication.cpp:14
boolbvt::convert_quantifier
virtual literalt convert_quantifier(const quantifier_exprt &expr)
Definition: boolbv_quantifier.cpp:206
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: bitvector_expr.h:430
boolbvt::convert_array_comprehension
virtual bvt convert_array_comprehension(const array_comprehension_exprt &)
Definition: boolbv.cpp:232
boolbvt::endianness_map
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
Definition: boolbv.h:103
index_exprt
Array index operator.
Definition: std_expr.h:1328
boolbvt::convert_floatbv_mod_rem
virtual bvt convert_floatbv_mod_rem(const binary_exprt &)
Definition: boolbv_floatbv_mod_rem.cpp:15
boolbvt::convert_not
virtual bvt convert_not(const not_exprt &expr)
Definition: boolbv_not.cpp:13
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
boolbvt::convert_typecast
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
Definition: boolbv_typecast.cpp:612
boolbvt::offset_mapt
std::vector< std::size_t > offset_mapt
Definition: boolbv.h:270
boolbvt::build_offset_map
offset_mapt build_offset_map(const struct_typet &src)
Definition: boolbv.cpp:591
arrayst
Definition: arrays.h:31
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3128
boolbvt::convert_rest
literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:330
arrayst::get_array_constraints
bool get_array_constraints
Definition: arrays.h:111
boolbvt::convert_power
virtual bvt convert_power(const binary_exprt &expr)
Definition: boolbv_power.cpp:12
constant_exprt
A constant literal expression.
Definition: std_expr.h:2753
arrayst::message_handler
message_handlert & message_handler
Definition: arrays.h:56
boolbvt::convert_function_application
virtual bvt convert_function_application(const function_application_exprt &expr)
Definition: boolbv.cpp:319
boolbvt::convert_div
virtual bvt convert_div(const div_exprt &expr)
Definition: boolbv_div.cpp:13
boolbvt::print_assignment
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: boolbv.cpp:585
boolbvt::get
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: boolbv_get.cpp:19
let_exprt
A let expression.
Definition: std_expr.h:2919
boolbv_map.h
mod_exprt
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
boolbvt::convert_update
virtual bvt convert_update(const update_exprt &)
Definition: boolbv_update.cpp:14
not_exprt
Boolean negation.
Definition: std_expr.h:2127
boolbvt::convert_with
virtual bvt convert_with(const with_exprt &expr)
Definition: boolbv_with.cpp:15
boolbvt::convert_complex_imag
virtual bvt convert_complex_imag(const complex_imag_exprt &expr)
Definition: boolbv_complex.cpp:54