Generalized cofactors for BDDs and ADDs. More...

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

Include dependency graph for cuddGenCof.c:

Data Structures
struct	MarkCacheKey

Macros
#define	DD_LIC_DC 0

#define	DD_LIC_1 1

#define	DD_LIC_0 2

#define	DD_LIC_NL 3

Typedefs
typedef struct MarkCacheKey	MarkCacheKey

Functions
DdNode *	Cudd_bddConstrain (DdManager dd, DdNode f, DdNode *c)
	Computes f constrain c. More...

DdNode *	Cudd_bddRestrict (DdManager dd, DdNode f, DdNode *c)
	BDD restrict according to Coudert and Madre's algorithm (ICCAD90). More...

DdNode *	Cudd_bddNPAnd (DdManager dd, DdNode f, DdNode *g)
	Computes f non-polluting-and g. More...

DdNode *	Cudd_addConstrain (DdManager dd, DdNode f, DdNode *c)
	Computes f constrain c for ADDs. More...

DdNode **	Cudd_bddConstrainDecomp (DdManager dd, DdNode f)
	BDD conjunctive decomposition as in McMillan's CAV96 paper. More...

DdNode *	Cudd_addRestrict (DdManager dd, DdNode f, DdNode *c)
	ADD restrict according to Coudert and Madre's algorithm (ICCAD90). More...

DdNode **	Cudd_bddCharToVect (DdManager dd, DdNode f)
	Computes a vector of BDDs whose image equals a non-zero function. More...

DdNode *	Cudd_bddLICompaction (DdManager dd, DdNode f, DdNode *c)
	Performs safe minimization of a BDD. More...

DdNode *	Cudd_bddSqueeze (DdManager dd, DdNode l, DdNode *u)
	Finds a small BDD in a function interval. More...

DdNode *	Cudd_bddInterpolate (DdManager dd, DdNode l, DdNode *u)
	Finds an interpolant of two functions. More...

DdNode *	Cudd_bddMinimize (DdManager dd, DdNode f, DdNode *c)
	Finds a small BDD that agrees with `f` over `c`. More...

DdNode *	Cudd_SubsetCompress (DdManager dd, DdNode f, int nvars, int threshold)
	Find a dense subset of BDD `f`. More...

DdNode *	Cudd_SupersetCompress (DdManager dd, DdNode f, int nvars, int threshold)
	Find a dense superset of BDD `f`. More...

DdNode *	cuddBddConstrainRecur (DdManager dd, DdNode f, DdNode *c)
	Performs the recursive step of Cudd_bddConstrain. More...

DdNode *	cuddBddRestrictRecur (DdManager dd, DdNode f, DdNode *c)
	Performs the recursive step of Cudd_bddRestrict. More...

DdNode *	cuddBddNPAndRecur (DdManager manager, DdNode f, DdNode *g)
	Implements the recursive step of Cudd_bddAnd. More...

DdNode *	cuddAddConstrainRecur (DdManager dd, DdNode f, DdNode *c)
	Performs the recursive step of Cudd_addConstrain. More...

DdNode *	cuddAddRestrictRecur (DdManager dd, DdNode f, DdNode *c)
	Performs the recursive step of Cudd_addRestrict. More...

DdNode *	cuddBddLICompaction (DdManager dd, DdNode f, DdNode *c)
	Performs safe minimization of a BDD. More...

static int	cuddBddConstrainDecomp (DdManager dd, DdNode f, DdNode **decomp)
	Performs the recursive step of Cudd_bddConstrainDecomp. More...

static DdNode *	cuddBddCharToVect (DdManager dd, DdNode f, DdNode *x)
	Performs the recursive step of Cudd_bddCharToVect. More...

static int	cuddBddLICMarkEdges (DdManager dd, DdNode f, DdNode c, st_table table, st_table *cache)
	Performs the edge marking step of Cudd_bddLICompaction. More...

static DdNode *	cuddBddLICBuildResult (DdManager dd, DdNode f, st_table cache, st_table table)
	Builds the result of Cudd_bddLICompaction. More...

static int	MarkCacheHash (void const *ptr, int modulus)
	Hash function for the computed table of cuddBddLICMarkEdges. More...

static int	MarkCacheCompare (const void ptr1, const void ptr2)
	Comparison function for the computed table of cuddBddLICMarkEdges. More...

static enum st_retval	MarkCacheCleanUp (void key, void value, void *arg)
	Frees memory associated with computed table of cuddBddLICMarkEdges. More...

static DdNode *	cuddBddSqueeze (DdManager dd, DdNode l, DdNode *u)
	Performs the recursive step of Cudd_bddSqueeze. More...

