Go to the documentation of this file.
10 #ifndef CPROVER_SOLVERS_FLATTENING_BOOLBV_H
11 #define CPROVER_SOLVERS_FLATTENING_BOOLBV_H
41 :
arrayst(_ns, _prop, message_handler),
58 void set_to(
const exprt &expr,
bool value)
override;
120 typedef std::unordered_map<const exprt, bvt, irep_hash>
bv_cachet;
124 const typet &src_type,
const bvt &src,
225 const exprt &new_value,
233 const std::vector<bool> &unknown,
235 const typet &type)
const;
248 :
expr(std::move(_expr)),
l(std::move(_l))
268 #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H
Operator to update elements in structs and arrays.
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
virtual literalt convert_overflow(const exprt &expr)
unbounded_arrayt unbounded_array
void convert_with_array(const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual bvt convert_member(const member_exprt &expr)
std::unordered_map< const exprt, bvt, irep_hash > bv_cachet
virtual literalt convert_bv_rel(const binary_relation_exprt &)
Flatten <, >, <= and >= expressions.
virtual bvt convert_byte_update(const byte_update_exprt &expr)
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
void post_process_quantifiers()
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)
virtual void post_process()
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
virtual bvt convert_cond(const cond_exprt &)
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
The type of an expression, extends irept.
std::vector< literalt > bvt
std::list< quantifiert > quantifier_listt
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)
The trinary if-then-else operator.
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const
void convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
Real part of the expression describing a complex number.
virtual bvt convert_mod(const mod_exprt &expr)
Union constructor from single element.
virtual bvt convert_vector(const vector_exprt &expr)
virtual bvt convert_symbol(const exprt &expr)
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
Base class for all expressions.
Generic base class for unary expressions.
virtual bool literal(const exprt &expr, std::size_t bit, literalt &literal) const
A base class for binary expressions.
virtual literalt convert_onehot(const unary_exprt &expr)
virtual bvt convert_abs(const abs_exprt &expr)
Concatenation of bit-vector operands.
A base class for quantifier expressions.
virtual bvt convert_union(const union_exprt &expr)
Vector constructor from list of elements.
virtual bvt convert_case(const exprt &expr)
virtual bvt convert_add_sub(const exprt &expr)
virtual bvt convert_constant(const constant_exprt &expr)
virtual literalt convert_extractbit(const extractbit_exprt &expr)
virtual bvt convert_concatenation(const concatenation_exprt &expr)
quantifiert(exprt _expr, literalt _l)
Struct constructor from list of elements.
virtual bvt convert_mult(const mult_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void post_process() override
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
Expression classes for byte-level operators.
virtual bvt convert_array(const exprt &expr)
Flatten array.
boolbv_widtht boolbv_width
void conversion_failed(const exprt &expr, bvt &bv)
virtual bvt convert_bv_literals(const exprt &expr)
virtual void clear_cache()
numbering< irep_idt > string_numbering
virtual bvt convert_extractbits(const extractbits_exprt &expr)
Semantic type conversion from/to floating-point formats.
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
Array constructor from single element.
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)
virtual literalt convert_ieee_float_rel(const binary_relation_exprt &)
Application of (mathematical) function.
Binary multiplication Associativity is not specified.
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)
void post_process() override
The unary minus expression.
exprt bv_get_cache(const exprt &expr) const
virtual bvt convert_bv_reduction(const unary_exprt &expr)
void convert_with_union(const union_typet &type, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
std::vector< exprt > operandst
Complex constructor from a pair of numbers.
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...
void clear_cache() override
virtual bvt convert_bswap(const bswap_exprt &expr)
nonstd::optional< T > optionalt
mp_integer get_value(const bvt &bv)
virtual exprt make_free_bv_expr(const typet &type)
Operator to update elements in structs and arrays.
quantifier_listt quantifier_list
virtual exprt bv_get_unbounded_array(const exprt &) const
Extract member of struct or union.
virtual bvt convert_let(const let_exprt &)
virtual bvt convert_bitwise(const exprt &expr)
const boolbv_mapt & get_map() const
virtual bvt convert_floatbv_op(const ieee_float_op_exprt &)
Theory of Arrays with Extensionality.
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Structure type, corresponds to C style structs.
virtual bvt convert_struct(const struct_exprt &expr)
exprt bv_get(const bvt &bv, const typet &type) const
void convert_with_bv(const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
A base class for relations, i.e., binary predicates whose two operands have the same type.
Imaginary part of the expression describing a complex number.
virtual literalt convert_equality(const equal_exprt &expr)
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
The byte swap expression.
virtual bvt convert_replication(const replication_exprt &expr)
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)
Semantic type conversion.
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)
A constant literal expression.
boolbvt(const namespacet &_ns, propt &_prop, message_handlert &message_handler)
virtual bvt convert_function_application(const function_application_exprt &expr)
virtual bvt convert_div(const div_exprt &expr)
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.
virtual bvt convert_update(const update_exprt &)
virtual bvt convert_with(const with_exprt &expr)
virtual bvt convert_complex_imag(const complex_imag_exprt &expr)