Go to the documentation of this file.
34 const std::size_t bit,
37 if(expr.
type().
id()==ID_bool)
41 "boolean expressions shall be represented by a single bit and hence the "
42 "only valid bit index is 0");
47 if(expr.
id()==ID_symbol ||
48 expr.
id()==ID_nondet_symbol)
52 boolbv_mapt::mappingt::const_iterator it_m=
61 bit < map_entry.
literal_map.size(),
"bit index shall be within bounds");
68 else if(expr.
id()==ID_index)
75 const auto &index = index_expr.
index();
81 numeric_cast_v<std::size_t>(index_int * element_width);
85 else if(expr.
id()==ID_member)
95 for(
const auto &c : components)
97 const typet &subtype = c.type();
99 if(c.get_name() == component_name)
105 offset+=element_width;
108 INVARIANT(
false,
"struct type should have accessed component");
112 INVARIANT(
false,
"expression should have a corresponding literal");
122 std::pair<bv_cachet::iterator, bool> cache_result=
124 if(!cache_result.second)
126 return cache_result.first->second;
135 !expected_width || bv.size() == *expected_width,
136 "bitvector width shall match the indicated expected width",
140 cache_result.first->second = bv;
150 "variable number must be different from the unused variable number",
155 return cache_result.first->second;
176 if(expr.
type().
id()==ID_bool)
184 if(expr.
id()==ID_index)
186 else if(expr.
id()==ID_constraint_select_one)
188 else if(expr.
id()==ID_member)
190 else if(expr.
id()==ID_with)
192 else if(expr.
id()==ID_update)
194 else if(expr.
id()==ID_width)
209 if(expr.
type().
id()==ID_unsignedbv ||
210 expr.
type().
id()==ID_signedbv)
213 else if(expr.
id()==ID_case)
215 else if(expr.
id()==ID_cond)
217 else if(expr.
id()==ID_if)
219 else if(expr.
id()==ID_constant)
221 else if(expr.
id()==ID_typecast)
223 else if(expr.
id()==ID_symbol)
225 else if(expr.
id()==ID_bv_literals)
227 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
228 expr.
id()==
"no-overflow-plus" ||
229 expr.
id()==
"no-overflow-minus")
231 else if(expr.
id() == ID_mult)
233 else if(expr.
id()==ID_div)
235 else if(expr.
id()==ID_mod)
237 else if(expr.
id()==ID_shl || expr.
id()==ID_ashr || expr.
id()==ID_lshr ||
238 expr.
id()==ID_rol || expr.
id()==ID_ror)
240 else if(expr.
id()==ID_floatbv_plus || expr.
id()==ID_floatbv_minus ||
241 expr.
id()==ID_floatbv_mult || expr.
id()==ID_floatbv_div ||
242 expr.
id()==ID_floatbv_rem)
246 else if(expr.
id()==ID_floatbv_typecast)
248 else if(expr.
id()==ID_concatenation)
250 else if(expr.
id()==ID_replication)
252 else if(expr.
id()==ID_extractbits)
254 else if(expr.
id()==ID_bitnot || expr.
id()==ID_bitand ||
255 expr.
id()==ID_bitor || expr.
id()==ID_bitxor ||
256 expr.
id()==ID_bitxnor || expr.
id()==ID_bitnor ||
257 expr.
id()==ID_bitnand)
259 else if(expr.
id() == ID_unary_minus)
261 else if(expr.
id()==ID_unary_plus)
265 else if(expr.
id()==ID_abs)
267 else if(expr.
id() == ID_bswap)
269 else if(expr.
id()==ID_byte_extract_little_endian ||
270 expr.
id()==ID_byte_extract_big_endian)
272 else if(expr.
id()==ID_byte_update_little_endian ||
273 expr.
id()==ID_byte_update_big_endian)
275 else if(expr.
id()==ID_nondet_symbol ||
276 expr.
id()==
"quant_symbol")
278 else if(expr.
id()==ID_struct)
280 else if(expr.
id()==ID_union)
282 else if(expr.
id()==ID_string_constant)
285 else if(expr.
id()==ID_array)
287 else if(expr.
id()==ID_vector)
289 else if(expr.
id()==ID_complex)
291 else if(expr.
id()==ID_complex_real)
293 else if(expr.
id()==ID_complex_imag)
295 else if(expr.
id() == ID_array_comprehension)
297 else if(expr.
id()==ID_array_of)
299 else if(expr.
id()==ID_let)
301 else if(expr.
id()==ID_function_application)
304 else if(expr.
id()==ID_reduction_or || expr.
id()==ID_reduction_and ||
305 expr.
id()==ID_reduction_nor || expr.
id()==ID_reduction_nand ||
306 expr.
id()==ID_reduction_xor || expr.
id()==ID_reduction_xnor)
308 else if(expr.
id()==ID_not)
310 else if(expr.
id()==ID_power)
312 else if(expr.
id() == ID_popcount)
327 const auto size = numeric_cast<mp_integer>(array_size);
329 if(!size.has_value())
347 *size * tmp.size() == width,
348 "total bitvector width shall equal the number of operands times the size "
351 std::size_t offset = numeric_cast_v<std::size_t>(i * tmp.size());
353 for(std::size_t j=0; j<tmp.size(); j++)
372 if(bv_sub.size()!=width)
373 throw "bv_literals with wrong size";
375 for(std::size_t i=0; i<width; i++)
389 const irep_idt &identifier = expr.
get(ID_identifier);
406 return l.var_no() < prop.no_variables() || l.is_constant();
408 "variable number of non-constant literals should be within bounds",
431 if(expr.
id()==ID_typecast)
433 else if(expr.
id()==ID_equal)
435 else if(expr.
id()==ID_verilog_case_equality ||
436 expr.
id()==ID_verilog_case_inequality)
438 else if(expr.
id()==ID_notequal)
442 equal_exprt(notequal_expr.lhs(), notequal_expr.rhs()));
444 else if(expr.
id()==ID_ieee_float_equal ||
445 expr.
id()==ID_ieee_float_notequal)
449 else if(expr.
id()==ID_le || expr.
id()==ID_ge ||
450 expr.
id()==ID_lt || expr.
id()==ID_gt)
454 else if(expr.
id()==ID_extractbit)
456 else if(expr.
id()==ID_forall)
458 else if(expr.
id()==ID_exists)
460 else if(expr.
id()==ID_let)
465 "convert_let must return 1-bit vector for boolean let");
469 else if(expr.
id()==ID_index)
475 else if(expr.
id()==ID_member)
481 else if(expr.
id()==ID_case)
487 else if(expr.
id()==ID_cond)
493 else if(expr.
id()==ID_sign)
498 const irep_idt type_id = op.type().id();
499 if(type_id == ID_signedbv || type_id == ID_fixedbv || type_id == ID_floatbv)
500 return bv[bv.size()-1];
501 if(type_id == ID_unsignedbv)
504 else if(expr.
id()==ID_reduction_or || expr.
id()==ID_reduction_and ||
505 expr.
id()==ID_reduction_nor || expr.
id()==ID_reduction_nand ||
506 expr.
id()==ID_reduction_xor || expr.
id()==ID_reduction_xnor)
508 else if(expr.
id()==ID_onehot || expr.
id()==ID_onehot0)
512 else if(expr.
id()==ID_isnan)
517 if(op.type().id() == ID_floatbv)
520 return float_utils.
is_NaN(bv);
522 else if(op.type().id() == ID_fixedbv)
525 else if(expr.
id()==ID_isfinite)
530 if(op.type().id() == ID_floatbv)
537 else if(op.id() == ID_fixedbv)
540 else if(expr.
id()==ID_isinf)
545 if(op.type().id() == ID_floatbv)
550 else if(op.type().id() == ID_fixedbv)
553 else if(expr.
id()==ID_isnormal)
557 if(op.type().id() == ID_floatbv)
563 else if(op.type().id() == ID_fixedbv)
578 expr.
lhs().
id() == ID_symbol && type == expr.
rhs().
type() &&
579 type.
id() != ID_bool)
605 const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr);
613 exprt dest(ID_bv_literals, type);
615 bv_sub.resize(bv.size());
617 for(std::size_t i=0; i<bv.size(); i++)
634 if(type.
id()!=ID_array)
642 const auto s = numeric_cast<mp_integer>(size);
657 out << pair.first <<
"=" << pair.second.get_value(
prop) <<
'\n';
664 dest.reserve(components.size());
665 std::size_t offset = 0;
666 for(
const auto &comp : components)
668 dest.push_back(offset);
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const componentst & components() const
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual literalt convert_overflow(const exprt &expr)
unbounded_arrayt unbounded_array
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
bool equality_propagation
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
virtual bvt convert_member(const member_exprt &expr)
virtual literalt convert_bv_rel(const binary_relation_exprt &)
Flatten <, >, <= and >= expressions.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
virtual bvt convert_byte_update(const byte_update_exprt &expr)
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
virtual bvt convert_array_of(const array_of_exprt &expr)
Flatten arrays constructed from a single element.
virtual literalt convert_reduction(const unary_exprt &expr)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
virtual bvt convert_cond(const cond_exprt &)
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
virtual bvt convert_bitvector(const exprt &expr)
Converts an expression into its gate-level representation and returns a vector of literals correspond...
bool is_unbounded_array(const typet &type) const override
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
std::vector< literalt > bvt
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
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'.
virtual bvt convert_complex(const complex_exprt &expr)
irept & add(const irep_namet &name)
const std::size_t MAX_FLATTENED_ARRAY_SIZE
const irept & find(const irep_namet &name) const
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
virtual bvt convert_mod(const mod_exprt &expr)
const string_constantt & to_string_constant(const exprt &expr)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
virtual bvt convert_vector(const vector_exprt &expr)
virtual bvt convert_symbol(const exprt &expr)
virtual literalt new_variable()=0
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
Base class for all expressions.
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
std::vector< componentt > componentst
virtual bool literal(const exprt &expr, std::size_t bit, literalt &literal) const
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
virtual literalt convert_onehot(const unary_exprt &expr)
virtual bvt convert_abs(const abs_exprt &expr)
const symbol_exprt & arg() const
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
virtual bvt convert_union(const union_exprt &expr)
virtual bvt convert_case(const exprt &expr)
#define forall_literals(it, bv)
virtual literalt land(literalt a, literalt b)=0
Magic numbers used throughout the codebase.
const array_typet & type() const
virtual bvt convert_add_sub(const exprt &expr)
virtual bvt convert_constant(const constant_exprt &expr)
static var_not unused_var_no()
virtual literalt convert_extractbit(const extractbit_exprt &expr)
virtual bvt convert_concatenation(const concatenation_exprt &expr)
virtual void ignoring(const exprt &expr)
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
literalt is_infinity(const bvt &)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
#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...
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const exprt & size() const
virtual bvt convert_mult(const mult_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
typet & type()
Return the type of the expression.
bool literal(const symbol_exprt &expr, literalt &literal) const
void set_frozen(literalt)
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
virtual bvt convert_array(const exprt &expr)
Flatten array.
boolbv_widtht boolbv_width
literalt is_normal(const bvt &)
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
void record(const function_application_exprt &function_application)
void conversion_failed(const exprt &expr, bvt &bv)
virtual bvt convert_bv_literals(const exprt &expr)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
virtual bvt convert_extractbits(const extractbits_exprt &expr)
const std::string & id2string(const irep_idt &d)
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const exprt & struct_op() const
#define PRECONDITION(CONDITION)
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
const irep_idt & get_identifier() const
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
virtual bvt convert_if(const if_exprt &expr)
virtual bvt convert_complex_real(const complex_real_exprt &expr)
virtual exprt make_bv_expr(const typet &type, const bvt &bv)
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
virtual literalt convert_ieee_float_rel(const binary_relation_exprt &)
const std::string & id_string() const
const exprt & body() const
Application of (mathematical) function.
literalt const_literal(bool value)
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
virtual bvt convert_bv_reduction(const unary_exprt &expr)
literalt is_NaN(const bvt &)
const irep_idt & id() const
virtual void set_frozen(literalt)
virtual bvt convert_constraint_select_one(const exprt &expr)
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...
virtual bvt convert_bswap(const bswap_exprt &expr)
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
nonstd::optional< T > optionalt
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
virtual exprt make_free_bv_expr(const typet &type)
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
virtual literalt convert_rest(const exprt &expr)
Extract member of struct or union.
virtual bvt convert_let(const let_exprt &)
virtual bvt convert_bitwise(const exprt &expr)
bvt build_constant(const mp_integer &i, std::size_t width)
virtual bvt convert_floatbv_op(const ieee_float_op_exprt &)
Structure type, corresponds to C style structs.
virtual bvt convert_struct(const struct_exprt &expr)
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const irep_idt & get(const irep_namet &name) const
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
unsigned unsafe_string2unsigned(const std::string &str, int base)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
virtual literalt convert_equality(const equal_exprt &expr)
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
virtual bvt convert_replication(const replication_exprt &expr)
bool has_prefix(const std::string &s, const std::string &prefix)
irep_idt get_component_name() const
virtual literalt convert_quantifier(const quantifier_exprt &expr)
virtual bvt convert_array_comprehension(const array_comprehension_exprt &)
virtual bvt convert_not(const not_exprt &expr)
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
std::vector< std::size_t > offset_mapt
offset_mapt build_offset_map(const struct_typet &src)
Expression to define a mapping from an argument (index) to elements.
literalt convert_rest(const exprt &expr) override
virtual bvt convert_power(const binary_exprt &expr)
API to expression classes.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
virtual bvt convert_function_application(const function_application_exprt &expr)
virtual bvt convert_div(const div_exprt &expr)
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'current_context => expr' if value is true,...
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
virtual bvt convert_update(const update_exprt &)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
virtual bvt convert_with(const with_exprt &expr)
virtual bvt convert_complex_imag(const complex_imag_exprt &expr)