Functional composition and variable permutation of DDs. More...

#include "util.h"
#include "cuddInt.h"

Include dependency graph for cuddCompose.c:

Functions
DdNode *	Cudd_bddCompose (DdManager dd, DdNode f, DdNode *g, int v)
	Substitutes g for x_v in the BDD for f. More...

DdNode *	Cudd_addCompose (DdManager dd, DdNode f, DdNode *g, int v)
	Substitutes g for x_v in the ADD for f. More...

DdNode *	Cudd_addPermute (DdManager manager, DdNode node, int *permut)
	Permutes the variables of an ADD. More...

DdNode *	Cudd_addSwapVariables (DdManager dd, DdNode f, DdNode x, DdNode y, int n)
	Swaps two sets of variables of the same size (x and y) in the ADD f. More...

DdNode *	Cudd_bddPermute (DdManager manager, DdNode node, int *permut)
	Permutes the variables of a BDD. More...

DdNode *	Cudd_bddVarMap (DdManager manager, DdNode f)
	Remaps the variables of a BDD using the default variable map. More...

int	Cudd_SetVarMap (DdManager manager, DdNode x, DdNode *y, int n)
	Registers a variable mapping with the manager. More...

DdNode *	Cudd_bddSwapVariables (DdManager dd, DdNode f, DdNode x, DdNode y, int n)
	Swaps two sets of variables of the same size (x and y) in the BDD f. More...

DdNode *	Cudd_bddAdjPermuteX (DdManager dd, DdNode B, DdNode **x, int n)
	Rearranges a set of variables in the BDD B. More...

DdNode *	Cudd_addVectorCompose (DdManager dd, DdNode f, DdNode **vector)
	Composes an ADD with a vector of 0-1 ADDs. More...

DdNode *	Cudd_addGeneralVectorCompose (DdManager dd, DdNode f, DdNode vectorOn, DdNode vectorOff)
	Composes an ADD with a vector of ADDs. More...

DdNode *	Cudd_addNonSimCompose (DdManager dd, DdNode f, DdNode **vector)
	Composes an ADD with a vector of 0-1 ADDs. More...

DdNode *	Cudd_bddVectorCompose (DdManager dd, DdNode f, DdNode **vector)
	Composes a BDD with a vector of BDDs. More...

DdNode *	cuddBddComposeRecur (DdManager dd, DdNode f, DdNode g, DdNode proj)
	Performs the recursive step of Cudd_bddCompose. More...

DdNode *	cuddAddComposeRecur (DdManager dd, DdNode f, DdNode g, DdNode proj)
	Performs the recursive step of Cudd_addCompose. More...

static DdNode *	cuddAddPermuteRecur (DdManager manager, DdHashTable table, DdNode node, int permut)
	Implements the recursive step of Cudd_addPermute. More...

static DdNode *	cuddBddPermuteRecur (DdManager manager, DdHashTable table, DdNode node, int permut)
	Implements the recursive step of Cudd_bddPermute. More...

static DdNode *	cuddBddVarMapRecur (DdManager manager, DdNode f)
	Implements the recursive step of Cudd_bddVarMap. More...

static DdNode *	cuddAddVectorComposeRecur (DdManager dd, DdHashTable table, DdNode f, DdNode *vector, int deepest)
	Performs the recursive step of Cudd_addVectorCompose. More...

static DdNode *	cuddAddGeneralVectorComposeRecur (DdManager dd, DdHashTable table, DdNode f, DdNode vectorOn, DdNode *vectorOff, int deepest)
	Performs the recursive step of Cudd_addGeneralVectorCompose. More...

static DdNode *	cuddAddNonSimComposeRecur (DdManager dd, DdNode f, DdNode *vector, DdNode key, DdNode *cube, int lastsub)
	Performs the recursive step of Cudd_addNonSimCompose. More...

static DdNode *	cuddBddVectorComposeRecur (DdManager dd, DdHashTable table, DdNode f, DdNode *vector, int deepest)
	Performs the recursive step of Cudd_bddVectorCompose. More...

static int	ddIsIthAddVar (DdManager dd, DdNode f, unsigned int i)
	Comparison of a function to the i-th ADD variable. More...

static int	ddIsIthAddVarPair (DdManager dd, DdNode f, DdNode *g, unsigned int i)
	Comparison of a pair of functions to the i-th ADD variable. More...

Detailed Description

Functional composition and variable permutation of DDs.

The permutation functions use a local cache because the results to be remembered depend on the permutation being applied. Since the permutation is just an array, it cannot be stored in the global cache. There are different procedured for BDDs and ADDs. This is because bddPermuteRecur uses cuddBddIteRecur. If this were changed, the procedures could be merged.

Author: Fabio Somenzi and Kavita Ravi

Copyright

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Function Documentation

◆ Cudd_addCompose()

DdNode* Cudd_addCompose	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		int	v
	)

Substitutes g for x_v in the ADD for f.

v is the index of the variable to be substituted. g must be a 0-1 ADD. Cudd_bddCompose passes the corresponding projection function to the recursive procedure, so that the cache may be used.

Returns: the composed ADD if successful; NULL otherwise.

Side effects None

See also: Cudd_bddCompose

◆ Cudd_addGeneralVectorCompose()

DdNode* Cudd_addGeneralVectorCompose	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vectorOn,
		DdNode **	vectorOff
	)

Composes an ADD with a vector of ADDs.

Given a vector of ADDs, creates a new ADD by substituting the ADDs for the variables of the ADD f. vectorOn contains ADDs to be substituted for the x_v and vectorOff the ADDs to be substituted for x_v'. There should be an entry in vector for each variable in the manager. If no substitution is sought for a given variable, the corresponding projection function should be specified in the vector. This function implements simultaneous composition.

Returns: a pointer to the resulting ADD if successful; NULL otherwise.

Side effects None

See also: Cudd_addVectorCompose Cudd_addNonSimCompose Cudd_addPermute Cudd_addCompose Cudd_bddVectorCompose

◆ Cudd_addNonSimCompose()

DdNode* Cudd_addNonSimCompose	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vector
	)

Composes an ADD with a vector of 0-1 ADDs.

Given a vector of 0-1 ADDs, creates a new ADD by substituting the 0-1 ADDs for the variables of the ADD f. There should be an entry in vector for each variable in the manager. This function implements non-simultaneous composition. If any of the functions being composed depends on any of the variables being substituted, then the result depends on the order of composition, which in turn depends on the variable order: The variables farther from the roots in the order are substituted first.

Returns: a pointer to the resulting ADD if successful; NULL otherwise.

Side effects None

See also: Cudd_addVectorCompose Cudd_addPermute Cudd_addCompose

◆ Cudd_addPermute()

DdNode* Cudd_addPermute	(	DdManager *	manager,
		DdNode *	node,
		int *	permut
	)

Permutes the variables of an ADD.

Given a permutation in array permut, creates a new ADD with permuted variables. There should be an entry in array permut for each variable in the manager. The i-th entry of permut holds the index of the variable that is to substitute the i-th variable.

Returns: a pointer to the resulting ADD if successful; NULL otherwise.

Side effects None

See also: Cudd_bddPermute Cudd_addSwapVariables

◆ Cudd_addSwapVariables()

DdNode* Cudd_addSwapVariables	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	x,
		DdNode **	y,
		int	n
	)

Swaps two sets of variables of the same size (x and y) in the ADD f.

The size is given by n. The two sets of variables are assumed to be disjoint.

Returns: a pointer to the resulting ADD if successful; NULL otherwise.

Side effects None

See also: Cudd_addPermute Cudd_bddSwapVariables

◆ Cudd_addVectorCompose()

DdNode* Cudd_addVectorCompose	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vector
	)

Composes an ADD with a vector of 0-1 ADDs.

Given a vector of 0-1 ADDs, creates a new ADD by substituting the 0-1 ADDs for the variables of the ADD f. There should be an entry in vector for each variable in the manager. If no substitution is sought for a given variable, the corresponding projection function should be specified in the vector. This function implements simultaneous composition.

Returns: a pointer to the resulting ADD if successful; NULL otherwise.

Side effects None

See also: Cudd_addNonSimCompose Cudd_addPermute Cudd_addCompose Cudd_bddVectorCompose

◆ Cudd_bddAdjPermuteX()

DdNode* Cudd_bddAdjPermuteX	(	DdManager *	dd,
		DdNode *	B,
		DdNode **	x,
		int	n
	)

Rearranges a set of variables in the BDD B.

The size of the set is given by n. This procedure is intended for the ‘randomization’ of the priority functions.

Returns: a pointer to the BDD if successful; NULL otherwise.

Side effects None

See also: Cudd_bddPermute Cudd_bddSwapVariables Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_PrioritySelect

◆ Cudd_bddCompose()

DdNode* Cudd_bddCompose	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		int	v
	)

Substitutes g for x_v in the BDD for f.

v is the index of the variable to be substituted. Cudd_bddCompose passes the corresponding projection function to the recursive procedure, so that the cache may be used.

Returns: the composed BDD if successful; NULL otherwise.

Side effects None

See also: Cudd_addCompose

◆ Cudd_bddPermute()

DdNode* Cudd_bddPermute	(	DdManager *	manager,
		DdNode *	node,
		int *	permut
	)

