cprover
Loading...
Searching...
No Matches
boolbv.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "boolbv.h"
10
11#include <util/arith_tools.h>
12#include <util/bitvector_expr.h>
14#include <util/byte_operators.h>
15#include <util/config.h>
16#include <util/floatbv_expr.h>
17#include <util/magic.h>
18#include <util/mp_arith.h>
19#include <util/simplify_expr.h>
20#include <util/std_expr.h>
22
24
25#include "literal_vector_expr.h"
26
27#include <algorithm>
28
30{
31 const bool little_endian =
33 return endianness_map(type, little_endian);
34}
35
40 const exprt &expr,
41 std::optional<std::size_t> expected_width)
42{
43 // check cache first
44 std::pair<bv_cachet::iterator, bool> cache_result=
45 bv_cache.insert(std::make_pair(expr, bvt()));
46
47 // get a reference to the cache entry
48 auto &cache_entry = cache_result.first->second;
49
50 if(!cache_result.second)
51 {
52 // Found in cache
53 return cache_entry;
54 }
55
56 // Iterators into hash_maps do not remain valid when inserting
57 // more elements recursively. C++11 ยง23.2.5/13
58 // However, the _reference_ to the entry does!
59 cache_entry = convert_bitvector(expr);
60
62 !expected_width || cache_entry.size() == *expected_width,
63 "bitvector width shall match the indicated expected width",
66
67 // check
68 for(const auto &literal : cache_entry)
69 {
70 if(freeze_all && !literal.is_constant())
71 prop.set_frozen(literal);
72
74 literal.var_no() != literalt::unused_var_no(),
75 "variable number must be different from the unused variable number",
78 }
79
80 return cache_entry;
81}
82
84{
85 if(expr.type().id() == ID_bool)
86 return prop_conv_solvert::handle(expr);
87 auto bv = convert_bv(expr);
88 set_frozen(bv); // for incremental usage
89 return literal_vector_exprt{bv, expr.type()};
90}
91
95{
96 ignoring(expr);
97
98 // try to make it free bits
99 std::size_t width=boolbv_width(expr.type());
100 return prop.new_variables(width);
101}
102
109{
110 if(expr.is_boolean())
111 return {convert(expr)};
112
113 if(expr.id()==ID_index)
114 return convert_index(to_index_expr(expr));
115 else if(expr.id()==ID_constraint_select_one)
117 else if(expr.id()==ID_member)
118 return convert_member(to_member_expr(expr));
119 else if(expr.id()==ID_with)
120 return convert_with(to_with_expr(expr));
121 else if(expr.id()==ID_update)
122 return convert_update(to_update_expr(expr));
123 else if(expr.id() == ID_update_bit)
125 else if(expr.id()==ID_case)
126 return convert_case(expr);
127 else if(expr.id()==ID_cond)
128 return convert_cond(to_cond_expr(expr));
129 else if(expr.id()==ID_if)
130 return convert_if(to_if_expr(expr));
131 else if(expr.is_constant())
133 else if(expr.id()==ID_typecast)
135 else if(expr.id()==ID_symbol)
136 return convert_symbol(to_symbol_expr(expr));
137 else if(expr.id()==ID_plus || expr.id()==ID_minus ||
138 expr.id()=="no-overflow-plus" ||
139 expr.id()=="no-overflow-minus")
140 return convert_add_sub(expr);
141 else if(expr.id() == ID_mult)
142 return convert_mult(to_mult_expr(expr));
143 else if(expr.id()==ID_div)
144 return convert_div(to_div_expr(expr));
145 else if(expr.id()==ID_mod)
146 return convert_mod(to_mod_expr(expr));
147 else if(expr.id()==ID_shl || expr.id()==ID_ashr || expr.id()==ID_lshr ||
148 expr.id()==ID_rol || expr.id()==ID_ror)
149 return convert_shift(to_shift_expr(expr));
150 else if(
151 expr.id() == ID_floatbv_plus || expr.id() == ID_floatbv_minus ||
152 expr.id() == ID_floatbv_mult || expr.id() == ID_floatbv_div)
153 {
155 }
156 else if(expr.id() == ID_floatbv_mod)
158 else if(expr.id() == ID_floatbv_rem)
160 else if(expr.id()==ID_floatbv_typecast)
162 else if(expr.id()==ID_concatenation)
164 else if(expr.id()==ID_replication)
166 else if(expr.id()==ID_extractbits)
168 else if(expr.id()==ID_bitnot || expr.id()==ID_bitand ||
169 expr.id()==ID_bitor || expr.id()==ID_bitxor ||
170 expr.id()==ID_bitxnor || expr.id()==ID_bitnor ||
171 expr.id()==ID_bitnand)
172 return convert_bitwise(expr);
173 else if(expr.id() == ID_unary_minus)
175 else if(expr.id()==ID_unary_plus)
176 {
177 return convert_bitvector(to_unary_plus_expr(expr).op());
178 }
179 else if(expr.id()==ID_abs)
180 return convert_abs(to_abs_expr(expr));
181 else if(expr.id() == ID_bswap)
182 return convert_bswap(to_bswap_expr(expr));
183 else if(expr.id()==ID_byte_extract_little_endian ||
184 expr.id()==ID_byte_extract_big_endian)
186 else if(expr.id()==ID_byte_update_little_endian ||
187 expr.id()==ID_byte_update_big_endian)
189 else if(expr.id()==ID_nondet_symbol ||
190 expr.id()=="quant_symbol")
191 return convert_symbol(expr);
192 else if(expr.id()==ID_struct)
193 return convert_struct(to_struct_expr(expr));
194 else if(expr.id()==ID_union)
195 return convert_union(to_union_expr(expr));
196 else if(expr.id() == ID_empty_union)
198 else if(expr.id()==ID_string_constant)
199 return convert_bitvector(
201 else if(expr.id() == ID_named_term)
202 {
203 const auto &named_term_expr = to_named_term_expr(expr);
204 set_to_true(equal_exprt(named_term_expr.symbol(), named_term_expr.value()));
205 return convert_symbol(named_term_expr.symbol());
206 }
207 else if(expr.id()==ID_array)
208 return convert_array(expr);
209 else if(expr.id()==ID_complex)
210 return convert_complex(to_complex_expr(expr));
211 else if(expr.id()==ID_complex_real)
213 else if(expr.id()==ID_complex_imag)
215 else if(expr.id() == ID_array_comprehension)
217 else if(expr.id()==ID_array_of)
219 else if(expr.id()==ID_let)
220 return convert_let(to_let_expr(expr));
221 else if(expr.id()==ID_function_application)
224 else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
225 expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
226 expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
228 else if(expr.id()==ID_not)
229 return convert_not(to_not_expr(expr));
230 else if(expr.id()==ID_power)
231 return convert_power(to_binary_expr(expr));
232 else if(expr.id() == ID_popcount)
233 return convert_bv(simplify_expr(to_popcount_expr(expr).lower(), ns));
234 else if(expr.id() == ID_count_leading_zeros)
235 {
236 return convert_bv(
238 }
239 else if(expr.id() == ID_count_trailing_zeros)
240 {
241 return convert_bv(
243 }
244 else if(expr.id() == ID_bitreverse)
246 else if(expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
248 else if(
249 const auto overflow_with_result =
251 {
252 return convert_overflow_result(*overflow_with_result);
253 }
254 else if(expr.id() == ID_find_first_set)
255 return convert_bv(simplify_expr(to_find_first_set_expr(expr).lower(), ns));
256 else if(expr.id() == ID_literal_vector)
257 return to_literal_vector_expr(expr).bv();
258
259 return conversion_failed(expr);
260}
261
263{
264 std::size_t width=boolbv_width(expr.type());
265
266 const exprt &array_size = expr.type().size();
267
268 const auto size = numeric_cast_v<mp_integer>(to_constant_expr(array_size));
269
270 typet counter_type = expr.arg().type();
271
272 bvt bv;
273 bv.resize(width);
274
275 for(mp_integer i = 0; i < size; ++i)
276 {
277 exprt counter=from_integer(i, counter_type);
278
279 exprt body = expr.instantiate({counter});
280
281 const bvt &tmp = convert_bv(body);
282
283 INVARIANT(
284 size * tmp.size() == width,
285 "total bitvector width shall equal the number of operands times the size "
286 "per operand");
287
288 std::size_t offset = numeric_cast_v<std::size_t>(i * tmp.size());
289
290 for(std::size_t j=0; j<tmp.size(); j++)
291 bv[offset+j]=tmp[j];
292 }
293
294 return bv;
295}
296
298{
299 const typet &type=expr.type();
300 std::size_t width=boolbv_width(type);
301
302 const irep_idt &identifier = expr.get(ID_identifier);
303 CHECK_RETURN(!identifier.empty());
304
305 bvt bv = map.get_literals(identifier, type, width);
306
308 std::all_of(
309 bv.begin(),
310 bv.end(),
311 [this](const literalt &l) {
312 return l.var_no() < prop.no_variables() || l.is_constant();
313 }),
314 "variable number of non-constant literals should be within bounds",
315 id2string(identifier));
316
317 return bv;
318}
319
320
322 const function_application_exprt &expr)
323{
324 // record
325 functions.record(expr);
326
327 // make it free bits
328 return prop.new_variables(boolbv_width(expr.type()));
329}
330
331
333{
334 PRECONDITION(expr.is_boolean());
335
336 if(expr.id()==ID_typecast)
338 else if(expr.id()==ID_equal)
339 return convert_equality(to_equal_expr(expr));
340 else if(expr.id()==ID_verilog_case_equality ||
341 expr.id()==ID_verilog_case_inequality)
343 else if(expr.id()==ID_notequal)
344 {
345 const auto &notequal_expr = to_notequal_expr(expr);
346 return !convert_equality(
347 equal_exprt(notequal_expr.lhs(), notequal_expr.rhs()));
348 }
349 else if(expr.id()==ID_ieee_float_equal ||
350 expr.id()==ID_ieee_float_notequal)
351 {
353 }
354 else if(expr.id()==ID_le || expr.id()==ID_ge ||
355 expr.id()==ID_lt || expr.id()==ID_gt)
356 {
358 }
359 else if(expr.id()==ID_extractbit)
361 else if(expr.id()==ID_forall)
363 else if(expr.id()==ID_exists)
365 else if(expr.id()==ID_let)
366 {
367 bvt bv=convert_let(to_let_expr(expr));
368
369 DATA_INVARIANT(bv.size()==1,
370 "convert_let must return 1-bit vector for boolean let");
371
372 return bv[0];
373 }
374 else if(expr.id()==ID_index)
375 {
377 CHECK_RETURN(bv.size() == 1);
378 return bv[0];
379 }
380 else if(expr.id()==ID_member)
381 {
383 CHECK_RETURN(bv.size() == 1);
384 return bv[0];
385 }
386 else if(expr.id()==ID_case)
387 {
388 bvt bv=convert_case(expr);
389 CHECK_RETURN(bv.size() == 1);
390 return bv[0];
391 }
392 else if(expr.id()==ID_cond)
393 {
394 bvt bv = convert_cond(to_cond_expr(expr));
395 CHECK_RETURN(bv.size() == 1);
396 return bv[0];
397 }
398 else if(expr.id()==ID_sign)
399 {
400 const auto &op = to_sign_expr(expr).op();
401 const bvt &bv = convert_bv(op);
402 CHECK_RETURN(!bv.empty());
403 const irep_idt type_id = op.type().id();
404 if(type_id == ID_signedbv || type_id == ID_fixedbv || type_id == ID_floatbv)
405 return bv[bv.size()-1];
406 if(type_id == ID_unsignedbv)
407 return const_literal(false);
408 }
409 else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and ||
410 expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
411 expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)
412 return convert_reduction(to_unary_expr(expr));
413 else if(expr.id()==ID_onehot || expr.id()==ID_onehot0)
414 return convert_onehot(to_unary_expr(expr));
415 else if(
416 const auto binary_overflow =
418 {
419 return convert_binary_overflow(*binary_overflow);
420 }
421 else if(
422 const auto unary_overflow =
424 {
425 return convert_unary_overflow(*unary_overflow);
426 }
427 else if(expr.id()==ID_isnan)
428 {
429 const auto &op = to_unary_expr(expr).op();
430 const bvt &bv = convert_bv(op);
431
432 if(op.type().id() == ID_floatbv)
433 {
434 float_utilst float_utils(prop, to_floatbv_type(op.type()));
435 return float_utils.is_NaN(bv);
436 }
437 else if(op.type().id() == ID_fixedbv)
438 return const_literal(false);
439 }
440 else if(expr.id()==ID_isfinite)
441 {
442 const auto &op = to_unary_expr(expr).op();
443 const bvt &bv = convert_bv(op);
444
445 if(op.type().id() == ID_floatbv)
446 {
447 float_utilst float_utils(prop, to_floatbv_type(op.type()));
448 return prop.land(
449 !float_utils.is_infinity(bv),
450 !float_utils.is_NaN(bv));
451 }
452 else if(op.id() == ID_fixedbv)
453 return const_literal(true);
454 }
455 else if(expr.id()==ID_isinf)
456 {
457 const auto &op = to_unary_expr(expr).op();
458 const bvt &bv = convert_bv(op);
459
460 if(op.type().id() == ID_floatbv)
461 {
462 float_utilst float_utils(prop, to_floatbv_type(op.type()));
463 return float_utils.is_infinity(bv);
464 }
465 else if(op.type().id() == ID_fixedbv)
466 return const_literal(false);
467 }
468 else if(expr.id()==ID_isnormal)
469 {
470 const auto &op = to_unary_expr(expr).op();
471
472 if(op.type().id() == ID_floatbv)
473 {
474 const bvt &bv = convert_bv(op);
475 float_utilst float_utils(prop, to_floatbv_type(op.type()));
476 return float_utils.is_normal(bv);
477 }
478 else if(op.type().id() == ID_fixedbv)
479 return const_literal(true);
480 }
481 else if(expr.id() == ID_function_application)
482 {
484 return prop.new_variable();
485 }
486
487 return SUB::convert_rest(expr);
488}
489
491{
493 return true;
494
495 const typet &type = expr.lhs().type();
496
497 if(
498 expr.lhs().id() == ID_symbol && type == expr.rhs().type() &&
499 type.id() != ID_bool)
500 {
501 // see if it is an unbounded array
502 if(is_unbounded_array(type))
503 return true;
504
505 const bvt &bv1=convert_bv(expr.rhs());
506
507 const irep_idt &identifier=
509
510 map.set_literals(identifier, type, bv1);
511
512 if(freeze_all)
513 set_frozen(bv1);
514
515 return false;
516 }
517
518 return true;
519}
520
521void boolbvt::set_to(const exprt &expr, bool value)
522{
523 PRECONDITION(expr.is_boolean());
524
525 const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr);
526 if(value && equal_expr && !boolbv_set_equality_to_true(*equal_expr))
527 return;
528 SUB::set_to(expr, value);
529}
530
531bool boolbvt::is_unbounded_array(const typet &type) const
532{
533 if(type.id()!=ID_array)
534 return false;
535
537 return true;
538
539 const auto &size_opt = bv_width.get_width_opt(type);
540 if(!size_opt.has_value())
541 return true;
542
544 if(*size_opt > MAX_FLATTENED_ARRAY_SIZE)
545 return true;
546
547 return false;
548}
549
551{
552 // to ensure freshness of the new identifiers
554
556 result.reserve(binding.variables().size());
557
558 for(const auto &binding : binding.variables())
559 {
560 const auto &old_identifier = binding.get_identifier();
561
562 // produce a new identifier
563 const irep_idt new_identifier =
564 "boolbvt::scope::" + std::to_string(scope_counter) +
565 "::" + id2string(old_identifier);
566
567 result.emplace_back(new_identifier, binding.type());
568 }
569
570 return result;
571}
572
573void boolbvt::print_assignment(std::ostream &out) const
574{
576 map.show(out);
577}
578
580{
581 const struct_typet::componentst &components = src.components();
582 offset_mapt dest;
583 dest.reserve(components.size());
584 std::size_t offset = 0;
585 for(const auto &comp : components)
586 {
587 dest.push_back(offset);
588 offset += boolbv_width(comp.type());
589 }
590 return dest;
591}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
API to expression classes for bitvectors.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const find_first_set_exprt & to_find_first_set_expr(const exprt &expr)
Cast an exprt to a find_first_set_exprt.
const update_bit_exprt & to_update_bit_expr(const exprt &expr)
Cast an exprt to an update_bit_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
Pre-defined bitvector types.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Expression classes for byte-level operators.
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:3405
const array_typet & type() const
Definition std_expr.h:3419
const symbol_exprt & arg() const
Definition std_expr.h:3429
const exprt & size() const
Definition std_types.h:840
const namespacet & ns
Definition arrays.h:56
exprt & lhs()
Definition std_expr.h:668
exprt & rhs()
Definition std_expr.h:678
A base class for variable bindings (quantifiers, let, lambda)
Definition std_expr.h:3099
variablest & variables()
Definition std_expr.h:3120
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
Definition std_expr.cpp:177
std::vector< symbol_exprt > variablest
Definition std_expr.h:3101
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
void show(std::ostream &out) const
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
virtual std::optional< std::size_t > get_width_opt(const typet &type) const
virtual bvt convert_with(const with_exprt &expr)
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:135
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 const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition boolbv.cpp:39
std::size_t scope_counter
Definition boolbv.h:283
virtual bvt convert_constraint_select_one(const exprt &expr)
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 &)
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
offset_mapt build_offset_map(const struct_typet &src)
Definition boolbv.cpp:579
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:108
binding_exprt::variablest fresh_binding(const binding_exprt &)
create new, unique variables for the given binding
Definition boolbv.cpp:550
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:531
virtual bvt convert_mod(const mod_exprt &expr)
virtual bvt convert_add_sub(const exprt &expr)
virtual bvt convert_constant(const constant_exprt &expr)
virtual literalt convert_quantifier(const quantifier_exprt &expr)
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
Definition boolbv.cpp:490
virtual bvt convert_mult(const mult_exprt &expr)
exprt handle(const exprt &) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
Definition boolbv.cpp:83
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:321
virtual bvt convert_cond(const cond_exprt &)
virtual bvt convert_empty_union(const empty_union_exprt &expr)
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:521
virtual bvt convert_byte_update(const byte_update_exprt &expr)
boolbv_widtht bv_width
Definition boolbv.h:116
virtual literalt convert_extractbit(const extractbit_exprt &expr)
unbounded_arrayt unbounded_array
Definition boolbv.h:88
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:573
virtual bvt convert_not(const not_exprt &expr)
virtual bvt convert_extractbits(const extractbits_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
std::vector< std::size_t > offset_mapt
Definition boolbv.h:276
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)
virtual literalt convert_binary_overflow(const binary_overflow_exprt &expr)
virtual bvt convert_array_of(const array_of_exprt &expr)
Flatten arrays constructed from a single element.
virtual bvt convert_floatbv_mod_rem(const binary_exprt &)
virtual bvt convert_saturating_add_sub(const binary_exprt &expr)
virtual bvt convert_overflow_result(const overflow_result_exprt &expr)
virtual bvt convert_bitwise(const exprt &expr)
virtual bvt convert_array_comprehension(const array_comprehension_exprt &)
Definition boolbv.cpp:262
virtual bvt convert_bv_reduction(const unary_exprt &expr)
virtual literalt convert_equality(const equal_exprt &expr)
functionst functions
Definition boolbv.h:120
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition boolbv.cpp:94
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
Definition boolbv.h:108
virtual literalt convert_unary_overflow(const unary_overflow_exprt &expr)
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:102
virtual bvt convert_case(const exprt &expr)
virtual bvt convert_symbol(const exprt &expr)
Definition boolbv.cpp:297
virtual bvt convert_update_bit(const update_bit_exprt &)
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_bitreverse(const bitreverse_exprt &expr)
virtual bvt convert_replication(const replication_exprt &expr)
literalt convert_rest(const exprt &expr) override
Definition boolbv.cpp:332
virtual bvt convert_abs(const abs_exprt &expr)
boolbv_mapt map
Definition boolbv.h:123
struct configt::ansi_ct ansi_c
virtual void print_assignment(std::ostream &out) const =0
Print satisfying assignment to out.
void set_to_true(const exprt &)
For a Boolean expression expr, add the constraint 'expr'.
virtual void set_to(const exprt &, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:89
Maps a big-endian offset to a little-endian offset.
Equality.
Definition std_expr.h:1361
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
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:15
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:388
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)
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
virtual literalt land(literalt a, literalt b)=0
virtual void set_frozen(literalt)
Definition prop.h:117
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition prop.cpp:30
virtual literalt new_variable()=0
Structure type, corresponds to C style structs.
Definition std_types.h:231
const componentst & components() const
Definition std_types.h:147
std::vector< componentt > componentst
Definition std_types.h:140
const irep_idt & get_identifier() const
Definition std_expr.h:160
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:391
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:81
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.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
std::vector< literalt > bvt
Definition literal.h:201
literalt const_literal(bool value)
Definition literal.h:188
const literal_vector_exprt & to_literal_vector_expr(const exprt &expr)
Cast a generic exprt to a literal_vector_exprt.
Magic numbers used throughout the codebase.
const std::size_t MAX_FLATTENED_ARRAY_SIZE
Definition magic.h:11
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#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:437
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition std_expr.h:1895
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition std_expr.h:1598
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:895
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition std_expr.h:556
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1533
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition std_expr.h:1272
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition std_expr.h:1132
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition std_expr.h:3472
const named_term_exprt & to_named_term_expr(const exprt &expr)
Cast an exprt to a named_term_exprt.
Definition std_expr.h:3654
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1660
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition std_expr.h:3379
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2102
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition std_expr.h:1201
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition std_expr.h:1445
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3320
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition std_expr.h:466
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2450
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2933
const empty_union_exprt & to_empty_union_expr(const exprt &expr)
Cast an exprt to an empty_union_exprt.
Definition std_expr.h:1855
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition std_expr.h:2048
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1811
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition std_expr.h:2005
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3037
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2352
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition std_expr.h:2533
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition std_expr.h:1960
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition std_expr.h:2735
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition std_expr.h:514
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1402
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition std_expr.h:621
const string_constantt & to_string_constant(const exprt &expr)
endiannesst endianness
Definition config.h:209