Functions for BDD decomposition. More...

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

Include dependency graph for cuddDecomp.c:

Data Structures
struct	Conjuncts
	Type of a pair of conjoined BDDs. More...

struct	NodeStat
	Stats for one node. More...

Macros
#define	DEPTH 5

#define	THRESHOLD 10

#define	NONE 0

#define	PAIR_ST 1

#define	PAIR_CR 2

#define	G_ST 3

#define	G_CR 4

#define	H_ST 5

#define	H_CR 6

#define	BOTH_G 7

#define	BOTH_H 8

#define	FactorsNotStored(factors) ((int)((ptrint)(factors) & 01))

#define	FactorsComplement(factors) ((Conjuncts *)((ptrint)(factors) \| 01))

#define	FactorsUncomplement(factors) ((Conjuncts *)((ptrint)(factors) ^ 01))

Typedefs
typedef struct Conjuncts	Conjuncts
	Type of a pair of conjoined BDDs.

typedef struct NodeStat	NodeStat
	Stats for one node.

Functions
int	Cudd_bddApproxConjDecomp (DdManager dd, DdNode f, DdNode ***conjuncts)
	Performs two-way conjunctive decomposition of a BDD. More...

int	Cudd_bddApproxDisjDecomp (DdManager dd, DdNode f, DdNode ***disjuncts)
	Performs two-way disjunctive decomposition of a BDD. More...

int	Cudd_bddIterConjDecomp (DdManager dd, DdNode f, DdNode ***conjuncts)
	Performs two-way conjunctive decomposition of a BDD. More...

int	Cudd_bddIterDisjDecomp (DdManager dd, DdNode f, DdNode ***disjuncts)
	Performs two-way disjunctive decomposition of a BDD. More...

int	Cudd_bddGenConjDecomp (DdManager dd, DdNode f, DdNode ***conjuncts)
	Performs two-way conjunctive decomposition of a BDD. More...

int	Cudd_bddGenDisjDecomp (DdManager dd, DdNode f, DdNode ***disjuncts)
	Performs two-way disjunctive decomposition of a BDD. More...

int	Cudd_bddVarConjDecomp (DdManager dd, DdNode f, DdNode ***conjuncts)
	Performs two-way conjunctive decomposition of a BDD. More...

int	Cudd_bddVarDisjDecomp (DdManager dd, DdNode f, DdNode ***disjuncts)
	Performs two-way disjunctive decomposition of a BDD. More...

static NodeStat *	CreateBotDist (DdNode node, st_table distanceTable)
	Get longest distance of node from constant. More...

static double	CountMinterms (DdManager dd, DdNode node, double max, st_table mintermTable, FILE fp)
	Count the number of minterms of each node ina a BDD and store it in a hash table. More...

static void	ConjunctsFree (DdManager dd, Conjuncts factors)
	Free factors structure. More...

static int	PairInTables (DdNode g, DdNode h, st_table *ghTable)
	Check whether the given pair is in the tables. More...

static Conjuncts *	CheckTablesCacheAndReturn (DdManager manager, DdNode node, DdNode g, DdNode h, st_table ghTable, st_table cacheTable)
	Check the tables for the existence of pair and return one combination, cache the result. More...

static Conjuncts *	PickOnePair (DdManager manager, DdNode node, DdNode g1, DdNode h1, DdNode g2, DdNode h2, st_table ghTable, st_table cacheTable)
	Check the tables for the existence of pair and return one combination, store in cache. More...

static Conjuncts *	CheckInTables (DdManager manager, DdNode node, DdNode g1, DdNode h1, DdNode g2, DdNode h2, st_table ghTable, st_table cacheTable, int *outOfMem)
	Check if the two pairs exist in the table. More...

static Conjuncts *	ZeroCase (DdManager dd, DdNode node, Conjuncts factorsNv, st_table ghTable, st_table *cacheTable, int switched)
	If one child is zero, do explicitly what Restrict does or better. More...

static Conjuncts *	BuildConjuncts (DdManager dd, DdNode node, st_table distanceTable, st_table cacheTable, int approxDistance, int maxLocalRef, st_table ghTable, st_table mintermTable, int32_t *lastTimeG)
	Builds the conjuncts recursively, bottom up. More...