Permutes the variables of a BDD.

Given a permutation in array permut, creates a new BDD with permuted variables. There should be an entry in array permut for each variable in the manager. The i-th entry of permut holds the index of the variable that is to substitute the i-th variable.

Returns: a pointer to the resulting BDD if successful; NULL otherwise.

Side effects None

See also: Cudd_addPermute Cudd_bddSwapVariables

◆ Cudd_bddSwapVariables()

DdNode* Cudd_bddSwapVariables	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	x,
		DdNode **	y,
		int	n
	)

Swaps two sets of variables of the same size (x and y) in the BDD f.

The size is given by n. The two sets of variables are assumed to be disjoint.

Returns: a pointer to the resulting BDD if successful; NULL otherwise.

Side effects None

See also: Cudd_bddPermute Cudd_addSwapVariables

◆ Cudd_bddVarMap()

DdNode* Cudd_bddVarMap	(	DdManager *	manager,
		DdNode *	f
	)

Remaps the variables of a BDD using the default variable map.

A typical use of this function is to swap two sets of variables. The variable map must be registered with Cudd_SetVarMap.

Returns: a pointer to the resulting BDD if successful; NULL otherwise.

Side effects None

See also: Cudd_bddPermute Cudd_bddSwapVariables Cudd_SetVarMap

Parameters

manager	DD manager
f	function in which to remap variables

◆ Cudd_bddVectorCompose()

DdNode* Cudd_bddVectorCompose	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vector
	)

Composes a BDD with a vector of BDDs.

Given a vector of BDDs, creates a new BDD by substituting the BDDs for the variables of the BDD f. There should be an entry in vector for each variable in the manager. If no substitution is sought for a given variable, the corresponding projection function should be specified in the vector. This function implements simultaneous composition.

Returns: a pointer to the resulting BDD if successful; NULL otherwise.

Side effects None

See also: Cudd_bddPermute Cudd_bddCompose Cudd_addVectorCompose

◆ Cudd_SetVarMap()

int Cudd_SetVarMap	(	DdManager *	manager,
		DdNode **	x,
		DdNode **	y,
		int	n
	)

Registers a variable mapping with the manager.

Registers with the manager a variable mapping described by two sets of variables. This variable mapping is then used by functions like Cudd_bddVarMap. This function is convenient for those applications that perform the same mapping several times. However, if several different permutations are used, it may be more efficient not to rely on the registered mapping, because changing mapping causes the cache to be cleared. (The initial setting, however, does not clear the cache.) The two sets of variables (x and y) must have the same size (x and y). The size is given by n. The two sets of variables are normally disjoint, but this restriction is not imposeded by the function. When new variables are created, the map is automatically extended (each new variable maps to itself). The typical use, however, is to wait until all variables are created, and then create the map.

Returns: 1 if the mapping is successfully registered with the manager; 0 otherwise.

Side effects Modifies the manager. May clear the cache.

See also: Cudd_bddVarMap Cudd_bddPermute Cudd_bddSwapVariables

Parameters

manager	DD manager
x	first array of variables
y	second array of variables
n	length of both arrays

◆ cuddAddComposeRecur()

DdNode* cuddAddComposeRecur	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		DdNode *	proj
	)

Performs the recursive step of Cudd_addCompose.

Returns: the composed BDD if successful; NULL otherwise.

Side effects None

See also: Cudd_addCompose

◆ cuddAddGeneralVectorComposeRecur()

static DdNode* cuddAddGeneralVectorComposeRecur	(	DdManager *	dd,
		DdHashTable *	table,
		DdNode *	f,
		DdNode **	vectorOn,
		DdNode **	vectorOff,
		int	deepest
	)

static

Performs the recursive step of Cudd_addGeneralVectorCompose.

Side effects None

Parameters

dd	DD manager
table	computed table
f	ADD in which to compose
vectorOn	functions to substitute for x_i
vectorOff	functions to substitute for x_i'
deepest	depth of deepest substitution

◆ cuddAddNonSimComposeRecur()

static DdNode* cuddAddNonSimComposeRecur	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	vector,
		DdNode *	key,
		DdNode *	cube,
		int	lastsub
	)

static

Performs the recursive step of Cudd_addNonSimCompose.

Side effects None

◆ cuddAddPermuteRecur()

static DdNode* cuddAddPermuteRecur	(	DdManager *	manager,
		DdHashTable *	table,
		DdNode *	node,
		int *	permut
	)

static

Implements the recursive step of Cudd_addPermute.

