cprover
boolbv.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "boolbv.h"
10 
11 #include <algorithm>
12 #include <map>
13 #include <set>
14 
15 #include <util/arith_tools.h>
16 #include <util/bitvector_expr.h>
17 #include <util/floatbv_expr.h>
18 #include <util/magic.h>
19 #include <util/mp_arith.h>
20 #include <util/prefix.h>
21 #include <util/replace_expr.h>
22 #include <util/std_expr.h>
23 #include <util/std_types.h>
24 #include <util/string2int.h>
25 #include <util/string_constant.h>
26 #include <util/symbol.h>
27 #include <util/threeval.h>
28 
29 #include "boolbv_type.h"
30 
33 
37 const bvt &
38 boolbvt::convert_bv(const exprt &expr, optionalt<std::size_t> expected_width)
39 {
40  // check cache first
41  std::pair<bv_cachet::iterator, bool> cache_result=
42  bv_cache.insert(std::make_pair(expr, bvt()));
43  if(!cache_result.second)
44  {
45  return cache_result.first->second;
46  }
47 
48  // Iterators into hash_maps supposedly stay stable
49  // even though we are inserting more elements recursively.
50 
51  cache_result.first->second = convert_bitvector(expr);
52 
54  !expected_width || cache_result.first->second.size() == *expected_width,
55  "bitvector width shall match the indicated expected width",
56  expr.find_source_location(),
58 
59  // check
60  for(const auto &literal : cache_result.first->second)
61  {
62  if(freeze_all && !literal.is_constant())
63  prop.set_frozen(literal);
64 
66  literal.var_no() != literalt::unused_var_no(),
67  "variable number must be different from the unused variable number",
68  expr.find_source_location(),
70  }
71 
72  return cache_result.first->second;
73 }
74 
78 {
79  ignoring(expr);
80 
81  // try to make it free bits
82  std::size_t width=boolbv_width(expr.type());
83  return prop.new_variables(width);
84 }
85 
92 {
93  if(expr.type().id()==ID_bool)
94  {
95  bvt bv;
96  bv.resize(1);
97  bv[0]=convert(expr);
98  return bv;
99  }
100 
101  if(expr.id()==ID_index)
102  return convert_index(to_index_expr(expr));
103  else if(expr.id()==ID_constraint_select_one)
104  return convert_constraint_select_one(expr);
105  else if(expr.id()==ID_member)
106  return convert_member(to_member_expr(expr));
107  else if(expr.id()==ID_with)
108  return convert_with(to_with_expr(expr));
109  else if(expr.id()==ID_update)
110  return convert_update(to_update_expr(expr));
111  else if(expr.id()==ID_width)
112  {
113  std::size_t result_width=boolbv_width(expr.type());
114 
115  if(result_width==0)
116  return conversion_failed(expr);
117 
118  if(expr.operands().size()!=1)
119  return conversion_failed(expr);
120 
121  std::size_t op_width = boolbv_width(to_unary_expr(expr).op().type());
122 
123  if(op_width==0)
124  return conversion_failed(expr);
125 
126  if(expr.type().id()==ID_unsignedbv ||
127  expr.type().id()==ID_signedbv)
128  return bv_utils.build_constant(op_width/8, result_width);
129  }
130  else if(expr.id()==ID_case)
131  return convert_case(expr);
132  else if(expr.id()==ID_cond)
133  return convert_cond(to_cond_expr(expr));
134  else if(expr.id()==ID_if)
135  return convert_if(to_if_expr(expr));
136  else if(expr.id()==ID_constant)
137  return convert_constant(to_constant_expr(expr));
138  else if(expr.id()==ID_typecast)
140  else if(expr.id()==ID_symbol)
141  return convert_symbol(to_symbol_expr(expr));
142  else if(expr.id()==ID_bv_literals)
143  return convert_bv_literals(expr);
144  else if(expr.id()==ID_plus || expr.id()==ID_minus ||
145  expr.id()=="no-overflow-plus" ||
146  expr.id()=="no-overflow-minus")
147  return convert_add_sub(expr);
148  else if(expr.id() == ID_mult)
149  return convert_mult(to_mult_expr(expr));
150  else if(expr.id()==ID_div)
151  return convert_div(to_div_expr(expr));
152  else if(expr.id()==ID_mod)
153  return convert_mod(to_mod_expr(expr));
154  else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr ||
155  expr.id()==ID_rol || expr.id()==ID_ror)
156  return convert_shift(to_shift_expr(expr));
157  else if(expr.id()==ID_floatbv_plus || expr.id()==ID_floatbv_minus ||
158  expr.id()==ID_floatbv_mult || expr.id()==ID_floatbv_div ||
159  expr.id()==ID_floatbv_rem)
160  {
162  }
163  else if(expr.id()==ID_floatbv_typecast)
165  else if(expr.id()==ID_concatenation)
167  else if(expr.id()==ID_replication)
169  else if(expr.id()==ID_extractbits)
171  else if(expr.id()==ID_bitnot || expr.id()==ID_bitand ||
172  expr.id()==ID_bitor || expr.id()==ID_bitxor ||
173  expr.id()==ID_bitxnor || expr.id()==ID_bitnor ||
174  expr.id()==ID_bitnand)
175  return convert_bitwise(expr);
176  else if(expr.id() == ID_unary_minus)
178  else if(expr.id()==ID_unary_plus)
179  {
180  return convert_bitvector(to_unary_plus_expr(expr).op());
181  }
182  else if(expr.id()==ID_abs)
183  return convert_abs(to_abs_expr(expr));
184  else if(expr.id() == ID_bswap)
185  return convert_bswap(to_bswap_expr(expr));
186  else if(expr.id()==ID_byte_extract_little_endian ||
187  expr.id()==ID_byte_extract_big_endian)
189  else if(expr.id()==ID_byte_update_little_endian ||
190  expr.id()==ID_byte_update_big_endian)
192  else if(expr.id()==ID_nondet_symbol ||
193  expr.id()=="quant_symbol")
194  return convert_symbol(expr);
195  else if(expr.id()==ID_struct)
196  return convert_struct(to_struct_expr(expr));
197  else if(expr.id()==ID_union)
198  return convert_union(to_union_expr(expr));
199  else if(expr.id()==ID_string_constant)
200  return convert_bitvector(
202  else if(expr.id()==ID_array)
203  return convert_array(expr);
204  else if(expr.id()==ID_vector)
205  return convert_vector(to_vector_expr(expr));
206  else if(expr.id()==ID_complex)
207  return convert_complex(to_complex_expr(expr));
208  else if(expr.id()==ID_complex_real)
210  else if(expr.id()==ID_complex_imag)
212  else if(expr.id() == ID_array_comprehension)
214  else if(expr.id()==ID_array_of)
215  return convert_array_of(to_array_of_expr(expr));
216  else if(expr.id()==ID_let)
217  return convert_let(to_let_expr(expr));
218  else if(expr.id()==ID_function_application)
221  else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
222  expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
223  expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
224  return convert_bv_reduction(to_unary_expr(expr));
225  else if(expr.id()==ID_not)
226  return convert_not(to_not_expr(expr));
227  else if(expr.id()==ID_power)
228  return convert_power(to_binary_expr(expr));
229  else if(expr.id() == ID_popcount)
231 
232  return conversion_failed(expr);
233 }
234 
236 {
237  std::size_t width=boolbv_width(expr.type());
238 
239  if(width==0)
240  return conversion_failed(expr);
241 
242  const exprt &array_size = expr.type().size();
243 
244  const auto size = numeric_cast<mp_integer>(array_size);
245 
246  if(!size.has_value())
247  return conversion_failed(expr);
248 
249  typet counter_type = expr.arg().type();
250 
251  bvt bv;
252  bv.resize(width);
253 
254  for(mp_integer i = 0; i < *size; ++i)
255  {
256  exprt counter=from_integer(i, counter_type);
257 
258  exprt body = expr.body();
259  replace_expr(expr.arg(), counter, body);
260 
261  const bvt &tmp = convert_bv(body);
262 
263  INVARIANT(
264  *size * tmp.size() == width,
265  "total bitvector width shall equal the number of operands times the size "
266  "per operand");
267 
268  std::size_t offset = numeric_cast_v<std::size_t>(i * tmp.size());
269 
270  for(std::size_t j=0; j<tmp.size(); j++)
271  bv[offset+j]=tmp[j];
272  }
273 
274  return bv;
275 }
276 
278 {
279  std::size_t width=boolbv_width(expr.type());
280 
281  if(width==0)
282  return conversion_failed(expr);
283 
284  bvt bv;
285  bv.resize(width);
286 
287  const irept::subt &bv_sub=expr.find(ID_bv).get_sub();
288 
289  if(bv_sub.size()!=width)
290  throw "bv_literals with wrong size";
291 
292  for(std::size_t i=0; i<width; i++)
293  bv[i].set(unsafe_string2unsigned(id2string(bv_sub[i].id())));
294 
295  return bv;
296 }
297 
299 {
300  const typet &type=expr.type();
301  std::size_t width=boolbv_width(type);
302 
303  const irep_idt &identifier = expr.get(ID_identifier);
304  CHECK_RETURN(!identifier.empty());
305 
306  bvt bv = map.get_literals(identifier, type, width);
307 
309  std::all_of(
310  bv.begin(),
311  bv.end(),
312  [this](const literalt &l) {
313  return l.var_no() < prop.no_variables() || l.is_constant();
314  }),
315  "variable number of non-constant literals should be within bounds",
316  id2string(identifier));
317 
318  return bv;
319 }
320 
321 
323  const function_application_exprt &expr)
324 {
325  // record
326  functions.record(expr);
327 
328  // make it free bits
329  return prop.new_variables(boolbv_width(expr.type()));
330 }
331 
332 
334 {
335  PRECONDITION(expr.type().id() == ID_bool);
336 
337  if(expr.id()==ID_typecast)
338  return convert_typecast(to_typecast_expr(expr));
339  else if(expr.id()==ID_equal)
340  return convert_equality(to_equal_expr(expr));
341  else if(expr.id()==ID_verilog_case_equality ||
342  expr.id()==ID_verilog_case_inequality)
344  else if(expr.id()==ID_notequal)
345  {
346  const auto &notequal_expr = to_notequal_expr(expr);
347  return !convert_equality(
348  equal_exprt(notequal_expr.lhs(), notequal_expr.rhs()));
349  }
350  else if(expr.id()==ID_ieee_float_equal ||
351  expr.id()==ID_ieee_float_notequal)
352  {
354  }
355  else if(expr.id()==ID_le || expr.id()==ID_ge ||
356  expr.id()==ID_lt || expr.id()==ID_gt)
357  {
359  }
360  else if(expr.id()==ID_extractbit)
362  else if(expr.id()==ID_forall)
364  else if(expr.id()==ID_exists)
366  else if(expr.id()==ID_let)
367  {
368  bvt bv=convert_let(to_let_expr(expr));
369 
370  DATA_INVARIANT(bv.size()==1,
371  "convert_let must return 1-bit vector for boolean let");
372 
373  return bv[0];
374  }
375  else if(expr.id()==ID_index)
376  {
377  bvt bv=convert_index(to_index_expr(expr));
378  CHECK_RETURN(bv.size() == 1);
379  return bv[0];
380  }
381  else if(expr.id()==ID_member)
382  {
384  CHECK_RETURN(bv.size() == 1);
385  return bv[0];
386  }
387  else if(expr.id()==ID_case)
388  {
389  bvt bv=convert_case(expr);
390  CHECK_RETURN(bv.size() == 1);
391  return bv[0];
392  }
393  else if(expr.id()==ID_cond)
394  {
395  bvt bv = convert_cond(to_cond_expr(expr));
396  CHECK_RETURN(bv.size() == 1);
397  return bv[0];
398  }
399  else if(expr.id()==ID_sign)
400  {
401  const auto &op = to_sign_expr(expr).op();
402  const bvt &bv = convert_bv(op);
403  CHECK_RETURN(!bv.empty());
404  const irep_idt type_id = op.type().id();
405  if(type_id == ID_signedbv || type_id == ID_fixedbv || type_id == ID_floatbv)
406  return bv[bv.size()-1];
407  if(type_id == ID_unsignedbv)
408  return const_literal(false);
409  }
410  else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
411  expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
412  expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
413  return convert_reduction(to_unary_expr(expr));
414  else if(expr.id()==ID_onehot || expr.id()==ID_onehot0)
415  return convert_onehot(to_unary_expr(expr));
416  else if(has_prefix(expr.id_string(), "overflow-"))
417  return convert_overflow(expr);
418  else if(expr.id()==ID_isnan)
419  {
420  const auto &op = to_unary_expr(expr).op();
421  const bvt &bv = convert_bv(op);
422 
423  if(op.type().id() == ID_floatbv)
424  {
425  float_utilst float_utils(prop, to_floatbv_type(op.type()));
426  return float_utils.is_NaN(bv);
427  }
428  else if(op.type().id() == ID_fixedbv)
429  return const_literal(false);
430  }
431  else if(expr.id()==ID_isfinite)
432  {
433  const auto &op = to_unary_expr(expr).op();
434  const bvt &bv = convert_bv(op);
435 
436  if(op.type().id() == ID_floatbv)
437  {
438  float_utilst float_utils(prop, to_floatbv_type(op.type()));
439  return prop.land(
440  !float_utils.is_infinity(bv),
441  !float_utils.is_NaN(bv));
442  }
443  else if(op.id() == ID_fixedbv)
444  return const_literal(true);
445  }
446  else if(expr.id()==ID_isinf)
447  {
448  const auto &op = to_unary_expr(expr).op();
449  const bvt &bv = convert_bv(op);
450 
451  if(op.type().id() == ID_floatbv)
452  {
453  float_utilst float_utils(prop, to_floatbv_type(op.type()));
454  return float_utils.is_infinity(bv);
455  }
456  else if(op.type().id() == ID_fixedbv)
457  return const_literal(false);
458  }
459  else if(expr.id()==ID_isnormal)
460  {
461  const auto &op = to_unary_expr(expr).op();
462 
463  if(op.type().id() == ID_floatbv)
464  {
465  const bvt &bv = convert_bv(op);
466  float_utilst float_utils(prop, to_floatbv_type(op.type()));
467  return float_utils.is_normal(bv);
468  }
469  else if(op.type().id() == ID_fixedbv)
470  return const_literal(true);
471  }
472  else if(expr.id() == ID_function_application)
473  {
475  return prop.new_variable();
476  }
477 
478  return SUB::convert_rest(expr);
479 }
480 
482 {
484  return true;
485 
486  const typet &type = expr.lhs().type();
487 
488  if(
489  expr.lhs().id() == ID_symbol && type == expr.rhs().type() &&
490  type.id() != ID_bool)
491  {
492  // see if it is an unbounded array
493  if(is_unbounded_array(type))
494  return true;
495 
496  const bvt &bv1=convert_bv(expr.rhs());
497 
498  const irep_idt &identifier=
500 
501  map.set_literals(identifier, type, bv1);
502 
503  if(freeze_all)
504  set_frozen(bv1);
505 
506  return false;
507  }
508 
509  return true;
510 }
511 
512 void boolbvt::set_to(const exprt &expr, bool value)
513 {
514  PRECONDITION(expr.type().id() == ID_bool);
515 
516  const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr);
517  if(value && equal_expr && !boolbv_set_equality_to_true(*equal_expr))
518  return;
519  SUB::set_to(expr, value);
520 }
521 
522 exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv)
523 {
524  exprt dest(ID_bv_literals, type);
525  irept::subt &bv_sub=dest.add(ID_bv).get_sub();
526  bv_sub.resize(bv.size());
527 
528  for(std::size_t i=0; i<bv.size(); i++)
529  bv_sub[i].id(std::to_string(bv[i].get()));
530  return dest;
531 }
532 
534 {
535  const std::size_t width = boolbv_width(type);
536  PRECONDITION(width != 0);
537  bvt bv(width);
538  for(auto &lit : bv)
539  lit = prop.new_variable();
540  return make_bv_expr(type, bv);
541 }
542 
543 bool boolbvt::is_unbounded_array(const typet &type) const
544 {
545  if(type.id()!=ID_array)
546  return false;
547 
549  return true;
550 
551  const exprt &size=to_array_type(type).size();
552 
553  const auto s = numeric_cast<mp_integer>(size);
554  if(!s.has_value())
555  return true;
556 
558  if(*s > MAX_FLATTENED_ARRAY_SIZE)
559  return true;
560 
561  return false;
562 }
563 
564 void boolbvt::print_assignment(std::ostream &out) const
565 {
567  map.show(out);
568 }
569 
571 {
572  const struct_typet::componentst &components = src.components();
573  offset_mapt dest;
574  dest.reserve(components.size());
575  std::size_t offset = 0;
576  for(const auto &comp : components)
577  {
578  dest.push_back(offset);
579  offset += boolbv_width(comp.type());
580  }
581  return dest;
582 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3025
const exprt & body() const
Definition: std_expr.h:3059
const array_typet & type() const
Definition: std_expr.h:3039
const symbol_exprt & arg() const
Definition: std_expr.h:3049
const exprt & size() const
Definition: std_types.h:976
const namespacet & ns
Definition: arrays.h:54
exprt & lhs()
Definition: std_expr.h:581
exprt & rhs()
Definition: std_expr.h:591
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:75
void show(std::ostream &out) const
Definition: boolbv_map.cpp:35
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
Definition: boolbv_map.cpp:41
virtual bvt convert_bv_literals(const exprt &expr)
Definition: boolbv.cpp:277
virtual bvt convert_with(const with_exprt &expr)
Definition: boolbv_with.cpp:16
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:132
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 bvt convert_constraint_select_one(const exprt &expr)
virtual exprt make_free_bv_expr(const typet &type)
Definition: boolbv.cpp:533
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 &)
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 &)
Definition: boolbv_let.cpp:15
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
offset_mapt build_offset_map(const struct_typet &src)
Definition: boolbv.cpp:570
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:91
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:543
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:38
virtual bvt convert_mod(const mod_exprt &expr)
Definition: boolbv_mod.cpp:12
virtual bvt convert_add_sub(const exprt &expr)
virtual bvt convert_constant(const constant_exprt &expr)
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:124
virtual literalt convert_quantifier(const quantifier_exprt &expr)
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
Definition: boolbv.cpp:481
virtual bvt convert_mult(const mult_exprt &expr)
Definition: boolbv_mult.cpp:13
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:322
virtual bvt convert_cond(const cond_exprt &)
Definition: boolbv_cond.cpp:13
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:512
virtual bvt convert_byte_update(const byte_update_exprt &expr)
virtual literalt convert_extractbit(const extractbit_exprt &expr)
unbounded_arrayt unbounded_array
Definition: boolbv.h:82
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: boolbv_get.cpp:20
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:564
virtual bvt convert_not(const not_exprt &expr)
Definition: boolbv_not.cpp:12
virtual bvt convert_extractbits(const extractbits_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
virtual bvt convert_update(const update_exprt &)
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
virtual bvt convert_div(const div_exprt &expr)
Definition: boolbv_div.cpp:13
virtual bvt convert_array_of(const array_of_exprt &expr)
Flatten arrays constructed from a single element.
bv_utilst bv_utils
Definition: boolbv.h:109
virtual bvt convert_bitwise(const exprt &expr)
virtual bvt convert_array_comprehension(const array_comprehension_exprt &)
Definition: boolbv.cpp:235
virtual bvt convert_bv_reduction(const unary_exprt &expr)
virtual literalt convert_equality(const equal_exprt &expr)
functionst functions
Definition: boolbv.h:112
virtual bvt convert_vector(const vector_exprt &expr)
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:96
virtual bvt convert_case(const exprt &expr)
Definition: boolbv_case.cpp:13
virtual exprt make_bv_expr(const typet &type, const bvt &bv)
Definition: boolbv.cpp:522
virtual bvt convert_symbol(const exprt &expr)
Definition: boolbv.cpp:298
virtual literalt convert_overflow(const exprt &expr)
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
virtual bvt convert_power(const binary_exprt &expr)
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
virtual bvt convert_concatenation(const concatenation_exprt &expr)
virtual bvt convert_struct(const struct_exprt &expr)
virtual bvt convert_replication(const replication_exprt &expr)
literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:333
std::vector< std::size_t > offset_mapt
Definition: boolbv.h:271
virtual bvt convert_abs(const abs_exprt &expr)
Definition: boolbv_abs.cpp:17
boolbv_mapt map
Definition: boolbv.h:115
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:13
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Equality.
Definition: std_expr.h:1140
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:179
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:96
literalt is_NaN(const bvt &)
literalt is_infinity(const bvt &)
literalt is_normal(const bvt &)
Application of (mathematical) function.
void record(const function_application_exprt &function_application)
Definition: functions.cpp:14
subt & get_sub()
Definition: irep.h:466
irept & add(const irep_namet &name)
Definition: irep.cpp:113
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
const std::string & id_string() const
Definition: irep.h:410
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
static var_not unused_var_no()
Definition: literal.h:176
void set_frozen(literalt)
virtual void ignoring(const exprt &expr)
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
virtual literalt convert_rest(const exprt &expr)
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'current_context => expr' if value is true,...
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
virtual literalt land(literalt a, literalt b)=0
virtual void set_frozen(literalt)
Definition: prop.h:114
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
virtual literalt new_variable()=0
Structure type, corresponds to C style structs.
Definition: std_types.h:226
const componentst & components() const
Definition: std_types.h:142
std::vector< componentt > componentst
Definition: std_types.h:135
const irep_idt & get_identifier() const
Definition: std_expr.h:110
The type of an expression, extends irept.
Definition: type.h:28
const exprt & op() const
Definition: std_expr.h:294
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
Definition: popcount.cpp:17
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: floatbv_expr.h:425
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: floatbv_expr.h:68
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
std::vector< literalt > bvt
Definition: literal.h:201
literalt const_literal(bool value)
Definition: literal.h:188
Magic numbers used throughout the codebase.
const std::size_t MAX_FLATTENED_ARRAY_SIZE
Definition: magic.h:11
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
BigInt mp_integer
Definition: mp_arith.h:19
nonstd::optional< T > optionalt
Definition: optional.h:35
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition: invariant.h:438
API to expression classes.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1223
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2422
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:2940
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:465
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1075
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1412
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:3088
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1716
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2067
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1563
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:421
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1030
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1501
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2235
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1606
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1362
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1180
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1671
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:329
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1761
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:532
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:371
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:724
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:961
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:2999
Pre-defined types.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1431
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:38
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Symbol table entry.