static int	cuddConjunctsAux (DdManager dd, DdNode f, DdNode c1, DdNode c2)
	Computes two conjunctive factors of f and places them in c1 and c2. More...

Detailed Description

Functions for BDD decomposition.

Author: Kavita Ravi, 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.

Function Documentation

◆ BuildConjuncts()

static Conjuncts* BuildConjuncts	(	DdManager *	dd,
		DdNode *	node,
		st_table *	distanceTable,
		st_table *	cacheTable,
		int	approxDistance,
		int	maxLocalRef,
		st_table *	ghTable,
		st_table *	mintermTable,
		int32_t *	lastTimeG
	)

static

Builds the conjuncts recursively, bottom up.

Constants are returned as (f, f). The cache is checked for previously computed result. The decomposition points are determined by the local reference count of this node and the longest distance from the constant. At the decomposition point, the factors returned are (f, 1). Recur on the two children. The order is determined by the heavier branch. Combine the factors of the two children and pick the one that already occurs in the gh table. Occurence in g is indicated by value 1, occurence in h by 2, occurence in both by 3.

See also: cuddConjunctsAux

◆ CheckInTables()

static Conjuncts* CheckInTables	(	DdManager *	manager,
		DdNode *	node,
		DdNode *	g1,
		DdNode *	h1,
		DdNode *	g2,
		DdNode *	h2,
		st_table *	ghTable,
		st_table *	cacheTable,
		int *	outOfMem
	)

static

Check if the two pairs exist in the table.

If any of the conjuncts do exist, store in the cache and return the corresponding pair.

See also: ZeroCase BuildConjuncts

◆ CheckTablesCacheAndReturn()

static Conjuncts* CheckTablesCacheAndReturn	(	DdManager *	manager,
		DdNode *	node,
		DdNode *	g,
		DdNode *	h,
		st_table *	ghTable,
		st_table *	cacheTable
	)

static

Check the tables for the existence of pair and return one combination, cache the result.

The assumption is that one of the conjuncts is already in the tables.

Side effects g and h referenced for the cache

See also: ZeroCase

◆ ConjunctsFree()

static void ConjunctsFree	(	DdManager *	dd,
		Conjuncts *	factors
	)

static

Free factors structure.

Side effects None

◆ CountMinterms()

static double CountMinterms	(	DdManager *	dd,
		DdNode *	node,
		double	max,
		st_table *	mintermTable,
		FILE *	fp
	)

static

Count the number of minterms of each node ina a BDD and store it in a hash table.

Side effects None

◆ CreateBotDist()

static NodeStat* CreateBotDist	(	DdNode *	node,
		st_table *	distanceTable
	)

static

Get longest distance of node from constant.

Returns: the distance of the root from the constant if successful; CUDD_OUT_OF_MEM otherwise.

Side effects None

◆ Cudd_bddApproxConjDecomp()

int Cudd_bddApproxConjDecomp	(	DdManager *	dd,
		DdNode *	f,
		DdNode ***	conjuncts
	)

Performs two-way conjunctive decomposition of a BDD.

This procedure owes its name to the use of supersetting to obtain an initial factor of the given function. The conjuncts produced by this procedure tend to be imbalanced.

Returns: the number of conjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise.

Side effects The factors are returned in an array as side effects.: The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the conjuncts are already referenced. If the function returns 0, the array for the conjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.

See also: Cudd_bddApproxDisjDecomp Cudd_bddIterConjDecomp Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox Cudd_bddSqueeze Cudd_bddLICompaction

Parameters

dd	manager
f	function to be decomposed
conjuncts	address of the first factor

◆ Cudd_bddApproxDisjDecomp()

int Cudd_bddApproxDisjDecomp	(	DdManager *	dd,
		DdNode *	f,
		DdNode ***	disjuncts
	)

Performs two-way disjunctive decomposition of a BDD.

The disjuncts produced by this procedure tend to be imbalanced.

Returns: the number of disjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise.

Side effects The two disjuncts are returned in an array as side effects.: The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the disjuncts are already referenced. If the function returns 0, the array for the disjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.

See also: Cudd_bddApproxConjDecomp Cudd_bddIterDisjDecomp Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp

Parameters

