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/mp_arith.h>
18 #include <util/expr.h>
19 #include <util/byte_operators.h>
20 
21 #include "bv_utils.h"
22 #include "boolbv_width.h"
23 #include "boolbv_map.h"
24 #include "arrays.h"
25 #include "functions.h"
26 
27 class extractbit_exprt;
28 class extractbits_exprt;
29 class member_exprt;
30 
31 class boolbvt:public arrayst
32 {
33 public:
35  const namespacet &_ns,
36  propt &_prop):
37  arrayst(_ns, _prop),
39  boolbv_width(_ns),
40  bv_utils(_prop),
41  functions(*this),
42  map(_prop, _ns, boolbv_width)
43  {
44  }
45 
46  virtual const bvt &convert_bv(const exprt &expr); // check cache
47  virtual bvt convert_bitvector(const exprt &expr); // no cache
48 
49  // overloading
50  exprt get(const exprt &expr) const override;
51  void set_to(const exprt &expr, bool value) override;
52  void print_assignment(std::ostream &out) const override;
53 
54  void clear_cache() override
55  {
57  bv_cache.clear();
58  }
59 
60  void post_process() override
61  {
65  }
66 
67  // get literals for variables/expressions, if available
68  virtual bool literal(
69  const exprt &expr,
70  std::size_t bit,
71  literalt &literal) const;
72 
73  using arrayst::literal;
74 
75  enum class unbounded_arrayt { U_NONE, U_ALL, U_AUTO };
77 
79  {
80  return get_value(bv, 0, bv.size());
81  }
82 
83  mp_integer get_value(const bvt &bv, std::size_t offset, std::size_t width);
84 
85  const boolbv_mapt &get_map() const
86  {
87  return map;
88  }
89 
91 
92 protected:
94 
95  // uninterpreted functions
97 
98  // the mapping from identifiers to literals
100 
101  // overloading
102  virtual literalt convert_rest(const exprt &expr) override;
103  virtual bool boolbv_set_equality_to_true(const equal_exprt &expr);
104 
105  // NOLINTNEXTLINE(readability/identifiers)
106  typedef arrayst SUB;
107 
108  void conversion_failed(const exprt &expr, bvt &bv)
109  {
110  bv=conversion_failed(expr);
111  }
112 
113  bvt conversion_failed(const exprt &expr);
114 
115  typedef std::unordered_map<const exprt, bvt, irep_hash> bv_cachet;
116  bv_cachet bv_cache;
117 
118  bool type_conversion(
119  const typet &src_type, const bvt &src,
120  const typet &dest_type, bvt &dest);
121 
122  virtual literalt convert_bv_rel(const exprt &expr);
123  virtual literalt convert_typecast(const typecast_exprt &expr);
124  virtual literalt convert_reduction(const unary_exprt &expr);
125  virtual literalt convert_onehot(const unary_exprt &expr);
126  virtual literalt convert_extractbit(const extractbit_exprt &expr);
127  virtual literalt convert_overflow(const exprt &expr);
128  virtual literalt convert_equality(const equal_exprt &expr);
130  const binary_relation_exprt &expr);
131  virtual literalt convert_ieee_float_rel(const exprt &expr);
132  virtual literalt convert_quantifier(const exprt &expr);
133 
134  virtual bvt convert_index(const exprt &array, const mp_integer &index);
135  virtual bvt convert_index(const index_exprt &expr);
136  virtual bvt convert_byte_extract(const byte_extract_exprt &expr);
137  virtual bvt convert_byte_update(const byte_update_exprt &expr);
138  virtual bvt convert_constraint_select_one(const exprt &expr);
139  virtual bvt convert_if(const if_exprt &expr);
140  virtual bvt convert_struct(const struct_exprt &expr);
141  virtual bvt convert_array(const exprt &expr);
142  virtual bvt convert_vector(const exprt &expr);
143  virtual bvt convert_complex(const exprt &expr);
144  virtual bvt convert_complex_real(const exprt &expr);
145  virtual bvt convert_complex_imag(const exprt &expr);
146  virtual bvt convert_lambda(const exprt &expr);
147  virtual bvt convert_array_of(const array_of_exprt &expr);
148  virtual bvt convert_union(const union_exprt &expr);
149  virtual bvt convert_bv_typecast(const typecast_exprt &expr);
150  virtual bvt convert_add_sub(const exprt &expr);
151  virtual bvt convert_mult(const exprt &expr);
152  virtual bvt convert_div(const div_exprt &expr);
153  virtual bvt convert_mod(const mod_exprt &expr);
154  virtual bvt convert_floatbv_op(const exprt &expr);
156  virtual bvt convert_member(const member_exprt &expr);
157  virtual bvt convert_with(const exprt &expr);
158  virtual bvt convert_update(const exprt &expr);
159  virtual bvt convert_case(const exprt &expr);
160  virtual bvt convert_cond(const exprt &expr);
161  virtual bvt convert_shift(const binary_exprt &expr);
162  virtual bvt convert_bitwise(const exprt &expr);
163  virtual bvt convert_unary_minus(const unary_exprt &expr);
164  virtual bvt convert_abs(const exprt &expr);
165  virtual bvt convert_concatenation(const exprt &expr);
166  virtual bvt convert_replication(const replication_exprt &expr);
167  virtual bvt convert_bv_literals(const exprt &expr);
168  virtual bvt convert_constant(const constant_exprt &expr);
169  virtual bvt convert_extractbits(const extractbits_exprt &expr);
170  virtual bvt convert_symbol(const exprt &expr);
171  virtual bvt convert_bv_reduction(const unary_exprt &expr);
172  virtual bvt convert_not(const not_exprt &expr);
173  virtual bvt convert_power(const binary_exprt &expr);
175  const function_application_exprt &expr);
176 
177  virtual void make_bv_expr(const typet &type, const bvt &bv, exprt &dest);
178  virtual void make_free_bv_expr(const typet &type, exprt &dest);
179 
180  void convert_with(
181  const typet &type,
182  const exprt &op1,
183  const exprt &op2,
184  const bvt &prev_bv,
185  bvt &next_bv);
186 
187  void convert_with_bv(
188  const typet &type,
189  const exprt &op1,
190  const exprt &op2,
191  const bvt &prev_bv,
192  bvt &next_bv);
193 
194  void convert_with_array(
195  const array_typet &type,
196  const exprt &op1,
197  const exprt &op2,
198  const bvt &prev_bv,
199  bvt &next_bv);
200 
201  void convert_with_union(
202  const union_typet &type,
203  const exprt &op1,
204  const exprt &op2,
205  const bvt &prev_bv,
206  bvt &next_bv);
207 
208  void convert_with_struct(
209  const struct_typet &type,
210  const exprt &op1,
211  const exprt &op2,
212  const bvt &prev_bv,
213  bvt &next_bv);
214 
215  void convert_update_rec(
216  const exprt::operandst &designator,
217  std::size_t d,
218  const typet &type,
219  std::size_t offset,
220  const exprt &new_value,
221  bvt &bv);
222 
223  virtual exprt bv_get_unbounded_array(const exprt &) const;
224 
225  virtual exprt bv_get_rec(
226  const bvt &bv,
227  const std::vector<bool> &unknown,
228  std::size_t offset,
229  const typet &type) const;
230 
231  exprt bv_get(const bvt &bv, const typet &type) const;
232  exprt bv_get_cache(const exprt &expr) const;
233 
234  // unbounded arrays
235  bool is_unbounded_array(const typet &type) const override;
236 
237  // quantifier instantiations
239  {
240  public:
243  };
244 
245  typedef std::list<quantifiert> quantifier_listt;
246  quantifier_listt quantifier_list;
247 
249 
250  typedef std::vector<std::size_t> offset_mapt;
251  void build_offset_map(const struct_typet &src, offset_mapt &dest);
252 
253  // strings
255 };
256 
257 #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H
boolbvt(const namespacet &_ns, propt &_prop)
Definition: boolbv.h:34
virtual bvt convert_case(const exprt &expr)
Definition: boolbv_case.cpp:13
virtual bvt convert_complex_real(const exprt &expr)
The type of an expression.
Definition: type.h:20
void print_assignment(std::ostream &out) const override
Definition: boolbv.cpp:697
std::vector< std::size_t > offset_mapt
Definition: boolbv.h:250
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
virtual bvt convert_with(const exprt &expr)
Definition: boolbv_with.cpp:18
Boolean negation.
Definition: std_expr.h:2648
virtual bvt convert_concatenation(const exprt &expr)
semantic type conversion
Definition: std_expr.h:1725
virtual bvt convert_abs(const exprt &expr)
Definition: boolbv_abs.cpp:17
bv_utilst bv_utils
Definition: boolbv.h:93
virtual literalt convert_ieee_float_rel(const exprt &expr)
BigInt mp_integer
Definition: mp_arith.h:19
virtual bvt convert_array_of(const array_of_exprt &expr)
arrayst SUB
Definition: boolbv.h:106
virtual bvt convert_bv_reduction(const unary_exprt &expr)
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
application of (mathematical) function
Definition: std_expr.h:3785
void post_process() override
Definition: arrays.h:33
virtual exprt bv_get_unbounded_array(const exprt &) const
Definition: boolbv_get.cpp:300
void convert_with_array(const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual literalt convert_onehot(const unary_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
virtual literalt convert_overflow(const exprt &expr)
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
boolbv_widtht boolbv_width
Definition: boolbv.h:90
virtual literalt convert_equality(const equal_exprt &expr)
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:673
virtual bvt convert_replication(const replication_exprt &expr)
virtual bvt convert_bv_literals(const exprt &expr)
Definition: boolbv.cpp:357
virtual bvt convert_struct(const struct_exprt &expr)
virtual bvt convert_function_application(const function_application_exprt &expr)
Definition: boolbv.cpp:413
void clear_cache() override
Definition: boolbv.h:54
The trinary if-then-else operator.
Definition: std_expr.h:2771
virtual bvt convert_lambda(const exprt &expr)
Definition: boolbv.cpp:310
void build_offset_map(const struct_typet &src, offset_mapt &dest)
Definition: boolbv.cpp:708
A constant literal expression.
Definition: std_expr.h:3685
Structure type.
Definition: std_types.h:296
void post_process() override
Definition: boolbv.h:60
virtual bool literal(const exprt &expr, literalt &literal) const
Definition: prop_conv.cpp:46
virtual bvt convert_constant(const constant_exprt &expr)
virtual bvt convert_symbol(const exprt &expr)
Definition: boolbv.cpp:378
Definition: boolbv.h:31
virtual bvt convert_mult(const exprt &expr)
Definition: boolbv_mult.cpp:13
Extract member of struct or union.
Definition: std_expr.h:3214
equality
Definition: std_expr.h:1082
virtual bvt convert_complex(const exprt &expr)
virtual literalt convert_quantifier(const exprt &expr)
virtual bvt convert_update(const exprt &expr)
virtual void clear_cache()
Definition: prop_conv.h:110
void convert_with_union(const union_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual literalt convert_bv_rel(const exprt &expr)
Expression classes for byte-level operators.
virtual bvt convert_add_sub(const exprt &expr)
division (integer and real)
Definition: std_expr.h:854
A generic base class for binary expressions.
Definition: std_expr.h:471
virtual literalt convert_reduction(const unary_exprt &expr)
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
Theory of Arrays with Extensionality.
functionst functions
Definition: boolbv.h:96
virtual void make_free_bv_expr(const typet &type, exprt &dest)
Definition: boolbv.cpp:653
union constructor from single element
Definition: std_expr.h:1389
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:2505
virtual bvt convert_bitvector(const exprt &expr)
Definition: boolbv.cpp:154
virtual bvt convert_floatbv_op(const exprt &expr)
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
Generic base class for unary expressions.
Definition: std_expr.h:221
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
Definition: boolbv.cpp:590
virtual bool literal(const exprt &expr, std::size_t bit, literalt &literal) const
Definition: boolbv.cpp:31
numbering< irep_idt > string_numbering
Definition: boolbv.h:254
virtual bvt convert_union(const union_exprt &expr)
array constructor from single element
Definition: std_expr.h:1252
virtual bvt convert_extractbits(const extractbits_exprt &expr)
Definition: arrays.h:28
quantifier_listt quantifier_list
Definition: boolbv.h:246
virtual literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:424
TO_BE_DOCUMENTED.
Definition: prop.h:22
virtual bvt convert_complex_imag(const exprt &expr)
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
virtual bvt convert_cond(const exprt &expr)
Definition: boolbv_cond.cpp:13
void post_process_quantifiers()
std::vector< exprt > operandst
Definition: expr.h:49
virtual bvt convert_not(const not_exprt &expr)
Definition: boolbv_not.cpp:12
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)
void convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual bvt convert_byte_update(const byte_update_exprt &expr)
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
mp_integer get_value(const bvt &bv)
Definition: boolbv.h:78
virtual bvt convert_constraint_select_one(const exprt &expr)
unbounded_arrayt unbounded_array
Definition: boolbv.h:76
virtual bvt convert_vector(const exprt &expr)
void convert_with_bv(const typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual bvt convert_array(const exprt &expr)
bv_cachet bv_cache
Definition: boolbv.h:116
virtual void make_bv_expr(const typet &type, const bvt &bv, exprt &dest)
Definition: boolbv.cpp:642
Uninterpreted Functions.
semantic type conversion from/to floating-point formats
Definition: std_expr.h:1783
Base class for all expressions.
Definition: expr.h:46
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
The union type.
Definition: std_types.h:424
virtual exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const
Definition: boolbv_get.cpp:68
virtual bvt convert_mod(const mod_exprt &expr)
Definition: boolbv_mod.cpp:12
virtual bvt convert_member(const member_exprt &expr)
const boolbv_mapt & get_map() const
Definition: boolbv.h:85
virtual bvt convert_if(const if_exprt &expr)
Definition: boolbv_if.cpp:12
arrays with given size
Definition: std_types.h:901
TO_BE_DOCUMENTED.
exprt bv_get(const bvt &bv, const typet &type) const
Definition: boolbv_get.cpp:280
boolbv_mapt map
Definition: boolbv.h:99
virtual bvt convert_unary_minus(const unary_exprt &expr)
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
exprt bv_get_cache(const exprt &expr) const
Definition: boolbv_get.cpp:287
virtual bvt convert_div(const div_exprt &expr)
Definition: boolbv_div.cpp:13
std::list< quantifiert > quantifier_listt
Definition: boolbv.h:245
void set_to(const exprt &expr, bool value) override
Definition: boolbv.cpp:621
virtual literalt convert_extractbit(const extractbit_exprt &expr)
TO_BE_DOCUMENTED.
struct constructor from list of elements
Definition: std_expr.h:1464
Bit-vector replication.
Definition: std_expr.h:2361
std::unordered_map< const exprt, bvt, irep_hash > bv_cachet
Definition: boolbv.h:115
std::vector< literalt > bvt
Definition: literal.h:197
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
binary modulo
Definition: std_expr.h:902
virtual bvt convert_bitwise(const exprt &expr)
virtual void post_process()
Definition: functions.h:34
unbounded_arrayt
Definition: boolbv.h:75
virtual bvt convert_power(const binary_exprt &expr)
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2434
array index operator
Definition: std_expr.h:1170