cprover
boolbvt Class Reference

#include <boolbv.h>

Inheritance diagram for boolbvt:
[legend]
Collaboration diagram for boolbvt:
[legend]

Classes

class  quantifiert
 

Public Types

enum  unbounded_arrayt { unbounded_arrayt::U_NONE, unbounded_arrayt::U_ALL, unbounded_arrayt::U_AUTO }
 
- Public Types inherited from arrayst
typedef equalityt SUB
 
- Public Types inherited from prop_conv_solvert
typedef std::map< irep_idt, literaltsymbolst
 
typedef std::unordered_map< exprt, literalt, irep_hashcachet
 
- Public Types inherited from decision_proceduret
enum  resultt { resultt::D_SATISFIABLE, resultt::D_UNSATISFIABLE, resultt::D_ERROR }
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 

Public Member Functions

 boolbvt (const namespacet &_ns, propt &_prop)
 
virtual const bvtconvert_bv (const exprt &expr)
 
virtual bvt convert_bitvector (const exprt &expr)
 Converts an expression into its gate-level representation and returns a vector of literals corresponding to the outputs of the Boolean circuit. More...
 
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_maptget_map () const
 
- Public Member Functions inherited from arrayst
 arrayst (const namespacet &_ns, propt &_prop)
 
literalt record_array_equality (const equal_exprt &expr)
 
void record_array_index (const index_exprt &expr)
 
- Public Member Functions inherited from equalityt
 equalityt (const namespacet &_ns, propt &_prop)
 
virtual literalt equality (const exprt &e1, const exprt &e2)
 
void post_process () override
 
- Public Member Functions inherited from prop_conv_solvert
 prop_conv_solvert (const namespacet &_ns, propt &_prop)
 
virtual ~prop_conv_solvert ()=default
 
void set_to (const exprt &expr, bool value) override
 
decision_proceduret::resultt dec_solve () override
 
void print_assignment (std::ostream &out) const override
 
std::string decision_procedure_text () const override
 
exprt get (const exprt &expr) const override
 
virtual tvt l_get (literalt a) const override
 
void set_frozen (literalt a) override
 
void set_assumptions (const bvt &_assumptions) override
 
bool has_set_assumptions () const override
 
void set_all_frozen () override
 
literalt convert (const exprt &expr) override
 
bool is_in_conflict (literalt l) const override
 determine whether a variable is in the final conflict More...
 
bool has_is_in_conflict () const override
 
virtual bool literal (const exprt &expr, literalt &literal) const
 
const cachetget_cache () const
 
const symbolstget_symbols () const
 
void set_time_limit_seconds (uint32_t lim) override
 
virtual void set_frozen (literalt a)
 
virtual void set_frozen (const bvt &)
 
- Public Member Functions inherited from prop_convt
 prop_convt (const namespacet &_ns)
 
virtual ~prop_convt ()
 
literalt operator() (const exprt &expr)
 
virtual void set_frozen (const bvt &)
 
- Public Member Functions inherited from decision_proceduret
 decision_proceduret (const namespacet &_ns)
 
void set_to_true (const exprt &expr)
 
void set_to_false (const exprt &expr)
 
resultt operator() ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

Public Attributes

unbounded_arrayt unbounded_array
 
boolbv_widtht boolbv_width
 
- Public Attributes inherited from prop_conv_solvert
bool use_cache = true
 
bool equality_propagation = true
 
bool freeze_all = false
 

Protected Types

typedef arrayst SUB
 
typedef std::unordered_map< const exprt, bvt, irep_hashbv_cachet
 
typedef std::list< quantifiertquantifier_listt
 
typedef std::vector< std::size_t > offset_mapt
 
- Protected Types inherited from arrayst
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_equalitytarray_equalitiest
 
typedef std::set< exprtindex_sett
 
typedef std::map< std::size_t, index_settindex_mapt
 
- Protected Types inherited from equalityt
typedef std::unordered_map< const exprt, unsigned, irep_hashelementst
 