dd	manager
f	function to be decomposed
disjuncts	address of the array of the disjuncts

◆ Cudd_bddGenConjDecomp()

int Cudd_bddGenConjDecomp	(	DdManager *	dd,
		DdNode *	f,
		DdNode ***	conjuncts
	)

Performs two-way conjunctive decomposition of a BDD.

This procedure owes its name to the fact tht it generalizes the decomposition based on the cofactors with respect to one variable. The conjuncts produced by this procedure tend to be balanced.

Returns: the number of conjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise.

Side effects The two factors are returned in an array as side effects.: The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the conjuncts are already referenced. If the function returns 0, the array for the conjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.

See also: Cudd_bddGenDisjDecomp Cudd_bddApproxConjDecomp Cudd_bddIterConjDecomp Cudd_bddVarConjDecomp

Parameters

dd	manager
f	function to be decomposed
conjuncts	address of the array of conjuncts

◆ Cudd_bddGenDisjDecomp()

int Cudd_bddGenDisjDecomp	(	DdManager *	dd,
		DdNode *	f,
		DdNode ***	disjuncts
	)

Performs two-way disjunctive decomposition of a BDD.

The disjuncts produced by this procedure tend to be balanced.

Returns: the number of disjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise.

Side effects The two disjuncts are returned in an array as side effects.: The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the disjuncts are already referenced. If the function returns 0, the array for the disjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.

See also: Cudd_bddGenConjDecomp Cudd_bddApproxDisjDecomp Cudd_bddIterDisjDecomp Cudd_bddVarDisjDecomp

Parameters

dd	manager
f	function to be decomposed
disjuncts	address of the array of the disjuncts

◆ Cudd_bddIterConjDecomp()

int Cudd_bddIterConjDecomp	(	DdManager *	dd,
		DdNode *	f,
		DdNode ***	conjuncts
	)

Performs two-way conjunctive decomposition of a BDD.

This procedure owes its name to the iterated use of supersetting to obtain a factor of the given function. The conjuncts produced by this procedure tend to be imbalanced.

Returns: the number of conjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise.

Side effects The factors are returned in an array as side effects.: The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the conjuncts are already referenced. If the function returns 0, the array for the conjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.

See also: Cudd_bddIterDisjDecomp Cudd_bddApproxConjDecomp Cudd_bddGenConjDecomp Cudd_bddVarConjDecomp Cudd_RemapOverApprox Cudd_bddSqueeze Cudd_bddLICompaction

Parameters

dd	manager
f	function to be decomposed
conjuncts	address of the array of conjuncts

◆ Cudd_bddIterDisjDecomp()

int Cudd_bddIterDisjDecomp	(	DdManager *	dd,
		DdNode *	f,
		DdNode ***	disjuncts
	)

Performs two-way disjunctive decomposition of a BDD.

The disjuncts produced by this procedure tend to be imbalanced.

Returns: the number of disjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise.

Side effects The two disjuncts are returned in an array as side effects.: The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the disjuncts are already referenced. If the function returns 0, the array for the disjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.

See also: Cudd_bddIterConjDecomp Cudd_bddApproxDisjDecomp Cudd_bddGenDisjDecomp Cudd_bddVarDisjDecomp

Parameters

dd	manager
f	function to be decomposed
disjuncts	address of the array of the disjuncts

◆ Cudd_bddVarConjDecomp()

int Cudd_bddVarConjDecomp	(	DdManager *	dd,
		DdNode *	f,
		DdNode ***	conjuncts
	)

Performs two-way conjunctive decomposition of a BDD.

