10#ifndef CPROVER_SOLVERS_FLATTENING_BOOLBV_H
11#define CPROVER_SOLVERS_FLATTENING_BOOLBV_H
68 void set_to(
const exprt &expr,
bool value)
override;
131 typedef std::unordered_map<const exprt, bvt, irep_hash>
bv_cachet;
135 const typet &src_type,
const bvt &src,
237 const exprt &new_value,
Theory of Arrays with Extensionality.
Expression to define a mapping from an argument (index) to elements.
Array constructor from single element.
message_handlert & message_handler
void finish_eager_conversion() override
bool get_array_constraints
A base class for binary expressions.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for relations, i.e., binary predicates whose two operands have the same type.
A base class for variable bindings (quantifiers, let, lambda)
std::vector< symbol_exprt > variablest
Reverse the order of bits in a bit-vector.
quantifiert(exprt _expr, literalt _l)
virtual bvt convert_with(const with_exprt &expr)
virtual bvt convert_array(const exprt &expr)
Flatten array.
void convert_with_bv(const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
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
std::size_t scope_counter
virtual bvt convert_constraint_select_one(const exprt &expr)
void convert_update_rec(const exprt::operandst &designator, std::size_t d, const typet &type, std::size_t offset, const exprt &new_value, bvt &bv)
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 &)
std::unordered_map< const exprt, bvt, irep_hash > bv_cachet
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
void finish_eager_conversion_quantifiers()
exprt bv_get(const bvt &bv, const typet &type) const
virtual bvt convert_mod(const mod_exprt &expr)
virtual bvt convert_add_sub(const exprt &expr)
virtual bvt convert_constant(const constant_exprt &expr)
numberingt< irep_idt > string_numbering
virtual literalt convert_quantifier(const quantifier_exprt &expr)
boolbvt(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
virtual exprt bv_get_unbounded_array(const exprt &) const
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset) const
void clear_cache() override
virtual bvt convert_mult(const mult_exprt &expr)
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 &)
void convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
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)
const boolbv_mapt & get_map() const
std::list< quantifiert > quantifier_listt
unbounded_arrayt unbounded_array
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
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)
exprt bv_get_cache(const exprt &expr) const
virtual bvt convert_extractbits(const extractbits_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
virtual bvt convert_update(const update_exprt &)
void finish_eager_conversion() override
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
virtual bvt convert_div(const div_exprt &expr)
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
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 &)
void convert_with_union(const union_typet &type, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
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.
quantifier_listt quantifier_list
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)
void convert_with_array(const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
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)
mp_integer get_value(const bvt &bv)
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
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
std::vector< std::size_t > offset_mapt
virtual bvt convert_abs(const abs_exprt &expr)
The byte swap expression.
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Complex constructor from a pair of numbers.
Imaginary part of the expression describing a complex number.
Real part of the expression describing a complex number.
Concatenation of bit-vector operands.
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
A constant literal expression.
Union constructor to support unions without any member (a GCC/Clang feature).
Maps a big-endian offset to a little-endian offset.
Base class for all expressions.
std::vector< exprt > operandst
Semantic type conversion from/to floating-point formats.
Application of (mathematical) function.
virtual void finish_eager_conversion()
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
The trinary if-then-else operator.
Extract member of struct or union.
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Binary multiplication Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
virtual void clear_cache()
A base class for quantifier expressions.
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
Semantic type conversion.
The type of an expression, extends irept.
Generic base class for unary expressions.
The unary minus expression.
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Union constructor from single element.
Operator to update elements in structs and arrays.
Operator to update elements in structs and arrays.
std::vector< literalt > bvt
nonstd::optional< T > optionalt