spot::bdd_dict Class Reference

Map BDD variables to formulas. More...

#include <spot/twa/bdddict.hh>

Collaboration diagram for spot::bdd_dict:

Classes
struct	bdd_info
	Information stored for one BDD variable. More...

Public Types
enum	var_type { anon = 0 , var , acc }
	Type of a BDD variable in the dictionary. More...
typedef std::map< formula, int >	fv_map
	Formula-to-BDD-variable maps.
typedef std::map< int, formula >	vf_map
	BDD-variable-to-formula maps.
typedef std::set< const void * >	ref_set
	BDD-variable reference counts.
typedef std::vector< bdd_info >	bdd_info_map
	Type of the per-variable information table.

Public Member Functions
	~bdd_dict ()
	Destroy the BDD dict.
int	varnum (formula f)
	Return the BDD variable number for a registered proposition.
formula	ap_from_var (int var) const
	Return the atomic proposition associated to a BDD variable.
void	unregister_all_my_variables (const void *me)
	Release all variables used by an object.
std::ostream &	dump (std::ostream &os) const
	Dump all variables for debugging.
void	assert_emptiness () const
	Make sure the dictionary is empty.
int	register_proposition (formula f, const void *for_me)
	Register an atomic proposition.
template<typename T >
int	register_proposition (formula f, std::shared_ptr< T > for_me)
	Register an atomic proposition.
int	has_registered_proposition (formula f, const void *me)
	Whether a proposition has already been registered.
template<typename T >
int	has_registered_proposition (formula f, std::shared_ptr< T > for_me)
	Whether a proposition has already been registered.
int	register_acceptance_variable (formula f, const void *for_me)
	Register an acceptance variable.
template<typename T >
int	register_acceptance_variable (formula f, std::shared_ptr< T > for_me)
	Register an acceptance variable.
int	register_anonymous_variables (int n, const void *for_me)
	Register anonymous BDD variables.
template<typename T >
int	register_anonymous_variables (int n, std::shared_ptr< T > for_me)
	Register anonymous BDD variables.
void	register_all_variables_of (const void *from_other, const void *for_me)
	Duplicate the variable usage of another object.
template<typename T >
void	register_all_variables_of (const void *from_other, std::shared_ptr< T > for_me)
	Duplicate the variable usage of another object.
template<typename T >
void	register_all_variables_of (std::shared_ptr< T > from_other, const void *for_me)
	Duplicate the variable usage of another object.
template<typename T , typename U >
void	register_all_variables_of (std::shared_ptr< T > from_other, std::shared_ptr< U > for_me)
	Duplicate the variable usage of another object.
void	register_all_propositions_of (const void *from_other, const void *for_me)
	Duplicate the proposition usage of another object.
template<typename T >
void	register_all_propositions_of (const void *from_other, std::shared_ptr< T > for_me)
	Duplicate the proposition usage of another object.
template<typename T >
void	register_all_propositions_of (std::shared_ptr< T > from_other, const void *for_me)
	Duplicate the proposition usage of another object.
template<typename T , typename U >
void	register_all_propositions_of (std::shared_ptr< T > from_other, std::shared_ptr< U > for_me)
	Duplicate the proposition usage of another object.
void	unregister_variable (int var, const void *me)
	Release a variable used by me.
template<typename T >
void	unregister_variable (int var, std::shared_ptr< T > me)
	Release a variable used by me.

Public Attributes
fv_map	var_map
	Maps atomic propositions to BDD variables.
fv_map	acc_map
	Maps acceptance conditions to BDD variables.
bdd_info_map	bdd_map
	Table mapping BDD variable numbers to their meaning.

Detailed Description

Map BDD variables to formulas.

The BDD library uses integers to designate Boolean variables in its decision diagrams. This class is used to map such integers to objects actually used in Spot. These objects are usually atomic propositions, but they can also be acceptance conditions.

When a BDD variable is registered using a bdd_dict, it is always associated to a "user" (or "owner") object. This is done by supplying the bdd_dict with a pointer to the intended user of the variable. When the user object dies, it should release the BDD variables it was using by calling (for instance) unregister_all_my_variables(), giving the same pointer. Variables can also by unregistered one by one using unregister_variable().

Member Typedef Documentation

bdd_info_map

typedef std::vector<bdd_info> spot::bdd_dict::bdd_info_map

Type of the per-variable information table.

fv_map

typedef std::map<formula, int> spot::bdd_dict::fv_map

Formula-to-BDD-variable maps.

ref_set