typedef std::map< std::pair< unsigned, unsigned >, literaltequalitiest
 
typedef std::map< unsigned, exprtelements_revt
 
typedef std::unordered_map< const typet, typestructt, irep_hashtypemapt
 

Protected Member Functions

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_bswap (const bswap_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_let (const let_exprt &)
 
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 abs_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 exprt make_bv_expr (const typet &type, const bvt &bv)
 
virtual exprt make_free_bv_expr (const typet &type)
 
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 ()
 
offset_mapt build_offset_map (const struct_typet &src)
 
- Protected Member Functions inherited from arrayst
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)
 
- Protected Member Functions inherited from equalityt
virtual literalt equality2 (const exprt &e1, const exprt &e2)
 
virtual void add_equality_constraints ()
 
virtual void add_equality_constraints (const typestructt &typestruct)
 
- Protected Member Functions inherited from prop_conv_solvert
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_idtstring_numbering
 
- Protected Attributes inherited from arrayst
array_equalitiest array_equalities
 
union_find< exprtarrays
 
index_mapt index_map
 
bool lazy_arrays
 
bool incremental_cache
 
std::list< lazy_constrainttlazy_array_constraints
 
std::map< exprt, bool > expr_map
 
std::set< std::size_t > update_indices
 
- Protected Attributes inherited from equalityt
typemapt typemap
 
- Protected Attributes inherited from prop_conv_solvert
bool post_processing_done = false
 
symbolst symbols
 
cachet cache
 
proptprop
 
- Protected Attributes inherited from decision_proceduret
const namespacetns
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 31 of file boolbv.h.

Member Typedef Documentation

◆ bv_cachet

typedef std::unordered_map<const exprt, bvt, irep_hash> boolbvt::bv_cachet
protected

Definition at line 115 of file boolbv.h.

◆ offset_mapt

typedef std::vector<std::size_t> boolbvt::offset_mapt
protected

Definition at line 252 of file boolbv.h.

◆ quantifier_listt

typedef std::list<quantifiert> boolbvt::quantifier_listt
protected

Definition at line 247 of file boolbv.h.

◆ SUB

typedef arrayst boolbvt::SUB
protected

Definition at line 106 of file boolbv.h.

Member Enumeration Documentation

◆ unbounded_arrayt

Enumerator
U_NONE 
U_ALL 
U_AUTO 

Definition at line 75 of file boolbv.h.

Constructor & Destructor Documentation

◆ boolbvt()

boolbvt::boolbvt ( const namespacet _ns,
propt _prop 
)
inline

Definition at line 34 of file boolbv.h.

Member Function Documentation

◆ boolbv_set_equality_to_true()

◆ build_offset_map()

boolbvt::offset_mapt boolbvt::build_offset_map ( const struct_typet src)
protected

Definition at line 663 of file boolbv.cpp.

References boolbv_width, and struct_union_typet::components().

Referenced by type_conversion().

◆ bv_get()

exprt boolbvt::bv_get ( const bvt bv,
const typet type 
) const
protected

Definition at line 279 of file boolbv_get.cpp.

References bv_get_rec().

Referenced by bv_get_cache().

◆ bv_get_cache()

exprt boolbvt::bv_get_cache ( const exprt expr) const
protected

Definition at line 286 of file boolbv_get.cpp.

References bv_cache, bv_get(), irept::id(), and exprt::type().

Referenced by bv_get_unbounded_array().

◆ bv_get_rec()

◆ bv_get_unbounded_array()

◆ clear_cache()

void boolbvt::clear_cache ( )
inlineoverridevirtual

Reimplemented from prop_conv_solvert.

Definition at line 54 of file boolbv.h.

References bv_cache, and prop_conv_solvert::clear_cache().

◆ conversion_failed() [1/2]

◆ conversion_failed() [2/2]

bvt boolbvt::conversion_failed ( const exprt expr)
protected

◆ convert_abs()

◆ convert_add_sub()

◆ convert_array()