static DdNode *	cuddBddInterpolate (DdManager dd, DdNode l, DdNode *u)
	Performs the recursive step of Cudd_bddInterpolate. More...

Detailed Description

Generalized cofactors for BDDs and ADDs.

Author: Fabio Somenzi

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.

Typedef Documentation

◆ MarkCacheKey

typedef struct MarkCacheKey MarkCacheKey

Key for the cache used in the edge marking phase.

Function Documentation

◆ Cudd_addConstrain()

DdNode* Cudd_addConstrain	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	c
	)

Computes f constrain c for ADDs.

Computes f constrain c (f @ c), for f an ADD and c a 0-1 ADD. List of special cases:

F @ 0 = 0
F @ 1 = F
0 @ c = 0
1 @ c = 1
F @ F = 1

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

Side effects None

See also: Cudd_bddConstrain

◆ Cudd_addRestrict()

DdNode* Cudd_addRestrict	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	c
	)

ADD restrict according to Coudert and Madre's algorithm (ICCAD90).

If application of restrict results in an ADD larger than the input ADD, the input ADD is returned.

Returns: the restricted ADD if successful; otherwise NULL.

Side effects None

See also: Cudd_addConstrain Cudd_bddRestrict

◆ Cudd_bddCharToVect()

DdNode** Cudd_bddCharToVect	(	DdManager *	dd,
		DdNode *	f
	)

Computes a vector of BDDs whose image equals a non-zero function.

The result depends on the variable order. The i-th component of the vector depends only on the first i variables in the order. Each BDD in the vector is not larger than the BDD of the given characteristic function. This function is based on the description of char-to-vect in "Verification of Sequential Machines Using Boolean Functional Vectors" by O. Coudert, C. Berthet and J. C. Madre.

Returns: a pointer to an array containing the result if successful; NULL otherwise. The size of the array equals the number of variables in the manager. The components of the solution have their reference counts already incremented (unlike the results of most other functions in the package).

Side effects None

See also: Cudd_bddConstrain

◆ Cudd_bddConstrain()

DdNode* Cudd_bddConstrain	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	c
	)

Computes f constrain c.

Computes f constrain c (f @ c). Uses a canonical form: (f' @ c) = (f @ c)'. (Note: this is not true for c.) List of special cases:

f @ 0 = 0
f @ 1 = f
0 @ c = 0
1 @ c = 1
f @ f = 1
f @ f'= 0

Note that if F=(f1,...,fn) and reordering takes place while computing F @ c, then the image restriction property (Img(F,c) = Img(F @ c)) is lost.

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

Side effects None

See also: Cudd_bddRestrict Cudd_addConstrain

◆ Cudd_bddConstrainDecomp()

DdNode** Cudd_bddConstrainDecomp	(	DdManager *	dd,
		DdNode *	f
	)

BDD conjunctive decomposition as in McMillan's CAV96 paper.

The decomposition is canonical only for a given variable order. If canonicity is required, variable ordering must be disabled after the decomposition has been computed. The components of the solution have their reference counts already incremented (unlike the results of most other functions in the package).

Returns: an array with one entry for each BDD variable in the manager if successful; otherwise NULL.

Side effects None

See also: Cudd_bddConstrain Cudd_bddExistAbstract

◆ Cudd_bddInterpolate()

DdNode* Cudd_bddInterpolate	(	DdManager *	dd,
		DdNode *	l,
		DdNode *	u
	)

Finds an interpolant of two functions.

Given BDDs l and u, representing the lower bound and upper bound of a function interval, Cudd_bddInterpolate produces the BDD of a function within the interval that only depends on the variables common to l and u.

The approach is based on quantification as in Cudd_bddRestrict(). The function assumes that l implies u, but does not check whether that's true.

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

Side effects None

See also: Cudd_bddRestrict Cudd_bddSqueeze

Parameters

dd	manager
l	lower bound
u	upper bound

◆ Cudd_bddLICompaction()

DdNode* Cudd_bddLICompaction	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	c
	)

Performs safe minimization of a BDD.

Given the BDD f of a function to be minimized and a BDD c representing the care set, Cudd_bddLICompaction produces the BDD of a function that agrees with f wherever c is 1. Safe minimization means that the size of the result is guaranteed not to exceed the size of f. This function is based on the DAC97 paper by Hong et al..

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

Side effects None

See also: Cudd_bddRestrict

Parameters

dd	manager
f	function to be minimized
c	constraint (care set)

◆ Cudd_bddMinimize()

DdNode* Cudd_bddMinimize	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	c
	)

Finds a small BDD that agrees with f over c.

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

Side effects None

See also: Cudd_bddRestrict Cudd_bddLICompaction Cudd_bddSqueeze