typedef std::set<const void*> spot::bdd_dict::ref_set

BDD-variable reference counts.

vf_map

typedef std::map<int, formula> spot::bdd_dict::vf_map

BDD-variable-to-formula maps.

Member Enumeration Documentation

var_type

enum spot::bdd_dict::var_type

Type of a BDD variable in the dictionary.

Variables can be anonymous (e.g., temporary), represent atomic propositions, or represent acceptance conditions.

Enumerator
anon	Anonymous variable (no formula associated).
var	Atomic-proposition variable.
acc	Acceptance-condition variable.

Constructor & Destructor Documentation

~bdd_dict()

spot::bdd_dict::~bdd_dict

(

)

Destroy the BDD dict.

This always calls assert_emptiness() to diagnose cases where variables have not been unregistered.

Member Function Documentation

ap_from_var()

formula spot::bdd_dict::ap_from_var ( int  var ) const

inline

Return the atomic proposition associated to a BDD variable.

Given a BDD variable number var, returns the atomic proposition formula it represents, or nullptr if the variable is not an atomic proposition (e.g., it is an acceptance variable or an anonymous variable).

assert_emptiness()

void spot::bdd_dict::assert_emptiness

(

)

const

Make sure the dictionary is empty.

This will print diagnostics if the dictionary is not empty. Use for debugging. This is called automatically by the destructor. When Spot is compiled in development mode (i.e., with ./configure –enable-devel), this function will abort if the dictionary is not empty.

The errors detected by this function usually indicate missing calls to unregister_variable() or unregister_all_my_variables().

dump()

std::ostream & spot::bdd_dict::dump

(

std::ostream &

os

)

const

Dump all variables for debugging.

Parameters

os	The output stream.

has_registered_proposition() [1/2]

int spot::bdd_dict::has_registered_proposition	(	formula	f,
		const void *	me
	)

Whether a proposition has already been registered.

If f has been registered for me, this returns a non-negative value that is the BDD variable number. Otherwise this returns -1.

has_registered_proposition() [2/2]

template<typename T >

int spot::bdd_dict::has_registered_proposition ( formula  f, std::shared_ptr< T >  for_me  )

inline

Whether a proposition has already been registered.

If f has been registered for me, this returns a non-negative value that is the BDD variable number. Otherwise this returns -1.

register_acceptance_variable() [1/2]

int spot::bdd_dict::register_acceptance_variable	(	formula	f,
		const void *	for_me
	)

Register an acceptance variable.

Return (and maybe allocate) a BDD variable designating an acceptance set associated to formula f. The for_me argument should point to the object using this BDD variable, this is used for reference counting. It is perfectly safe to call this function several times with the same arguments.

Returns

The variable number. Use bdd_ithvar() or bdd_nithvar() to convert this to a BDD.

register_acceptance_variable() [2/2]

template<typename T >

int spot::bdd_dict::register_acceptance_variable ( formula  f, std::shared_ptr< T >  for_me  )

inline

Register an acceptance variable.

Return (and maybe allocate) a BDD variable designating an acceptance set associated to formula f. The for_me argument should point to the object using this BDD variable, this is used for reference counting. It is perfectly safe to call this function several times with the same arguments.

Returns

The variable number. Use bdd_ithvar() or bdd_nithvar() to convert this to a BDD.

register_all_propositions_of() [1/4]

void spot::bdd_dict::register_all_propositions_of	(	const void *	from_other,
		const void *	for_me
	)

Duplicate the proposition usage of another object.

This tells this dictionary that the for_me object will be using the same BDD variables as the from_other objects. This ensures that the variables won't be freed when from_other is deleted if from_other is still alive.

register_all_propositions_of() [2/4]

template<typename T >

void spot::bdd_dict::register_all_propositions_of ( const void *  from_other, std::shared_ptr< T >  for_me  )

inline

Duplicate the proposition usage of another object.

This tells this dictionary that the for_me object will be using the same BDD variables as the from_other objects. This ensures that the variables won't be freed when from_other is deleted if from_other is still alive.

register_all_propositions_of() [3/4]

template<typename T >

void spot::bdd_dict::register_all_propositions_of ( std::shared_ptr< T >  from_other, const void *  for_me  )

inline

Duplicate the proposition usage of another object.

This tells this dictionary that the for_me object will be using the same BDD variables as the from_other objects. This ensures that the variables won't be freed when from_other is deleted if from_other is still alive.

register_all_propositions_of() [4/4]

template<typename T , typename U >