bvt boolbvt::convert_array ( const exprt expr)
protectedvirtual

◆ convert_array_of()

bvt boolbvt::convert_array_of ( const array_of_exprt expr)
protectedvirtual

◆ convert_bitvector()

bvt boolbvt::convert_bitvector ( const exprt expr)
virtual

Converts an expression into its gate-level representation and returns a vector of literals corresponding to the outputs of the Boolean circuit.

Parameters
exprExpression to convert
Returns
A vector of literals corresponding to the outputs of the Boolean circuit
Exceptions
bitvector_conversion_exceptiontraised if converting byte_extraction goes wrong. TODO: extend for other types of conversion exception (diffblue/cbmc#2103).

Reimplemented in bv_pointerst, and bv_cbmct.

Definition at line 163 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_bswap(), convert_bv(), 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_let(), 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(), lower_popcount(), decision_proceduret::ns, exprt::op0(), exprt::op1(), exprt::operands(), prop_conv_solvert::prop, to_abs_expr(), string_constantt::to_array_expr(), to_array_of_expr(), to_binary_expr(), to_bswap_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_let_expr(), to_member_expr(), to_mod_expr(), to_not_expr(), to_popcount_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 bv_pointerst::convert_bitvector(), and convert_bv().

◆ convert_bitwise()

◆ convert_bswap()

bvt boolbvt::convert_bswap ( const bswap_exprt expr)
protectedvirtual

◆ convert_bv()

const bvt & boolbvt::convert_bv ( const exprt expr)
virtual

Definition at line 116 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(), boolbv_set_equality_to_true(), convert_abs(), convert_add_sub(), convert_array(), convert_array_of(), bv_pointerst::convert_bitvector(), convert_bitvector(), convert_bitwise(), convert_bswap(), 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(), convert_ieee_float_rel(), convert_if(), convert_index(), convert_lambda(), convert_let(), 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(), 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().

◆ convert_bv_literals()

bvt boolbvt::convert_bv_literals ( const exprt expr)
protectedvirtual

◆ convert_bv_reduction()

◆ convert_bv_rel()

◆ convert_bv_typecast()

bvt boolbvt::convert_bv_typecast ( const typecast_exprt expr)
protectedvirtual

◆ convert_byte_extract()

◆ convert_byte_update()

◆ convert_case()

◆ convert_complex()

bvt boolbvt::convert_complex ( const exprt expr)
protectedvirtual

◆ convert_complex_imag()

bvt boolbvt::convert_complex_imag ( const exprt expr)
protectedvirtual

◆ convert_complex_real()

bvt boolbvt::convert_complex_real ( const exprt expr)
protectedvirtual

◆ convert_concatenation()

bvt boolbvt::convert_concatenation ( const exprt expr)
protectedvirtual

◆ convert_cond()

◆ convert_constant()

◆ convert_constraint_select_one()

◆ convert_div()

◆ convert_equality()

◆ convert_extractbit()

◆ convert_extractbits()

◆ convert_floatbv_op()

◆ convert_floatbv_typecast()

◆ convert_function_application()

bvt boolbvt::convert_function_application ( const function_application_exprt expr)
protectedvirtual

◆ convert_ieee_float_rel()

◆ convert_if()

◆ convert_index() [1/2]

◆ convert_index() [2/2]

◆ convert_lambda()

bvt boolbvt::convert_lambda ( const exprt expr)
protectedvirtual

◆ convert_let()

◆ convert_member()

◆ convert_mod()

bvt boolbvt::convert_mod ( const mod_exprt expr)
protectedvirtual

◆ convert_mult()

◆ convert_not()

◆ convert_onehot()

literalt boolbvt::convert_onehot ( const unary_exprt expr)
protectedvirtual

◆ convert_overflow()

◆ convert_power()

◆ convert_quantifier()

◆ convert_reduction()

literalt boolbvt::convert_reduction ( const unary_exprt expr)
protectedvirtual

◆ convert_replication()

bvt boolbvt::convert_replication ( const replication_exprt expr)
protectedvirtual

◆ convert_rest()

◆ convert_shift()

◆ convert_struct()

◆ convert_symbol()

◆ convert_typecast()

literalt boolbvt::convert_typecast ( const typecast_exprt expr)
protectedvirtual

◆ convert_unary_minus()

◆ convert_union()

◆ convert_update()

bvt boolbvt::convert_update ( const exprt expr)
protectedvirtual

◆ convert_update_rec()

◆ convert_vector()

bvt boolbvt::convert_vector ( const exprt expr)
protectedvirtual

◆ convert_verilog_case_equality()

◆ convert_with() [1/2]

◆ convert_with() [2/2]

◆ convert_with_array()

void boolbvt::convert_with_array ( const array_typet type,
const exprt op1,
const exprt op2,
const bvt prev_bv,
bvt next_bv 
)
protected

◆ convert_with_bv()

void boolbvt::convert_with_bv ( const typet type,
const exprt op1,
const exprt op2,
const bvt prev_bv,
bvt next_bv 
)
protected

◆ convert_with_struct()

void boolbvt::convert_with_struct ( const struct_typet type,
const exprt op1,
const exprt op2,
const bvt prev_bv,
bvt next_bv 
)
protected

◆ convert_with_union()

◆ get()

◆ get_map()

const boolbv_mapt& boolbvt::get_map ( ) const
inline

Definition at line 85 of file boolbv.h.

References map.

Referenced by cbmc_dimacst::write_dimacs().

◆ get_value() [1/2]

mp_integer boolbvt::get_value ( const bvt bv)
inline

Definition at line 78 of file boolbv.h.

Referenced by bv_refinementt::get_values().

◆ get_value() [2/2]

mp_integer boolbvt::get_value ( const bvt bv,
std::size_t  offset,
std::size_t  width 
)

◆ is_unbounded_array()

◆ literal()

◆ make_bv_expr()

exprt boolbvt::make_bv_expr ( const typet type,
const bvt bv 
)
protectedvirtual

Definition at line 611 of file boolbv.cpp.

References irept::add(), irept::get_sub(), and to_string().

Referenced by make_free_bv_expr().

◆ make_free_bv_expr()

exprt boolbvt::make_free_bv_expr ( const typet type)
protectedvirtual

◆ post_process()

void boolbvt::post_process ( )
inlineoverridevirtual

Reimplemented from arrayst.

Reimplemented in bv_pointerst.

Definition at line 60 of file boolbv.h.

References functions, arrayst::post_process(), functionst::post_process(), and post_process_quantifiers().

Referenced by bv_pointerst::post_process().

◆ post_process_quantifiers()

void boolbvt::post_process_quantifiers ( )
protected

◆ print_assignment()

void boolbvt::print_assignment ( std::ostream &  out) const
overridevirtual

◆ set_to()

void boolbvt::set_to ( const exprt expr,
bool  value 
)
overridevirtual

◆ type_conversion()

Member Data Documentation

◆ boolbv_width

◆ bv_cache

bv_cachet boolbvt::bv_cache
protected

Definition at line 116 of file boolbv.h.

Referenced by bv_get_cache(), clear_cache(), and convert_bv().

◆ bv_utils

◆ functions

functionst boolbvt::functions
protected

Definition at line 96 of file boolbv.h.

Referenced by convert_function_application(), and post_process().

◆ map

◆ quantifier_list

quantifier_listt boolbvt::quantifier_list
protected

Definition at line 248 of file boolbv.h.

Referenced by convert_quantifier(), and post_process_quantifiers().

◆ string_numbering

numbering<irep_idt> boolbvt::string_numbering
protected

Definition at line 256 of file boolbv.h.

Referenced by bv_get_rec(), and convert_constant().

◆ unbounded_array

unbounded_arrayt boolbvt::unbounded_array

Definition at line 76 of file boolbv.h.

Referenced by is_unbounded_array().


The documentation for this class was generated from the following files: