10 #ifndef CPROVER_SOLVERS_FLATTENING_BOOLBV_H 11 #define CPROVER_SOLVERS_FLATTENING_BOOLBV_H 51 void set_to(
const exprt &expr,
bool value)
override;
115 typedef std::unordered_map<const exprt, bvt, irep_hash>
bv_cachet;
119 const typet &src_type,
const bvt &src,
220 const exprt &new_value,
227 const std::vector<bool> &unknown,
229 const typet &type)
const;
257 #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H boolbvt(const namespacet &_ns, propt &_prop)
virtual bvt convert_case(const exprt &expr)
virtual bvt convert_complex_real(const exprt &expr)
The type of an expression.
void print_assignment(std::ostream &out) const override
std::vector< std::size_t > offset_mapt
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
virtual bvt convert_with(const exprt &expr)
virtual bvt convert_concatenation(const exprt &expr)
virtual bvt convert_abs(const exprt &expr)
virtual literalt convert_ieee_float_rel(const exprt &expr)
virtual bvt convert_array_of(const array_of_exprt &expr)
virtual bvt convert_bv_reduction(const unary_exprt &expr)
A generic base class for relations, i.e., binary predicates.
application of (mathematical) function
void post_process() override
virtual exprt bv_get_unbounded_array(const exprt &) const
void convert_with_array(const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual literalt convert_onehot(const unary_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
virtual literalt convert_overflow(const exprt &expr)
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
boolbv_widtht boolbv_width
virtual literalt convert_equality(const equal_exprt &expr)
bool is_unbounded_array(const typet &type) const override
virtual bvt convert_replication(const replication_exprt &expr)
virtual bvt convert_bv_literals(const exprt &expr)
virtual bvt convert_struct(const struct_exprt &expr)
virtual bvt convert_function_application(const function_application_exprt &expr)
void clear_cache() override
The trinary if-then-else operator.
virtual bvt convert_lambda(const exprt &expr)
void build_offset_map(const struct_typet &src, offset_mapt &dest)
A constant literal expression.
void post_process() override
virtual bool literal(const exprt &expr, literalt &literal) const
virtual bvt convert_constant(const constant_exprt &expr)
virtual bvt convert_symbol(const exprt &expr)
virtual bvt convert_mult(const exprt &expr)
Extract member of struct or union.
virtual bvt convert_complex(const exprt &expr)
virtual literalt convert_quantifier(const exprt &expr)
virtual bvt convert_update(const exprt &expr)
virtual void clear_cache()
void convert_with_union(const union_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual literalt convert_bv_rel(const exprt &expr)
Expression classes for byte-level operators.
virtual bvt convert_add_sub(const exprt &expr)
division (integer and real)
A generic base class for binary expressions.
virtual literalt convert_reduction(const unary_exprt &expr)
virtual const bvt & convert_bv(const exprt &expr)
Theory of Arrays with Extensionality.
virtual void make_free_bv_expr(const typet &type, exprt &dest)
union constructor from single element
virtual bvt convert_bitvector(const exprt &expr)
virtual bvt convert_floatbv_op(const exprt &expr)
void conversion_failed(const exprt &expr, bvt &bv)
Generic base class for unary expressions.
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
virtual bool literal(const exprt &expr, std::size_t bit, literalt &literal) const
numbering< irep_idt > string_numbering
virtual bvt convert_union(const union_exprt &expr)
array constructor from single element
virtual bvt convert_extractbits(const extractbits_exprt &expr)
quantifier_listt quantifier_list
virtual literalt convert_rest(const exprt &expr) override
virtual bvt convert_complex_imag(const exprt &expr)
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
virtual bvt convert_cond(const exprt &expr)
void post_process_quantifiers()
std::vector< exprt > operandst
virtual bvt convert_not(const not_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)
void convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual bvt convert_byte_update(const byte_update_exprt &expr)
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
mp_integer get_value(const bvt &bv)
virtual bvt convert_constraint_select_one(const exprt &expr)
unbounded_arrayt unbounded_array
virtual bvt convert_vector(const exprt &expr)
void convert_with_bv(const typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual bvt convert_array(const exprt &expr)
virtual void make_bv_expr(const typet &type, const bvt &bv, exprt &dest)
semantic type conversion from/to floating-point formats
Base class for all expressions.
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
virtual exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const
virtual bvt convert_mod(const mod_exprt &expr)
virtual bvt convert_member(const member_exprt &expr)
const boolbv_mapt & get_map() const
virtual bvt convert_if(const if_exprt &expr)
exprt bv_get(const bvt &bv, const typet &type) const
virtual bvt convert_unary_minus(const unary_exprt &expr)
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
exprt bv_get_cache(const exprt &expr) const
virtual bvt convert_div(const div_exprt &expr)
std::list< quantifiert > quantifier_listt
void set_to(const exprt &expr, bool value) override
virtual literalt convert_extractbit(const extractbit_exprt &expr)
struct constructor from list of elements
std::unordered_map< const exprt, bvt, irep_hash > bv_cachet
std::vector< literalt > bvt
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
virtual bvt convert_bitwise(const exprt &expr)
virtual void post_process()
virtual bvt convert_power(const binary_exprt &expr)