Recursively puts the ADD in the order given in the array permut. Checks for trivial cases to terminate recursion, then splits on the children of this node. Once the solutions for the children are obtained, it puts into the current position the node from the rest of the ADD that should be here. Then returns this ADD. The key here is that the node being visited is NOT put in its proper place by this instance, but rather is switched when its proper position is reached in the recursion tree.

The DdNode * that is returned is the same ADD as passed in as node, but in the new order.

Side effects None

See also: Cudd_addPermute cuddBddPermuteRecur

Parameters

manager	DD manager
table	computed table
node	ADD to be reordered
permut	permutation array

◆ cuddAddVectorComposeRecur()

static DdNode* cuddAddVectorComposeRecur	(	DdManager *	dd,
		DdHashTable *	table,
		DdNode *	f,
		DdNode **	vector,
		int	deepest
	)

static

Performs the recursive step of Cudd_addVectorCompose.

Side effects None

Parameters

dd	DD manager
table	computed table
f	ADD in which to compose
vector	functions to substitute
deepest	depth of deepest substitution

◆ cuddBddComposeRecur()

DdNode* cuddBddComposeRecur	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		DdNode *	proj
	)

Performs the recursive step of Cudd_bddCompose.

Exploits the fact that the composition of f' with g produces the complement of the composition of f with g to better utilize the cache.

Returns: the composed BDD if successful; NULL otherwise.

Side effects None

See also: Cudd_bddCompose

◆ cuddBddPermuteRecur()

static DdNode* cuddBddPermuteRecur	(	DdManager *	manager,
		DdHashTable *	table,
		DdNode *	node,
		int *	permut
	)

static

Implements the recursive step of Cudd_bddPermute.

Recursively puts the BDD in the order given in the array permut. Checks for trivial cases to terminate recursion, then splits on the children of this node. Once the solutions for the children are obtained, it puts into the current position the node from the rest of the BDD that should be here. Then returns this BDD. The key here is that the node being visited is NOT put in its proper place by this instance, but rather is switched when its proper position is reached in the recursion tree.

The DdNode * that is returned is the same BDD as passed in as node, but in the new order.

Side effects None

See also: Cudd_bddPermute cuddAddPermuteRecur

Parameters

manager	DD manager
table	computed table
node	BDD to be reordered
permut	permutation array

◆ cuddBddVarMapRecur()

static DdNode* cuddBddVarMapRecur	(	DdManager *	manager,
		DdNode *	f
	)

static

Implements the recursive step of Cudd_bddVarMap.

Returns: a pointer to the result if successful; NULL otherwise.

Side effects None

See also: Cudd_bddVarMap

Parameters

manager	DD manager
f	BDD to be remapped

◆ cuddBddVectorComposeRecur()

static DdNode* cuddBddVectorComposeRecur	(	DdManager *	dd,
		DdHashTable *	table,
		DdNode *	f,
		DdNode **	vector,
		int	deepest
	)

static

Performs the recursive step of Cudd_bddVectorCompose.

Side effects None

Parameters

dd	DD manager
table	computed table
f	BDD in which to compose
vector	functions to be composed
deepest	depth of the deepest substitution

◆ ddIsIthAddVar()

static int ddIsIthAddVar	(	DdManager *	dd,
		DdNode *	f,
		unsigned int	i
	)

static

Comparison of a function to the i-th ADD variable.

Returns: 1 if the function is the i-th ADD variable; 0 otherwise.

Side effects None

◆ ddIsIthAddVarPair()

static int ddIsIthAddVarPair	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g,
		unsigned int	i
	)

static

Comparison of a pair of functions to the i-th ADD variable.

Returns: 1 if the functions are the i-th ADD variable and its complement; 0 otherwise.

Side effects None

Functions

Detailed Description

Function Documentation

◆ Cudd_addCompose()

◆ Cudd_addGeneralVectorCompose()

◆ Cudd_addNonSimCompose()

◆ Cudd_addPermute()

◆ Cudd_addSwapVariables()

◆ Cudd_addVectorCompose()

◆ Cudd_bddAdjPermuteX()

◆ Cudd_bddCompose()

◆ Cudd_bddPermute()

◆ Cudd_bddSwapVariables()

◆ Cudd_bddVarMap()

◆ Cudd_bddVectorCompose()

◆ Cudd_SetVarMap()

◆ cuddAddComposeRecur()

◆ cuddAddGeneralVectorComposeRecur()

◆ cuddAddNonSimComposeRecur()

◆ cuddAddPermuteRecur()

◆ cuddAddVectorComposeRecur()

◆ cuddBddComposeRecur()

◆ cuddBddPermuteRecur()

◆ cuddBddVarMapRecur()

◆ cuddBddVectorComposeRecur()

◆ ddIsIthAddVar()

◆ ddIsIthAddVarPair()