cprover
|
#include <boolbv_map.h>
Classes | |
struct | map_bitt |
class | map_entryt |
Public Types | |
typedef std::vector< map_bitt > | literal_mapt |
typedef std::unordered_map< irep_idt, map_entryt, irep_id_hash > | mappingt |
Public Member Functions | |
boolbv_mapt (propt &_prop, const namespacet &_ns, const boolbv_widtht &_boolbv_width) | |
void | show () const |
map_entryt & | get_map_entry (const irep_idt &identifier, const typet &type) |
void | get_literals (const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals) |
void | set_literals (const irep_idt &identifier, const typet &type, const bvt &literals) |
Public Attributes | |
mappingt | mapping |
Protected Attributes | |
propt & | prop |
const namespacet & | ns |
const boolbv_widtht & | boolbv_width |
Definition at line 23 of file boolbv_map.h.
typedef std::vector<map_bitt> boolbv_mapt::literal_mapt |
Definition at line 41 of file boolbv_map.h.
typedef std::unordered_map<irep_idt, map_entryt, irep_id_hash> boolbv_mapt::mappingt |
Definition at line 58 of file boolbv_map.h.
|
inline |
Definition at line 26 of file boolbv_map.h.
void boolbv_mapt::get_literals | ( | const irep_idt & | identifier, |
const typet & | type, | ||
const std::size_t | width, | ||
bvt & | literals | ||
) |
Definition at line 84 of file boolbv_map.cpp.
References Forall_literals, get_map_entry(), literalt::l, boolbv_mapt::map_entryt::literal_map, propt::new_variable(), prop, and boolbv_mapt::map_entryt::width.
Referenced by bv_pointerst::convert_pointer_type(), and boolbvt::convert_symbol().
boolbv_mapt::map_entryt & boolbv_mapt::get_map_entry | ( | const irep_idt & | identifier, |
const typet & | type | ||
) |
Definition at line 49 of file boolbv_map.cpp.
References boolbv_width, boolbv_mapt::map_entryt::bvtype, namespace_baset::follow(), get_bvtype(), irept::id(), boolbv_mapt::map_entryt::literal_map, boolbv_mapt::map_entryt::map_entryt(), mapping, ns, boolbv_mapt::map_entryt::type, and boolbv_mapt::map_entryt::width.
Referenced by boolbvt::convert_index(), boolbvt::convert_symbol(), get_literals(), and set_literals().
void boolbv_mapt::set_literals | ( | const irep_idt & | identifier, |
const typet & | type, | ||
const bvt & | literals | ||
) |
Definition at line 121 of file boolbv_map.cpp.
References forall_literals, get_map_entry(), literalt::is_constant(), boolbv_mapt::map_entryt::literal_map, propt::no_variables(), prop, propt::set_equal(), and literalt::var_no().
Referenced by string_refinementt::boolbv_set_equality_to_true(), and boolbvt::boolbv_set_equality_to_true().
void boolbv_mapt::show | ( | ) | const |
Definition at line 75 of file boolbv_map.cpp.
References mapping.
|
protected |
Definition at line 81 of file boolbv_map.h.
Referenced by get_map_entry().
mappingt boolbv_mapt::mapping |
Definition at line 59 of file boolbv_map.h.
Referenced by boolbvt::get(), get_map_entry(), boolbvt::literal(), boolbvt::print_assignment(), and show().
|
protected |
Definition at line 80 of file boolbv_map.h.
Referenced by get_map_entry().
|
protected |
Definition at line 79 of file boolbv_map.h.
Referenced by get_literals(), and set_literals().