Conjunctively decomposes one BDD according to a variable. If f is the function of the BDD and x is the variable, the decomposition is (f+x)(f+x'). The variable is chosen so as to balance the sizes of the two conjuncts and to keep them small.

Returns: the number of conjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise.

Side effects The two factors are returned in an array as side effects.: The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the conjuncts are already referenced. If the function returns 0, the array for the conjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.

See also: Cudd_bddVarDisjDecomp Cudd_bddGenConjDecomp Cudd_bddApproxConjDecomp Cudd_bddIterConjDecomp

Parameters

dd	manager
f	function to be decomposed
conjuncts	address of the array of conjuncts

◆ Cudd_bddVarDisjDecomp()

int Cudd_bddVarDisjDecomp	(	DdManager *	dd,
		DdNode *	f,
		DdNode ***	disjuncts
	)

Performs two-way disjunctive decomposition of a BDD.

Performs two-way disjunctive decomposition of a BDD according to a variable. If f is the function of the BDD and x is the variable, the decomposition is f*x + f*x'. The variable is chosen so as to balance the sizes of the two disjuncts and to keep them small.

Returns: the number of disjuncts produced, that is, 2 if successful; 1 if no meaningful decomposition was found; 0 otherwise.

Side effects The two disjuncts are returned in an array as side effects.: The array is allocated by this function. It is the caller's responsibility to free it. On successful completion, the disjuncts are already referenced. If the function returns 0, the array for the disjuncts is not allocated. If the function returns 1, the only factor equals the function to be decomposed.

See also: Cudd_bddVarConjDecomp Cudd_bddApproxDisjDecomp Cudd_bddIterDisjDecomp Cudd_bddGenDisjDecomp

Parameters

dd	manager
f	function to be decomposed
disjuncts	address of the array of the disjuncts

◆ cuddConjunctsAux()

static int cuddConjunctsAux	(	DdManager *	dd,
		DdNode *	f,
		DdNode **	c1,
		DdNode **	c2
	)

static

Computes two conjunctive factors of f and places them in *c1 and *c2.

Sets up the required data - table of distances from the constant and local reference count. Also minterm table.

◆ PairInTables()

static int PairInTables	(	DdNode *	g,
		DdNode *	h,
		st_table *	ghTable
	)

static

Check whether the given pair is in the tables.

gTable and hTable are combined. absence in both is indicated by 0, presence in gTable is indicated by 1, presence in hTable by 2 and presence in both by 3. The values returned by this function are PAIR_ST, PAIR_CR, G_ST, G_CR, H_ST, H_CR, BOTH_G, BOTH_H, NONE. PAIR_ST implies g in gTable and h in hTable PAIR_CR implies g in hTable and h in gTable G_ST implies g in gTable and h not in any table G_CR implies g in hTable and h not in any table H_ST implies h in hTable and g not in any table H_CR implies h in gTable and g not in any table BOTH_G implies both in gTable BOTH_H implies both in hTable NONE implies none in table;

See also: CheckTablesCacheAndReturn CheckInTables

◆ PickOnePair()

static Conjuncts* PickOnePair	(	DdManager *	manager,
		DdNode *	node,
		DdNode *	g1,
		DdNode *	h1,
		DdNode *	g2,
		DdNode *	h2,
		st_table *	ghTable,
		st_table *	cacheTable
	)

static

Check the tables for the existence of pair and return one combination, store in cache.

The pair that has more pointers to it is picked. An approximation of the number of local pointers is made by taking the reference count of the pairs sent.

See also: ZeroCase BuildConjuncts

◆ ZeroCase()

static Conjuncts* ZeroCase	(	DdManager *	dd,
		DdNode *	node,
		Conjuncts *	factorsNv,
		st_table *	ghTable,
		st_table *	cacheTable,
		int	switched
	)

static

If one child is zero, do explicitly what Restrict does or better.

First separate a variable and its child in the base case. In case of a cube times a function, separate the cube and function. As a last resort, look in tables.

Side effects Frees the BDDs in factorsNv. factorsNv itself is not freed: because it is freed above.

See also: BuildConjuncts

Data Structures

Macros

Typedefs

Functions

Detailed Description

Function Documentation

◆ BuildConjuncts()

◆ CheckInTables()

◆ CheckTablesCacheAndReturn()

◆ ConjunctsFree()

◆ CountMinterms()

◆ CreateBotDist()

◆ Cudd_bddApproxConjDecomp()

◆ Cudd_bddApproxDisjDecomp()

◆ Cudd_bddGenConjDecomp()

◆ Cudd_bddGenDisjDecomp()

◆ Cudd_bddIterConjDecomp()

◆ Cudd_bddIterDisjDecomp()

◆ Cudd_bddVarConjDecomp()

◆ Cudd_bddVarDisjDecomp()

◆ cuddConjunctsAux()

◆ PairInTables()

◆ PickOnePair()

◆ ZeroCase()