void spot::bdd_dict::register_all_propositions_of ( std::shared_ptr< T >  from_other, std::shared_ptr< U >  for_me  )

inline

Duplicate the proposition usage of another object.

This tells this dictionary that the for_me object will be using the same BDD variables as the from_other objects. This ensures that the variables won't be freed when from_other is deleted if from_other is still alive.

register_all_variables_of() [1/4]

void spot::bdd_dict::register_all_variables_of	(	const void *	from_other,
		const void *	for_me
	)

Duplicate the variable usage of another object.

This tells this dictionary that the for_me object will be using the same BDD variables as the from_other objects. This ensures that the variables won't be freed when from_other is deleted if from_other is still alive.

register_all_variables_of() [2/4]

template<typename T >

void spot::bdd_dict::register_all_variables_of ( const void *  from_other, std::shared_ptr< T >  for_me  )

inline

Duplicate the variable usage of another object.

This tells this dictionary that the for_me object will be using the same BDD variables as the from_other objects. This ensures that the variables won't be freed when from_other is deleted if from_other is still alive.

register_all_variables_of() [3/4]

template<typename T >

void spot::bdd_dict::register_all_variables_of ( std::shared_ptr< T >  from_other, const void *  for_me  )

inline

Duplicate the variable usage of another object.

This tells this dictionary that the for_me object will be using the same BDD variables as the from_other objects. This ensures that the variables won't be freed when from_other is deleted if from_other is still alive.

register_all_variables_of() [4/4]

template<typename T , typename U >

void spot::bdd_dict::register_all_variables_of ( std::shared_ptr< T >  from_other, std::shared_ptr< U >  for_me  )

inline

Duplicate the variable usage of another object.

This tells this dictionary that the for_me object will be using the same BDD variables as the from_other objects. This ensures that the variables won't be freed when from_other is deleted if from_other is still alive.

register_anonymous_variables() [1/2]

int spot::bdd_dict::register_anonymous_variables	(	int	n,
		const void *	for_me
	)

Register anonymous BDD variables.

Return (and maybe allocate) n consecutive BDD variables which will be used only by for_me.

Returns

The variable number. Use bdd_ithvar() or bdd_nithvar() to convert this to a BDD.

register_anonymous_variables() [2/2]

template<typename T >

int spot::bdd_dict::register_anonymous_variables ( int  n, std::shared_ptr< T >  for_me  )

inline

Register anonymous BDD variables.

Return (and maybe allocate) n consecutive BDD variables which will be used only by for_me.

Returns

The variable number. Use bdd_ithvar() or bdd_nithvar() to convert this to a BDD.

register_proposition() [1/2]

int spot::bdd_dict::register_proposition	(	formula	f,
		const void *	for_me
	)

Register an atomic proposition.

Return (and maybe allocate) a BDD variable designating formula f. The for_me argument should point to the object using this BDD variable, this is used for reference counting. It is perfectly safe to call this function several times with the same arguments.

Returns

The variable number. Use bdd_ithvar() or bdd_nithvar() to convert this to a BDD.

register_proposition() [2/2]

template<typename T >

int spot::bdd_dict::register_proposition ( formula  f, std::shared_ptr< T >  for_me  )

inline

Register an atomic proposition.

Return (and maybe allocate) a BDD variable designating formula f. The for_me argument should point to the object using this BDD variable, this is used for reference counting. It is perfectly safe to call this function several times with the same arguments.

Returns

The variable number. Use bdd_ithvar() or bdd_nithvar() to convert this to a BDD.

unregister_all_my_variables()

void spot::bdd_dict::unregister_all_my_variables

(

const void *

me

)

Release all variables used by an object.

Usually called in the destructor of me.

unregister_variable() [1/2]

void spot::bdd_dict::unregister_variable	(	int	var,
		const void *	me
	)

Release a variable used by me.

unregister_variable() [2/2]

template<typename T >

void spot::bdd_dict::unregister_variable ( int  var, std::shared_ptr< T >  me  )

inline

Release a variable used by me.

varnum()

int spot::bdd_dict::varnum ( formula  f )

inline

Return the BDD variable number for a registered proposition.

Exceptions

std::out_of_range

if f is not a known proposition.

Member Data Documentation

acc_map

fv_map spot::bdd_dict::acc_map

Maps acceptance conditions to BDD variables.

bdd_map

bdd_info_map spot::bdd_dict::bdd_map

Table mapping BDD variable numbers to their meaning.

var_map

fv_map spot::bdd_dict::var_map

Maps atomic propositions to BDD variables.

---

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

• spot/twa/bdddict.hh