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 <cassert>
12 #include <map>
13 #include <set>
14 
15 #include <util/arith_tools.h>
16 #include <util/magic.h>
17 #include <util/mp_arith.h>
18 #include <util/prefix.h>
19 #include <util/replace_expr.h>
20 #include <util/std_expr.h>
21 #include <util/std_types.h>
22 #include <util/string2int.h>
23 #include <util/string_constant.h>
24 #include <util/symbol.h>
25 #include <util/threeval.h>
26 
27 #include "boolbv_type.h"
28 
31 
33  const exprt &expr,
34  const std::size_t bit,
35  literalt &dest) const
36 {
37  if(expr.type().id()==ID_bool)
38  {
39  assert(bit==0);
40  return prop_conv_solvert::literal(expr, dest);
41  }
42  else
43  {
44  if(expr.id()==ID_symbol ||
45  expr.id()==ID_nondet_symbol)
46  {
47  const irep_idt &identifier=expr.get(ID_identifier);
48 
49  boolbv_mapt::mappingt::const_iterator it_m=
50  map.mapping.find(identifier);
51 
52  if(it_m==map.mapping.end())
53  return true;
54 
55  const boolbv_mapt::map_entryt &map_entry=it_m->second;
56 
57  assert(bit<map_entry.literal_map.size());
58  if(!map_entry.literal_map[bit].is_set)
59  return true;
60 
61  dest=map_entry.literal_map[bit].l;
62  return false;
63  }
64  else if(expr.id()==ID_index)
65  {
66  const index_exprt &index_expr=to_index_expr(expr);
67 
68  std::size_t element_width=boolbv_width(index_expr.type());
69 
70  if(element_width==0)
71  throw "literal expects a bit-vector type";
72 
73  mp_integer index;
74  if(to_integer(index_expr.index(), index))
75  throw "literal expects constant index";
76 
77  std::size_t offset=integer2unsigned(index*element_width);
78 
79  return literal(index_expr.array(), bit+offset, dest);
80  }
81  else if(expr.id()==ID_member)
82  {
83  const member_exprt &member_expr=to_member_expr(expr);
84 
85  const struct_typet::componentst &components=
86  to_struct_type(expr.type()).components();
87  const irep_idt &component_name=member_expr.get_component_name();
88 
89  std::size_t offset=0;
90 
91  for(struct_typet::componentst::const_iterator
92  it=components.begin();
93  it!=components.end();
94  it++)
95  {
96  const typet &subtype=it->type();
97 
98  if(it->get_name()==component_name)
99  return literal(expr.op0(), bit+offset, dest);
100 
101  std::size_t element_width=boolbv_width(subtype);
102 
103  if(element_width==0)
104  throw "literal expects a bit-vector type";
105 
106  offset+=element_width;
107  }
108 
109  throw "failed to find component";
110  }
111  }
112 
113  throw "found no literal for expression";
114 }
115 
116 const bvt &boolbvt::convert_bv(const exprt &expr)
117 {
118  // check cache first
119  std::pair<bv_cachet::iterator, bool> cache_result=
120  bv_cache.insert(std::make_pair(expr, bvt()));
121  if(!cache_result.second)
122  {
123  return cache_result.first->second;
124  }
125 
126  // Iterators into hash_maps supposedly stay stable
127  // even though we are inserting more elements recursively.
128 
129  cache_result.first->second=convert_bitvector(expr);
130 
131  // check
132  forall_literals(it, cache_result.first->second)
133  {
134  if(freeze_all && !it->is_constant())
135  prop.set_frozen(*it);
136  if(it->var_no()==literalt::unused_var_no())
137  {
138  error() << "unused_var_no: " << expr.pretty() << eom;
139  assert(false);
140  }
141  }
142 
143  return cache_result.first->second;
144 }
145 
147 {
148  ignoring(expr);
149 
150  // try to make it free bits
151  std::size_t width=boolbv_width(expr.type());
152  return prop.new_variables(width);
153 }
154 
164 {
165  if(expr.type().id()==ID_bool)
166  {
167  bvt bv;
168  bv.resize(1);
169  bv[0]=convert(expr);
170  return bv;
171  }
172 
173  if(expr.id()==ID_index)
174  return convert_index(to_index_expr(expr));
175  else if(expr.id()==ID_constraint_select_one)
176  return convert_constraint_select_one(expr);
177  else if(expr.id()==ID_member)
178  return convert_member(to_member_expr(expr));
179  else if(expr.id()==ID_with)
180  return convert_with(expr);
181  else if(expr.id()==ID_update)
182  return convert_update(expr);
183  else if(expr.id()==ID_width)
184  {
185  std::size_t result_width=boolbv_width(expr.type());
186 
187  if(result_width==0)
188  return conversion_failed(expr);
189 
190  if(expr.operands().size()!=1)
191  return conversion_failed(expr);
192 
193  std::size_t op_width=boolbv_width(expr.op0().type());
194 
195  if(op_width==0)
196  return conversion_failed(expr);
197 
198  if(expr.type().id()==ID_unsignedbv ||
199  expr.type().id()==ID_signedbv)
200  return bv_utils.build_constant(op_width/8, result_width);
201  }
202  else if(expr.id()==ID_case)
203  return convert_case(expr);
204  else if(expr.id()==ID_cond)
205  return convert_cond(expr);
206  else if(expr.id()==ID_if)
207  return convert_if(to_if_expr(expr));
208  else if(expr.id()==ID_constant)
209  return convert_constant(to_constant_expr(expr));
210  else if(expr.id()==ID_typecast)
212  else if(expr.id()==ID_symbol)
213  return convert_symbol(to_symbol_expr(expr));
214  else if(expr.id()==ID_bv_literals)
215  return convert_bv_literals(expr);
216  else if(expr.id()==ID_plus || expr.id()==ID_minus ||
217  expr.id()=="no-overflow-plus" ||
218  expr.id()=="no-overflow-minus")
219  return convert_add_sub(expr);
220  else if(expr.id()==ID_mult ||
221  expr.id()=="no-overflow-mult")
222  return convert_mult(expr);
223  else if(expr.id()==ID_div)
224  return convert_div(to_div_expr(expr));
225  else if(expr.id()==ID_mod)
226  return convert_mod(to_mod_expr(expr));
227  else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr ||
228  expr.id()==ID_rol || expr.id()==ID_ror)
229  return convert_shift(to_shift_expr(expr));
230  else if(expr.id()==ID_floatbv_plus || expr.id()==ID_floatbv_minus ||
231  expr.id()==ID_floatbv_mult || expr.id()==ID_floatbv_div ||
232  expr.id()==ID_floatbv_rem)
233  return convert_floatbv_op(expr);
234  else if(expr.id()==ID_floatbv_typecast)
236  else if(expr.id()==ID_concatenation)
237  return convert_concatenation(expr);
238  else if(expr.id()==ID_replication)
240  else if(expr.id()==ID_extractbits)
242  else if(expr.id()==ID_bitnot || expr.id()==ID_bitand ||
243  expr.id()==ID_bitor || expr.id()==ID_bitxor ||
244  expr.id()==ID_bitxnor || expr.id()==ID_bitnor ||
245  expr.id()==ID_bitnand)
246  return convert_bitwise(expr);
247  else if(expr.id()==ID_unary_minus ||
248  expr.id()=="no-overflow-unary-minus")
249  return convert_unary_minus(to_unary_expr(expr));
250  else if(expr.id()==ID_unary_plus)
251  {
252  assert(expr.operands().size()==1);
253  return convert_bitvector(expr.op0());
254  }
255  else if(expr.id()==ID_abs)
256  return convert_abs(to_abs_expr(expr));
257  else if(expr.id() == ID_bswap)
258  return convert_bswap(to_bswap_expr(expr));
259  else if(expr.id()==ID_byte_extract_little_endian ||
260  expr.id()==ID_byte_extract_big_endian)
262  else if(expr.id()==ID_byte_update_little_endian ||
263  expr.id()==ID_byte_update_big_endian)
265  else if(expr.id()==ID_nondet_symbol ||
266  expr.id()=="quant_symbol")
267  return convert_symbol(expr);
268  else if(expr.id()==ID_struct)
269  return convert_struct(to_struct_expr(expr));
270  else if(expr.id()==ID_union)
271  return convert_union(to_union_expr(expr));
272  else if(expr.id()==ID_string_constant)
273  return convert_bitvector(
275  else if(expr.id()==ID_array)
276  return convert_array(expr);
277  else if(expr.id()==ID_vector)
278  return convert_vector(expr);
279  else if(expr.id()==ID_complex)
280  return convert_complex(expr);
281  else if(expr.id()==ID_complex_real)
282  return convert_complex_real(expr);
283  else if(expr.id()==ID_complex_imag)
284  return convert_complex_imag(expr);
285  else if(expr.id()==ID_lambda)
286  return convert_lambda(expr);
287  else if(expr.id()==ID_array_of)
288  return convert_array_of(to_array_of_expr(expr));
289  else if(expr.id()==ID_let)
290  return convert_let(to_let_expr(expr));
291  else if(expr.id()==ID_function_application)
294  else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
295  expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
296  expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
297  return convert_bv_reduction(to_unary_expr(expr));
298  else if(expr.id()==ID_not)
299  return convert_not(to_not_expr(expr));
300  else if(expr.id()==ID_power)
301  return convert_power(to_binary_expr(expr));
302  else if(expr.id()==ID_float_debug1 ||
303  expr.id()==ID_float_debug2)
304  {
305  assert(expr.operands().size()==2);
306  bvt bv0=convert_bitvector(expr.op0());
307  bvt bv1=convert_bitvector(expr.op1());
308  float_utilst float_utils(prop, to_floatbv_type(expr.type()));
309  bvt bv=expr.id()==ID_float_debug1?
310  float_utils.debug1(bv0, bv1):
311  float_utils.debug2(bv0, bv1);
312  return bv;
313  }
314  else if(expr.id() == ID_popcount)
316 
317  return conversion_failed(expr);
318 }
319 
321 {
322  std::size_t width=boolbv_width(expr.type());
323 
324  if(width==0)
325  return conversion_failed(expr);
326 
327  if(expr.operands().size()!=2)
328  throw "lambda takes two operands";
329 
330  if(expr.type().id()!=ID_array)
331  return conversion_failed(expr);
332 
333  const exprt &array_size=
334  to_array_type(expr.type()).size();
335 
336  mp_integer size;
337 
338  if(to_integer(array_size, size))
339  return conversion_failed(expr);
340 
341  typet counter_type=expr.op0().type();
342 
343  bvt bv;
344  bv.resize(width);
345 
346  for(mp_integer i=0; i<size; ++i)
347  {
348  exprt counter=from_integer(i, counter_type);
349 
350  exprt expr_op1(expr.op1());
351  replace_expr(expr.op0(), counter, expr_op1);
352 
353  const bvt &tmp=convert_bv(expr_op1);
354 
355  std::size_t offset=integer2unsigned(i*tmp.size());
356 
357  if(size*tmp.size()!=width)
358  throw "convert_lambda: unexpected operand width";
359 
360  for(std::size_t j=0; j<tmp.size(); j++)
361  bv[offset+j]=tmp[j];
362  }
363 
364  return bv;
365 }
366 
368 {
369  std::size_t width=boolbv_width(expr.type());
370 
371  if(width==0)
372  return conversion_failed(expr);
373 
374  bvt bv;
375  bv.resize(width);
376 
377  const irept::subt &bv_sub=expr.find(ID_bv).get_sub();
378 
379  if(bv_sub.size()!=width)
380  throw "bv_literals with wrong size";
381 
382  for(std::size_t i=0; i<width; i++)
383  bv[i].set(unsafe_string2int(id2string(bv_sub[i].id())));
384 
385  return bv;
386 }
387 
389 {
390  const typet &type=expr.type();
391  std::size_t width=boolbv_width(type);
392 
393  bvt bv;
394  bv.resize(width);
395 
396  const irep_idt &identifier=expr.get(ID_identifier);
397 
398  if(identifier.empty())
399  throw "convert_symbol got empty identifier";
400 
401  if(width==0)
402  {
403  // just put in map
404  map.get_map_entry(identifier, type);
405  }
406  else
407  {
408  map.get_literals(identifier, type, width, bv);
409 
410  forall_literals(it, bv)
411  if(it->var_no()>=prop.no_variables() &&
412  !it->is_constant())
413  {
414  error() << identifier << eom;
415  assert(false);
416  }
417  }
418 
419  return bv;
420 }
421 
422 
424  const function_application_exprt &expr)
425 {
426  // record
427  functions.record(expr);
428 
429  // make it free bits
430  return prop.new_variables(boolbv_width(expr.type()));
431 }
432 
433 
435 {
436  PRECONDITION(expr.type().id() == ID_bool);
437  const exprt::operandst &operands=expr.operands();
438 
439  if(expr.id()==ID_typecast)
440  return convert_typecast(to_typecast_expr(expr));
441  else if(expr.id()==ID_equal)
442  return convert_equality(to_equal_expr(expr));
443  else if(expr.id()==ID_verilog_case_equality ||
444  expr.id()==ID_verilog_case_inequality)
446  else if(expr.id()==ID_notequal)
447  {
448  DATA_INVARIANT(expr.operands().size() == 2, "notequal expects two operands");
449  return !convert_equality(equal_exprt(expr.op0(), expr.op1()));
450  }
451  else if(expr.id()==ID_ieee_float_equal ||
452  expr.id()==ID_ieee_float_notequal)
453  return convert_ieee_float_rel(expr);
454  else if(expr.id()==ID_le || expr.id()==ID_ge ||
455  expr.id()==ID_lt || expr.id()==ID_gt)
456  return convert_bv_rel(expr);
457  else if(expr.id()==ID_extractbit)
459  else if(expr.id()==ID_forall)
460  return convert_quantifier(expr);
461  else if(expr.id()==ID_exists)
462  return convert_quantifier(expr);
463  else if(expr.id()==ID_let)
464  {
465  bvt bv=convert_let(to_let_expr(expr));
466 
467  DATA_INVARIANT(bv.size()==1,
468  "convert_let must return 1-bit vector for boolean let");
469 
470  return bv[0];
471  }
472  else if(expr.id()==ID_index)
473  {
474  bvt bv=convert_index(to_index_expr(expr));
475  CHECK_RETURN(bv.size() == 1);
476  return bv[0];
477  }
478  else if(expr.id()==ID_member)
479  {
481  CHECK_RETURN(bv.size() == 1);
482  return bv[0];
483  }
484  else if(expr.id()==ID_case)
485  {
486  bvt bv=convert_case(expr);
487  CHECK_RETURN(bv.size() == 1);
488  return bv[0];
489  }
490  else if(expr.id()==ID_cond)
491  {
492  bvt bv=convert_cond(expr);
493  CHECK_RETURN(bv.size() == 1);
494  return bv[0];
495  }
496  else if(expr.id()==ID_sign)
497  {
498  DATA_INVARIANT(expr.operands().size() == 1, "sign expects one operand");
499  const bvt &bv=convert_bv(operands[0]);
500  CHECK_RETURN(!bv.empty());
501  const irep_idt type_id = operands[0].type().id();
502  if(type_id == ID_signedbv || type_id == ID_fixedbv || type_id == ID_floatbv)
503  return bv[bv.size()-1];
504  if(type_id == ID_unsignedbv)
505  return const_literal(false);
506  }
507  else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
508  expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
509  expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
510  return convert_reduction(to_unary_expr(expr));
511  else if(expr.id()==ID_onehot || expr.id()==ID_onehot0)
512  return convert_onehot(to_unary_expr(expr));
513  else if(has_prefix(expr.id_string(), "overflow-"))
514  return convert_overflow(expr);
515  else if(expr.id()==ID_isnan)
516  {
517  DATA_INVARIANT(expr.operands().size() == 1, "isnan expects one operand");
518  const bvt &bv=convert_bv(operands[0]);
519 
520  if(expr.op0().type().id()==ID_floatbv)
521  {
522  float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
523  return float_utils.is_NaN(bv);
524  }
525  else if(expr.op0().type().id() == ID_fixedbv)
526  return const_literal(false);
527  }
528  else if(expr.id()==ID_isfinite)
529  {
530  DATA_INVARIANT(expr.operands().size() == 1, "isfinite expects one operand");
531  const bvt &bv=convert_bv(operands[0]);
532  if(expr.op0().type().id()==ID_floatbv)
533  {
534  float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
535  return prop.land(
536  !float_utils.is_infinity(bv),
537  !float_utils.is_NaN(bv));
538  }
539  else if(expr.op0().type().id() == ID_fixedbv)
540  return const_literal(true);
541  }
542  else if(expr.id()==ID_isinf)
543  {
544  DATA_INVARIANT(expr.operands().size() == 1, "isinf expects one operand");
545  const bvt &bv=convert_bv(operands[0]);
546  if(expr.op0().type().id()==ID_floatbv)
547  {
548  float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
549  return float_utils.is_infinity(bv);
550  }
551  else if(expr.op0().type().id() == ID_fixedbv)
552  return const_literal(false);
553  }
554  else if(expr.id()==ID_isnormal)
555  {
556  DATA_INVARIANT(expr.operands().size() == 1, "isnormal expects one operand");
557  if(expr.op0().type().id()==ID_floatbv)
558  {
559  const bvt &bv = convert_bv(operands[0]);
560  float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
561  return float_utils.is_normal(bv);
562  }
563  else if(expr.op0().type().id() == ID_fixedbv)
564  return const_literal(true);
565  }
566 
567  return SUB::convert_rest(expr);
568 }
569 
571 {
573  return true;
574 
575  const typet &type=ns.follow(expr.lhs().type());
576 
577  if(expr.lhs().id()==ID_symbol &&
578  type==ns.follow(expr.rhs().type()) &&
579  type.id()!=ID_bool)
580  {
581  // see if it is an unbounded array
582  if(is_unbounded_array(type))
583  return true;
584 
585  const bvt &bv1=convert_bv(expr.rhs());
586 
587  const irep_idt &identifier=
588  to_symbol_expr(expr.lhs()).get_identifier();
589 
590  map.set_literals(identifier, type, bv1);
591 
592  if(freeze_all)
593  set_frozen(bv1);
594 
595  return false;
596  }
597 
598  return true;
599 }
600 
601 void boolbvt::set_to(const exprt &expr, bool value)
602 {
603  PRECONDITION(expr.type().id() == ID_bool);
604 
605  const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr);
606  if(value && equal_expr && !boolbv_set_equality_to_true(*equal_expr))
607  return;
608  SUB::set_to(expr, value);
609 }
610 
611 exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv)
612 {
613  exprt dest(ID_bv_literals, type);
614  irept::subt &bv_sub=dest.add(ID_bv).get_sub();
615  bv_sub.resize(bv.size());
616 
617  for(std::size_t i=0; i<bv.size(); i++)
618  bv_sub[i].id(std::to_string(bv[i].get()));
619  return dest;
620 }
621 
623 {
624  const std::size_t width = boolbv_width(type);
625  PRECONDITION(width != 0);
626  bvt bv(width);
627  for(auto &lit : bv)
628  lit = prop.new_variable();
629  return make_bv_expr(type, bv);
630 }
631 
632 bool boolbvt::is_unbounded_array(const typet &type) const
633 {
634  if(type.id()==ID_symbol)
635  return is_unbounded_array(ns.follow(type));
636 
637  if(type.id()!=ID_array)
638  return false;
639 
641  return true;
642 
643  const exprt &size=to_array_type(type).size();
644 
645  mp_integer s;
646  if(to_integer(size, s))
647  return true;
648 
651  return true;
652 
653  return false;
654 }
655 
656 void boolbvt::print_assignment(std::ostream &out) const
657 {
659  for(const auto &pair : map.mapping)
660  out << pair.first << "=" << pair.second.get_value(prop) << '\n';
661 }
662 
664 {
665  const struct_typet::componentst &components = src.components();
666  offset_mapt dest;
667  dest.reserve(components.size());
668  std::size_t offset = 0;
669  for(const auto &comp : components)
670  {
671  dest.push_back(offset);
672  offset += boolbv_width(comp.type());
673  }
674  return dest;
675 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
virtual bvt convert_case(const exprt &expr)
Definition: boolbv_case.cpp:13
virtual bvt convert_complex_real(const exprt &expr)
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:49
The type of an expression.
Definition: type.h:22
void print_assignment(std::ostream &out) const override
Definition: boolbv.cpp:656
std::vector< std::size_t > offset_mapt
Definition: boolbv.h:252
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
virtual bvt convert_with(const exprt &expr)
Definition: boolbv_with.cpp:19
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast a generic exprt to a bswap_exprt.
Definition: std_expr.h:542
virtual bvt convert_concatenation(const exprt &expr)
bv_utilst bv_utils
Definition: boolbv.h:93
virtual literalt convert_ieee_float_rel(const exprt &expr)
BigInt mp_integer
Definition: mp_arith.h:22
virtual bvt convert_array_of(const array_of_exprt &expr)
virtual bvt convert_bv_reduction(const unary_exprt &expr)
literal_mapt literal_map
Definition: boolbv_map.h:53
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
application of (mathematical) function
Definition: std_expr.h:4531
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:162
Symbol table entry.
virtual void set_frozen(literalt a)
Definition: prop.h:111
const mod_exprt & to_mod_expr(const exprt &expr)
Cast a generic exprt to a mod_exprt.
Definition: std_expr.h:1158
bool equality_propagation
Definition: prop_conv.h:112
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
const div_exprt & to_div_expr(const exprt &expr)
Cast a generic exprt to a div_exprt.
Definition: std_expr.h:1100
std::vector< irept > subt
Definition: irep.h:90
virtual literalt convert_onehot(const unary_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
virtual literalt convert_overflow(const exprt &expr)
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:39
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:632
virtual bvt convert_replication(const replication_exprt &expr)
static var_not unused_var_no()
Definition: literal.h:175
virtual bvt convert_bv_literals(const exprt &expr)
Definition: boolbv.cpp:367
std::vector< componentt > componentst
Definition: std_types.h:243
virtual bvt convert_struct(const struct_exprt &expr)
const componentst & components() const
Definition: std_types.h:245
virtual bvt convert_function_application(const function_application_exprt &expr)
Definition: boolbv.cpp:423
virtual bvt convert_lambda(const exprt &expr)
Definition: boolbv.cpp:320
typet & type()
Definition: expr.h:56
Magic numbers used throughout the codebase.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Structure type.
Definition: std_types.h:297
void set_to(const exprt &expr, bool value) override
Definition: prop_conv.cpp:365
virtual bool literal(const exprt &expr, literalt &literal) const
Definition: prop_conv.cpp:36
virtual bvt convert_constant(const constant_exprt &expr)
#define forall_literals(it, bv)
Definition: literal.h:202
virtual bvt convert_symbol(const exprt &expr)
Definition: boolbv.cpp:388
const let_exprt & to_let_expr(const exprt &expr)
Cast a generic exprt to a let_exprt.
Definition: std_expr.h:4755
subt & get_sub()
Definition: irep.h:245
virtual bvt convert_mult(const exprt &expr)
Definition: boolbv_mult.cpp:13
Extract member of struct or union.
Definition: std_expr.h:3871
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
equality
Definition: std_expr.h:1354
virtual bvt convert_complex(const exprt &expr)
virtual literalt convert_quantifier(const exprt &expr)
virtual bvt convert_update(const exprt &expr)
literalt is_normal(const bvt &)
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
Definition: irep.h:189
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
virtual bvt convert_abs(const abs_exprt &expr)
Definition: boolbv_abs.cpp:17
void print_assignment(std::ostream &out) const override
Definition: prop_conv.cpp:509
virtual literalt new_variable()=0
virtual literalt convert_bv_rel(const exprt &expr)
mappingt mapping
Definition: boolbv_map.h:59
virtual bvt convert_add_sub(const exprt &expr)
const replication_exprt & to_replication_expr(const exprt &expr)
Cast a generic exprt to a replication_exprt.
Definition: std_expr.h:2958
virtual literalt convert_reduction(const unary_exprt &expr)
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast a generic exprt to an extractbit_exprt.
Definition: std_expr.h:3039
virtual bvt convert_bswap(const bswap_exprt &expr)
functionst functions
Definition: boolbv.h:96
virtual size_t no_variables() const =0
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:121
offset_mapt build_offset_map(const struct_typet &src)
Definition: boolbv.cpp:663
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast a generic exprt to an array_of_exprt.
Definition: std_expr.h:1584
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:163
API to expression classes.
virtual bvt convert_floatbv_op(const exprt &expr)
exprt & op1()
Definition: expr.h:75
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast a generic exprt to a function_application_exprt.
Definition: std_expr.h:4585
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
mstreamt & error() const
Definition: message.h:302
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast a generic exprt to an extractbits_exprt.
Definition: std_expr.h:3137
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast a generic exprt to a binary_relation_exprt.
Definition: std_expr.h:803
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
Definition: boolbv.cpp:570
virtual bool literal(const exprt &expr, std::size_t bit, literalt &literal) const
Definition: boolbv.cpp:32
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const exprt & size() const
Definition: std_types.h:1014
const namespacet & ns
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
virtual bvt convert_union(const union_exprt &expr)
array_exprt to_array_expr() const
convert string into array constant
const typet & follow(const typet &) const
Definition: namespace.cpp:55
virtual bvt convert_extractbits(const extractbits_exprt &expr)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
Definition: std_expr.h:1838
literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:434
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4465
virtual bvt convert_complex_imag(const exprt &expr)
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast a generic exprt to a floatbv_typecast_exprt.
Definition: std_expr.h:2221
virtual bvt convert_let(const let_exprt &)
Definition: boolbv_let.cpp:14
virtual bvt convert_cond(const exprt &expr)
Definition: boolbv_cond.cpp:13
std::vector< exprt > operandst
Definition: expr.h:45
virtual bvt convert_not(const not_exprt &expr)
Definition: boolbv_not.cpp:12
literalt is_infinity(const bvt &)
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:202
virtual bvt convert_byte_update(const byte_update_exprt &expr)
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
literalt const_literal(bool value)
Definition: literal.h:187
literalt is_NaN(const bvt &)
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
Definition: popcount.cpp:16
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast a generic exprt to a popcount_exprt.
Definition: std_expr.h:4918
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
Definition: std_expr.h:1377
virtual exprt make_free_bv_expr(const typet &type)
Definition: boolbv.cpp:622
API to type classes.
virtual bvt convert_constraint_select_one(const exprt &expr)
void record(const function_application_exprt &function_application)
Definition: functions.cpp:16
unbounded_arrayt unbounded_array
Definition: boolbv.h:76
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
Definition: std_expr.h:2818
exprt & index()
Definition: std_expr.h:1496
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1373
virtual bvt convert_vector(const exprt &expr)
const string_constantt & to_string_constant(const exprt &expr)
virtual bvt convert_array(const exprt &expr)
bv_cachet bv_cache
Definition: boolbv.h:116
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
Definition: std_expr.h:1782
std::string to_string(const string_constraintt &expr)
Used for debug printing.
virtual bvt convert_mod(const mod_exprt &expr)
Definition: boolbv_mod.cpp:12
irep_idt get_component_name() const
Definition: std_expr.h:3895
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
Definition: std_expr.h:3254
irept & add(const irep_namet &name)
Definition: irep.cpp:306
virtual bvt convert_member(const member_exprt &expr)
virtual bvt convert_if(const if_exprt &expr)
Definition: boolbv_if.cpp:12
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv.cpp:331
void set_frozen(literalt a) override
Definition: prop_conv.h:90
const std::string & id_string() const
Definition: irep.h:192
const abs_exprt & to_abs_expr(const exprt &expr)
Cast a generic exprt to a abs_exprt.
Definition: std_expr.h:411
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
Definition: boolbv_map.cpp:84
const binary_exprt & to_binary_expr(const exprt &expr)
Cast a generic exprt to a binary_exprt.
Definition: std_expr.h:702
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)
virtual bvt convert_div(const div_exprt &expr)
Definition: boolbv_div.cpp:13
virtual exprt make_bv_expr(const typet &type, const bvt &bv)
Definition: boolbv.cpp:611
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
void set_to(const exprt &expr, bool value) override
Definition: boolbv.cpp:601
virtual literalt convert_extractbit(const extractbit_exprt &expr)
const std::size_t MAX_FLATTENED_ARRAY_SIZE
Definition: magic.h:11
const unary_exprt & to_unary_expr(const exprt &expr)
Cast a generic exprt to a unary_exprt.
Definition: std_expr.h:361
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
virtual void ignoring(const exprt &expr)
Definition: prop_conv.cpp:454
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:64
bool empty() const
Definition: dstring.h:61
exprt & array()
Definition: std_expr.h:1486
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
std::vector< literalt > bvt
Definition: literal.h:200
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
virtual bvt convert_bitwise(const exprt &expr)
virtual bvt convert_power(const binary_exprt &expr)
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition: expr_cast.h:91
array index operator
Definition: std_expr.h:1462