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/bitvector_types.h>
18 #include <util/config.h>
19 #include <util/floatbv_expr.h>
20 #include <util/magic.h>
21 #include <util/mp_arith.h>
22 #include <util/replace_expr.h>
23 #include <util/simplify_expr.h>
24 #include <util/std_expr.h>
25 #include <util/std_types.h>
26 #include <util/string2int.h>
27 #include <util/string_constant.h>
28 #include <util/symbol.h>
29 #include <util/threeval.h>
30 
31 #include "boolbv_type.h"
32 
35 
37 {
38  const bool little_endian =
40  return endianness_map(type, little_endian);
41 }
42 
46 const bvt &
47 boolbvt::convert_bv(const exprt &expr, optionalt<std::size_t> expected_width)
48 {
49  // check cache first
50  std::pair<bv_cachet::iterator, bool> cache_result=
51  bv_cache.insert(std::make_pair(expr, bvt()));
52  if(!cache_result.second)
53  {
54  return cache_result.first->second;
55  }
56 
57  // Iterators into hash_maps supposedly stay stable
58  // even though we are inserting more elements recursively.
59 
60  cache_result.first->second = convert_bitvector(expr);
61 
63  !expected_width || cache_result.first->second.size() == *expected_width,
64  "bitvector width shall match the indicated expected width",
65  expr.find_source_location(),
67 
68  // check
69  for(const auto &literal : cache_result.first->second)
70  {
71  if(freeze_all && !literal.is_constant())
72  prop.set_frozen(literal);
73 
75  literal.var_no() != literalt::unused_var_no(),
76  "variable number must be different from the unused variable number",
77  expr.find_source_location(),
79  }
80 
81  return cache_result.first->second;
82 }
83 
87 {
88  ignoring(expr);
89 
90  // try to make it free bits
91  std::size_t width=boolbv_width(expr.type());
92  return prop.new_variables(width);
93 }
94 
101 {
102  if(expr.type().id()==ID_bool)
103  return {convert(expr)};
104 
105  if(expr.id()==ID_index)
106  return convert_index(to_index_expr(expr));
107  else if(expr.id()==ID_constraint_select_one)
108  return convert_constraint_select_one(expr);
109  else if(expr.id()==ID_member)
110  return convert_member(to_member_expr(expr));
111  else if(expr.id()==ID_with)
112  return convert_with(to_with_expr(expr));
113  else if(expr.id()==ID_update)
114  return convert_update(to_update_expr(expr));
115  else if(expr.id()==ID_case)
116  return convert_case(expr);
117  else if(expr.id()==ID_cond)
118  return convert_cond(to_cond_expr(expr));
119  else if(expr.id()==ID_if)
120  return convert_if(to_if_expr(expr));
121  else if(expr.id()==ID_constant)
122  return convert_constant(to_constant_expr(expr));
123  else if(expr.id()==ID_typecast)
125  else if(expr.id()==ID_symbol)
126  return convert_symbol(to_symbol_expr(expr));
127  else if(expr.id()==ID_bv_literals)
128  return convert_bv_literals(expr);
129  else if(expr.id()==ID_plus || expr.id()==ID_minus ||
130  expr.id()=="no-overflow-plus" ||
131  expr.id()=="no-overflow-minus")
132  return convert_add_sub(expr);
133  else if(expr.id() == ID_mult)
134  return convert_mult(to_mult_expr(expr));
135  else if(expr.id()==ID_div)
136  return convert_div(to_div_expr(expr));
137  else if(expr.id()==ID_mod)
138  return convert_mod(to_mod_expr(expr));
139  else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr ||
140  expr.id()==ID_rol || expr.id()==ID_ror)
141  return convert_shift(to_shift_expr(expr));
142  else if(expr.id()==ID_floatbv_plus || expr.id()==ID_floatbv_minus ||
143  expr.id()==ID_floatbv_mult || expr.id()==ID_floatbv_div ||
144  expr.id()==ID_floatbv_rem)
145  {
147  }
148  else if(expr.id()==ID_floatbv_typecast)
150  else if(expr.id()==ID_concatenation)
152  else if(expr.id()==ID_replication)
154  else if(expr.id()==ID_extractbits)
156  else if(expr.id()==ID_bitnot || expr.id()==ID_bitand ||
157  expr.id()==ID_bitor || expr.id()==ID_bitxor ||
158  expr.id()==ID_bitxnor || expr.id()==ID_bitnor ||
159  expr.id()==ID_bitnand)
160  return convert_bitwise(expr);
161  else if(expr.id() == ID_unary_minus)
163  else if(expr.id()==ID_unary_plus)
164  {
165  return convert_bitvector(to_unary_plus_expr(expr).op());
166  }
167  else if(expr.id()==ID_abs)
168  return convert_abs(to_abs_expr(expr));
169  else if(expr.id() == ID_bswap)
170  return convert_bswap(to_bswap_expr(expr));
171  else if(expr.id()==ID_byte_extract_little_endian ||
172  expr.id()==ID_byte_extract_big_endian)
174  else if(expr.id()==ID_byte_update_little_endian ||
175  expr.id()==ID_byte_update_big_endian)
177  else if(expr.id()==ID_nondet_symbol ||
178  expr.id()=="quant_symbol")
179  return convert_symbol(expr);
180  else if(expr.id()==ID_struct)
181  return convert_struct(to_struct_expr(expr));
182  else if(expr.id()==ID_union)
183  return convert_union(to_union_expr(expr));
184  else if(expr.id()==ID_string_constant)
185  return convert_bitvector(
187  else if(expr.id()==ID_array)
188  return convert_array(expr);
189  else if(expr.id()==ID_vector)
190  return convert_vector(to_vector_expr(expr));
191  else if(expr.id()==ID_complex)
192  return convert_complex(to_complex_expr(expr));
193  else if(expr.id()==ID_complex_real)
195  else if(expr.id()==ID_complex_imag)
197  else if(expr.id() == ID_array_comprehension)
199  else if(expr.id()==ID_array_of)
200  return convert_array_of(to_array_of_expr(expr));
201  else if(expr.id()==ID_let)
202  return convert_let(to_let_expr(expr));
203  else if(expr.id()==ID_function_application)
206  else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
207  expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
208  expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
209  return convert_bv_reduction(to_unary_expr(expr));
210  else if(expr.id()==ID_not)
211  return convert_not(to_not_expr(expr));
212  else if(expr.id()==ID_power)
213  return convert_power(to_binary_expr(expr));
214  else if(expr.id() == ID_popcount)
215  return convert_bv(simplify_expr(to_popcount_expr(expr).lower(), ns));
216  else if(expr.id() == ID_count_leading_zeros)
217  {
218  return convert_bv(
220  }
221 
222  return conversion_failed(expr);
223 }
224 
226 {
227  std::size_t width=boolbv_width(expr.type());
228 
229  if(width==0)
230  return conversion_failed(expr);
231 
232  const exprt &array_size = expr.type().size();
233 
234  const auto size = numeric_cast<mp_integer>(array_size);
235 
236  if(!size.has_value())
237  return conversion_failed(expr);
238 
239  typet counter_type = expr.arg().type();
240 
241  bvt bv;
242  bv.resize(width);
243 
244  for(mp_integer i = 0; i < *size; ++i)
245  {
246  exprt counter=from_integer(i, counter_type);
247 
248  exprt body = expr.body();
249  replace_expr(expr.arg(), counter, body);
250 
251  const bvt &tmp = convert_bv(body);
252 
253  INVARIANT(
254  *size * tmp.size() == width,
255  "total bitvector width shall equal the number of operands times the size "
256  "per operand");
257 
258  std::size_t offset = numeric_cast_v<std::size_t>(i * tmp.size());
259 
260  for(std::size_t j=0; j<tmp.size(); j++)
261  bv[offset+j]=tmp[j];
262  }
263 
264  return bv;
265 }
266 
268 {
269  std::size_t width=boolbv_width(expr.type());
270 
271  if(width==0)
272  return conversion_failed(expr);
273 
274  bvt bv;
275  bv.resize(width);
276 
277  const irept::subt &bv_sub=expr.find(ID_bv).get_sub();
278 
279  if(bv_sub.size()!=width)
280  throw "bv_literals with wrong size";
281 
282  for(std::size_t i=0; i<width; i++)
283  bv[i].set(unsafe_string2unsigned(id2string(bv_sub[i].id())));
284 
285  return bv;
286 }
287 
289 {
290  const typet &type=expr.type();
291  std::size_t width=boolbv_width(type);
292 
293  const irep_idt &identifier = expr.get(ID_identifier);
294  CHECK_RETURN(!identifier.empty());
295 
296  bvt bv = map.get_literals(identifier, type, width);
297 
299  std::all_of(
300  bv.begin(),
301  bv.end(),
302  [this](const literalt &l) {
303  return l.var_no() < prop.no_variables() || l.is_constant();
304  }),
305  "variable number of non-constant literals should be within bounds",
306  id2string(identifier));
307 
308  return bv;
309 }
310 
311 
313  const function_application_exprt &expr)
314 {
315  // record
316  functions.record(expr);
317 
318  // make it free bits
319  return prop.new_variables(boolbv_width(expr.type()));
320 }
321 
322 
324 {
325  PRECONDITION(expr.type().id() == ID_bool);
326 
327  if(expr.id()==ID_typecast)
328  return convert_typecast(to_typecast_expr(expr));
329  else if(expr.id()==ID_equal)
330  return convert_equality(to_equal_expr(expr));
331  else if(expr.id()==ID_verilog_case_equality ||
332  expr.id()==ID_verilog_case_inequality)
334  else if(expr.id()==ID_notequal)
335  {
336  const auto &notequal_expr = to_notequal_expr(expr);
337  return !convert_equality(
338  equal_exprt(notequal_expr.lhs(), notequal_expr.rhs()));
339  }
340  else if(expr.id()==ID_ieee_float_equal ||
341  expr.id()==ID_ieee_float_notequal)
342  {
344  }
345  else if(expr.id()==ID_le || expr.id()==ID_ge ||
346  expr.id()==ID_lt || expr.id()==ID_gt)
347  {
349  }
350  else if(expr.id()==ID_extractbit)
352  else if(expr.id()==ID_forall)
354  else if(expr.id()==ID_exists)
356  else if(expr.id()==ID_let)
357  {
358  bvt bv=convert_let(to_let_expr(expr));
359 
360  DATA_INVARIANT(bv.size()==1,
361  "convert_let must return 1-bit vector for boolean let");
362 
363  return bv[0];
364  }
365  else if(expr.id()==ID_index)
366  {
367  bvt bv=convert_index(to_index_expr(expr));
368  CHECK_RETURN(bv.size() == 1);
369  return bv[0];
370  }
371  else if(expr.id()==ID_member)
372  {
374  CHECK_RETURN(bv.size() == 1);
375  return bv[0];
376  }
377  else if(expr.id()==ID_case)
378  {
379  bvt bv=convert_case(expr);
380  CHECK_RETURN(bv.size() == 1);
381  return bv[0];
382  }
383  else if(expr.id()==ID_cond)
384  {
385  bvt bv = convert_cond(to_cond_expr(expr));
386  CHECK_RETURN(bv.size() == 1);
387  return bv[0];
388  }
389  else if(expr.id()==ID_sign)
390  {
391  const auto &op = to_sign_expr(expr).op();
392  const bvt &bv = convert_bv(op);
393  CHECK_RETURN(!bv.empty());
394  const irep_idt type_id = op.type().id();
395  if(type_id == ID_signedbv || type_id == ID_fixedbv || type_id == ID_floatbv)
396  return bv[bv.size()-1];
397  if(type_id == ID_unsignedbv)
398  return const_literal(false);
399  }
400  else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
401  expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
402  expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
403  return convert_reduction(to_unary_expr(expr));
404  else if(expr.id()==ID_onehot || expr.id()==ID_onehot0)
405  return convert_onehot(to_unary_expr(expr));
406  else if(
407  expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
408  expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl ||
409  expr.id() == ID_overflow_unary_minus)
410  {
411  return convert_overflow(expr);
412  }
413  else if(expr.id()==ID_isnan)
414  {
415  const auto &op = to_unary_expr(expr).op();
416  const bvt &bv = convert_bv(op);
417 
418  if(op.type().id() == ID_floatbv)
419  {
420  float_utilst float_utils(prop, to_floatbv_type(op.type()));
421  return float_utils.is_NaN(bv);
422  }
423  else if(op.type().id() == ID_fixedbv)
424  return const_literal(false);
425  }
426  else if(expr.id()==ID_isfinite)
427  {
428  const auto &op = to_unary_expr(expr).op();
429  const bvt &bv = convert_bv(op);
430 
431  if(op.type().id() == ID_floatbv)
432  {
433  float_utilst float_utils(prop, to_floatbv_type(op.type()));
434  return prop.land(
435  !float_utils.is_infinity(bv),
436  !float_utils.is_NaN(bv));
437  }
438  else if(op.id() == ID_fixedbv)
439  return const_literal(true);
440  }
441  else if(expr.id()==ID_isinf)
442  {
443  const auto &op = to_unary_expr(expr).op();
444  const bvt &bv = convert_bv(op);
445 
446  if(op.type().id() == ID_floatbv)
447  {
448  float_utilst float_utils(prop, to_floatbv_type(op.type()));
449  return float_utils.is_infinity(bv);
450  }
451  else if(op.type().id() == ID_fixedbv)
452  return const_literal(false);
453  }
454  else if(expr.id()==ID_isnormal)
455  {
456  const auto &op = to_unary_expr(expr).op();
457 
458  if(op.type().id() == ID_floatbv)
459  {
460  const bvt &bv = convert_bv(op);
461  float_utilst float_utils(prop, to_floatbv_type(op.type()));
462  return float_utils.is_normal(bv);
463  }
464  else if(op.type().id() == ID_fixedbv)
465  return const_literal(true);
466  }
467  else if(expr.id() == ID_function_application)
468  {
470  return prop.new_variable();
471  }
472 
473  return SUB::convert_rest(expr);
474 }
475 
477 {
479  return true;
480 
481  const typet &type = expr.lhs().type();
482 
483  if(
484  expr.lhs().id() == ID_symbol && type == expr.rhs().type() &&
485  type.id() != ID_bool)
486  {
487  // see if it is an unbounded array
488  if(is_unbounded_array(type))
489  return true;
490 
491  const bvt &bv1=convert_bv(expr.rhs());
492 
493  const irep_idt &identifier=
495 
496  map.set_literals(identifier, type, bv1);
497 
498  if(freeze_all)
499  set_frozen(bv1);
500 
501  return false;
502  }
503 
504  return true;
505 }
506 
507 void boolbvt::set_to(const exprt &expr, bool value)
508 {
509  PRECONDITION(expr.type().id() == ID_bool);
510 
511  const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr);
512  if(value && equal_expr && !boolbv_set_equality_to_true(*equal_expr))
513  return;
514  SUB::set_to(expr, value);
515 }
516 
517 exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv)
518 {
519  exprt dest(ID_bv_literals, type);
520  irept::subt &bv_sub=dest.add(ID_bv).get_sub();
521  bv_sub.resize(bv.size());
522 
523  for(std::size_t i=0; i<bv.size(); i++)
524  bv_sub[i].id(std::to_string(bv[i].get()));
525  return dest;
526 }
527 
529 {
530  const std::size_t width = boolbv_width(type);
531  PRECONDITION(width != 0);
532  bvt bv = prop.new_variables(width);
533  return make_bv_expr(type, bv);
534 }
535 
536 bool boolbvt::is_unbounded_array(const typet &type) const
537 {
538  if(type.id()!=ID_array)
539  return false;
540 
542  return true;
543 
544  const exprt &size=to_array_type(type).size();
545 
546  const auto s = numeric_cast<mp_integer>(size);
547  if(!s.has_value())
548  return true;
549 
551  if(*s > MAX_FLATTENED_ARRAY_SIZE)
552  return true;
553 
554  return false;
555 }
556 
557 void boolbvt::print_assignment(std::ostream &out) const
558 {
560  map.show(out);
561 }
562 
564 {
565  const struct_typet::componentst &components = src.components();
566  offset_mapt dest;
567  dest.reserve(components.size());
568  std::size_t offset = 0;
569  for(const auto &comp : components)
570  {
571  dest.push_back(offset);
572  offset += boolbv_width(comp.type());
573  }
574  return dest;
575 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
boolbvt::convert_bv_typecast
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
Definition: boolbv_typecast.cpp:18
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
boolbvt::convert_overflow
virtual literalt convert_overflow(const exprt &expr)
Definition: boolbv_overflow.cpp:15
boolbvt::unbounded_array
unbounded_arrayt unbounded_array
Definition: boolbv.h:82
to_array_comprehension_expr
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:3076
to_vector_expr
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1500
prop_conv_solvert::equality_propagation
bool equality_propagation
Definition: prop_conv_solver.h:73
to_update_expr
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:2421
to_extractbit_expr
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: bitvector_expr.h:411
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
boolbvt::map
boolbv_mapt map
Definition: boolbv.h:117
boolbvt::convert_member
virtual bvt convert_member(const member_exprt &expr)
Definition: boolbv_member.cpp:91
boolbvt::convert_bv_rel
virtual literalt convert_bv_rel(const binary_relation_exprt &)
Flatten <, >, <= and >= expressions.
Definition: boolbv_bv_rel.cpp:18
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1029
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:590
boolbvt::convert_byte_update
virtual bvt convert_byte_update(const byte_update_exprt &expr)
Definition: boolbv_byte_update.cpp:18
arith_tools.h
mp_arith.h
to_array_expr
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1411
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
boolbvt::convert_cond
virtual bvt convert_cond(const cond_exprt &)
Definition: boolbv_cond.cpp:13
propt::new_variables
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
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:100
boolbvt::is_unbounded_array
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:536
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
float_utilst
Definition: float_utils.h:18
typet
The type of an expression, extends irept.
Definition: type.h:28
float_utils.h
bvt
std::vector< literalt > bvt
Definition: literal.h:201
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
threeval.h
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: bitvector_types.h:367
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2151
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:507
boolbvt::convert_complex
virtual bvt convert_complex(const complex_exprt &expr)
Definition: boolbv_complex.cpp:13
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:122
boolbv_mapt::get_literals
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
Definition: boolbv_map.cpp:41
MAX_FLATTENED_ARRAY_SIZE
const std::size_t MAX_FLATTENED_ARRAY_SIZE
Definition: magic.h:11
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:112
boolbvt::convert_mod
virtual bvt convert_mod(const mod_exprt &expr)
Definition: boolbv_mod.cpp:12
boolbv_type.h
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
to_array_of_expr
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1361
boolbvt::convert_vector
virtual bvt convert_vector(const vector_exprt &expr)
Definition: boolbv_vector.cpp:12
prop_conv_solvert::freeze_all
bool freeze_all
Definition: prop_conv_solver.h:74
boolbvt::convert_symbol
virtual bvt convert_symbol(const exprt &expr)
Definition: boolbv.cpp:288
propt::new_variable
virtual literalt new_variable()=0
string_constant.h
boolbvt::convert_index
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
Definition: boolbv_index.cpp:284
exprt
Base class for all expressions.
Definition: expr.h:54
to_complex_expr
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1670
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:580
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1562
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
array_comprehension_exprt::arg
const symbol_exprt & arg() const
Definition: std_expr.h:3037
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
boolbvt::convert_union
virtual bvt convert_union(const union_exprt &expr)
Definition: boolbv_union.cpp:11
configt::ansi_c
struct configt::ansi_ct ansi_c
boolbvt::convert_case
virtual bvt convert_case(const exprt &expr)
Definition: boolbv_case.cpp:13
propt::land
virtual literalt land(literalt a, literalt b)=0
equal_exprt
Equality.
Definition: std_expr.h:1139
magic.h
Magic numbers used throughout the codebase.
array_comprehension_exprt::type
const array_typet & type() const
Definition: std_expr.h:3027
boolbvt::functions
functionst functions
Definition: boolbv.h:114
to_popcount_expr
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: bitvector_expr.h:667
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
boolbvt::convert_constant
virtual bvt convert_constant(const constant_exprt &expr)
Definition: boolbv_constant.cpp:13
literalt::unused_var_no
static var_not unused_var_no()
Definition: literal.h:176
boolbvt::convert_extractbit
virtual literalt convert_extractbit(const extractbit_exprt &expr)
Definition: boolbv_extractbit.cpp:20
boolbvt::convert_concatenation
virtual bvt convert_concatenation(const concatenation_exprt &expr)
Definition: boolbv_concatenation.cpp:14
to_floatbv_typecast_expr
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: floatbv_expr.h:68
prop_conv_solvert::ignoring
virtual void ignoring(const exprt &expr)
Definition: prop_conv_solver.cpp:453
expr_lowering.h
to_unary_plus_expr
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:464
to_complex_real_expr
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1715
float_utilst::is_infinity
literalt is_infinity(const bvt &)
Definition: float_utils.cpp:670
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
INVARIANT_WITH_DIAGNOSTICS
#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
to_bswap_expr
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Definition: bitvector_expr.h:63
array_typet::size
const exprt & size() const
Definition: std_types.h:765
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
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
prop_conv_solvert::set_frozen
void set_frozen(literalt)
Definition: prop_conv_solver.cpp:28
boolbvt::convert_byte_extract
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
Definition: boolbv_byte_extract.cpp:36
boolbvt::boolbv_set_equality_to_true
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
Definition: boolbv.cpp:476
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
@ IS_LITTLE_ENDIAN
to_cond_expr
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:2987
boolbvt::convert_array
virtual bvt convert_array(const exprt &expr)
Flatten array.
Definition: boolbv_array.cpp:16
boolbv_mapt::show
void show(std::ostream &out) const
Definition: boolbv_map.cpp:35
float_utilst::is_normal
literalt is_normal(const bvt &)
Definition: float_utils.cpp:219
to_mod_expr
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1074
functionst::record
void record(const function_application_exprt &function_application)
Definition: functions.cpp:14
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:126
boolbvt::bv_cache
bv_cachet bv_cache
Definition: boolbv.h:134
boolbvt::convert_bv_literals
virtual bvt convert_bv_literals(const exprt &expr)
Definition: boolbv.cpp:267
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:960
boolbvt::convert_extractbits
virtual bvt convert_extractbits(const extractbits_exprt &expr)
Definition: boolbv_extractbits.cpp:14
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
boolbvt::boolbv_width
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:96
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:120
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:192
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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
bitvector_types.h
Pre-defined bitvector types.
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
std_types.h
Pre-defined types.
boolbvt::make_bv_expr
virtual exprt make_bv_expr(const typet &type, const bvt &bv)
Definition: boolbv.cpp:517
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:2928
boolbvt::convert_ieee_float_rel
virtual literalt convert_ieee_float_rel(const binary_relation_exprt &)
Definition: boolbv_ieee_float_rel.cpp:17
array_comprehension_exprt::body
const exprt & body() const
Definition: std_expr.h:3047
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:194
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
to_notequal_expr
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1222
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2557
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:420
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
boolbvt::convert_bv_reduction
virtual bvt convert_bv_reduction(const unary_exprt &expr)
Definition: boolbv_reduction.cpp:54
float_utilst::is_NaN
literalt is_NaN(const bvt &)
Definition: float_utils.cpp:698
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:407
propt::set_frozen
virtual void set_frozen(literalt)
Definition: prop.h:114
dstringt::empty
bool empty() const
Definition: dstring.h:88
floatbv_expr.h
API to expression classes for floating-point arithmetic.
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
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:47
boolbvt::convert_bswap
virtual bvt convert_bswap(const bswap_exprt &expr)
Definition: boolbv_bswap.cpp:14
to_complex_imag_expr
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1760
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
boolbvt::make_free_bv_expr
virtual exprt make_free_bv_expr(const typet &type)
Definition: boolbv.cpp:528
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: bitvector_expr.h:278
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:154
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2234
sharing_treet< irept, forward_list_as_mapt< irep_namet, irept > >::subt
typename dt::subt subt
Definition: irep.h:171
prop_conv_solvert::convert_rest
virtual literalt convert_rest(const exprt &expr)
Definition: prop_conv_solver.cpp:335
config
configt config
Definition: config.cpp:24
simplify_expr.h
to_ieee_float_op_expr
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
irep_pretty_diagnosticst
Definition: irep.h:514
to_concatenation_expr
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: bitvector_expr.h:618
boolbvt::convert_let
virtual bvt convert_let(const let_exprt &)
Definition: boolbv_let.cpp:15
boolbvt::convert_bitwise
virtual bvt convert_bitwise(const exprt &expr)
Definition: boolbv_bitwise.cpp:13
boolbvt::convert_floatbv_op
virtual bvt convert_floatbv_op(const ieee_float_op_exprt &)
Definition: boolbv_floatbv_op.cpp:83
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
boolbvt::convert_struct
virtual bvt convert_struct(const struct_exprt &expr)
Definition: boolbv_struct.cpp:13
to_quantifier_expr
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: mathematical_expr.h:316
to_sign_expr
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:531
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2066
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
replace_expr
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Definition: replace_expr.cpp:12
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
boolbvt::unbounded_arrayt::U_ALL
@ U_ALL
literalt
Definition: literal.h:26
unsafe_string2unsigned
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:38
irept::get_sub
subt & get_sub()
Definition: irep.h:467
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1179
prop_conv_solvert::print_assignment
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: prop_conv_solver.cpp:521
endianness_mapt
Maps a big-endian offset to a little-endian offset.
Definition: endianness_map.h:31
config.h
boolbvt::convert_equality
virtual literalt convert_equality(const equal_exprt &expr)
Definition: boolbv_equality.cpp:16
to_extractbits_expr
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: bitvector_expr.h:499
boolbvt::convert_unary_minus
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
Definition: boolbv_unary_minus.cpp:20
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2611
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:205
boolbv.h
replace_expr.h
boolbvt::convert_array_comprehension
virtual bvt convert_array_comprehension(const array_comprehension_exprt &)
Definition: boolbv.cpp:225
boolbvt::endianness_map
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
Definition: boolbv.h:102
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
boolbvt::convert_not
virtual bvt convert_not(const not_exprt &expr)
Definition: boolbv_not.cpp:13
boolbvt::convert_typecast
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
Definition: boolbv_typecast.cpp:611
boolbvt::offset_mapt
std::vector< std::size_t > offset_mapt
Definition: boolbv.h:273
boolbvt::build_offset_map
offset_mapt build_offset_map(const struct_typet &src)
Definition: boolbv.cpp:563
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3013
boolbvt::convert_rest
literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:323
boolbvt::convert_power
virtual bvt convert_power(const binary_exprt &expr)
Definition: boolbv_power.cpp:12
std_expr.h
API to expression classes.
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:723
boolbvt::convert_function_application
virtual bvt convert_function_application(const function_application_exprt &expr)
Definition: boolbv.cpp:312
boolbvt::convert_div
virtual bvt convert_div(const div_exprt &expr)
Definition: boolbv_div.cpp:13
to_function_application_expr
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
Definition: mathematical_expr.h:244
boolbvt::print_assignment
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: boolbv.cpp:557
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:20
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:157
to_count_leading_zeros_expr
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
Definition: bitvector_expr.h:899
bitvector_expr.h
API to expression classes for bitvectors.
to_replication_expr
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
Definition: bitvector_expr.h:567
prop_conv_solvert::set_to
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'current_context => expr' if value is true,...
Definition: prop_conv_solver.cpp:534
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1605
to_abs_expr
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:370
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:128
boolbv_mapt::set_literals
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:75
boolbvt::convert_update
virtual bvt convert_update(const update_exprt &)
Definition: boolbv_update.cpp:14
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700
boolbvt::convert_with
virtual bvt convert_with(const with_exprt &expr)
Definition: boolbv_with.cpp:16
boolbvt::convert_complex_imag
virtual bvt convert_complex_imag(const complex_imag_exprt &expr)
Definition: boolbv_complex.cpp:54