A dictionary that maps variable names to indices and vice versa. More...

#include <VarMgr.h>

Public Member Functions
	VarMgr ()
	Constructs a VarMgr with no variables.

void	create_named_variables (const std::vector< std::string > &variable_names)
	Creates BDD variables and associates each with a name. More...

std::size_t	create_state_variables (std::size_t variable_count)
	Creates and stores state variables. More...

std::size_t	create_product_state_space (const std::vector< std::size_t > &automaton_ids)
	Registers a new automaton ID associated with a product state space. More...

CUDD::BDD	state_variable (std::size_t automaton_id, std::size_t i) const
	Returns the i-th state variable for a given automaton.

CUDD::BDD	state_vector_to_bdd (std::size_t automaton_id, const std::vector< int > &state_vector) const
	Converts a state vector to a BDD. More...

void	partition_variables (const std::vector< std::string > &input_names, const std::vector< std::string > &output_names)
	Partitions the named variables between inputs and outputs. More...

std::shared_ptr< CUDD::Cudd >	cudd_mgr () const
	Returns the CUDD manager used to create the variables.

CUDD::BDD	name_to_variable (const std::string &name) const
	Returns the index of the variable with the given name.

std::string	index_to_name (int index) const
	Returns the name of the variable at index index.

std::size_t	total_variable_count () const
	Returns the total number of variables, including named and state.

std::size_t	total_state_variable_count () const
	Returns the total number of state variables.

std::size_t	state_variable_count (std::size_t automaton_id) const
	Returns the number of state variables for a given automaton.

std::size_t	input_variable_count () const
	Returns the number of input variables.

std::size_t	output_variable_count () const
	Returns the number of output variables.

CUDD::BDD	input_cube () const
	Returns a BDD formed by the conjunction of all input variables.

CUDD::BDD	output_cube () const
	Returns a BDD formed by the conjunction of all output variables.

CUDD::BDD	state_variables_cube (std::size_t automaton_id) const
	Returns a BDD formed by the conjunction of all state variables of automaton automaton_id.

std::vector< int >	make_eval_vector (std::size_t automaton_id, const std::vector< int > &state_vector) const
	Creates a valid input to CUDD::BDD::Eval. More...

std::vector< int >	make_state_eval_vector (std::size_t automaton_id, const std::vector< int > &state_vector) const
	Creates a valid input to CUDD::BDD::Eval. More...

std::vector< CUDD::BDD >	make_compose_vector (std::size_t automaton_id, const std::vector< CUDD::BDD > &state_bdds) const
	Creates a valid input to CUDD::BDD::VectorCompose. More...

std::vector< std::string >	variable_labels () const
	Returns a vector with a label for each variable. More...

std::vector< std::string >	input_variable_labels () const
	Returns a vector with a label for each input variable. More...

std::vector< std::string >	output_variable_labels () const
	Returns a vector with a label for each output variable. More...

std::vector< std::string >	state_variable_labels (std::size_t automaton_id) const
	Returns a vector with a label for each state variable. More...

void	dump_dot (const CUDD::ADD &add, const std::string &filename) const
	Saves an ADD in a .dot file. More...

void	dump_dot (const std::vector< CUDD::ADD > &adds, const std::vector< std::string > &function_labels, const std::string &filename) const
	Saves ADDs to a .dot file with corresponding labels. More...

std::size_t	automaton_num () const
	Returns the number of DFAs the manager handles.

std::string	bdd_to_string (const CUDD::BDD &bdd) const
	Prints a BDD as a Boolean formula, where each variable has a specific label. More...

std::size_t	create_complement_state_space (const std::size_t automaton_id)
	Create the state space when complementing a DFA.

Detailed Description

A dictionary that maps variable names to indices and vice versa.

Member Function Documentation

◆ bdd_to_string()

std::string Syft::VarMgr::bdd_to_string ( const CUDD::BDD & bdd ) const

Prints a BDD as a Boolean formula, where each variable has a specific label.

Parameters

A	given BDD.

Returns: A string that represents a Boolean formula.

◆ create_named_variables()

void Syft::VarMgr::create_named_variables ( const std::vector< std::string > & variable_names )

Creates BDD variables and associates each with a name.

Parameters

variable_names The names of the variables to create. A new variable is only created if a variable by that name does not already exist.

◆ create_product_state_space()

std::size_t Syft::VarMgr::create_product_state_space ( const std::vector< std::size_t > & automaton_ids )

Registers a new automaton ID associated with a product state space.

This function does not create new state variables. Instead, the variables associated with the new ID are the union of all variables for the automata that form the product.

Parameters

automaton_ids A vector of automaton IDs all of which must already exist in the manager.

Returns: The automaton ID for the automaton formed by taking the product of the automata whose IDs were provided in automaton_ids.

◆ create_state_variables()

std::size_t Syft::VarMgr::create_state_variables ( std::size_t variable_count )

Creates and stores state variables.

Multiple calls of this function create separate groups of state variables. The call generates an ID for the automaton whose state space the variables represent, so that the correct group of variables can be retrieved later.

Parameters

variable_count The number of state variables to create.

Returns: The automaton ID the variables are associated with.

◆ dump_dot() [1/2]

void Syft::VarMgr::dump_dot	(	const CUDD::ADD &	add,
		const std::string &	filename
	)		const

