cprover
|
#include <boolbv.h>
Classes | |
class | quantifiert |
Public Types | |
enum | unbounded_arrayt { unbounded_arrayt::U_NONE, unbounded_arrayt::U_ALL, unbounded_arrayt::U_AUTO } |
![]() | |
typedef equalityt | SUB |
![]() | |
typedef std::map< irep_idt, literalt > | symbolst |
typedef std::unordered_map< exprt, literalt, irep_hash > | cachet |
![]() | |
enum | resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR } |
Public Member Functions | |
boolbvt (const namespacet &_ns, propt &_prop) | |
virtual const bvt & | convert_bv (const exprt &expr) |
virtual bvt | convert_bitvector (const exprt &expr) |
exprt | get (const exprt &expr) const override |
void | set_to (const exprt &expr, bool value) override |
void | print_assignment (std::ostream &out) const override |
void | clear_cache () override |
void | post_process () override |
virtual bool | literal (const exprt &expr, std::size_t bit, literalt &literal) const |
mp_integer | get_value (const bvt &bv) |
mp_integer | get_value (const bvt &bv, std::size_t offset, std::size_t width) |
const boolbv_mapt & | get_map () const |
![]() | |
arrayst (const namespacet &_ns, propt &_prop) | |
literalt | record_array_equality (const equal_exprt &expr) |
void | record_array_index (const index_exprt &expr) |
![]() | |
equalityt (const namespacet &_ns, propt &_prop) | |
virtual literalt | equality (const exprt &e1, const exprt &e2) |
void | post_process () override |
![]() | |
prop_conv_solvert (const namespacet &_ns, propt &_prop) | |
virtual | ~prop_conv_solvert () |
virtual decision_proceduret::resultt | dec_solve () override |
virtual std::string | decision_procedure_text () const override |
virtual tvt | l_get (literalt a) const override |
virtual void | set_frozen (literalt a) override |
virtual void | set_assumptions (const bvt &_assumptions) override |
virtual bool | has_set_assumptions () const override |
virtual void | set_all_frozen () override |
virtual literalt | convert (const exprt &expr) override |
virtual bool | is_in_conflict (literalt l) const override |
determine whether a variable is in the final conflict More... | |
virtual bool | has_is_in_conflict () const override |
virtual bool | literal (const exprt &expr, literalt &literal) const |
const cachet & | get_cache () const |
const symbolst & | get_symbols () const |
![]() | |
prop_convt (const namespacet &_ns) | |
virtual | ~prop_convt () |
literalt | operator() (const exprt &expr) |
virtual void | set_frozen (const bvt &) |
![]() | |
decision_proceduret (const namespacet &_ns) | |
void | set_to_true (const exprt &expr) |
void | set_to_false (const exprt &expr) |
resultt | operator() () |
virtual bool | in_core (const exprt &expr) |
Public Attributes | |
unbounded_arrayt | unbounded_array |
boolbv_widtht | boolbv_width |
![]() | |
bool | use_cache |
bool | equality_propagation |
bool | freeze_all |
Protected Types | |
typedef arrayst | SUB |
typedef std::unordered_map< const exprt, bvt, irep_hash > | bv_cachet |
typedef std::list< quantifiert > | quantifier_listt |
typedef std::vector< std::size_t > | offset_mapt |
![]() | |
enum | lazy_typet { lazy_typet::ARRAY_ACKERMANN, lazy_typet::ARRAY_WITH, lazy_typet::ARRAY_IF, lazy_typet::ARRAY_OF, lazy_typet::ARRAY_TYPECAST } |
typedef std::list< array_equalityt > | array_equalitiest |
typedef std::set< exprt > | index_sett |
typedef std::map< std::size_t, index_sett > | index_mapt |
![]() | |
typedef std::unordered_map< const exprt, unsigned, irep_hash > | elementst |
typedef std::map< std::pair< unsigned, unsigned >, literalt > | equalitiest |
typedef std::map< unsigned, exprt > | elements_revt |
typedef std::unordered_map< const typet, typestructt, irep_hash > | typemapt |
Protected Member Functions | |
virtual literalt | convert_rest (const exprt &expr) override |
virtual bool | boolbv_set_equality_to_true (const equal_exprt &expr) |
void | conversion_failed (const exprt &expr, bvt &bv) |
bvt | conversion_failed (const exprt &expr) |
bool | type_conversion (const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest) |
virtual literalt | convert_bv_rel (const exprt &expr) |
virtual literalt | convert_typecast (const typecast_exprt &expr) |
conversion from bitvector types to boolean More... | |
virtual literalt | convert_reduction (const unary_exprt &expr) |
virtual literalt | convert_onehot (const unary_exprt &expr) |
virtual literalt | convert_extractbit (const extractbit_exprt &expr) |
virtual literalt | convert_overflow (const exprt &expr) |
virtual literalt | convert_equality (const equal_exprt &expr) |
virtual literalt | convert_verilog_case_equality (const binary_relation_exprt &expr) |
virtual literalt | convert_ieee_float_rel (const exprt &expr) |
virtual literalt | convert_quantifier (const exprt &expr) |
virtual bvt | convert_index (const exprt &array, const mp_integer &index) |
index operator with constant index More... | |
virtual bvt | convert_index (const index_exprt &expr) |
virtual bvt | convert_byte_extract (const byte_extract_exprt &expr) |
virtual bvt | convert_byte_update (const byte_update_exprt &expr) |
virtual bvt | convert_constraint_select_one (const exprt &expr) |
virtual bvt | convert_if (const if_exprt &expr) |
virtual bvt | convert_struct (const struct_exprt &expr) |
virtual bvt | convert_array (const exprt &expr) |
virtual bvt | convert_vector (const exprt &expr) |
virtual bvt | convert_complex (const exprt &expr) |
virtual bvt | convert_complex_real (const exprt &expr) |
virtual bvt | convert_complex_imag (const exprt &expr) |
virtual bvt | convert_lambda (const exprt &expr) |
virtual bvt | convert_array_of (const array_of_exprt &expr) |
virtual bvt | convert_union (const union_exprt &expr) |
virtual bvt | convert_bv_typecast (const typecast_exprt &expr) |
virtual bvt | convert_add_sub (const exprt &expr) |
virtual bvt | convert_mult (const exprt &expr) |
virtual bvt | convert_div (const div_exprt &expr) |
virtual bvt | convert_mod (const mod_exprt &expr) |
virtual bvt | convert_floatbv_op (const exprt &expr) |
virtual bvt | convert_floatbv_typecast (const floatbv_typecast_exprt &expr) |
virtual bvt | convert_member (const member_exprt &expr) |
virtual bvt | convert_with (const exprt &expr) |
virtual bvt | convert_update (const exprt &expr) |
virtual bvt | convert_case (const exprt &expr) |
virtual bvt | convert_cond (const exprt &expr) |
virtual bvt | convert_shift (const binary_exprt &expr) |
virtual bvt | convert_bitwise (const exprt &expr) |
virtual bvt | convert_unary_minus (const unary_exprt &expr) |
virtual bvt | convert_abs (const exprt &expr) |
virtual bvt | convert_concatenation (const exprt &expr) |
virtual bvt | convert_replication (const replication_exprt &expr) |
virtual bvt | convert_bv_literals (const exprt &expr) |
virtual bvt | convert_constant (const constant_exprt &expr) |
virtual bvt | convert_extractbits (const extractbits_exprt &expr) |
virtual bvt | convert_symbol (const exprt &expr) |
virtual bvt | convert_bv_reduction (const unary_exprt &expr) |
virtual bvt | convert_not (const not_exprt &expr) |
virtual bvt | convert_power (const binary_exprt &expr) |
virtual bvt | convert_function_application (const function_application_exprt &expr) |
virtual void | make_bv_expr (const typet &type, const bvt &bv, exprt &dest) |
virtual void | make_free_bv_expr (const typet &type, exprt &dest) |
void | convert_with (const typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_bv (const typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_array (const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_union (const union_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
void | convert_with_struct (const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv) |
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 exprt | bv_get_unbounded_array (const exprt &) const |
virtual exprt | bv_get_rec (const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const |
exprt | bv_get (const bvt &bv, const typet &type) const |
exprt | bv_get_cache (const exprt &expr) const |
bool | is_unbounded_array (const typet &type) const override |
void | post_process_quantifiers () |
void | build_offset_map (const struct_typet &src, offset_mapt &dest) |
![]() | |
virtual void | post_process_arrays () |
void | add_array_constraint (const lazy_constraintt &lazy, bool refine=true) |
adds array constraints (refine=true...lazily for the refinement loop) More... | |
void | add_array_constraints () |
void | add_array_Ackermann_constraints () |
void | add_array_constraints_equality (const index_sett &index_set, const array_equalityt &array_equality) |
void | add_array_constraints (const index_sett &index_set, const exprt &expr) |
void | add_array_constraints_if (const index_sett &index_set, const if_exprt &exprt) |
void | add_array_constraints_with (const index_sett &index_set, const with_exprt &expr) |
void | add_array_constraints_update (const index_sett &index_set, const update_exprt &expr) |
void | add_array_constraints_array_of (const index_sett &index_set, const array_of_exprt &exprt) |
void | update_index_map (bool update_all) |
void | update_index_map (std::size_t i) |
merge the indices into the root More... | |
void | collect_arrays (const exprt &a) |
void | collect_indices () |
void | collect_indices (const exprt &a) |
![]() | |
virtual literalt | equality2 (const exprt &e1, const exprt &e2) |
virtual void | add_equality_constraints () |
virtual void | add_equality_constraints (const typestructt &typestruct) |
![]() | |
virtual bool | get_bool (const exprt &expr, tvt &value) const |
get a boolean value from counter example if not valid More... | |
virtual literalt | convert_bool (const exprt &expr) |
virtual bool | set_equality_to_true (const equal_exprt &expr) |
virtual literalt | get_literal (const irep_idt &symbol) |
virtual void | ignoring (const exprt &expr) |
Protected Attributes | |
bv_utilst | bv_utils |
functionst | functions |
boolbv_mapt | map |
bv_cachet | bv_cache |
quantifier_listt | quantifier_list |
numbering< irep_idt > | string_numbering |
![]() | |
array_equalitiest | array_equalities |
union_find< exprt > | arrays |
index_mapt | index_map |
bool | lazy_arrays |
bool | incremental_cache |
std::list< lazy_constraintt > | lazy_array_constraints |
std::map< exprt, bool > | expr_map |
std::set< std::size_t > | update_indices |
![]() | |
typemapt | typemap |
![]() | |
bool | post_processing_done |
symbolst | symbols |
cachet | cache |
propt & | prop |
![]() | |
const namespacet & | ns |
Additional Inherited Members |
|
protected |
|
protected |
|
protected |
|
protected |
|
strong |
|
inline |
Definition at line 34 of file boolbv.h.
References convert_bitvector(), convert_bv(), print_assignment(), and set_to().
|
protectedvirtual |
Reimplemented in string_refinementt.
Definition at line 590 of file boolbv.cpp.
References convert_bv(), prop_conv_solvert::equality_propagation, namespace_baset::follow(), prop_conv_solvert::freeze_all, irept::id(), is_unbounded_array(), binary_relation_exprt::lhs(), map, decision_proceduret::ns, binary_relation_exprt::rhs(), prop_conv_solvert::set_frozen(), boolbv_mapt::set_literals(), to_symbol_expr(), and exprt::type().
Referenced by set_to().
|
protected |
Definition at line 708 of file boolbv.cpp.
References boolbv_width, and struct_union_typet::components().
Referenced by type_conversion().
Definition at line 280 of file boolbv_get.cpp.
References bv_get_rec().
Referenced by bv_get_cache().
Definition at line 287 of file boolbv_get.cpp.
References bv_cache, bv_get(), irept::id(), and exprt::type().
Referenced by bv_get_unbounded_array().
|
protectedvirtual |
Reimplemented in bv_pointerst.
Definition at line 68 of file boolbv_get.cpp.
References binary2integer(), boolbv_width, struct_union_typet::components(), namespace_baset::follow(), namespace_baset::follow_tag(), get_bvtype(), irept::get_string(), tvt::get_value(), irept::id(), integer2string(), IS_C_ENUM, IS_RANGE, IS_UNKNOWN, propt::l_get(), decision_proceduret::ns, unary_exprt::op(), exprt::op0(), exprt::op1(), exprt::operands(), prop_conv_solvert::prop, exprt::reserve_operands(), union_exprt::set_component_name(), constant_exprt::set_value(), string2integer(), string_numbering, typet::subtype(), to_struct_tag_type(), to_struct_type(), to_union_tag_type(), to_union_type(), tvt::TV_FALSE, tvt::TV_TRUE, and tvt::TV_UNKNOWN.
Referenced by bv_get(), bv_pointerst::bv_get_rec(), and get().
Definition at line 300 of file boolbv_get.cpp.
References index_exprt::array(), arrayst::arrays, bv_get_cache(), exprt::copy_to_operands(), union_find< T >::find_number(), from_integer(), numbering< T >::get_number(), irept::id(), index_exprt::index(), arrayst::index_map, integer2size_t(), integer2string(), irept::is_nil(), decision_proceduret::ns, exprt::operands(), messaget::result(), irept::set(), simplify_expr(), array_typet::size(), typet::subtype(), to_array_type(), to_integer(), and exprt::type().
Referenced by get().
|
inlineoverridevirtual |
Reimplemented from prop_conv_solvert.
Definition at line 54 of file boolbv.h.
References bv_cache, and prop_conv_solvert::clear_cache().
Definition at line 108 of file boolbv.h.
Referenced by convert_abs(), convert_add_sub(), convert_array(), convert_array_of(), bv_pointerst::convert_bitvector(), convert_bitvector(), convert_bitwise(), convert_bv_literals(), convert_bv_reduction(), convert_bv_typecast(), convert_byte_extract(), convert_case(), convert_complex(), convert_complex_imag(), convert_complex_real(), convert_concatenation(), convert_cond(), convert_constant(), convert_constraint_select_one(), convert_div(), convert_extractbits(), convert_floatbv_op(), convert_floatbv_typecast(), convert_index(), convert_lambda(), convert_mod(), convert_mult(), convert_not(), bv_pointerst::convert_pointer_type(), convert_power(), convert_replication(), convert_shift(), convert_unary_minus(), convert_union(), convert_update(), convert_vector(), and convert_with().
Definition at line 145 of file boolbv.cpp.
References boolbv_width, prop_conv_solvert::ignoring(), propt::new_variables(), prop_conv_solvert::prop, and exprt::type().
Definition at line 17 of file boolbv_abs.cpp.
References float_utilst::abs(), bv_utilst::absolute_value(), boolbv_width, bv_utils, conversion_failed(), convert_bv(), get_bvtype(), IS_FIXED, IS_FLOAT, IS_SIGNED, IS_UNSIGNED, exprt::op0(), exprt::operands(), prop_conv_solvert::prop, to_floatbv_type(), and exprt::type().
Referenced by convert_bitvector().
Definition at line 17 of file boolbv_add_sub.cpp.
References bv_utilst::add_sub(), float_utilst::add_sub(), bv_utilst::add_sub_no_overflow(), boolbv_width, bv_utils, conversion_failed(), convert_bv(), namespace_baset::follow(), irept::id(), irept::id_string(), decision_proceduret::ns, exprt::op0(), exprt::operands(), irept::pretty(), prop_conv_solvert::prop, bv_utilst::SIGNED, typet::subtype(), to_floatbv_type(), exprt::type(), and bv_utilst::UNSIGNED.
Referenced by convert_bitvector().
Definition at line 12 of file boolbv_array.cpp.
References boolbv_width, conversion_failed(), convert_bv(), forall_expr, forall_literals, exprt::has_operands(), irept::id(), exprt::operands(), and exprt::type().
Referenced by convert_bitvector().
|
protectedvirtual |
Definition at line 14 of file boolbv_array_of.cpp.
References boolbv_width, conversion_failed(), convert_bv(), irept::id(), is_unbounded_array(), exprt::op0(), array_typet::size(), typet::subtype(), to_array_type(), to_integer(), and exprt::type().
Referenced by convert_bitvector().
Reimplemented in bv_pointerst, and bv_cbmct.
Definition at line 154 of file boolbv.cpp.
References boolbv_width, bv_utilst::build_constant(), bv_utils, conversion_failed(), prop_conv_solvert::convert(), convert_abs(), convert_add_sub(), convert_array(), convert_array_of(), convert_bitwise(), convert_bv_literals(), convert_bv_reduction(), convert_bv_typecast(), convert_byte_extract(), convert_byte_update(), convert_case(), convert_complex(), convert_complex_imag(), convert_complex_real(), convert_concatenation(), convert_cond(), convert_constant(), convert_constraint_select_one(), convert_div(), convert_extractbits(), convert_floatbv_op(), convert_floatbv_typecast(), convert_function_application(), convert_if(), convert_index(), convert_lambda(), convert_member(), convert_mod(), convert_mult(), convert_not(), convert_power(), convert_replication(), convert_shift(), convert_struct(), convert_symbol(), convert_unary_minus(), convert_union(), convert_update(), convert_vector(), convert_with(), irept::id(), exprt::op0(), exprt::op1(), exprt::operands(), prop_conv_solvert::prop, string_constantt::to_array_expr(), to_array_of_expr(), to_binary_expr(), to_byte_extract_expr(), to_byte_update_expr(), to_constant_expr(), to_div_expr(), to_extractbits_expr(), to_floatbv_type(), to_floatbv_typecast_expr(), to_function_application_expr(), to_if_expr(), to_index_expr(), to_member_expr(), to_mod_expr(), to_not_expr(), to_replication_expr(), to_shift_expr(), to_string_constant(), to_struct_expr(), to_symbol_expr(), to_typecast_expr(), to_unary_expr(), to_union_expr(), and exprt::type().
Referenced by boolbvt(), bv_pointerst::convert_bitvector(), and convert_bv().
Definition at line 12 of file boolbv_bitwise.cpp.
References boolbv_width, bv_utils, conversion_failed(), convert_bv(), forall_operands, irept::id(), bv_utilst::inverted(), propt::land(), propt::lequal(), propt::lnand(), propt::lnor(), propt::lor(), propt::lxor(), exprt::op0(), exprt::operands(), prop_conv_solvert::prop, and exprt::type().
Referenced by convert_bitvector(), and bv_pointerst::convert_pointer_type().
Definition at line 115 of file boolbv.cpp.
References bv_cache, convert_bitvector(), messaget::eom(), messaget::error(), forall_literals, prop_conv_solvert::freeze_all, irept::pretty(), prop_conv_solvert::prop, propt::set_frozen(), and literalt::unused_var_no().
Referenced by bv_refinementt::add_approximation(), bv_minimizet::add_objective(), string_refinementt::boolbv_set_equality_to_true(), boolbv_set_equality_to_true(), boolbvt(), convert_abs(), convert_add_sub(), convert_array(), convert_array_of(), bv_pointerst::convert_bitvector(), convert_bitwise(), convert_bv_reduction(), convert_bv_rel(), convert_bv_typecast(), convert_byte_extract(), convert_byte_update(), convert_case(), convert_complex(), convert_complex_imag(), convert_complex_real(), convert_concatenation(), convert_cond(), convert_constant(), convert_constraint_select_one(), convert_div(), convert_equality(), convert_extractbit(), convert_extractbits(), convert_floatbv_op(), convert_floatbv_typecast(), string_refinementt::convert_function_application(), convert_ieee_float_rel(), convert_if(), convert_index(), convert_lambda(), convert_member(), convert_mod(), convert_mult(), convert_not(), convert_onehot(), convert_overflow(), bv_pointerst::convert_pointer_type(), convert_power(), convert_reduction(), convert_replication(), bv_pointerst::convert_rest(), convert_rest(), convert_shift(), convert_struct(), string_refinementt::convert_symbol(), convert_typecast(), convert_unary_minus(), convert_union(), convert_update(), convert_update_rec(), convert_vector(), convert_verilog_case_equality(), convert_with(), convert_with_array(), convert_with_struct(), convert_with_union(), bv_refinementt::freeze_lazy_constraints(), bv_pointerst::offset_arithmetic(), and type_conversion().
Definition at line 357 of file boolbv.cpp.
References boolbv_width, conversion_failed(), irept::find(), irept::get_sub(), id2string(), exprt::type(), and unsafe_string2int().
Referenced by convert_bitvector().
|
protectedvirtual |
Definition at line 52 of file boolbv_reduction.cpp.
References const_literal(), conversion_failed(), convert_bv(), irept::get_int(), irept::id(), propt::land(), propt::lor(), propt::lselect(), propt::lxor(), unary_exprt::op(), prop_conv_solvert::prop, and exprt::type().
Referenced by convert_bitvector().
Definition at line 17 of file boolbv_bv_rel.cpp.
References bv_utils, convert_bv(), prop_conv_solvert::convert_rest(), equalityt::equality(), float_utilst::GE, get_bvtype(), float_utilst::GT, propt::has_set_to(), irept::id(), IS_FIXED, IS_FLOAT, IS_SIGNED, IS_UNSIGNED, IS_VERILOG_SIGNED, IS_VERILOG_UNSIGNED, propt::l_set_to_true(), float_utilst::LE, propt::limplies(), literal(), float_utilst::LT, exprt::op0(), exprt::op1(), exprt::operands(), prop_conv_solvert::prop, bv_utilst::rel(), float_utilst::relation(), bv_utilst::SIGNED, to_floatbv_type(), exprt::type(), and bv_utilst::UNSIGNED.
Referenced by convert_rest().
|
protectedvirtual |
Definition at line 20 of file boolbv_typecast.cpp.
References conversion_failed(), convert_bv(), namespace_baset::follow(), decision_proceduret::ns, typecast_exprt::op(), exprt::type(), and type_conversion().
Referenced by convert_bitvector().
|
protectedvirtual |
Definition at line 37 of file boolbv_byte_extract.cpp.
References boolbv_width, const_literal(), conversion_failed(), prop_conv_solvert::convert(), convert_bv(), equalityt::equality(), flatten_byte_extract(), from_integer(), propt::has_set_to(), irept::id(), integer2unsigned(), is_unbounded_array(), propt::l_set_to_true(), propt::land(), propt::lequal(), binary_relation_exprt::lhs(), propt::limplies(), propt::lselect(), map_bv(), propt::new_variable(), decision_proceduret::ns, byte_extract_exprt::offset(), byte_extract_exprt::op(), exprt::operands(), irept::pretty(), prop_conv_solvert::prop, binary_relation_exprt::rhs(), to_c_bit_field_type(), to_integer(), and exprt::type().
Referenced by convert_bitvector(), and bv_pointerst::convert_pointer_type().
|
protectedvirtual |
Definition at line 18 of file boolbv_byte_update.cpp.
References prop_conv_solvert::convert(), convert_bv(), equalityt::equality(), from_integer(), irept::id(), integer2size_t(), integer2unsigned(), binary_relation_exprt::lhs(), propt::lselect(), endianness_mapt::map_bit(), decision_proceduret::ns, byte_update_exprt::offset(), exprt::op0(), exprt::operands(), prop_conv_solvert::prop, binary_relation_exprt::rhs(), to_integer(), exprt::type(), and byte_update_exprt::value().
Referenced by convert_bitvector().
Definition at line 13 of file boolbv_case.cpp.
References boolbv_width, bv_utils, const_literal(), conversion_failed(), convert_bv(), bv_utilst::equal(), Forall_literals, forall_operands, propt::l_set_to_true(), propt::land(), propt::limplies(), propt::lor(), propt::new_variable(), exprt::operands(), prop_conv_solvert::prop, exprt::type(), and VALUE.
Referenced by convert_bitvector(), and convert_rest().
Definition at line 12 of file boolbv_complex.cpp.
References boolbv_width, conversion_failed(), convert_bv(), forall_expr, forall_literals, irept::id(), exprt::operands(), and exprt::type().
Referenced by convert_bitvector().
Definition at line 66 of file boolbv_complex.cpp.
References boolbv_width, conversion_failed(), convert_bv(), exprt::op0(), exprt::operands(), and exprt::type().
Referenced by convert_bitvector().
Definition at line 48 of file boolbv_complex.cpp.
References boolbv_width, conversion_failed(), convert_bv(), exprt::op0(), exprt::operands(), and exprt::type().
Referenced by convert_bitvector().
Definition at line 12 of file boolbv_concatenation.cpp.
References boolbv_width, conversion_failed(), convert_bv(), forall_expr, exprt::operands(), and exprt::type().
Referenced by convert_bitvector(), and bv_pointerst::convert_pointer_type().
Definition at line 13 of file boolbv_cond.cpp.
References boolbv_width, bv_utils, const_literal(), conversion_failed(), prop_conv_solvert::convert(), convert_bv(), bv_utilst::equal(), Forall_literals, forall_operands, propt::has_set_to(), propt::l_set_to_true(), propt::land(), propt::limplies(), propt::lor(), propt::lselect(), propt::new_variable(), exprt::operands(), prop_conv_solvert::prop, and exprt::type().
Referenced by convert_bitvector(), and convert_rest().
|
protectedvirtual |
Definition at line 12 of file boolbv_constant.cpp.
References boolbv_width, bv_utilst::build_constant(), bv_utils, const_literal(), conversion_failed(), convert_bv(), enumeration_typet::elements(), messaget::eom(), messaget::error(), exprt::find_source_location(), forall_operands, range_typet::get_from(), constant_exprt::get_value(), irept::id(), id2string(), integer2binary(), exprt::operands(), irept::pretty(), messaget::mstreamt::source_location, string2integer(), string_numbering, to_enumeration_type(), to_range_type(), and exprt::type().
Referenced by convert_bitvector().
Definition at line 12 of file boolbv_constraint_select_one.cpp.
References boolbv_width, bv_utils, conversion_failed(), convert_bv(), bv_utilst::equal(), forall_operands, propt::has_set_to(), irept::id(), propt::lcnf(), propt::lselect(), propt::new_variable(), propt::new_variables(), exprt::op0(), exprt::operands(), prop_conv_solvert::prop, and exprt::type().
Referenced by convert_bitvector().
Reimplemented in bv_refinementt.
Definition at line 13 of file boolbv_div.cpp.
References boolbv_width, bv_utils, const_literal(), conversion_failed(), convert_bv(), bv_utilst::divider(), irept::id(), exprt::op0(), exprt::op1(), bv_utilst::sign_extension(), bv_utilst::SIGNED, to_fixedbv_type(), exprt::type(), and bv_utilst::UNSIGNED.
Referenced by convert_bitvector(), and bv_refinementt::convert_div().
|
protectedvirtual |
Definition at line 20 of file boolbv_equality.cpp.
References base_type_eq(), bv_utils, convert_bv(), bv_utilst::equal(), flatten_byte_operators(), has_byte_operator(), is_unbounded_array(), binary_relation_exprt::lhs(), propt::new_variable(), decision_proceduret::ns, irept::pretty(), prop_conv_solvert::prop, arrayst::record_array_equality(), binary_relation_exprt::rhs(), to_equal_expr(), and exprt::type().
Referenced by convert_rest().
|
protectedvirtual |
Definition at line 18 of file boolbv_extractbit.cpp.
References address_bits(), boolbv_width, prop_conv_solvert::convert(), convert_bv(), prop_conv_solvert::convert_rest(), equalityt::equality(), from_integer(), propt::has_set_to(), index_type(), integer2size_t(), integer2unsigned(), propt::l_set_to_true(), propt::lequal(), binary_relation_exprt::lhs(), propt::limplies(), propt::lselect(), exprt::make_typecast(), propt::new_variable(), exprt::operands(), prop_conv_solvert::prop, binary_relation_exprt::rhs(), bitvector_typet::set_width(), to_integer(), and exprt::type().
Referenced by convert_rest().
|
protectedvirtual |
Definition at line 13 of file boolbv_extractbits.cpp.
References boolbv_width, conversion_failed(), convert_bv(), messaget::eom(), messaget::error(), exprt::find_source_location(), integer2unsigned(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), irept::pretty(), messaget::mstreamt::source_location, to_integer(), and exprt::type().
Referenced by convert_bitvector().
Reimplemented in bv_refinementt.
Definition at line 75 of file boolbv_floatbv_op.cpp.
References float_utilst::add_sub(), boolbv_width, conversion_failed(), convert_bv(), float_utilst::div(), namespace_baset::follow(), irept::id(), irept::id_string(), float_utilst::mul(), decision_proceduret::ns, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), irept::pretty(), prop_conv_solvert::prop, float_utilst::rem(), float_utilst::set_rounding_mode(), float_utilst::spec, typet::subtype(), to_floatbv_type(), and exprt::type().
Referenced by convert_bitvector(), and bv_refinementt::convert_floatbv_op().
|
protectedvirtual |
Definition at line 18 of file boolbv_floatbv_op.cpp.
References float_utilst::conversion(), conversion_failed(), convert_bv(), namespace_baset::follow(), float_utilst::from_signed_integer(), float_utilst::from_unsigned_integer(), bitvector_typet::get_width(), irept::id(), decision_proceduret::ns, floatbv_typecast_exprt::op(), exprt::op0(), prop_conv_solvert::prop, floatbv_typecast_exprt::rounding_mode(), float_utilst::set_rounding_mode(), float_utilst::spec, to_floatbv_type(), float_utilst::to_signed_integer(), to_signedbv_type(), float_utilst::to_unsigned_integer(), to_unsignedbv_type(), and exprt::type().
Referenced by convert_bitvector().
|
protectedvirtual |
Reimplemented in string_refinementt.
Definition at line 413 of file boolbv.cpp.
References boolbv_width, functions, propt::new_variables(), prop_conv_solvert::prop, functionst::record(), and exprt::type().
Referenced by convert_bitvector().
Definition at line 17 of file boolbv_ieee_float_rel.cpp.
References convert_bv(), prop_conv_solvert::convert_rest(), float_utilst::EQ, get_bvtype(), irept::id(), IS_FLOAT, exprt::op0(), exprt::op1(), exprt::operands(), prop_conv_solvert::prop, float_utilst::relation(), to_floatbv_type(), and exprt::type().
Referenced by convert_rest().
Definition at line 12 of file boolbv_if.cpp.
References boolbv_width, bv_utils, if_exprt::cond(), prop_conv_solvert::convert(), convert_bv(), if_exprt::false_case(), irept::pretty(), bv_utilst::select(), if_exprt::true_case(), and exprt::type().
Referenced by convert_bitvector(), and bv_pointerst::convert_pointer_type().
|
protectedvirtual |
index operator with constant index
Definition at line 293 of file boolbv_index.cpp.
References boolbv_width, conversion_failed(), convert_bv(), namespace_baset::follow(), integer2size_t(), propt::new_variable(), decision_proceduret::ns, prop_conv_solvert::prop, typet::subtype(), to_array_type(), and exprt::type().
Referenced by convert_bitvector(), convert_index(), bv_pointerst::convert_pointer_type(), and convert_rest().
|
protectedvirtual |
Definition at line 17 of file boolbv_index.cpp.
References index_exprt::array(), boolbv_width, bv_utils, conversion_failed(), prop_conv_solvert::convert(), convert_bv(), convert_index(), equalityt::equality(), namespace_baset::follow(), forall_expr, from_integer(), boolbv_mapt::get_map_entry(), propt::has_set_to(), irept::id(), index_exprt::index(), integer2size_t(), irept::is_nil(), is_unbounded_array(), propt::l_set_to_true(), propt::land(), propt::lequal(), binary_relation_exprt::lhs(), propt::limplies(), propt::lselect(), map, propt::new_variable(), decision_proceduret::ns, exprt::op0(), exprt::op1(), exprt::operands(), prop_conv_solvert::prop, arrayst::record_array_index(), messaget::result(), binary_relation_exprt::rhs(), simplify_expr(), array_typet::size(), to_array_type(), to_integer(), to_symbol_expr(), and exprt::type().
Definition at line 310 of file boolbv.cpp.
References boolbv_width, conversion_failed(), convert_bv(), from_integer(), irept::id(), integer2unsigned(), exprt::op0(), exprt::op1(), exprt::operands(), replace_expr(), to_array_type(), to_integer(), and exprt::type().
Referenced by convert_bitvector().
|
protectedvirtual |
Definition at line 16 of file boolbv_member.cpp.
References base_type_eq(), boolbv_width, byte_extract_id(), struct_union_typet::components(), convert_bv(), messaget::eom(), messaget::error(), exprt::find_source_location(), namespace_baset::follow(), from_integer(), member_exprt::get_component_name(), irept::id(), index_type(), decision_proceduret::ns, irept::pretty(), messaget::mstreamt::source_location, member_exprt::struct_op(), to_struct_type(), and exprt::type().
Referenced by convert_bitvector(), bv_pointerst::convert_pointer_type(), and convert_rest().
Reimplemented in bv_refinementt.
Definition at line 12 of file boolbv_mod.cpp.
References boolbv_width, bv_utils, conversion_failed(), convert_bv(), bv_utilst::divider(), irept::id(), exprt::op0(), exprt::op1(), bv_utilst::SIGNED, exprt::type(), and bv_utilst::UNSIGNED.
Referenced by convert_bitvector(), and bv_refinementt::convert_mod().
Reimplemented in bv_refinementt.
Definition at line 13 of file boolbv_mult.cpp.
References boolbv_width, bv_utils, conversion_failed(), convert_bv(), irept::id(), bv_utilst::multiplier(), bv_utilst::multiplier_no_overflow(), exprt::op0(), exprt::operands(), bv_utilst::sign_extension(), bv_utilst::SIGNED, bv_utilst::signed_multiplier(), to_fixedbv_type(), exprt::type(), and bv_utilst::UNSIGNED.
Referenced by convert_bitvector(), and bv_refinementt::convert_mult().
Definition at line 12 of file boolbv_not.cpp.
References bv_utils, const_literal(), conversion_failed(), convert_bv(), irept::get_int(), irept::id(), bv_utilst::is_zero(), propt::lselect(), not_exprt::op(), prop_conv_solvert::prop, exprt::type(), bv_utilst::verilog_bv_has_x_or_z(), and bv_utilst::verilog_bv_normal_bits().
Referenced by convert_bitvector().
|
protectedvirtual |
Definition at line 12 of file boolbv_onehot.cpp.
References const_literal(), convert_bv(), irept::id(), propt::land(), propt::lor(), unary_exprt::op(), and prop_conv_solvert::prop.
Referenced by convert_rest().
Definition at line 16 of file boolbv_overflow.cpp.
References bv_utils, convert_bv(), prop_conv_solvert::convert_rest(), bv_utilst::extension(), has_prefix(), irept::id(), id2string(), irept::id_string(), propt::land(), propt::lor(), propt::lxor(), bv_utilst::multiplier(), exprt::op0(), exprt::operands(), bv_utilst::overflow_add(), bv_utilst::overflow_negate(), bv_utilst::overflow_sub(), prop_conv_solvert::prop, messaget::result(), bv_utilst::SIGNED, exprt::type(), unsafe_string2unsigned(), and bv_utilst::UNSIGNED.
Referenced by convert_rest().
|
protectedvirtual |
Definition at line 12 of file boolbv_power.cpp.
References boolbv_width, bv_utilst::build_constant(), bv_utils, conversion_failed(), convert_bv(), bv_utilst::equal(), namespace_baset::follow(), irept::id(), bv_utilst::LEFT, propt::new_variables(), decision_proceduret::ns, exprt::op0(), exprt::op1(), prop_conv_solvert::prop, bv_utilst::select(), bv_utilst::shift(), and exprt::type().
Referenced by convert_bitvector().
Definition at line 204 of file boolbv_quantifier.cpp.
References prop_conv_solvert::convert_rest(), boolbvt::quantifiert::expr, instantiate_quantifier(), propt::new_variable(), decision_proceduret::ns, prop_conv_solvert::prop, and quantifier_list.
Referenced by convert_rest().
|
protectedvirtual |
Definition at line 12 of file boolbv_reduction.cpp.
References convert_bv(), irept::id(), propt::land(), propt::lor(), propt::lxor(), unary_exprt::op(), and prop_conv_solvert::prop.
Referenced by convert_rest().
|
protectedvirtual |
Definition at line 13 of file boolbv_replication.cpp.
References boolbv_width, conversion_failed(), convert_bv(), integer2unsigned(), exprt::op0(), exprt::op1(), to_integer(), and exprt::type().
Referenced by convert_bitvector().
Reimplemented from prop_conv_solvert.
Reimplemented in string_refinementt, and bv_pointerst.
Definition at line 424 of file boolbv.cpp.
References const_literal(), convert_bv(), convert_bv_rel(), convert_case(), convert_cond(), convert_equality(), convert_extractbit(), convert_ieee_float_rel(), convert_index(), convert_member(), convert_onehot(), convert_overflow(), convert_quantifier(), convert_reduction(), prop_conv_solvert::convert_rest(), convert_typecast(), convert_verilog_case_equality(), messaget::eom(), messaget::error(), has_prefix(), irept::id(), irept::id_string(), float_utilst::is_infinity(), float_utilst::is_NaN(), float_utilst::is_normal(), propt::land(), exprt::op0(), exprt::op1(), exprt::operands(), irept::pretty(), prop_conv_solvert::prop, to_binary_relation_expr(), to_equal_expr(), to_extractbit_expr(), to_floatbv_type(), to_index_expr(), to_member_expr(), to_typecast_expr(), to_unary_expr(), and exprt::type().
Referenced by bv_pointerst::convert_rest().
|
protectedvirtual |
Definition at line 15 of file boolbv_shift.cpp.
References bv_utilst::ARIGHT, boolbv_width, bv_utils, conversion_failed(), convert_bv(), irept::id(), integer2size_t(), exprt::is_constant(), bv_utilst::LEFT, bv_utilst::LRIGHT, exprt::op0(), exprt::op1(), exprt::operands(), bv_utilst::shift(), to_integer(), and exprt::type().
Referenced by convert_bitvector(), and bv_pointerst::convert_pointer_type().
|
protectedvirtual |
Definition at line 14 of file boolbv_struct.cpp.
References base_type_eq(), boolbv_width, struct_union_typet::components(), convert_bv(), messaget::eom(), messaget::error(), exprt::find_source_location(), namespace_baset::follow(), decision_proceduret::ns, exprt::operands(), irept::pretty(), messaget::mstreamt::source_location, to_struct_type(), and exprt::type().
Referenced by convert_bitvector().
Reimplemented in string_refinementt.
Definition at line 378 of file boolbv.cpp.
References boolbv_width, dstringt::empty(), messaget::eom(), messaget::error(), forall_literals, irept::get(), boolbv_mapt::get_literals(), boolbv_mapt::get_map_entry(), map, propt::no_variables(), prop_conv_solvert::prop, and exprt::type().
Referenced by convert_bitvector(), and string_refinementt::convert_symbol().
|
protectedvirtual |
conversion from bitvector types to boolean
Definition at line 593 of file boolbv_typecast.cpp.
References const_literal(), convert_bv(), prop_conv_solvert::convert_rest(), irept::get_string(), irept::id(), propt::lor(), exprt::op0(), exprt::operands(), prop_conv_solvert::prop, string2integer(), and exprt::type().
Referenced by convert_rest().
|
protectedvirtual |
Definition at line 17 of file boolbv_unary_minus.cpp.
References boolbv_width, bv_utils, conversion_failed(), convert_bv(), namespace_baset::follow(), get_bvtype(), irept::id(), IS_FIXED, IS_FLOAT, IS_SIGNED, IS_UNKNOWN, IS_UNSIGNED, propt::l_set_to(), bv_utilst::negate(), float_utilst::negate(), bv_utilst::negate_no_overflow(), decision_proceduret::ns, exprt::op0(), exprt::operands(), bv_utilst::overflow_negate(), prop_conv_solvert::prop, typet::subtype(), to_floatbv_type(), and exprt::type().
Referenced by convert_bitvector().
|
protectedvirtual |
Definition at line 15 of file boolbv_union.cpp.
References configt::ansi_c, boolbv_width, config, conversion_failed(), convert_bv(), configt::ansi_ct::endianness, configt::ansi_ct::IS_BIG_ENDIAN, configt::ansi_ct::IS_LITTLE_ENDIAN, propt::new_variable(), decision_proceduret::ns, unary_exprt::op(), exprt::op0(), prop_conv_solvert::prop, and exprt::type().
Referenced by convert_bitvector().
Definition at line 20 of file boolbv_update.cpp.
References boolbv_width, conversion_failed(), convert_bv(), convert_update_rec(), exprt::op1(), exprt::op2(), exprt::operands(), and exprt::type().
Referenced by convert_bitvector().
|
protected |
Definition at line 44 of file boolbv_update.cpp.
References boolbv_width, bv_utilst::build_constant(), bv_utils, struct_union_typet::components(), convert_bv(), bv_utilst::equal(), namespace_baset::follow(), irept::get(), struct_union_typet::get_component(), irept::id(), integer2size_t(), irept::is_nil(), propt::lselect(), irept::make_nil(), decision_proceduret::ns, exprt::op0(), exprt::operands(), prop_conv_solvert::prop, to_array_type(), to_integer(), to_struct_type(), to_union_type(), and exprt::type().
Referenced by convert_update().
Definition at line 12 of file boolbv_vector.cpp.
References boolbv_width, conversion_failed(), convert_bv(), forall_expr, forall_literals, irept::id(), exprt::operands(), and exprt::type().
Referenced by convert_bitvector().
|
protectedvirtual |
Definition at line 65 of file boolbv_equality.cpp.
References base_type_eq(), bv_utils, convert_bv(), bv_utilst::equal(), irept::id(), binary_relation_exprt::lhs(), decision_proceduret::ns, irept::pretty(), binary_relation_exprt::rhs(), and exprt::type().
Referenced by convert_rest().
Definition at line 18 of file boolbv_with.cpp.
References boolbv_width, conversion_failed(), convert_bv(), messaget::eom(), messaget::error(), exprt::find_source_location(), irept::id(), exprt::op0(), exprt::operands(), messaget::mstreamt::source_location, typet::subtype(), and exprt::type().
Referenced by convert_bitvector(), and convert_with().
|
protected |
Definition at line 74 of file boolbv_with.cpp.
References convert_with(), convert_with_array(), convert_with_bv(), convert_with_struct(), convert_with_union(), messaget::error(), namespace_baset::follow(), irept::id(), decision_proceduret::ns, typet::source_location(), messaget::mstreamt::source_location, to_array_type(), to_struct_type(), and to_union_type().
|
protected |
Definition at line 104 of file boolbv_with.cpp.
References prop_conv_solvert::convert(), convert_bv(), messaget::eom(), messaget::error(), from_integer(), integer2unsigned(), is_unbounded_array(), propt::lselect(), prop_conv_solvert::prop, array_typet::size(), typet::source_location(), messaget::mstreamt::source_location, to_integer(), and exprt::type().
Referenced by convert_with().
|
protected |
Definition at line 173 of file boolbv_with.cpp.
References prop_conv_solvert::convert(), from_integer(), integer2size_t(), propt::lselect(), prop_conv_solvert::prop, to_integer(), and exprt::type().
Referenced by convert_with().
|
protected |
Definition at line 205 of file boolbv_with.cpp.
References base_type_eq(), boolbv_width, struct_union_typet::components(), convert_bv(), messaget::eom(), messaget::error(), irept::get(), decision_proceduret::ns, irept::pretty(), typet::source_location(), messaget::mstreamt::source_location, and exprt::type().
Referenced by convert_with().
|
protected |
Definition at line 261 of file boolbv_with.cpp.
References configt::ansi_c, config, convert_bv(), configt::ansi_ct::endianness, messaget::eom(), messaget::error(), configt::ansi_ct::IS_BIG_ENDIAN, configt::ansi_ct::IS_LITTLE_ENDIAN, endianness_mapt::map_bit(), decision_proceduret::ns, typet::source_location(), messaget::mstreamt::source_location, and exprt::type().
Referenced by convert_with().
Reimplemented from prop_conv_solvert.
Definition at line 21 of file boolbv_get.cpp.
References bv_get_rec(), bv_get_unbounded_array(), prop_conv_solvert::get(), irept::get(), irept::id(), is_unbounded_array(), boolbv_mapt::map_entryt::literal_map, map, boolbv_mapt::mapping, boolbv_mapt::map_entryt::type, and boolbv_mapt::map_entryt::width.
Referenced by string_refinementt::check_axioms().
|
inline |
|
inline |
Definition at line 78 of file boolbv.h.
Referenced by bv_refinementt::get_values(), and string_refinementt::sum_over_map().
mp_integer boolbvt::get_value | ( | const bvt & | bv, |
std::size_t | offset, | ||
std::size_t | width | ||
) |
Definition at line 417 of file boolbv_get.cpp.
References tvt::get_value(), propt::l_get(), prop_conv_solvert::prop, tvt::TV_FALSE, tvt::TV_TRUE, and tvt::TV_UNKNOWN.
|
overrideprotectedvirtual |
Implements arrayst.
Definition at line 673 of file boolbv.cpp.
References namespace_baset::follow(), irept::id(), decision_proceduret::ns, array_typet::size(), to_array_type(), to_integer(), U_ALL, U_AUTO, and unbounded_array.
Referenced by string_refinementt::boolbv_set_equality_to_true(), boolbv_set_equality_to_true(), convert_array_of(), convert_byte_extract(), convert_equality(), convert_index(), convert_with_array(), and get().
Definition at line 31 of file boolbv.cpp.
References index_exprt::array(), boolbv_width, irept::get(), member_exprt::get_component_name(), irept::id(), index_exprt::index(), integer2unsigned(), prop_conv_solvert::literal(), boolbv_mapt::map_entryt::literal_map, map, boolbv_mapt::mapping, exprt::op0(), to_index_expr(), to_integer(), to_member_expr(), to_struct_type(), and exprt::type().
Referenced by convert_bv_rel(), and post_process().
Definition at line 642 of file boolbv.cpp.
References irept::add(), and irept::get_sub().
Referenced by make_free_bv_expr().
Definition at line 653 of file boolbv.cpp.
References boolbv_width, messaget::eom(), messaget::error(), Forall_literals, make_bv_expr(), propt::new_variable(), irept::pretty(), and prop_conv_solvert::prop.
Referenced by bv_cbmct::convert_waitfor(), and bv_cbmct::convert_waitfor_symbol().
|
inlineoverridevirtual |
Reimplemented from arrayst.
Reimplemented in bv_pointerst.
Definition at line 60 of file boolbv.h.
References functions, literal(), prop_conv_solvert::literal(), arrayst::post_process(), functionst::post_process(), and post_process_quantifiers().
Referenced by bv_pointerst::post_process().
|
protected |
Definition at line 220 of file boolbv_quantifier.cpp.
References prop_conv_solvert::convert_bool(), literalt::l, prop_conv_solvert::prop, quantifier_list, and propt::set_equal().
Referenced by post_process().
|
overridevirtual |
Reimplemented from prop_conv_solvert.
Definition at line 697 of file boolbv.cpp.
References map, boolbv_mapt::mapping, and prop_conv_solvert::prop.
Referenced by boolbvt().
|
overridevirtual |
Reimplemented from prop_conv_solvert.
Reimplemented in bv_refinementt.
Definition at line 621 of file boolbv.cpp.
References boolbv_set_equality_to_true(), messaget::eom(), messaget::error(), irept::id(), irept::pretty(), prop_conv_solvert::set_to(), to_equal_expr(), and exprt::type().
Referenced by boolbvt(), counterexample_beautificationt::operator()(), and bv_refinementt::set_to().
|
protected |
Definition at line 35 of file boolbv_typecast.cpp.
References bv_utilst::add(), boolbv_width, bv_utilst::build_constant(), build_offset_map(), bv_utils, c_bit_field_replacement_type(), struct_union_typet::components(), const_literal(), convert_bv(), namespace_baset::follow(), forall_literals, Forall_literals, ieee_floatt::from_integer(), float_utilst::from_signed_integer(), float_utilst::from_unsigned_integer(), get_bvtype(), fixedbv_typet::get_fraction_bits(), range_typet::get_from(), irept::id(), bv_utilst::incrementer(), IS_BV, IS_C_BIT_FIELD, IS_C_BOOL, IS_C_ENUM, IS_FIXED, IS_FLOAT, IS_RANGE, IS_SIGNED, IS_UNSIGNED, IS_VERILOG_SIGNED, IS_VERILOG_UNSIGNED, float_utilst::is_zero(), bv_utilst::is_zero(), propt::land(), propt::lor(), propt::new_variable(), decision_proceduret::ns, prop_conv_solvert::prop, float_utilst::spec, typet::subtype(), to_c_bit_field_type(), ieee_floatt::to_expr(), to_fixedbv_type(), to_floatbv_type(), to_range_type(), to_struct_type(), type_conversion(), and bv_utilst::zero_extension().
Referenced by convert_bv_typecast(), and type_conversion().
boolbv_widtht boolbvt::boolbv_width |
Definition at line 90 of file boolbv.h.
Referenced by bv_refinementt::add_approximation(), build_offset_map(), bv_get_rec(), conversion_failed(), convert_abs(), convert_add_sub(), convert_array(), convert_array_of(), bv_pointerst::convert_bitvector(), convert_bitvector(), convert_bitwise(), string_refinementt::convert_bool_bv(), convert_bv_literals(), convert_byte_extract(), convert_case(), convert_complex(), convert_complex_imag(), convert_complex_real(), convert_concatenation(), convert_cond(), convert_constant(), convert_constraint_select_one(), convert_div(), convert_extractbit(), convert_extractbits(), convert_floatbv_op(), convert_function_application(), convert_if(), convert_index(), convert_lambda(), convert_member(), convert_mod(), convert_mult(), convert_power(), convert_replication(), convert_shift(), convert_struct(), convert_symbol(), convert_unary_minus(), convert_union(), convert_update(), convert_update_rec(), convert_vector(), convert_with(), convert_with_struct(), literal(), make_free_bv_expr(), and type_conversion().
|
protected |
Definition at line 116 of file boolbv.h.
Referenced by bv_get_cache(), clear_cache(), and convert_bv().
|
protected |
Definition at line 93 of file boolbv.h.
Referenced by bv_refinementt::check_SAT(), convert_abs(), convert_add_sub(), bv_pointerst::convert_address_of_rec(), bv_pointerst::convert_bitvector(), convert_bitvector(), convert_bitwise(), convert_bv_rel(), convert_case(), convert_cond(), convert_constant(), convert_constraint_select_one(), convert_div(), convert_equality(), convert_if(), convert_index(), convert_mod(), bv_refinementt::convert_mult(), convert_mult(), convert_not(), convert_overflow(), bv_pointerst::convert_pointer_type(), convert_power(), bv_pointerst::convert_rest(), convert_shift(), convert_unary_minus(), convert_update_rec(), convert_verilog_case_equality(), bv_pointerst::do_postponed(), bv_pointerst::offset_arithmetic(), and type_conversion().
|
protected |
Definition at line 96 of file boolbv.h.
Referenced by convert_function_application(), and post_process().
|
protected |
Definition at line 99 of file boolbv.h.
Referenced by string_refinementt::boolbv_set_equality_to_true(), boolbv_set_equality_to_true(), convert_index(), bv_pointerst::convert_pointer_type(), convert_symbol(), get(), get_map(), literal(), print_assignment(), and string_refinementt::simplify_sum().
|
protected |
Definition at line 246 of file boolbv.h.
Referenced by convert_quantifier(), and post_process_quantifiers().
Definition at line 254 of file boolbv.h.
Referenced by bv_get_rec(), and convert_constant().
unbounded_arrayt boolbvt::unbounded_array |
Definition at line 76 of file boolbv.h.
Referenced by bv_refinementt::arrays_overapproximated(), cbmc_solverst::get_default(), and is_unbounded_array().