31 const bool little_endian =
41 std::optional<std::size_t> expected_width)
44 std::pair<bv_cachet::iterator, bool> cache_result=
48 auto &cache_entry = cache_result.first->second;
50 if(!cache_result.second)
62 !expected_width || cache_entry.size() == *expected_width,
63 "bitvector width shall match the indicated expected width",
68 for(
const auto &literal : cache_entry)
71 prop.set_frozen(literal);
75 "variable number must be different from the unused variable number",
85 if(expr.
type().
id() == ID_bool)
100 return prop.new_variables(width);
113 if(expr.
id()==ID_index)
115 else if(expr.
id()==ID_constraint_select_one)
117 else if(expr.
id()==ID_member)
119 else if(expr.
id()==ID_with)
121 else if(expr.
id()==ID_update)
123 else if(expr.
id() == ID_update_bit)
125 else if(expr.
id()==ID_case)
127 else if(expr.
id()==ID_cond)
129 else if(expr.
id()==ID_if)
133 else if(expr.
id()==ID_typecast)
135 else if(expr.
id()==ID_symbol)
137 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
138 expr.
id()==
"no-overflow-plus" ||
139 expr.
id()==
"no-overflow-minus")
141 else if(expr.
id() == ID_mult)
143 else if(expr.
id()==ID_div)
145 else if(expr.
id()==ID_mod)
147 else if(expr.
id()==ID_shl || expr.
id()==ID_ashr || expr.
id()==ID_lshr ||
148 expr.
id()==ID_rol || expr.
id()==ID_ror)
151 expr.
id() == ID_floatbv_plus || expr.
id() == ID_floatbv_minus ||
152 expr.
id() == ID_floatbv_mult || expr.
id() == ID_floatbv_div)
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_floatbv_round_to_integral)
165 else if(expr.
id()==ID_concatenation)
167 else if(expr.
id()==ID_replication)
169 else if(expr.
id()==ID_extractbits)
171 else if(expr.
id() == ID_zero_extend)
173 else if(expr.
id()==ID_bitnot || expr.
id()==ID_bitand ||
174 expr.
id()==ID_bitor || expr.
id()==ID_bitxor ||
175 expr.
id()==ID_bitxnor || expr.
id()==ID_bitnor ||
176 expr.
id()==ID_bitnand)
178 else if(expr.
id() == ID_unary_minus)
180 else if(expr.
id()==ID_unary_plus)
184 else if(expr.
id()==ID_abs)
186 else if(expr.
id() == ID_bswap)
188 else if(expr.
id()==ID_byte_extract_little_endian ||
189 expr.
id()==ID_byte_extract_big_endian)
191 else if(expr.
id()==ID_byte_update_little_endian ||
192 expr.
id()==ID_byte_update_big_endian)
194 else if(expr.
id()==ID_nondet_symbol ||
195 expr.
id()==
"quant_symbol")
197 else if(expr.
id()==ID_struct)
199 else if(expr.
id()==ID_union)
201 else if(expr.
id() == ID_empty_union)
203 else if(expr.
id()==ID_string_constant)
206 else if(expr.
id() == ID_named_term)
212 else if(expr.
id()==ID_array)
214 else if(expr.
id()==ID_complex)
216 else if(expr.
id()==ID_complex_real)
218 else if(expr.
id()==ID_complex_imag)
220 else if(expr.
id() == ID_array_comprehension)
222 else if(expr.
id()==ID_array_of)
224 else if(expr.
id()==ID_let)
226 else if(expr.
id()==ID_function_application)
229 else if(expr.
id()==ID_reduction_or || expr.
id()==ID_reduction_and ||
230 expr.
id()==ID_reduction_nor || expr.
id()==ID_reduction_nand ||
231 expr.
id()==ID_reduction_xor || expr.
id()==ID_reduction_xnor)
233 else if(expr.
id()==ID_not)
235 else if(expr.
id()==ID_power)
237 else if(expr.
id() == ID_popcount)
239 else if(expr.
id() == ID_count_leading_zeros)
244 else if(expr.
id() == ID_count_trailing_zeros)
249 else if(expr.
id() == ID_bitreverse)
251 else if(expr.
id() == ID_saturating_minus || expr.
id() == ID_saturating_plus)
254 const auto overflow_with_result =
259 else if(expr.
id() == ID_find_first_set)
261 else if(expr.
id() == ID_literal_vector)
289 size * tmp.size() == width,
290 "total bitvector width shall equal the number of operands times the size "
295 for(std::size_t j=0; j<tmp.size(); j++)
307 const irep_idt &identifier = expr.
get(ID_identifier);
310 bvt bv =
map.get_literals(identifier, type, width);
317 return l.var_no() < prop.no_variables() || l.is_constant();
319 "variable number of non-constant literals should be within bounds",
341 if(expr.
id()==ID_typecast)
343 else if(expr.
id()==ID_equal)
345 else if(expr.
id()==ID_verilog_case_equality ||
346 expr.
id()==ID_verilog_case_inequality)
348 else if(expr.
id()==ID_notequal)
352 equal_exprt(notequal_expr.lhs(), notequal_expr.rhs()));
354 else if(expr.
id()==ID_ieee_float_equal ||
355 expr.
id()==ID_ieee_float_notequal)
359 else if(expr.
id()==ID_le || expr.
id()==ID_ge ||
360 expr.
id()==ID_lt || expr.
id()==ID_gt)
364 else if(expr.
id()==ID_extractbit)
366 else if(expr.
id()==ID_forall)
368 else if(expr.
id()==ID_exists)
370 else if(expr.
id()==ID_let)
375 "convert_let must return 1-bit vector for boolean let");
379 else if(expr.
id()==ID_index)
385 else if(expr.
id()==ID_member)
391 else if(expr.
id()==ID_case)
397 else if(expr.
id()==ID_cond)
403 else if(expr.
id()==ID_sign)
408 const irep_idt type_id = op.type().id();
409 if(type_id == ID_signedbv || type_id == ID_fixedbv || type_id == ID_floatbv)
410 return bv[bv.size()-1];
411 if(type_id == ID_unsignedbv)
414 else if(expr.
id()==ID_reduction_or || expr.
id()==ID_reduction_and ||
415 expr.
id()==ID_reduction_nor || expr.
id()==ID_reduction_nand ||
416 expr.
id()==ID_reduction_xor || expr.
id()==ID_reduction_xnor)
418 else if(expr.
id() == ID_onehot)
420 else if(expr.
id() == ID_onehot0)
423 const auto binary_overflow =
429 const auto unary_overflow =
434 else if(expr.
id()==ID_isnan)
439 if(op.type().id() == ID_floatbv)
442 return float_utils.
is_NaN(bv);
444 else if(op.type().id() == ID_fixedbv)
447 else if(expr.
id()==ID_isfinite)
452 if(op.type().id() == ID_floatbv)
459 else if(op.id() == ID_fixedbv)
462 else if(expr.
id()==ID_isinf)
467 if(op.type().id() == ID_floatbv)
472 else if(op.type().id() == ID_fixedbv)
475 else if(expr.
id()==ID_isnormal)
479 if(op.type().id() == ID_floatbv)
485 else if(op.type().id() == ID_fixedbv)
488 else if(expr.
id() == ID_function_application)
491 return prop.new_variable();
505 expr.
lhs().
id() == ID_symbol && type == expr.
rhs().
type() &&
506 type.
id() != ID_bool)
517 map.set_literals(identifier, type, bv1);
540 if(type.
id()!=ID_array)
546 const auto &size_opt =
bv_width.get_width_opt(type);
547 if(!size_opt.has_value())
563 result.reserve(binding.
variables().size());
565 for(
const auto &binding : binding.
variables())
567 const auto &old_identifier = binding.get_identifier();
574 result.emplace_back(new_identifier, binding.
type());
590 dest.reserve(components.size());
591 std::size_t offset = 0;
592 for(
const auto &comp : components)
594 dest.push_back(offset);
API to expression classes for bitvectors.
const onehot0_exprt & to_onehot0_expr(const exprt &expr)
Cast an exprt to a onehot0_exprt.
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 onehot_exprt & to_onehot_expr(const exprt &expr)
Cast an exprt to a onehot_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 zero_extend_exprt & to_zero_extend_expr(const exprt &expr)
Cast an exprt to a zero_extend_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.
const array_typet & type() const
const symbol_exprt & arg() const
const exprt & size() const
A base class for variable bindings (quantifiers, let, lambda)
exprt instantiate(const exprt::operandst &) const
substitute free occurrences of the variables in where() by the given values
std::vector< symbol_exprt > variablest
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.
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...
std::size_t scope_counter
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)
virtual bvt convert_bitvector(const exprt &expr)
Converts an expression into its gate-level representation and returns a vector of literals correspond...
binding_exprt::variablest fresh_binding(const binding_exprt &)
create new, unique variables for the given binding
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
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)
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...
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)
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)
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'.
virtual bvt convert_byte_update(const byte_update_exprt &expr)
virtual literalt convert_extractbit(const extractbit_exprt &expr)
unbounded_arrayt unbounded_array
virtual bvt convert_floatbv_op(const ieee_float_op_exprt &)
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
virtual bvt convert_not(const not_exprt &expr)
virtual bvt convert_extractbits(const extractbits_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
virtual bvt convert_update(const update_exprt &)
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
virtual bvt convert_div(const div_exprt &expr)
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 &)
virtual bvt convert_bv_reduction(const unary_exprt &expr)
virtual literalt convert_equality(const equal_exprt &expr)
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
virtual literalt convert_unary_overflow(const unary_overflow_exprt &expr)
virtual std::size_t boolbv_width(const typet &type) const
virtual bvt convert_case(const exprt &expr)
virtual bvt convert_symbol(const exprt &expr)
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
virtual bvt convert_floatbv_round_to_integral(const floatbv_round_to_integral_exprt &)
std::vector< std::size_t > offset_mapt
virtual bvt convert_abs(const abs_exprt &expr)
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'.
Maps a big-endian offset to a little-endian offset.
Base class for all expressions.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
bool is_boolean() const
Return whether the expression represents a Boolean.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
literalt is_NaN(const bvt &)
literalt is_infinity(const bvt &)
literalt is_normal(const bvt &)
Application of (mathematical) function.
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
static var_not unused_var_no()
void set_frozen(literalt)
bool equality_propagation
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...
Structure type, corresponds to C style structs.
const componentst & components() const
std::vector< componentt > componentst
const irep_idt & get_identifier() const
The type of an expression, extends irept.
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.
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_round_to_integral_exprt & to_floatbv_round_to_integral_expr(const exprt &expr)
Cast an exprt to a floatbv_round_to_integral_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)
std::vector< literalt > bvt
literalt const_literal(bool value)
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
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)
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#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...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
const named_term_exprt & to_named_term_expr(const exprt &expr)
Cast an exprt to a named_term_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const empty_union_exprt & to_empty_union_expr(const exprt &expr)
Cast an exprt to an empty_union_exprt.
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
const string_constantt & to_string_constant(const exprt &expr)