boolbv_mapt Class Reference

#include <boolbv_map.h>

Collaboration diagram for boolbv_mapt:

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

Detailed Description

Definition at line 23 of file boolbv_map.h.

Member Typedef Documentation

literal_mapt

typedef std::vector<map_bitt> boolbv_mapt::literal_mapt

Definition at line 41 of file boolbv_map.h.

mappingt

typedef std::unordered_map<irep_idt, map_entryt, irep_id_hash> boolbv_mapt::mappingt

Definition at line 58 of file boolbv_map.h.

Constructor & Destructor Documentation

boolbv_mapt()

boolbv_mapt::boolbv_mapt ( propt &  _prop, const namespacet &  _ns, const boolbv_widtht &  _boolbv_width  )

inline

Definition at line 26 of file boolbv_map.h.

Member Function Documentation

get_literals()

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(), and prop.

Referenced by bv_pointerst::convert_pointer_type(), and boolbvt::convert_symbol().

get_map_entry()

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, 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().

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().

show()

void boolbv_mapt::show

(

)

const

Definition at line 75 of file boolbv_map.cpp.

References mapping.

Member Data Documentation

boolbv_width

const boolbv_widtht& boolbv_mapt::boolbv_width

protected

Definition at line 81 of file boolbv_map.h.

Referenced by get_map_entry().

mapping

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().

ns

const namespacet& boolbv_mapt::ns

protected

Definition at line 80 of file boolbv_map.h.

Referenced by get_map_entry().

prop

propt& boolbv_mapt::prop

protected

Definition at line 79 of file boolbv_map.h.

Referenced by get_literals(), boolbv_mapt::map_entryt::get_value(), and set_literals().

---

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

• solvers/flattening/boolbv_map.h
• solvers/flattening/boolbv_map.cpp