◆ Cudd_bddNPAnd()

DdNode* Cudd_bddNPAnd	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	g
	)

Computes f non-polluting-and g.

The non-polluting AND of f and g is a hybrid of AND and Restrict. From Restrict, this operation takes the idea of existentially quantifying the top variable of the second operand if it does not appear in the first. Therefore, the variables that appear in the result also appear in f. For the rest, the function behaves like AND. Since the two operands play different roles, non-polluting AND is not commutative.

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

Side effects None

See also: Cudd_bddConstrain Cudd_bddRestrict

◆ Cudd_bddRestrict()

DdNode* Cudd_bddRestrict	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	c
	)

BDD restrict according to Coudert and Madre's algorithm (ICCAD90).

If application of restrict results in a BDD larger than the input BDD, the input BDD is returned.

Returns: the restricted BDD if successful; otherwise NULL.

Side effects None

See also: Cudd_bddConstrain Cudd_addRestrict

◆ Cudd_bddSqueeze()

DdNode* Cudd_bddSqueeze	(	DdManager *	dd,
		DdNode *	l,
		DdNode *	u
	)

Finds a small BDD in a function interval.

Given BDDs l and u, representing the lower bound and upper bound of a function interval, Cudd_bddSqueeze produces the BDD of a function within the interval with a small BDD.

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

Side effects None

See also: Cudd_bddRestrict Cudd_bddLICompaction

Parameters

dd	manager
l	lower bound
u	upper bound

◆ Cudd_SubsetCompress()

DdNode* Cudd_SubsetCompress	(	DdManager *	dd,
		DdNode *	f,
		int	nvars,
		int	threshold
	)

Find a dense subset of BDD f.

Density is the ratio of number of minterms to number of nodes. Uses several techniques in series. It is more expensive than other subsetting procedures, but often produces better results. See Cudd_SubsetShortPaths for a description of the threshold and nvars parameters.

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

Side effects None

See also: Cudd_RemapUnderApprox Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch Cudd_bddSqueeze

Parameters

dd	manager
f	BDD whose subset is sought
nvars	number of variables in the support of f
threshold	maximum number of nodes in the subset

◆ Cudd_SupersetCompress()

DdNode* Cudd_SupersetCompress	(	DdManager *	dd,
		DdNode *	f,
		int	nvars,
		int	threshold
	)

Find a dense superset of BDD f.

Density is the ratio of number of minterms to number of nodes. Uses several techniques in series. It is more expensive than other supersetting procedures, but often produces better results. See Cudd_SupersetShortPaths for a description of the threshold and nvars parameters.

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

Side effects None

See also: Cudd_SubsetCompress Cudd_SupersetRemap Cudd_SupersetShortPaths Cudd_SupersetHeavyBranch Cudd_bddSqueeze

Parameters

dd	manager
f	BDD whose superset is sought
nvars	number of variables in the support of f
threshold	maximum number of nodes in the superset

◆ cuddAddConstrainRecur()

DdNode* cuddAddConstrainRecur	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	c
	)

Performs the recursive step of Cudd_addConstrain.

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

Side effects None

See also: Cudd_addConstrain

◆ cuddAddRestrictRecur()

DdNode* cuddAddRestrictRecur	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	c
	)

Performs the recursive step of Cudd_addRestrict.

Returns: the restricted ADD if successful; otherwise NULL.

Side effects None

See also: Cudd_addRestrict

◆ cuddBddCharToVect()

static DdNode* cuddBddCharToVect	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	x
	)

static

Performs the recursive step of Cudd_bddCharToVect.

This function maintains the invariant that f is non-zero.

Returns: the i-th component of the vector if successful; otherwise NULL.

Side effects None

See also: Cudd_bddCharToVect

◆ cuddBddConstrainDecomp()

static int cuddBddConstrainDecomp	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	decomp
	)

static

Performs the recursive step of Cudd_bddConstrainDecomp.

Returns: f super (i) if successful; otherwise NULL.

Side effects None

See also: Cudd_bddConstrainDecomp

◆ cuddBddConstrainRecur()

DdNode* cuddBddConstrainRecur	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	c
	)

Performs the recursive step of Cudd_bddConstrain.

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

Side effects None

See also: Cudd_bddConstrain

◆ cuddBddInterpolate()

static DdNode* cuddBddInterpolate	(	DdManager *	dd,
		DdNode *	l,
		DdNode *	u
	)

static

Performs the recursive step of Cudd_bddInterpolate.

This procedure exploits the fact that if we complement and swap the bounds of the interval we obtain a valid solution by taking the complement of the solution to the original problem. Therefore, we can enforce the condition that the upper bound is always regular.

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