Saves an ADD in a .dot file.

Uses ADD for better visualization in the .dot file. To call with a BDD, use dump_dot(bdd.Add(), filename).

Parameters

An	ADD add and filename.

◆ dump_dot() [2/2]

void Syft::VarMgr::dump_dot	(	const std::vector< CUDD::ADD > &	adds,
		const std::vector< std::string > &	function_labels,
		const std::string &	filename
	)		const

Saves ADDs to a .dot file with corresponding labels.

Parameters

adds	A vector of ADDs to be saved to file.
function_labels	A vector such that function_labels[i] contains the label for adds[i]. The labels appear above the corresponding ADD in the file.
filename	The name of the .dot file.

◆ input_variable_labels()

std::vector< std::string > Syft::VarMgr::input_variable_labels ( ) const

Returns a vector with a label for each input variable.

To be used with CUDD::Cudd::DumpDot.

Returns: A vector v such that v[i] contains the name of the i-th input variable.

◆ make_compose_vector()

std::vector< CUDD::BDD > Syft::VarMgr::make_compose_vector	(	std::size_t	automaton_id,
		const std::vector< CUDD::BDD > &	state_bdds
	)		const

Creates a valid input to CUDD::BDD::VectorCompose.

Parameters

automaton_id	The ID of the automaton whose variables to use.
state_bdds	A vector containing one BDD for each state variable of the automaton.

Returns: A vector with one position for each BDD variable, including both named and state variables, where the index corresponding to the i-th state variable of the requested automaton contains state_bdds[i]. Indices corresponding to other variables have the identity BDD for that variable.

◆ make_eval_vector()

std::vector< int > Syft::VarMgr::make_eval_vector	(	std::size_t	automaton_id,
		const std::vector< int > &	state_vector
	)		const

Creates a valid input to CUDD::BDD::Eval.

Parameters

automaton_id	The ID of the automaton whose variables to use.
state_vector	A vector of 1s and 0s encoding a state's binary representation.

Returns: A vector with one position for each BDD variable, including both named and state variables, where the index corresponding to the i-th state variable of the requested automaton contains state_vector[i]. Indices corresponding to other variables have a 0.

◆ make_state_eval_vector()

std::vector< int > Syft::VarMgr::make_state_eval_vector	(	std::size_t	automaton_id,
		const std::vector< int > &	state_vector
	)		const

Creates a valid input to CUDD::BDD::Eval.

Parameters

automaton_id	The ID of the automaton whose variables to use.
state_vector	A vector of 1s and 0s encoding a state's binary representation.

Returns: A vector with one position for each BDD variable, including only state variables, where the index corresponding to the i-th state variable of the requested automaton contains state_vector[i]. Indices corresponding to other variables have a 0.

◆ output_variable_labels()

std::vector< std::string > Syft::VarMgr::output_variable_labels ( ) const

Returns a vector with a label for each output variable.

To be used with CUDD::Cudd::DumpDot.

Returns: A vector v such that v[i] contains the name of the i-th output variable.

◆ partition_variables()

void Syft::VarMgr::partition_variables	(	const std::vector< std::string > &	input_names,
		const std::vector< std::string > &	output_names
	)

Partitions the named variables between inputs and outputs.

Parameters

input_names	The names of the variables that should be considered inputs.
output_names	The names of the variables that should be considered outputs.

◆ state_variable_labels()

std::vector< std::string > Syft::VarMgr::state_variable_labels ( std::size_t automaton_id ) const

Returns a vector with a label for each state variable.

To be used with CUDD::Cudd::DumpDot.

Returns: A vector v such that v[i] has a label for the i-th state variable. The label is the same as the one used in variable_labels().

◆ state_vector_to_bdd()

CUDD::BDD Syft::VarMgr::state_vector_to_bdd	(	std::size_t	automaton_id,
		const std::vector< int > &	state_vector
	)		const

Converts a state vector to a BDD.

Parameters

automaton_id	The ID of the automaton whose variables to use.
state_vector	A vector of 1s and 0s encoding a state's binary representation.

Returns: A BDD representing a conjunction (l_1 & l_2 & ... & l_n) where l_i = !x_i if state_vector[i] = 0 and l_i = x_i otherwise, where x_i is the i-th state variable of the automaton with the given ID.

◆ variable_labels()

std::vector< std::string > Syft::VarMgr::variable_labels ( ) const

Returns a vector with a label for each variable.

To be used with CUDD::Cudd::DumpDot.

Returns: A vector v such that v[i] has a label for the variable with index i. For named variables the label is the variable's name. For state variables the label is a representation that indicates which automaton the variable is from and which bit of the state it represents.

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

src/synthesis/header/VarMgr.h
src/synthesis/source/VarMgr.cpp

Public Member Functions

Detailed Description

Member Function Documentation

◆ bdd_to_string()

◆ create_named_variables()

◆ create_product_state_space()

◆ create_state_variables()

◆ dump_dot() [1/2]

◆ dump_dot() [2/2]

◆ input_variable_labels()

◆ make_compose_vector()

◆ make_eval_vector()

◆ make_state_eval_vector()

◆ output_variable_labels()

◆ partition_variables()

◆ state_variable_labels()

◆ state_vector_to_bdd()

◆ variable_labels()