Side effects None

See also: Cudd_bddInterpolate

◆ cuddBddLICBuildResult()

static DdNode* cuddBddLICBuildResult	(	DdManager *	dd,
		DdNode *	f,
		st_table *	cache,
		st_table *	table
	)

static

Builds the result of Cudd_bddLICompaction.

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

Side effects None

See also: Cudd_bddLICompaction cuddBddLICMarkEdges

◆ cuddBddLICMarkEdges()

static int cuddBddLICMarkEdges	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	c,
		st_table *	table,
		st_table *	cache
	)

static

Performs the edge marking step of Cudd_bddLICompaction.

Returns: the LUB of the markings of the two outgoing edges of f if successful; otherwise CUDD_OUT_OF_MEM.

Side effects None

See also: Cudd_bddLICompaction cuddBddLICBuildResult

◆ cuddBddLICompaction()

DdNode* cuddBddLICompaction	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	c
	)

Performs safe minimization of a BDD.

Given the BDD f of a function to be minimized and a BDD c representing the care set, Cudd_bddLICompaction produces the BDD of a function that agrees with f wherever c is 1. Safe minimization means that the size of the result is guaranteed not to exceed the size of f. This function is based on the DAC97 paper by Hong et al..

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

Side effects None

See also: Cudd_bddLICompaction

Parameters

dd	manager
f	function to be minimized
c	constraint (care set)

◆ cuddBddNPAndRecur()

DdNode* cuddBddNPAndRecur	(	DdManager *	manager,
		DdNode *	f,
		DdNode *	g
	)

Implements the recursive step of Cudd_bddAnd.

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

Side effects None

See also: Cudd_bddNPAnd

◆ cuddBddRestrictRecur()

DdNode* cuddBddRestrictRecur	(	DdManager *	dd,
		DdNode *	f,
		DdNode *	c
	)

Performs the recursive step of Cudd_bddRestrict.

Returns: the restricted BDD if successful; otherwise NULL.

Side effects None

See also: Cudd_bddRestrict

◆ cuddBddSqueeze()

static DdNode* cuddBddSqueeze	(	DdManager *	dd,
		DdNode *	l,
		DdNode *	u
	)

static

Performs the recursive step of Cudd_bddSqueeze.

This procedure exploits the fact that if we complement and swap the bounds of the interval we obtain a valid solution by taking the complement of the solution to the original problem. Therefore, we can enforce the condition that the upper bound is always regular.

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

Side effects None

See also: Cudd_bddSqueeze

◆ MarkCacheCleanUp()

static enum st_retval MarkCacheCleanUp	(	void *	key,
		void *	value,
		void *	arg
	)

static

Frees memory associated with computed table of cuddBddLICMarkEdges.

Returns: ST_CONTINUE.

Side effects None

See also: Cudd_bddLICompaction

◆ MarkCacheCompare()

static int MarkCacheCompare	(	const void *	ptr1,
		const void *	ptr2
	)

static

Comparison function for the computed table of cuddBddLICMarkEdges.

Returns: 0 if the two nodes of the key are equal; 1 otherwise.

Side effects None

See also: Cudd_bddLICompaction

◆ MarkCacheHash()

static int MarkCacheHash	(	void const *	ptr,
		int	modulus
	)

static

Hash function for the computed table of cuddBddLICMarkEdges.

Returns: the bucket number.

Side effects None

See also: Cudd_bddLICompaction

Data Structures

Macros

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ MarkCacheKey

Function Documentation

◆ Cudd_addConstrain()

◆ Cudd_addRestrict()

◆ Cudd_bddCharToVect()

◆ Cudd_bddConstrain()

◆ Cudd_bddConstrainDecomp()

◆ Cudd_bddInterpolate()

◆ Cudd_bddLICompaction()

◆ Cudd_bddMinimize()

◆ Cudd_bddNPAnd()

◆ Cudd_bddRestrict()

◆ Cudd_bddSqueeze()

◆ Cudd_SubsetCompress()

◆ Cudd_SupersetCompress()

◆ cuddAddConstrainRecur()

◆ cuddAddRestrictRecur()

◆ cuddBddCharToVect()

◆ cuddBddConstrainDecomp()

◆ cuddBddConstrainRecur()

◆ cuddBddInterpolate()

◆ cuddBddLICBuildResult()

◆ cuddBddLICMarkEdges()

◆ cuddBddLICompaction()

◆ cuddBddNPAndRecur()

◆ cuddBddRestrictRecur()

◆ cuddBddSqueeze()

◆ MarkCacheCleanUp()

◆ MarkCacheCompare()

◆ MarkCacheHash()