static unsigned int AssessPathLength( unsigned int * pathLengthArray, array determining number of nodes belonging to the different path lengths int threshold, threshold to determine maximum allowable nodes in the subset int numVars, maximum number of variables unsigned int * excess, number of nodes labeled maxpath required in the subset FILE * fp where to write messages )
cuddSubsetSP.c
static int BAapplyBias( DdManager * dd, DdNode * f, DdNode * b, ApproxInfo * info, DdHashTable * cache )
cuddBiasedUnderApprox
cuddApprox.c
static int BAmarkNodes( DdManager * dd, manager DdNode * f, function to be analyzed ApproxInfo * info, info on BDD int threshold, when to stop approximating double quality1, minimum improvement for accepted changes when b=1 double quality0 minimum improvement for accepted changes when b=0 )
cuddBiasedUnderApprox
cuddApprox.c
static Conjuncts * BuildConjuncts( DdManager * dd, DdNode * node, st_table * distanceTable, st_table * cacheTable, int approxDistance, int maxLocalRef, st_table * ghTable, st_table * mintermTable )
cuddConjunctsAux
cuddDecomp.c
static DdNode * BuildSubsetBdd( DdManager * dd, DD manager GlobalInfo_t * gInfo, global information st_table * pathTable, path table with path lengths and computed results DdNode * node, current node struct AssortedInfo * info, assorted information structure st_table * subsetNodeTable table storing computed results )
cuddSubsetSP.c
static DdNode * BuildSubsetBdd( DdManager * dd, DD manager DdNode * node, current node int * size, current size of the subset st_table * visitedTable, visited table storing all node data int threshold, st_table * storeTable, st_table * approxTable )
cuddSubsetHB.c
CUDD_VALUE_TYPE *þvalueþ(
)
CUDD_VALUE_TYPE *þvalueþ(
)
CUDD_VALUE_TYPE þcþ(
)
CUDD_VALUE_TYPE þepþ(
)
CUDD_VALUE_TYPE þupperþ(
)
CUDD_VALUE_TYPE þvalueþ(
)
CUDD_VALUE_TYPE þvalueþ(
)
static Conjuncts * CheckInTables( DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable, int * outOfMem )
ZeroCase
BuildConjuncts
cuddDecomp.c
static Conjuncts * CheckTablesCacheAndReturn( DdNode * node, DdNode * g, DdNode * h, st_table * ghTable, st_table * cacheTable )
ZeroCase
cuddDecomp.c
static void ConjunctsFree( DdManager * dd, Conjuncts * factors )
cuddDecomp.c
static enum st_retval CorrelCleanUp( char * key, char * value, char * arg )
cuddBddCorr.c
static int CorrelCompare( const char * key1, const char * key2 )
cuddBddCorr.c
static int CorrelHash( char * key, int modulus )
cuddBddCorr.c
static double CountMinterms( DdNode * node, double max, st_table * mintermTable, FILE * fp )
cuddDecomp.c
static NodeStat * CreateBotDist( DdNode * node, st_table * distanceTable )
cuddDecomp.c
static int CreateBotDist( DdNode * node, current node st_table * pathTable, path table with path lengths unsigned int * pathLengthArray, array that stores number of nodes belonging to a particular path length. FILE * fp where to write messages )
CreatePathTable
CreateTopDist
AssessPathLength
cuddSubsetSP.c
static st_table * CreatePathTable( DdManager * dd, DD manager GlobalInfo_t * gInfo, global information DdNode * node, root of function unsigned int * pathLengthArray, array of path lengths to store nodes labeled with the various path lengths FILE * fp where to write messages )
CreateTopDist
CreateBotDist
cuddSubsetSP.c
static void CreateTopDist( DdManager * dd, DD manager GlobalInfo_t * gInfo, global information st_table * pathTable, hast table to store path lengths int parentPage, the pointer to the page on which the first parent in the queue is to be found. int parentQueueIndex, pointer to the first parent on the page int topLen, current distance from the root DdNode ** childPage, pointer to the page on which the first child is to be added. int childQueueIndex, pointer to the first child int numParents, number of parents to process in this recursive call FILE * fp where to write messages )
CreatePathTable
CreateBotDist
cuddSubsetSP.c
Cudd_AggregationType þgcþ(
)
Cudd_HookType þwhereþ(
)
Cudd_HookType þwhereþ(
)
Cudd_HookType þwhereþ(
)
Cudd_ReorderingType *þmethodþ(
)
Cudd_ReorderingType *þmethodþ(
)
Cudd_ReorderingType þmethodþ(
)
Cudd_ReorderingType þmethodþ(
)
DD_PRFP þPifuncþfunction used to build Pi if it is NULL(
)
DdApaDigit þliteralþ(
)
DdApaNumber þbþ(
)
DdApaNumber þdestþ(
)
DdApaNumber þdiffþ(
)
DdApaNumber þnumberþ(
)
DdApaNumber þnumberþ(
)
DdApaNumber þquotientþ(
)
DdApaNumber þquotientþ(
)
DdApaNumber þsecondþ(
)
DdApaNumber þsumþ(
)
DdGen *þgenþ(
)
DdGen *þgenþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þddþ(
)
DdManager *þmanagerþ(
)
DdManager *þtableþ(
)
DdManager *þtableþ(
)
DdManager *þtableþ(
)
DdManager *þtableþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdManager *þuniqueþ(
)
DdNode ***þconjunctsþaddress of the array of conjuncts(
)
DdNode ***þconjunctsþaddress of the array of conjuncts(
)
DdNode ***þconjunctsþaddress of the array of conjuncts(
)
DdNode ***þconjunctsþaddress of the first factor(
)
DdNode ***þdisjunctsþaddress of the array of the disjuncts(
)
DdNode ***þdisjunctsþaddress of the array of the disjuncts(
)
DdNode ***þdisjunctsþaddress of the array of the disjuncts(
)
DdNode ***þdisjunctsþaddress of the array of the disjuncts(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þgþ(
)
DdNode **þnodeþ(
)
DdNode **þnodeþ(
)
DdNode **þonlyGþcube of variables only in g(
)
DdNode **þvectorOffþ(
)
DdNode **þvectorþ(
)
DdNode **þvectorþ(
)
DdNode **þvectorþ(
)
DdNode **þyþarray of y variables(
)
DdNode **þyþarray of y variables(
)
DdNode **þyþarray of y variables(
)
DdNode **þyþarray of y variables(
)
DdNode **þyþarray of y variables(
)
DdNode **þzdd_Iþ(
)
DdNode **þzþarray of z variables(
)
DdNode **þzþarray of z variables(
)
DdNode *þBþ(
)
DdNode *þBþ(
)
DdNode *þDþ(
)
DdNode *þDþ(
)
DdNode *þPþ(
)
DdNode *þPþ(
)
DdNode *þQþ(
)
DdNode *þQþ(
)
DdNode *þQþ(
)
DdNode *þQþ(
)
DdNode *þUþ(
)
DdNode *þYþ(
)
DdNode *þbckþ(
)
DdNode *þcubeþ(
)
DdNode *þcubeþ(
)
DdNode *þcubeþ(
)
DdNode *þcubeþ(
)
DdNode *þcubeþ(
)
DdNode *þcubeþ(
)
DdNode *þcubeþ(
)
DdNode *þcþ(
)
DdNode *þcþ(
)
DdNode *þcþ(
)
DdNode *þcþ(
)
DdNode *þcþ(
)
DdNode *þcþ(
)
DdNode *þcþconstraint (care set)(
)
DdNode *þepsilonþ(
)
DdNode *þfþ(
)
DdNode *þfþ(
)
DdNode *þfþ(
)
DdNode *þfþ(
)
DdNode *þfþ(
)
DdNode *þfþ(
)
DdNode *þfþ(
)
DdNode *þfþ(
)
DdNode *þfþ(
)
DdNode *þfþ(
)
DdNode *þfþ(
)
DdNode *þfþ(
)
DdNode *þfþ(
)
DdNode *þfþ(
)
DdNode *þfþDD whose support is sought(
)
DdNode *þfþDD whose support is sought(
)
DdNode *þfþDD whose support size is sought(
)
DdNode *þfþZDD whose support is sought(
)
DdNode *þfþfunction against which to expand(
)
DdNode *þfþfunction in which to remap variables(
)
DdNode *þfþfunction of which the cube is to be made a prime(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþ(
)
DdNode *þgþsecond operand(
)
DdNode *þhþ(
)
DdNode *þhþ(
)
DdNode *þhþ(
)
DdNode *þhþ(
)
DdNode *þhþ(
)
DdNode *þnodeþ(
)
DdNode *þnodeþ(
)
DdNode *þnodeþ(
)
DdNode *þnodeþ(
)
DdNode *þnodeþ(
)
DdNode *þnodeþ(
)
DdNode *þnodeþ(
)
DdNode *þnodeþ(
)
DdNode *þnodeþ(
)
DdNode *þnodeþ(
)
DdNode *þnodeþ(
)
DdNode *þnodeþ(
)
DdNode *þnþ(
)
DdNode *þnþ(
)
DdNode *þnþ(
)
DdNode *þnþ(
)
DdNode *þnþ(
)
DdNode *þp_nodeþ(
)
DdNode *þphaseBddþcube of the phases(
)
DdNode *þuþ(
)
DdNode *þuþupper bound(
)
DdNode *þvarþvariable(
)
DdTlcInfo *þtþ(
)
EpDouble *þepdþ(
)
FILE *þfpþ(
)
FILE *þfpþ(
)
FILE *þfpþ(
)
FILE *þfpþ(
)
FILE *þfpþ(
)
FILE *þfpþpointer to the dump file(
)
FILE *þfpþpointer to the dump file(
)
FILE *þfpþpointer to the dump file(
)
FILE *þfpþpointer to the dump file(
)
FILE *þfpþpointer to the dump file(
)
static enum st_retval MarkCacheCleanUp( char * key, char * value, char * arg )
Cudd_bddLICompaction
cuddGenCof.c
static int MarkCacheCompare( const char * ptr1, const char * ptr2 )
Cudd_bddLICompaction
cuddGenCof.c
static int MarkCacheHash( char * ptr, int modulus )
Cudd_bddLICompaction
cuddGenCof.c
MtrNode *þtreeþ(
)
MtrNode *þtreeþ(
)
static int PMX( int maxvar )
cuddGenetic.c
static int PairInTables( DdNode * g, DdNode * h, st_table * ghTable )
CheckTablesCacheAndReturn
CheckInTables
cuddDecomp.c
static Conjuncts * PickOnePair( DdNode * node, DdNode * g1, DdNode * h1, DdNode * g2, DdNode * h2, st_table * ghTable, st_table * cacheTable )
ZeroCase
BuildConjuncts
cuddDecomp.c
static DdNode * RAbuildSubset( DdManager * dd, DD manager DdNode * node, current node ApproxInfo * info node info )
cuddRemapUnderApprox
cuddApprox.c
static int RAmarkNodes( DdManager * dd, manager DdNode * f, function to be analyzed ApproxInfo * info, info on BDD int threshold, when to stop approximating double quality minimum improvement for accepted changes )
cuddRemapUnderApprox
cuddApprox.c
static void
ResizeCountMintermPages(
)
cuddSubsetHB.c
static void
ResizeCountNodePages(
)
cuddSubsetHB.c
static void
ResizeNodeDataPages(
)
cuddSubsetHB.c
static void ResizeNodeDistPages( DdManager * dd, DD manager GlobalInfo_t * gInfo global information )
cuddSubsetSP.c
static void ResizeQueuePages( DdManager * dd, DD manager GlobalInfo_t * gInfo global information )
cuddSubsetSP.c
static void StoreNodes( st_table * storeTable, DdManager * dd, DdNode * node )
StoreNodes
cuddSubsetHB.c
static double SubsetCountMintermAux( DdNode * node, function to analyze double max, number of minterms of constant 1 st_table * table visitedTable table )
SubsetCountMinterm
cuddSubsetHB.c
static st_table * SubsetCountMinterm( DdNode * node, function to be analyzed int nvars number of variables node depends on )
SubsetCountMintermAux
cuddSubsetHB.c
static int SubsetCountNodesAux( DdNode * node, current node st_table * table, table to update node count, also serves as visited table. double max maximum number of variables )
SubsetCountNodes
cuddSubsetHB.c
static int SubsetCountNodes( DdNode * node, function to be analyzed st_table * table, node quality table int nvars number of variables node depends on )
SubsetCountNodesAux
cuddSubsetHB.c
static DdNode * UAbuildSubset( DdManager * dd, DD manager DdNode * node, current node ApproxInfo * info node info )
cuddUnderApprox
cuddApprox.c
static int UAmarkNodes( DdManager * dd, manager DdNode * f, function to be analyzed ApproxInfo * info, info on BDD int threshold, when to stop approximating int safe, enforce safe approximation double quality minimum improvement for accepted changes )
cuddUnderApprox
cuddApprox.c
static Conjuncts * ZeroCase( DdManager * dd, DdNode * node, Conjuncts * factorsNv, st_table * ghTable, st_table * cacheTable, int switched )
BuildConjuncts
cuddDecomp.c
static DdNode * addBddDoInterval( DdManager * dd, DdNode * f, DdNode * l, DdNode * u )
addBddDoThreshold
addBddDoStrictThreshold
cuddBridge.c
static DdNode * addBddDoIthBit( DdManager * dd, DdNode * f, DdNode * index )
cuddBridge.c
static DdNode * addBddDoStrictThreshold( DdManager * dd, DdNode * f, DdNode * val )
addBddDoThreshold
cuddBridge.c
static DdNode * addBddDoThreshold( DdManager * dd, DdNode * f, DdNode * val )
addBddDoStrictThreshold
cuddBridge.c
static int addCheckPositiveCube( DdManager * manager, DdNode * cube )
cuddAddAbs.c
static DdNode * addDoIthBit( DdManager * dd, DdNode * f, DdNode * index )
cuddAddFind.c
static DdNode * addMMRecur( DdManager * dd, DdNode * A, DdNode * B, int topP, int * vars )
cuddMatMult.c
static int addMultiplicityGroups( DdManager * dd, manager MtrNode * treenode, current tree node int multiplicity, how many ZDD vars per BDD var char * vmask, variable pairs for which a group has been already built char * lmask levels for which a group has already been built )
Cudd_zddVarsFromBddVars
cuddAPI.c
static DdNode * addTriangleRecur( DdManager * dd, DdNode * f, DdNode * g, int * vars, DdNode * cube )
cuddMatMult.c
static void addVarToConst( DdNode * f, DdNode ** gp, DdNode ** hp, DdNode * one, DdNode * zero )
cuddAddIte.c
static DdNode * addWalshInt( DdManager * dd, DdNode ** x, DdNode ** y, int n )
cuddAddWalsh.c
static int array_compare( const char * array1, const char * array2 )
cuddGenetic.c
static int array_hash( char * array, int modulus )
cuddGenetic.c
static double bddAnnotateMintermCount( DdManager * manager, DdNode * node, double max, st_table * table )
cuddSplit.c
static int bddCheckPositiveCube( DdManager * manager, DdNode * cube )
cuddBddAbs.c
static double bddCorrelationAux( DdManager * dd, DdNode * f, DdNode * g, st_table * table )
bddCorrelationWeightsAux
cuddBddCorr.c
static double bddCorrelationWeightsAux( DdManager * dd, DdNode * f, DdNode * g, double * prob, st_table * table )
bddCorrelationAux
cuddBddCorr.c
static void bddFixTree( DdManager * table, MtrNode * treenode )
cuddReorder.c
static int bddVarToCanonicalSimple( DdManager * dd, DdNode ** fp, DdNode ** gp, DdNode ** hp, unsigned int * topfp, unsigned int * topgp, unsigned int * tophp )
bddVarToConst
bddVarToCanonical
cuddBddIte.c
static int bddVarToCanonical( DdManager * dd, DdNode ** fp, DdNode ** gp, DdNode ** hp, unsigned int * topfp, unsigned int * topgp, unsigned int * tophp )
bddVarToConst
bddVarToCanonicalSimple
cuddBddIte.c
static void bddVarToConst( DdNode * f, DdNode ** gp, DdNode ** hp, DdNode * one )
bddVarToCanonical
bddVarToCanonicalSimple
cuddBddIte.c
static int beforep( DdHalfWord var1a, short phase1a, DdHalfWord var1b, short phase1b, DdHalfWord var2a, short phase2a, DdHalfWord var2b, short phase2b )
equalp
cuddEssent.c
static BitVector * bitVectorAlloc( int size )
bitVectorClear
bitVectorFree
cuddEssent.c
static void bitVectorFree( BitVector * vector )
bitVectorAlloc
cuddEssent.c
static int build_dd( DdManager * table, int num, the index of the individual to be built int lower, int upper )
cuddGenetic.c
char *þstringþ(
)
char *þstrþpointer to string to use if != NULL(
)
static int checkSymmInfo( DdManager * table, DdHalfWord * symmInfo, int index, int level )
initSymmInfo
cuddExact.c
static DdTlcInfo * computeClausesWithUniverse( DdTlcInfo * Cres, list of clauses for child DdHalfWord label, variable labeling the current node short phase 0 if E child is zero; 1 if T child is zero )
computeClauses
cuddEssent.c
static DdTlcInfo * computeClauses( DdTlcInfo * Tres, list of clauses for T child DdTlcInfo * Eres, list of clauses for E child DdHalfWord label, variable labeling the current node int size number of variables in the manager )
computeClausesWithUniverse
cuddEssent.c
static int computeLB( DdManager * table, manager DdHalfWord * order, optimal order for the subset int roots, roots between lower and upper int cost, minimum cost for the subset int lower, lower level to be reordered int upper, upper level to be reordered int level offset for the current top bottom var )
cuddExact.c
static int computeSavings( DdManager * dd, DdNode * f, DdNode * skip, ApproxInfo * info, DdLevelQueue * queue )
UAmarkNodes
RAmarkNodes
BAmarkNodes
cuddApprox.c
static void copyOrder( DdManager * table, int * array, int lower, int upper )
cuddAnneal.c
static DdNode * createResult( DdManager * dd, unsigned int index, unsigned int phase, DdNode * cube, CUDD_VALUE_TYPE distance )
cuddBddClosestCube
separateCube
cuddPriority.c
DdNode * cuddAddApplyRecur( DdManager * dd, DD_AOP op, DdNode * f, DdNode * g )
cuddAddMonadicApplyRecur
cuddAddApply.c
DdNode * cuddAddBddDoPattern( DdManager * dd, DdNode * f )
cuddBridge.c
DdNode * cuddAddCmplRecur( DdManager * dd, DdNode * f )
Cudd_addCmpl
cuddAddIte.c
DdNode * cuddAddComposeRecur( DdManager * dd, DdNode * f, DdNode * g, DdNode * proj )
Cudd_addCompose
cuddCompose.c
DdNode * cuddAddConstrainRecur( DdManager * dd, DdNode * f, DdNode * c )
Cudd_addConstrain
cuddGenCof.c
DdNode * cuddAddExistAbstractRecur( DdManager * manager, DdNode * f, DdNode * cube )
cuddAddAbs.c
static DdNode * cuddAddGeneralVectorComposeRecur( DdManager * dd, DD manager DdHashTable * table, computed table DdNode * f, ADD in which to compose DdNode ** vectorOn, functions to substitute for x_i DdNode ** vectorOff, functions to substitute for x_i' int deepest depth of deepest substitution )
cuddCompose.c
DdNode * cuddAddIteRecur( DdManager * dd, DdNode * f, DdNode * g, DdNode * h )
Cudd_addIte
cuddAddIte.c
DdNode * cuddAddMonadicApplyRecur( DdManager * dd, DD_MAOP op, DdNode * f )
cuddAddApplyRecur
cuddAddApply.c
DdNode * cuddAddNegateRecur( DdManager * dd, DdNode * f )
cuddAddNeg.c
static DdNode * cuddAddNonSimComposeRecur( DdManager * dd, DdNode * f, DdNode ** vector, DdNode * key, DdNode * cube, int lastsub )
cuddCompose.c
DdNode * cuddAddOrAbstractRecur( DdManager * manager, DdNode * f, DdNode * cube )
cuddAddAbs.c
static DdNode * cuddAddOuterSumRecur( DdManager * dd, DdNode * M, DdNode * r, DdNode * c )
cuddMatMult.c
static DdNode * cuddAddPermuteRecur( DdManager * manager, DD manager DdHashTable * table, computed table DdNode * node, ADD to be reordered int * permut permutation array )
The DdNode * that is returned is the same ADD as passed in as node, but in the new order.
Cudd_addPermute
cuddBddPermuteRecur
cuddCompose.c
DdNode * cuddAddRestrictRecur( DdManager * dd, DdNode * f, DdNode * c )
Cudd_addRestrict
cuddGenCof.c
DdNode * cuddAddRoundOffRecur( DdManager * dd, DdNode * f, double trunc )
cuddAddNeg.c
DdNode * cuddAddScalarInverseRecur( DdManager * dd, DdNode * f, DdNode * epsilon )
cuddAddInv.c
DdNode * cuddAddUnivAbstractRecur( DdManager * manager, DdNode * f, DdNode * cube )
cuddAddAbs.c
static DdNode * cuddAddVectorComposeRecur( DdManager * dd, DD manager DdHashTable * table, computed table DdNode * f, ADD in which to compose DdNode ** vector, functions to substitute int deepest depth of deepest substitution )
cuddCompose.c
DdNode * cuddAllocNode( DdManager * unique )
cuddDynamicAllocNode
cuddTable.c
int cuddAnnealing( DdManager * table, int lower, int upper )
cuddAnneal.c
static DdApaNumber cuddApaCountMintermAux( DdNode * node, int digits, DdApaNumber max, DdApaNumber min, st_table * table )
|f'| = max - |f|.
The procedure expects the argument "node" to be a regular pointer, and
guarantees this condition is met in the recursive calls.
For efficiency, the result of a call is cached only if the node has
a reference count greater than 1.
Returns the number of minterms of the function rooted at node.
cuddApa.c
static enum st_retval cuddApaStCountfree( char * key, char * value, char * arg )
cuddApa.c
int cuddBddAlignToZdd( DdManager * table DD manager )
M be the ratio of the two numbers. cuddBddAlignToZdd
then considers the ZDD variables from M*i to
(M+1)*i-1 as corresponding to BDD variable
i. This function should be normally called from
Cudd_zddReduceHeap, which clears the cache. Returns 1 in case of
success; 0 otherwise.
Cudd_ShuffleHeap
Cudd_zddReduceHeap
cuddReorder.c
DdNode * cuddBddAndAbstractRecur( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube )
Cudd_bddAndAbstract
cuddAndAbs.c
DdNode * cuddBddAndRecur( DdManager * manager, DdNode * f, DdNode * g )
Cudd_bddAnd
cuddBddIte.c
DdNode * cuddBddBooleanDiffRecur( DdManager * manager, DdNode * f, DdNode * var )
cuddBddAbs.c
static DdNode * cuddBddCharToVect( DdManager * dd, DdNode * f, DdNode * x )
Cudd_bddCharToVect
cuddGenCof.c
static DdNode * cuddBddClipAndAbsRecur( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube, int distance, int direction )
Cudd_bddClippingAndAbstract
cuddClip.c
DdNode * cuddBddClippingAndAbstract( DdManager * dd, manager DdNode * f, first conjunct DdNode * g, second conjunct DdNode * cube, cube of variables to be abstracted int maxDepth, maximum recursion depth int direction under (0) or over (1) approximation )
Cudd_bddClippingAndAbstract
cuddClip.c
static DdNode * cuddBddClippingAndRecur( DdManager * manager, DdNode * f, DdNode * g, int distance, int direction )
cuddBddClippingAnd
cuddClip.c
DdNode * cuddBddClippingAnd( DdManager * dd, manager DdNode * f, first conjunct DdNode * g, second conjunct int maxDepth, maximum recursion depth int direction under (0) or over (1) approximation )
Cudd_bddClippingAnd
cuddClip.c
DdNode * cuddBddClosestCube( DdManager * dd, DdNode * f, DdNode * g, CUDD_VALUE_TYPE bound )
f and g according to the following formula.
H(f,g) = min(H(ft,gt), H(fe,ge), H(ft,ge)+1, H(fe,gt)+1)
Bounding is based on the following observations.
bound is set at the largest value of the distance
that we are still interested in. Therefore, we desist when
(bound == -1) and (F != not(G)) or (bound == 0) and (F == not(G)).
If we were maximally aggressive in using the bound, we would always
set the bound to the minimum distance seen thus far minus one. That
is, we would maintain the invariant
bound < minD,
except at the very beginning, when we have no value for
minD.
However, we do not use bound < minD when examining the
two negative cofactors, because we try to find a large cube at
minimum distance. To do so, we try to find a cube in the negative
cofactors at the same or smaller distance from the cube found in the
positive cofactors.
When we compute H(ft,ge) and H(fe,gt) we
know that we are going to add 1 to the result of the recursive call
to account for the difference in the splitting variable. Therefore,
we decrease the bound correspondingly.
Another important observation concerns the need of examining all
four pairs of cofators only when both f and
g depend on the top variable.
Suppose gt == ge == g. (That is, g does
not depend on the top variable.) Then
H(f,g) = min(H(ft,g), H(fe,g), H(ft,g)+1, H(fe,g)+1)
= min(H(ft,g), H(fe,g)) .
Therefore, under these circumstances, we skip the two "cross" cases.An interesting feature of this function is the scheme used for caching the results in the global computed table. Since we have a cube and a distance, we combine them to form an ADD. The combination replaces the zero child of the top node of the cube with the negative of the distance. (The use of the negative is to avoid ambiguity with 1.) The degenerate cases (zero and one) are treated specially because the distance is known (0 for one, and infinity for zero).
Cudd_bddClosestCube
cuddPriority.c
DdNode * cuddBddComposeRecur( DdManager * dd, DdNode * f, DdNode * g, DdNode * proj )
Cudd_bddCompose
cuddCompose.c
static int cuddBddConstrainDecomp( DdManager * dd, DdNode * f, DdNode ** decomp )
Cudd_bddConstrainDecomp
cuddGenCof.c
DdNode * cuddBddConstrainRecur( DdManager * dd, DdNode * f, DdNode * c )
Cudd_bddConstrain
cuddGenCof.c
DdNode * cuddBddExistAbstractRecur( DdManager * manager, DdNode * f, DdNode * cube )
Cudd_bddExistAbstract
Cudd_bddUnivAbstract
cuddBddAbs.c
DdNode * cuddBddIntersectRecur( DdManager * dd, DdNode * f, DdNode * g )
Cudd_bddIntersect
cuddBddIte.c
DdNode * cuddBddIsop( DdManager * dd, DdNode * L, DdNode * U )
Cudd_bddIsop
cuddZddIsop.c
DdNode * cuddBddIteRecur( DdManager * dd, DdNode * f, DdNode * g, DdNode * h )
cuddBddIte.c
static DdNode * cuddBddLICBuildResult( DdManager * dd, DdNode * f, st_table * cache, st_table * table )
Cudd_bddLICompaction
cuddBddLICMarkEdges
cuddGenCof.c
static int cuddBddLICMarkEdges( DdManager * dd, DdNode * f, DdNode * c, st_table * table, st_table * cache )
f
if successful; otherwise CUDD_OUT_OF_MEM.
Cudd_bddLICompaction
cuddBddLICBuildResult
cuddGenCof.c
DdNode * cuddBddLICompaction( DdManager * dd, manager DdNode * f, function to be minimized DdNode * c constraint (care set) )
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.
Cudd_bddLICompaction
cuddGenCof.c
DdNode * cuddBddLiteralSetIntersectionRecur( DdManager * dd, DdNode * f, DdNode * g )
cuddLiteral.c
DdNode * cuddBddMakePrime( DdManager * dd, manager DdNode * cube, cube to be expanded DdNode * f function of which the cube is to be made a prime )
cuddSat.c
DdNode * cuddBddNPAndRecur( DdManager * manager, DdNode * f, DdNode * g )
Cudd_bddNPAnd
cuddGenCof.c
static DdNode * cuddBddPermuteRecur( DdManager * manager, DD manager DdHashTable * table, computed table DdNode * node, BDD to be reordered int * permut permutation array )
The DdNode * that is returned is the same BDD as passed in as node, but in the new order.
Cudd_bddPermute
cuddAddPermuteRecur
cuddCompose.c
DdNode * cuddBddRestrictRecur( DdManager * dd, DdNode * f, DdNode * c )
Cudd_bddRestrict
cuddGenCof.c
static DdNode * cuddBddSqueeze( DdManager * dd, DdNode * l, DdNode * u )
Cudd_bddSqueeze
cuddGenCof.c
static DdNode * cuddBddTransferRecur( DdManager * ddS, DdManager * ddD, DdNode * f, st_table * table )
cuddBddTransfer
cuddBridge.c
DdNode * cuddBddTransfer( DdManager * ddS, DdManager * ddD, DdNode * f )
Cudd_bddTransfer
cuddBridge.c
static DdNode * cuddBddVarMapRecur( DdManager * manager, DD manager DdNode * f BDD to be remapped )
Cudd_bddVarMap
cuddCompose.c
static DdNode * cuddBddVectorComposeRecur( DdManager * dd, DD manager DdHashTable * table, computed table DdNode * f, BDD in which to compose DdNode ** vector, functions to be composed int deepest depth of the deepest substitution )
cuddCompose.c
DdNode * cuddBddXorExistAbstractRecur( DdManager * manager, DdNode * f, DdNode * g, DdNode * cube )
Cudd_bddAndAbstract
cuddBddAbs.c
DdNode * cuddBddXorRecur( DdManager * manager, DdNode * f, DdNode * g )
Cudd_bddXor
cuddBddIte.c
DdNode * cuddBiasedUnderApprox( DdManager * dd, DD manager DdNode * f, current DD DdNode * b, bias function int numVars, maximum number of variables int threshold, threshold under which approximation stops double quality1, minimum improvement for accepted changes when b=1 double quality0 minimum improvement for accepted changes when b=0 )
Cudd_BiasedUnderApprox
cuddApprox.c
DdNode * cuddCProjectionRecur( DdManager * dd, DdNode * R, DdNode * Y, DdNode * Ysupp )
Cudd_CProjection
cuddPriority.c
void cuddCacheFlush( DdManager * table )
cuddCache.c
void cuddCacheInsert1( DdManager * table, DD_CTFP1 op, DdNode * f, DdNode * data )
cuddCacheInsert
cuddCacheInsert2
cuddCache.c
void cuddCacheInsert2( DdManager * table, DD_CTFP op, DdNode * f, DdNode * g, DdNode * data )
cuddCacheInsert
cuddCacheInsert1
cuddCache.c
void cuddCacheInsert( DdManager * table, ptruint op, DdNode * f, DdNode * g, DdNode * h, DdNode * data )
cuddCacheInsert2
cuddCacheInsert1
cuddCache.c
DdNode * cuddCacheLookup1Zdd( DdManager * table, DD_CTFP1 op, DdNode * f )
cuddCacheLookupZdd
cuddCacheLookup2Zdd
cuddCache.c
DdNode * cuddCacheLookup1( DdManager * table, DD_CTFP1 op, DdNode * f )
cuddCacheLookup
cuddCacheLookup2
cuddCache.c
DdNode * cuddCacheLookup2Zdd( DdManager * table, DD_CTFP op, DdNode * f, DdNode * g )
cuddCacheLookupZdd
cuddCacheLookup1Zdd
cuddCache.c
DdNode * cuddCacheLookup2( DdManager * table, DD_CTFP op, DdNode * f, DdNode * g )
cuddCacheLookup
cuddCacheLookup1
cuddCache.c
DdNode * cuddCacheLookupZdd( DdManager * table, ptruint op, DdNode * f, DdNode * g, DdNode * h )
cuddCacheLookup2Zdd
cuddCacheLookup1Zdd
cuddCache.c
DdNode * cuddCacheLookup( DdManager * table, ptruint op, DdNode * f, DdNode * g, DdNode * h )
cuddCacheLookup2
cuddCacheLookup1
cuddCache.c
int cuddCacheProfile( DdManager * table, FILE * fp )
cuddCache.c
void cuddCacheResize( DdManager * table )
cuddCache.c
static int cuddCheckCollisionOrdering( DdManager * unique, int i, int j )
cuddTable.c
void cuddClearDeathRow( DdManager * table )
Cudd_DelayedDerefBdd
Cudd_IterDerefBdd
Cudd_CheckZeroRef
cuddGarbageCollect
cuddRef.c
DdNode * cuddCofactorRecur( DdManager * dd, DdNode * f, DdNode * g )
Cudd_Cofactor
cuddCof.c
int cuddCollectNodes( DdNode * f, st_table * visited )
cuddUtil.c
int cuddComputeFloorLog2( unsigned int value )
cuddCache.c
static int cuddConjunctsAux( DdManager * dd, DdNode * f, DdNode ** c1, DdNode ** c2 )
cuddDecomp.c
DdNode * cuddConstantLookup( DdManager * table, ptruint op, DdNode * f, DdNode * g, DdNode * h )
cuddCacheLookup
cuddCache.c
int cuddDestroySubtables( DdManager * unique, int n )
cuddInsertSubtables
Cudd_SetVarMap
cuddTable.c
static void cuddDoRebalance( DdNodePtr ** stack, int stackN )
cuddTable.c
DdNode * cuddDynamicAllocNode( DdManager * table )
cuddAllocNode
cuddReorder.c
static int cuddEstimateCofactorSimple( DdNode * node, int i )
cuddUtil.c
static int cuddEstimateCofactor( DdManager * dd, st_table * table, DdNode * node, int i, int phase, DdNode ** ptr )
cuddUtil.c
int cuddExact( DdManager * table, int lower, int upper )
cuddExact.c
static int cuddFindParent( DdManager * table, DdNode * node )
cuddTable.c
void cuddFreeTable( DdManager * unique )
cuddInitTable
cuddTable.c
int cuddGarbageCollect( DdManager * unique, int clearCache )
cuddTable.c
int cuddGa( DdManager * table, manager int lower, lowest level to be reordered int upper highest level to be reorderded )
cuddGenetic.c
void cuddGetBranches( DdNode * g, DdNode ** g1, DdNode ** g0 )
cuddCof.c
int cuddHashTableGenericInsert( DdHashTable * hash, DdNode * f, void * value )
cuddHashTableInsert1
cuddHashTableGenericLookup
cuddLCache.c
void * cuddHashTableGenericLookup( DdHashTable * hash, DdNode * f )
cuddHashTableLookup1
cuddHashTableGenericInsert
cuddLCache.c
void cuddHashTableGenericQuit( DdHashTable * hash )
cuddHashTableInit
cuddLCache.c
DdHashTable * cuddHashTableInit( DdManager * manager, unsigned int keySize, unsigned int initSize )
cuddHashTableQuit
cuddLCache.c
int cuddHashTableInsert1( DdHashTable * hash, DdNode * f, DdNode * value, ptrint count )
cuddHashTableInsert
cuddHashTableInsert2
cuddHashTableInsert3
cuddHashTableLookup1
cuddLCache.c
int cuddHashTableInsert2( DdHashTable * hash, DdNode * f, DdNode * g, DdNode * value, ptrint count )
cuddHashTableInsert
cuddHashTableInsert1
cuddHashTableInsert3
cuddHashTableLookup2
cuddLCache.c
int cuddHashTableInsert3( DdHashTable * hash, DdNode * f, DdNode * g, DdNode * h, DdNode * value, ptrint count )
cuddHashTableInsert
cuddHashTableInsert1
cuddHashTableInsert2
cuddHashTableLookup3
cuddLCache.c
int cuddHashTableInsert( DdHashTable * hash, DdNodePtr * key, DdNode * value, ptrint count )
[cuddHashTableInsert1
cuddHashTableInsert2
cuddHashTableInsert3
cuddHashTableLookup
cuddLCache.c
DdNode * cuddHashTableLookup1( DdHashTable * hash, DdNode * f )
cuddHashTableLookup
cuddHashTableLookup2
cuddHashTableLookup3
cuddHashTableInsert1
cuddLCache.c
DdNode * cuddHashTableLookup2( DdHashTable * hash, DdNode * f, DdNode * g )
cuddHashTableLookup
cuddHashTableLookup1
cuddHashTableLookup3
cuddHashTableInsert2
cuddLCache.c
DdNode * cuddHashTableLookup3( DdHashTable * hash, DdNode * f, DdNode * g, DdNode * h )
cuddHashTableLookup
cuddHashTableLookup1
cuddHashTableLookup2
cuddHashTableInsert3
cuddLCache.c
DdNode * cuddHashTableLookup( DdHashTable * hash, DdNodePtr * key )
cuddHashTableLookup1
cuddHashTableLookup2
cuddHashTableLookup3
cuddHashTableInsert
cuddLCache.c
void cuddHashTableQuit( DdHashTable * hash )
cuddHashTableInit
cuddLCache.c
static int cuddHashTableResize( DdHashTable * hash )
cuddHashTableInsert
cuddLCache.c
int cuddHeapProfile( DdManager * dd )
cuddCheck.c
int cuddInitCache( DdManager * unique, unique table unsigned int cacheSize, initial size of the cache unsigned int maxCacheSize cache size beyond which no resizing occurs )
Cudd_Init
cuddCache.c
int cuddInitInteract( DdManager * table )
cuddInteract.c
int cuddInitLinear( DdManager * table )
cuddLinear.c
DdManager * cuddInitTable( unsigned int numVars, Initial number of BDD variables (and subtables) unsigned int numVarsZ, Initial number of ZDD variables (and subtables) unsigned int numSlots, Initial size of the BDD subtables unsigned int looseUpTo Limit for fast table growth )
Cudd_Init
cuddFreeTable
cuddTable.c
int cuddInsertSubtables( DdManager * unique, int n, int level )
cuddDestroySubtables
cuddTable.c
int cuddIsInDeathRow( DdManager * dd, DdNode * f )
Cudd_DelayedDerefBdd
cuddClearDeathRow
cuddRef.c
void cuddLevelQueueDequeue( DdLevelQueue * queue, int level )
cuddLevelQueueEnqueue
cuddLevelQ.c
void * cuddLevelQueueEnqueue( DdLevelQueue * queue, level queue void * key, key to be enqueued int level level at which to insert )
cuddLevelQueueInit
cuddLevelQueueDequeue
cuddLevelQ.c
void * cuddLevelQueueFirst( DdLevelQueue * queue, level queue void * key, key to be enqueued int level level at which to insert )
cuddLevelQueueEnqueue
cuddLevelQ.c
DdLevelQueue * cuddLevelQueueInit( int levels, number of levels int itemSize, size of the item int numBuckets initial number of hash buckets )
cuddLevelQueueQuit
cuddLevelQueueEnqueue
cuddLevelQueueDequeue
cuddLevelQ.c
void cuddLevelQueueQuit( DdLevelQueue * queue )
cuddLevelQueueInit
cuddLevelQ.c
int cuddLinearAndSifting( DdManager * table, int lower, int upper )
cuddLinear.c
int cuddLinearInPlace( DdManager * table, int x, int y )
cuddSwapInPlace
cuddLinear.c
static void cuddLocalCacheAddToList( DdLocalCache * cache )
cuddLCache.c
void cuddLocalCacheClearAll( DdManager * manager )
cuddLCache.c
void cuddLocalCacheClearDead( DdManager * manager )
cuddLCache.c
DdLocalCache * cuddLocalCacheInit( DdManager * manager, manager unsigned int keySize, size of the key (number of operands) unsigned int cacheSize, Initial size of the cache unsigned int maxCacheSize Size of the cache beyond which no resizing occurs )
cuddInitCache
cuddLCache.c
void cuddLocalCacheInsert( DdLocalCache * cache, DdNodePtr * key, DdNode * value )
cuddLCache.c
DdNode * cuddLocalCacheLookup( DdLocalCache * cache, DdNodePtr * key )
cuddLCache.c
int cuddLocalCacheProfile( DdLocalCache * cache )
cuddLCache.c
void cuddLocalCacheQuit( DdLocalCache * cache cache to be shut down )
cuddLocalCacheInit
cuddLCache.c
static void cuddLocalCacheRemoveFromList( DdLocalCache * cache )
cuddLCache.c
static void cuddLocalCacheResize( DdLocalCache * cache )
cuddLCache.c
DdNode * cuddMakeBddFromZddCover( DdManager * dd, DdNode * node )
Cudd_MakeBddFromZddCover
cuddZddIsop.c
static int cuddMinHammingDistRecur( DdNode * f, int * minterm, DdHashTable * table, int upperBound )
Cudd_MinHammingDist
cuddPriority.c
int cuddNextHigh( DdManager * table, int x )
cuddNextLow
cuddReorder.c
int cuddNextLow( DdManager * table, int x )
cuddNextHigh
cuddReorder.c
static int cuddNodeArrayRecur( DdNode * f, DdNodePtr * table, int index )
cuddUtil.c
DdNodePtr * cuddNodeArray( DdNode * f, int * n )
Cudd_FirstNode
cuddUtil.c
static void cuddOrderedInsert( DdNodePtr * root, DdNodePtr node )
cuddOrderedThread
cuddTable.c
static DdNode * cuddOrderedThread( DdNode * root, DdNode * list )
cuddOrderedInsert
cuddTable.c
void cuddPrintNode( DdNode * f, FILE * fp )
cuddCheck.c
void cuddPrintVarGroups( DdManager * dd, manager MtrNode * root, root of the group tree int zdd, 0: BDD; 1: ZDD int silent flag to check tree syntax only )
cuddCheck.c
int cuddP( DdManager * dd, DdNode * f )
Cudd_PrintDebug
cuddUtil.c
void cuddReclaimZdd( DdManager * table, DdNode * n )
cuddReclaim
cuddRef.c
void cuddReclaim( DdManager * table, DdNode * n )
cuddReclaimZdd
cuddRef.c
void cuddRehash( DdManager * unique, int i )
cuddTable.c
DdNode * cuddRemapUnderApprox( DdManager * dd, DD manager DdNode * f, current DD int numVars, maximum number of variables int threshold, threshold under which approximation stops double quality minimum improvement for accepted changes )
Cudd_RemapUnderApprox
cuddApprox.c
int cuddResizeLinear( DdManager * table )
cuddLinear.c
int cuddResizeTableZdd( DdManager * unique, int index )
ddResizeTable
cuddTable.c
void cuddSetInteract( DdManager * table, int x, int y )
cuddInteract.c
void cuddShrinkDeathRow( DdManager * table )
cuddClearDeathRow
cuddRef.c
void cuddShrinkSubtable( DdManager * unique, int i )
cuddRehash
cuddTable.c
int cuddSifting( DdManager * table, int lower, int upper )
cuddReorder.c
void cuddSlowTableGrowth( DdManager * unique )
cuddTable.c
DdNode * cuddSolveEqnRecur( DdManager * bdd, DdNode * F, the left-hand side of the equation DdNode * Y, the cube of remaining y variables DdNode ** G, the array of solutions int n, number of unknowns int * yIndex, array holding the y variable indices int i level of recursion )
Cudd_SolveEqn
Cudd_VerifySol
cuddSolve.c
DdNode* cuddSplitSetRecur( DdManager * manager, st_table * mtable, int * varSeen, DdNode * p, double n, double max, int index )
cuddSplit.c
enum st_retval cuddStCountfree( char * key, char * value, char * arg )
cuddUtil.c
DdNode * cuddSubsetHeavyBranch( DdManager * dd, DD manager DdNode * f, current DD int numVars, maximum number of variables int threshold threshold size for the subset )
Cudd_SubsetHeavyBranch
cuddSubsetHB.c
DdNode * cuddSubsetShortPaths( DdManager * dd, DD manager DdNode * f, function to be subset int numVars, total number of variables in consideration int threshold, maximum number of nodes allowed in the subset int hardlimit flag determining whether threshold should be respected strictly )
Cudd_SubsetShortPaths
cuddSubsetSP.c
int cuddSwapInPlace( DdManager * table, int x, int y )
cuddReorder.c
int cuddSwapping( DdManager * table, int lower, int upper, Cudd_ReorderingType heuristic )
cuddReorder.c
int cuddSymmCheck( DdManager * table, int x, int y )
cuddSymmetry.c
int cuddSymmSiftingConv( DdManager * table, int lower, int upper )
cuddSymmSifting
cuddSymmetry.c
int cuddSymmSifting( DdManager * table, int lower, int upper )
cuddSymmSiftingConv
cuddSymmetry.c
int cuddTestInteract( DdManager * table, int x, int y )
cuddInteract.c
int cuddTimesInDeathRow( DdManager * dd, DdNode * f )
Cudd_DelayedDerefBdd
cuddClearDeathRow
cuddIsInDeathRow
cuddRef.c
int cuddTreeSifting( DdManager * table, DD table Cudd_ReorderingType method reordering method for the groups of leaves )
cuddGroup.c
DdNode * cuddUnderApprox( DdManager * dd, DD manager DdNode * f, current DD int numVars, maximum number of variables int threshold, threshold under which approximation stops int safe, enforce safe approximation double quality minimum improvement for accepted changes )
Cudd_UnderApprox
cuddApprox.c
DdNode * cuddUniqueConst( DdManager * unique, CUDD_VALUE_TYPE value )
cuddTable.c
DdNode * cuddUniqueInterIVO( DdManager * unique, int index, DdNode * T, DdNode * E )
cuddUniqueInter
Cudd_MakeBddFromZddCover
cuddTable.c
DdNode * cuddUniqueInterZdd( DdManager * unique, int index, DdNode * T, DdNode * E )
cuddUniqueInter
cuddTable.c
DdNode * cuddUniqueInter( DdManager * unique, int index, DdNode * T, DdNode * E )
cuddUniqueInterZdd
cuddTable.c
static DdNode * cuddUniqueLookup( DdManager * unique, int index, DdNode * T, DdNode * E )
cuddUniqueInter
cuddUtil.c
void cuddUpdateInteractionMatrix( DdManager * table, int xindex, int yindex )
cuddLinear.c
DdNode * cuddVerifySol( DdManager * bdd, DdNode * F, the left-hand side of the equation DdNode ** G, the array of solutions int * yIndex, array holding the y variable indices int n number of unknowns )
Cudd_VerifySol
cuddSolve.c
int cuddWindowReorder( DdManager * table, DD table int low, lowest index to reorder int high, highest index to reorder Cudd_ReorderingType submethod window reordering option )
cuddWindow.c
static void cuddXorLinear( DdManager * table, int x, int y )
cuddLinear.c
int cuddZddAlignToBdd( DdManager * table DD manager )
M be the ratio of the two numbers. cuddZddAlignToBdd
then considers the ZDD variables from M*i to
(M+1)*i-1 as corresponding to BDD variable
i. This function should be normally called from
Cudd_ReduceHeap, which clears the cache. Returns 1 in case of
success; 0 otherwise.
Cudd_zddShuffleHeap
Cudd_ReduceHeap
cuddZddReord.c
DdNode * cuddZddChangeAux( DdManager * zdd, DdNode * P, DdNode * zvar )
cuddZddSetop.c
DdNode * cuddZddChange( DdManager * dd, DdNode * P, int var )
Cudd_zddChange
cuddZddSetop.c
DdNode * cuddZddComplement( DdManager * dd, DdNode * node )
cuddZddFuncs.c
static double cuddZddCountDoubleStep( DdNode * P, st_table * table, DdNode * base, DdNode * empty )
cuddZddCount.c
static int cuddZddCountStep( DdNode * P, st_table * table, DdNode * base, DdNode * empty )
cuddZddCount.c
static int cuddZddDagInt( DdNode * n, st_table * tab )
cuddZddMisc.c
DdNode * cuddZddDiff( DdManager * zdd, DdNode * P, DdNode * Q )
cuddZddSetop.c
DdNode * cuddZddDivideF( DdManager * dd, DdNode * f, DdNode * g )
Cudd_zddDivideF
cuddZddFuncs.c
DdNode * cuddZddDivide( DdManager * dd, DdNode * f, DdNode * g )
Cudd_zddDivide
cuddZddFuncs.c
void cuddZddFreeUniv( DdManager * zdd )
cuddZddInitUniv
cuddInit.c
int cuddZddGetCofactors2( DdManager * dd, DdNode * f, int v, DdNode ** f1, DdNode ** f0 )
cuddZddGetCofactors3
cuddZddFuncs.c
int cuddZddGetCofactors3( DdManager * dd, DdNode * f, int v, DdNode ** f1, DdNode ** f0, DdNode ** fd )
cuddZddGetCofactors2
cuddZddFuncs.c
int cuddZddGetNegVarIndex( DdManager * dd, int index )
cuddZddFuncs.c
int cuddZddGetNegVarLevel( DdManager * dd, int index )
cuddZddFuncs.c
DdNode * cuddZddGetNodeIVO( DdManager * dd, int index, DdNode * g, DdNode * h )
cuddZddGetNode
cuddZddIsop
cuddTable.c
DdNode * cuddZddGetNode( DdManager * zdd, int id, DdNode * T, DdNode * E )
cuddUniqueInterZdd
cuddTable.c
int cuddZddGetPosVarIndex( DdManager * dd, int index )
cuddZddFuncs.c
int cuddZddGetPosVarLevel( DdManager * dd, int index )
cuddZddFuncs.c
int cuddZddInitUniv( DdManager * zdd )
cuddZddFreeUniv
cuddInit.c
DdNode * cuddZddIntersect( DdManager * zdd, DdNode * P, DdNode * Q )
cuddZddSetop.c
DdNode * cuddZddIsop( DdManager * dd, DdNode * L, DdNode * U, DdNode ** zdd_I )
Cudd_zddIsop
cuddZddIsop.c
DdNode * cuddZddIte( DdManager * dd, DdNode * f, DdNode * g, DdNode * h )
cuddZddSetop.c
static int cuddZddLinearAux( DdManager * table, int x, int xLow, int xHigh )
cuddZddLin.c
static int cuddZddLinearBackward( DdManager * table, int size, Move * moves )
cuddZddLin.c
static Move * cuddZddLinearDown( DdManager * table, int x, int xHigh, Move * prevMoves )
cuddZddLin.c
static int cuddZddLinearInPlace( DdManager * table, int x, int y )
cuddZddSwapInPlace
cuddLinearInPlace
cuddZddLin.c
int cuddZddLinearSifting( DdManager * table, int lower, int upper )
cuddZddLin.c
static Move * cuddZddLinearUp( DdManager * table, int y, int xLow, Move * prevMoves )
cuddZddLin.c
int cuddZddNextHigh( DdManager * table, int x )
cuddZddReord.c
int cuddZddNextLow( DdManager * table, int x )
cuddZddReord.c
DdNode * cuddZddProduct( DdManager * dd, DdNode * f, DdNode * g )
Cudd_zddProduct
cuddZddFuncs.c
int cuddZddP( DdManager * zdd, DdNode * f )
Cudd_zddPrintDebug
cuddZddUtil.c
static int cuddZddSiftingAux( DdManager * table, int x, int x_low, int x_high )
cuddZddReord.c
static int cuddZddSiftingBackward( DdManager * table, Move * moves, int size )
cuddZddReord.c
static Move * cuddZddSiftingDown( DdManager * table, int x, int x_high, int initial_size )
cuddZddReord.c
static Move * cuddZddSiftingUp( DdManager * table, int x, int x_low, int initial_size )
cuddZddReord.c
int cuddZddSifting( DdManager * table, int lower, int upper )
cuddZddReord.c
DdNode * cuddZddSubset0( DdManager * dd, DdNode * P, int var )
cuddZddSubset1
Cudd_zddSubset0
cuddZddSetop.c
DdNode * cuddZddSubset1( DdManager * dd, DdNode * P, int var )
cuddZddSubset0
Cudd_zddSubset1
cuddZddSetop.c
int cuddZddSwapInPlace( DdManager * table, int x, int y )
cuddZddReord.c
int cuddZddSwapping( DdManager * table, int lower, int upper, Cudd_ReorderingType heuristic )
cuddZddReord.c
int cuddZddSymmCheck( DdManager * table, int x, int y )
cuddZddSymm.c
static int cuddZddSymmSiftingAux( DdManager * table, int x, int x_low, int x_high )
cuddZddSymm.c
static int cuddZddSymmSiftingBackward( DdManager * table, Move * moves, int size )
cuddZddSymm.c
static int cuddZddSymmSiftingConvAux( DdManager * table, int x, int x_low, int x_high )
cuddZddSymm.c
int cuddZddSymmSiftingConv( DdManager * table, int lower, int upper )
cuddZddSymmSifting
cuddZddSymm.c
static Move * cuddZddSymmSifting_down( DdManager * table, int x, int x_high, int initial_size )
cuddZddSymm.c
static Move * cuddZddSymmSifting_up( DdManager * table, int x, int x_low, int initial_size )
cuddZddSymm.c
int cuddZddSymmSifting( DdManager * table, int lower, int upper )
cuddZddSymmSiftingConv
cuddZddSymm.c
static void cuddZddSymmSummary( DdManager * table, int lower, int upper, int * symvars, int * symgroups )
cuddZddSymm.c
int cuddZddTreeSifting( DdManager * table, DD table Cudd_ReorderingType method reordering method for the groups of leaves )
cuddZddGroup.c
DdNode * cuddZddUnateProduct( DdManager * dd, DdNode * f, DdNode * g )
Cudd_zddUnateProduct
cuddZddFuncs.c
static Move* cuddZddUndoMoves( DdManager * table, Move * moves )
cuddZddLin.c
DdNode * cuddZddUnion( DdManager * zdd, DdNode * P, DdNode * Q )
cuddZddSetop.c
int cuddZddUniqueCompare( int * ptr_x, int * ptr_y )
cuddZddReord.c
DdNode * cuddZddWeakDivF( DdManager * dd, DdNode * f, DdNode * g )
Cudd_zddWeakDivF
cuddZddFuncs.c
DdNode * cuddZddWeakDiv( DdManager * dd, DdNode * f, DdNode * g )
Cudd_zddWeakDiv
cuddZddFuncs.c
static DdNode * ddBddMaximallyExpand( DdManager * dd, manager DdNode * lb, cube to be expanded DdNode * ub, upper bound cube DdNode * f function against which to expand )
cuddSat.c
static int ddBddShortestPathUnate( DdManager * dd, DdNode * f, int * phases, st_table * table )
getShortest
cuddSat.c
static DdNode * ddBddToAddRecur( DdManager * dd, DdNode * B )
cuddBridge.c
static int ddCheckPermuation( DdManager * table, MtrNode * treenode, int * perm, int * invperm )
cuddReorder.c
static void ddClearFlag( DdNode * f )
ddSupportStep
ddFindSupport
ddLeavesInt
ddDagInt
cuddUtil.c
static void ddClearGlobal( DdManager * table, int lower, int maxlevel )
ddCountRoots
cuddExact.c
static void ddClearGlobal( DdManager * table )
cuddInteract.c
static void ddClearLocal( DdNode * f )
cuddInteract.c
static void ddClearVars( DdManager * dd, int SP )
cuddUtil.c
static double * ddCofMintermAux( DdManager * dd, DdNode * node, st_table * table )
cuddSign.c
static int ddCountInternalMtrNodes( DdManager * table, MtrNode * treenode )
cuddGroup.c
static double ddCountMintermAux( DdNode * node, double max, DdHashTable * table )
cuddUtil.c
static double ddCountPathAux( DdNode * node, st_table * table )
cuddUtil.c
static double ddCountPathsToNonZero( DdNode * N, st_table * table )
cuddUtil.c
static int ddCountRoots( DdManager * table, int lower, int upper )
ddClearGlobal
cuddExact.c
static void ddCreateGroup( DdManager * table, int x, int y )
cuddGroup.c
static int ddDagInt( DdNode * n )
cuddUtil.c
static void ddDissolveGroup( DdManager * table, int x, int y )
cuddGroup.c
static int ddDoDumpBlif( DdManager * dd, DdNode * f, FILE * fp, st_table * visited, char ** names, int mv )
cuddExport.c
static int ddDoDumpDDcal( DdManager * dd, DdNode * f, FILE * fp, st_table * visited, char ** names, ptruint mask )
cuddExport.c
static int ddDoDumpDaVinci( DdManager * dd, DdNode * f, FILE * fp, st_table * visited, char ** names, ptruint mask )
cuddExport.c
static int ddDoDumpFactoredForm( DdManager * dd, DdNode * f, FILE * fp, char ** names )
Cudd_DumpFactoredForm
cuddExport.c
static int ddEpdCountMintermAux( DdNode * node, EpDouble * max, EpDouble * epd, st_table * table )
cuddUtil.c
static enum st_retval ddEpdFree( char * key, char * value, char * arg )
cuddUtil.c
static int ddExchange( DdManager * table, int x, int y, double temp )
cuddAnneal.c
static int ddExtSymmCheck( DdManager * table, int x, int y )
cuddGroup.c
static DdNode * ddFindEssentialRecur( DdManager * dd, DdNode * f )
cuddEssent.c
static void ddFindNodeHiLo( DdManager * table, MtrNode * treenode, int * lower, int * upper )
cuddGroup.c
static void ddFindSupport( DdManager * dd, DdNode * f, int * SP )
cuddUtil.c
static DdTlcInfo * ddFindTwoLiteralClausesRecur( DdManager * dd, DdNode * f, st_table * table )
Cudd_FindTwoLiteralClauses
cuddEssent.c
static DdNode * ddGetLargestCubeUnate( DdManager * dd, DdNode * f, int * phases, st_table * table )
getPath
cuddSat.c
static int ddGroupMoveBackward( DdManager * table, int x, int y )
cuddGroup.c
static int ddGroupMove( DdManager * table, int x, int y, Move ** moves )
cuddGroup.c
static int ddGroupSiftingAux( DdManager * table, int x, int xLow, int xHigh, DD_CHKFP checkFunction, int lazyFlag )
cuddGroup.c
static int ddGroupSiftingBackward( DdManager * table, Move * moves, int size, int upFlag, int lazyFlag )
cuddGroup.c
static int ddGroupSiftingDown( DdManager * table, int x, int xHigh, DD_CHKFP checkFunction, Move ** moves )
cuddGroup.c
static int ddGroupSiftingUp( DdManager * table, int y, int xLow, DD_CHKFP checkFunction, Move ** moves )
cuddGroup.c
static int ddGroupSifting( DdManager * table, int lower, int upper, DD_CHKFP checkFunction, int lazyFlag )
cuddGroup.c
static int ddIsVarHandled( DdManager * dd, int index )
cuddGroup.c
static int ddJumpingAux( DdManager * table, int x, int x_low, int x_high, double temp )
cuddAnneal.c
static Move * ddJumpingDown( DdManager * table, int x, int x_high, int initial_size )
cuddAnneal.c
static Move * ddJumpingUp( DdManager * table, int x, int x_low, int initial_size )
cuddAnneal.c
static int ddLeavesInt( DdNode * n )
Cudd_CountLeaves
cuddUtil.c
static int ddLinearAndSiftingAux( DdManager * table, int x, int xLow, int xHigh )
cuddLinear.c
static int ddLinearAndSiftingBackward( DdManager * table, int size, Move * moves )
cuddLinear.c
static Move * ddLinearAndSiftingDown( DdManager * table, int x, int xHigh, Move * prevMoves )
cuddLinear.c
static Move * ddLinearAndSiftingUp( DdManager * table, int y, int xLow, Move * prevMoves )
cuddLinear.c
static int ddLinearUniqueCompare( int * ptrX, int * ptrY )
cuddLinear.c
static void ddMergeGroups( DdManager * table, MtrNode * treenode, int low, int high )
cuddGroup.c
static int ddNoCheck( DdManager * table, int x, int y )
cuddGroup.c
static void ddPatchTree( DdManager * dd, MtrNode * treenode )
cuddTable.c
static int ddPermuteWindow3( DdManager * table, int x )
cuddWindow.c
static int ddPermuteWindow4( DdManager * table, int w )
cuddWindow.c
static int ddPickArbitraryMinterms( DdManager * dd, DdNode * node, int nvars, int nminterms, char ** string )
Cudd_bddPickArbitraryMinterms
cuddUtil.c
static int ddPickRepresentativeCube( DdManager * dd, DdNode * node, double * weight, char * string )
cuddUtil.c
static void ddPrintMintermAux( DdManager * dd, manager DdNode * node, current node int * list current recursion path )
cuddUtil.c
static void ddRehashZdd( DdManager * unique, int i )
cuddRehash
cuddTable.c
static int ddReorderChildren( DdManager * table, MtrNode * treenode, Cudd_ReorderingType method )
cuddGroup.c
static int ddReorderPostprocess( DdManager * table )
cuddReorder.c
static int ddReorderPreprocess( DdManager * table )
cuddReorder.c
static void ddReportRefMess( DdManager * unique, manager int i, table in which the problem occurred const char * caller procedure that detected the problem )
cuddGarbageCollect
cuddGarbageCollectZdd
cuddTable.c
static int ddResetVarHandled( DdManager * dd, int index )
cuddGroup.c
static int ddResizeTable( DdManager * unique, int index, int amount )
Cudd_Reserve
cuddResizeTableZdd
cuddTable.c
static int ddSecDiffCheck( DdManager * table, int x, int y )
cuddGroup.c
static int ddSetVarHandled( DdManager * dd, int index )
cuddGroup.c
static int ddShuffle( DdManager * table, DdHalfWord * permutation, int lower, int upper )
cuddExact.c
static int ddShuffle( DdManager * table, int * permutation )
cuddReorder.c
static int ddSiftUp( DdManager * table, int x, int xLow )
cuddExact.c
static int ddSiftUp( DdManager * table, int x, int xLow )
cuddReorder.c
static int ddSiftingAux( DdManager * table, int x, int xLow, int xHigh )
cuddReorder.c
static int ddSiftingBackward( DdManager * table, int size, Move * moves )
cuddReorder.c
static Move * ddSiftingDown( DdManager * table, int x, int xHigh )
cuddReorder.c
static Move * ddSiftingUp( DdManager * table, int y, int xLow )
cuddReorder.c
static void ddSuppInteract( DdNode * f, char * support )
cuddInteract.c
static void ddSupportStep( DdNode * f, int * support )
ddClearFlag
cuddUtil.c
static Move * ddSwapAny( DdManager * table, int x, int y )
cuddReorder.c
static int ddSymmGroupMoveBackward( DdManager * table, int x, int y )
cuddSymmetry.c
static int ddSymmGroupMove( DdManager * table, int x, int y, Move ** moves )
cuddSymmetry.c
static int ddSymmSiftingAux( DdManager * table, int x, int xLow, int xHigh )
cuddSymmetry.c
static int ddSymmSiftingBackward( DdManager * table, Move * moves, int size )
cuddSymmetry.c
static int ddSymmSiftingConvAux( DdManager * table, int x, int xLow, int xHigh )
cuddSymmetry.c
static Move * ddSymmSiftingDown( DdManager * table, int x, int xHigh )
cuddSymmetry.c
static Move * ddSymmSiftingUp( DdManager * table, int y, int xLow )
cuddSymmetry.c
static void ddSymmSummary( DdManager * table, int lower, int upper, int * symvars, int * symgroups )
cuddSymmetry.c
static int ddSymmUniqueCompare( int * ptrX, int * ptrY )
cuddSymmetry.c
static int ddTreeSiftingAux( DdManager * table, MtrNode * treenode, Cudd_ReorderingType method )
cuddGroup.c
static Move* ddUndoMoves( DdManager * table, Move * moves )
cuddLinear.c
static int ddUniqueCompareGroup( int * ptrX, int * ptrY )
cuddGroup.c
static int ddUniqueCompare( int * ptrX, int * ptrY )
cuddReorder.c
static void ddUpdateInteract( DdManager * table, char * support )
cuddInteract.c
static int ddUpdateMtrTree( DdManager * table, MtrNode * treenode, int * perm, int * invperm )
cuddReorder.c
static int ddVarGroupCheck( DdManager * table, int x, int y )
cuddGroup.c
static int ddWindow2( DdManager * table, int low, int high )
cuddWindow.c
static int ddWindow3( DdManager * table, int low, int high )
cuddWindow.c
static int ddWindow4( DdManager * table, int low, int high )
cuddWindow.c
static int ddWindowConv2( DdManager * table, int low, int high )
cuddWindow.c
static int ddWindowConv3( DdManager * table, int low, int high )
cuddWindow.c
static int ddWindowConv4( DdManager * table, int low, int high )
cuddWindow.c
static void debugCheckParent( DdManager * table, DdNode * node )
debugFindParent
cuddCheck.c
static void debugFindParent( DdManager * table, DdNode * node )
cuddCheck.c
double *þprobþ( )
double þmgþ( )
double þmgþ( )
double þmþ( )
double þquality0þminimum improvement for accepted changes when b=0( )
double þquality0þminimum improvement for accepted changes when b=0( )
double þqualityþminimum improvement for accepted changes( )
double þqualityþminimum improvement for accepted changes( )
double þqualityþminimum improvement for accepted changes( )
double þqualityþminimum improvement for accepted changes( )
static int dp2( DdManager * dd, DdNode * f, st_table * t )
cuddUtil.c
static DdTlcInfo * emptyClauseSet( )
cuddEssent.c
static int equalp( DdHalfWord var1a, short phase1a, DdHalfWord var1b, short phase1b, DdHalfWord var2a, short phase2a, DdHalfWord var2b, short phase2b )
beforep
cuddEssent.c
static int find_best( )
cuddGenetic.c
static void fixVarTree( MtrNode * treenode, int * perm, int size )
cuddAPI.c
static void freeMatrix( DdHalfWord ** matrix )
getMatrix
cuddExact.c
static enum st_retval freePathPair( char * key, char * value, char * arg )
cuddSat.c
static NodeData * gatherInfoAux( DdNode * node, function to analyze ApproxInfo * info, info on BDD int parity gather parity information )
gatherInfo
cuddApprox.c
static ApproxInfo * gatherInfo( DdManager * dd, manager DdNode * node, function to be analyzed int numVars, number of variables node depends on int parity gather parity information )
cuddUnderApprox
gatherInfoAux
cuddApprox.c
static int gcd( int x, int y )
cuddExact.c
static DdNode * getCube( DdManager * manager, st_table * visited, DdNode * f, int cost )
cuddSat.c
static cuddPathPair getLargest( DdNode * root, st_table * visited )
cuddSat.c
static int getLevelKeys( DdManager * table, int l )
cuddExact.c
static DdHalfWord ** getMatrix( int rows, number of rows int cols number of columns )
freeMatrix
cuddExact.c
static int getMaxBinomial( int n )
binomial(n,k) = n/k * binomial(n-1,k-1).
Returns the computed value if successful; -1 if out of range.
cuddExact.c
static DdNode * getPath( DdManager * manager, st_table * visited, DdNode * f, int * weight, int cost )
cuddSat.c
static cuddPathPair getShortest( DdNode * root, int * cost, int * support, st_table * visited )
cuddSat.c
static void hashDelete( DdLevelQueue * queue, DdQueueItem * item )
cuddLevelQueueDequeue
hashInsert
cuddLevelQ.c
static int hashInsert( DdLevelQueue * queue, DdQueueItem * item )
cuddLevelQueueEnqueue
cuddLevelQ.c
static DdQueueItem * hashLookup( DdLevelQueue * queue, void * key )
cuddLevelQueueEnqueue
hashInsert
cuddLevelQ.c
static int hashResize( DdLevelQueue * queue )
hashInsert
cuddLevelQ.c
static int impliedp( DdHalfWord var1, short phase1, DdHalfWord var2, short phase2, BitVector * olv, BitVector * olp )
cuddEssent.c
static int indexCompare( const void * a, const void * b )
cuddUtil.c
static DdHalfWord * initSymmInfo( DdManager * table, int lower, int upper )
checkSymmInfo
cuddExact.c
int **þcubeþ( )
int **þcubeþ( )
int **þindicesþarray containing (on return) the indices( )
int **þindicesþarray containing (on return) the indices( )
int **þpathþ( )
int **þpathþ( )
int *þarrayþ( )
int *þarrayþ( )
int *þdigitsþ( )
int *þdistanceþ( )
int *þinputsþ( )
int *þlengthþ( )
int *þlengthþ( )
int *þpermutationþrequired variable permutation( )
int *þpermutationþrequired variable permutation( )
int *þpermutþ( )
int *þpermutþ( )
int *þphase2þ( )
int *þweightþ( )
int þNþ( )
int þamountþ( )
int þarcviolationþ( )
int þbinaryDigitsþ( )
int þbitþ( )
int þbitþ( )
int þcycleþ( )
int þdigitsþ( )
int þdirectionþunder (0) or over (1) approximation( )
int þdirectionþunder (0) or over (1) approximation( )
int þhardlimitþflag: 1 if threshold is a hard limit( )
int þhardlimitþflag: 1 if threshold is a hard limit( )
int þindexþ( )
int þindexþ( )
int þindexþ( )
int þindexþ( )
int þindexþ( )
int þindexþ( )
int þindexþ( )
int þindexþ( )
int þindexþ( )
int þindexþ( )
int þindexþvariable index( )
int þindexþvariable index( )
int þindexþvariable index( )
int þindexþvariable index( )
int þindexþvariable index( )
int þindexþvariable index( )
int þindexþvariable index( )
int þiþ( )
int þiþ( )
int þiþ( )
int þiþ( )
int þiþ( )
int þiþ( )
int þiþ( )
int þiþ( )
int þiþ( )
int þiþ( )
int þiþ( )
int þiþ( )
int þkþnumber of minterms to find( )
int þlevelþ( )
int þlevelþ( )
int þminsizeþbound below which no reordering occurs( )
int þminsizeþbound below which no reordering occurs( )
int þmultiplicityþhow many ZDD variables are created for each BDD variable( )
int þmvarsþsize of maskVars(
)
int þmvþ0: blif, 1: blif-MV( )
int þmvþ0: blif, 1: blif-MV( )
int þnVarsþ( )
int þnumberXoversþ( )
int þnvarsþ( )
int þnvarsþ( )
int þnvarsþ( )
int þnvarsþsize of the support of f( )
int þnzþ( )
int þnzþ( )
int þnzþ( )
int þnþ( )
int þnþ( )
int þnþ( )
int þnþ( )
int þnþ( )
int þnþ( )
int þnþ( )
int þnþ( )
int þnþlength of both arrays( )
int þnþnumbers of unknowns( )
int þnþnumbers of unknowns( )
int þnþsize of vars(
)
int þnþsize of the array( )
int þnþsize of the array( )
int þnþsize of the array( )
int þpairIndexþcorresponding variable index( )
int þpathþ( )
int þphaseþ( )
int þphaseþ1: positive; 0: negative( )
int þpopulationSizeþ( )
int þpowerþ( )
int þprecisionþ( )
int þprecisionþ( )
int þprþ( )
int þprþ( )
int þprþverbosity level( )
int þprþverbosity level( )
int þrecombþ( )
int þsmsþ( )
int þsmvþ( )
int þsymmviolationþ( )
int þsyþstep of column variables( )
int þsyþstep of column variables( )
int þthresholdþmaximum number of nodes in the subset( )
int þthresholdþmaximum number of nodes in the subset( )
int þthresholdþmaximum number of nodes in the superset( )
int þthresholdþmaximum number of nodes in the superset( )
int þtopþindex of top variable( )
int þupperBoundþdistance above which an approximate answer is OK( )
int þupperþ( )
int þupperþ( )
int þvarþ( )
int þvarþ( )
int þvarþ( )
int þvþ( )
int þvþ( )
int þxþ( )
int þyþcolumn index( )
static int largest( )
cuddGenetic.c
long þseedþ( )
long þsizeþsize of the allocation that failed( )
static int make_random( DdManager * table, int lower )
cuddGenetic.c
static DdNode * mintermsFromUniverse( DdManager * manager, DdNode ** vars, int numVars, double n, int index )
cuddSplit.c
static int oneliteralp( DdHalfWord var )
cuddEssent.c
static void pushDown( DdHalfWord * order, int j, int level )
cuddExact.c
static int rand_int( int a )
cuddGenetic.c
static double random_generator( )
cuddAnneal.c
static int restoreOrder( DdManager * table, int * array, int lower, int upper )
cuddAnneal.c
static int roulette( int * p1, int * p2 )
cuddGenetic.c
static DdNode * selectMintermsFromUniverse( DdManager * manager, int * varSeen, double n )
cuddSplit.c
static int sentinelp( DdHalfWord var1, DdHalfWord var2 )
cuddEssent.c
static DdNode * separateCube( DdManager * dd, DdNode * f, CUDD_VALUE_TYPE * distance )
cuddBddClosestCube
createResult
cuddPriority.c
static int siftBackwardProb( DdManager * table, Move * moves, int size, double temp )
cuddAnneal.c
static int sift_up( DdManager * table, int x, int x_low )
cuddGenetic.c
static enum st_retval stPathTableDdFree( char * key, char * value, char * arg )
cuddSubsetSP.c
static enum st_retval st_zdd_count_dbl_free( char * key, char * value, char * arg )
cuddZddCount.c
static enum st_retval st_zdd_countfree( char * key, char * value, char * arg )
cuddZddCount.c
static int stopping_criterion( int c1, int c2, int c3, int c4, double temp )
cuddAnneal.c
static DdTlcInfo * tlcInfoAlloc( )
Cudd_tlcInfoFree
cuddEssent.c
unsigned int þfactorþ( )
unsigned int þhrþ( )
unsigned int þlimitþ( )
unsigned int þlimitþ( )
unsigned int þlimitþ( )
unsigned int þlimitþ( )
unsigned int þlimitþ( )
unsigned int þlimitþ( )
unsigned int þlutþ( )
unsigned int þmaxLiveþ( )
unsigned int þmcþ( )
unsigned int þmrþ( )
unsigned int þnextþ( )
unsigned int þpþ( )
unsigned int þsecondDenþ( )
unsigned int þtypeþMTR_DEFAULT or MTR_FIXED( )
unsigned int þtypeþMTR_DEFAULT or MTR_FIXED( )
unsigned int þupperBþupper bound( )
unsigned long þincreaseþ( )
unsigned long þmaxMemoryþ( )
unsigned long þmaxMemoryþtarget maximum memory occupation( )
unsigned long þstþ( )
unsigned long þtlþ( )
static int updateEntry( DdManager * table, DdHalfWord * order, int level, int cost, DdHalfWord ** orders, int * costs, int subsets, char * mask, int lower, int upper )
cuddExact.c
static void updateParity( DdNode * node, function to analyze ApproxInfo * info, info on BDD int newparity new parity for node )
gatherInfoAux
cuddApprox.c
static int updateRefs( DdManager * dd, DdNode * f, DdNode * skip, ApproxInfo * info, DdLevelQueue * queue )
UAmarkNodes
RAmarkNodes
BAmarkNodes
cuddApprox.c
static int updateUB( DdManager * table, int oldBound, DdHalfWord * bestOrder, int lower, int upper )
cuddExact.c
void *þdataþ( )
void *þdataþ( )
void *þdataþ( )
static void zddClearFlag( DdNode * f )
zddSupportStep
cuddZddUtil.c
static int zddCountInternalMtrNodes( DdManager * table, MtrNode * treenode )
cuddZddGroup.c
static void zddFindNodeHiLo( DdManager * table, MtrNode * treenode, int * lower, int * upper )
cuddZddGroup.c
static void zddFixTree( DdManager * table, MtrNode * treenode )
cuddZddReord.c
static int zddGroupMoveBackward( DdManager * table, int x, int y )
cuddZddGroup.c
static int zddGroupMove( DdManager * table, int x, int y, Move ** moves )
cuddZddGroup.c
static int zddGroupSiftingAux( DdManager * table, int x, int xLow, int xHigh )
cuddZddGroup.c
static int zddGroupSiftingBackward( DdManager * table, Move * moves, int size )
cuddZddGroup.c
static int zddGroupSiftingDown( DdManager * table, int x, int xHigh, Move ** moves )
cuddZddGroup.c
static int zddGroupSiftingUp( DdManager * table, int y, int xLow, Move ** moves )
cuddZddGroup.c
static int zddGroupSifting( DdManager * table, int lower, int upper )
cuddZddGroup.c
static void zddMergeGroups( DdManager * table, MtrNode * treenode, int low, int high )
cuddZddGroup.c
static DdNode * zddPortFromBddStep( DdManager * dd, DdNode * B, int expected )
cuddZddPort.c
static DdNode * zddPortToBddStep( DdManager * dd, manager DdNode * f, ZDD to be converted int depth recursion depth )
cuddZddPort.c
static void zddPrintCoverAux( DdManager * zdd, manager DdNode * node, current node int level, depth in the recursion int * list current recursion path )
cuddZddUtil.c
static int zddReorderChildren( DdManager * table, MtrNode * treenode, Cudd_ReorderingType method )
cuddZddGroup.c
static int zddReorderPostprocess( DdManager * table )
cuddZddReord.c
static void zddReorderPreprocess( DdManager * table )
cuddZddReord.c
static int zddShuffle( DdManager * table, int * permutation )
cuddZddReord.c
static int zddSiftUp( DdManager * table, int x, int xLow )
cuddZddReord.c
static void zddSupportStep( DdNode * f, int * support )
zddClearFlag
cuddZddUtil.c
static Move * zddSwapAny( DdManager * table, int x, int y )
cuddZddReord.c
static int zddTreeSiftingAux( DdManager * table, MtrNode * treenode, Cudd_ReorderingType method )
cuddZddGroup.c
static int zddUniqueCompareGroup( int * ptrX, int * ptrY )
cuddZddGroup.c
static void zddVarToConst( DdNode * f, DdNode ** gp, DdNode ** hp, DdNode * base, DdNode * empty )
cuddZddSetop.c
static int zdd_group_move_backward( DdManager * table, int x, int y )
cuddZddSymm.c
static int zdd_group_move( DdManager * table, int x, int y, Move ** moves )
cuddZddSymm.c
static void zdd_print_minterm_aux( DdManager * zdd, manager DdNode * node, current node int level, depth in the recursion int * list current recursion path )
cuddZddUtil.c
static DdNode * zdd_subset0_aux( DdManager * zdd, DdNode * P, DdNode * zvar )
cuddZddSetop.c
static DdNode * zdd_subset1_aux( DdManager * zdd, DdNode * P, DdNode * zvar )
cuddZddSetop.c
static int zp2( DdManager * zdd, DdNode * f, st_table * t )
cuddZddUtil.c
þþ( )
( )
cuddAllocNode
cuddDynamicAllocNode
cuddDeallocMove
cuddInt.h
( )
cuddDeallocNode
cuddDynamicAllocNode
cuddInt.h
( )
cuddTable.c
( )
bitVectorAlloc
cuddEssent.c
( )
cuddInt.h
( )
cuddCompose.c
( )
cuddCompose.c
( )
Cudd_Not
cudd.h
( )
Cudd_NotCond
cudd.h
( )
ddLCHash3
ddLCHash
cuddLCache.c
( )
ddLCHash2
ddLCHash
cuddLCache.c
( )
ddLCHash3
ddLCHash
cuddLCache.c
( )
cuddInt.h
( )
cuddLCache.c
( )
ddMin
cuddInt.h
( )
ddMax
cuddInt.h
( )
Cudd_Deref
cuddInt.h
( )
cuddInt.h
( )
DD_MSDIGIT
cuddInt.h
( )
DD_LSDIGIT
cuddInt.h
( )
cuddAllocNode
cuddDynamicAllocNode
cuddLCache.c
( )
Cudd_ReadPermZdd
cuddInt.h
( )
Cudd_ReadPerm
cuddInt.h
( )
ddHash
ddCHash
cuddInt.h
( )
ddHash
ddCHash2
cuddInt.h
( )
hashInsert
hashLookup
hashDelete
cuddLevelQ.c
( )
ddCHash
ddCHash2
cuddInt.h
( )
Cudd_Ref
cuddInt.h
( )
CAUTION: It is assumed that dynamic reordering will not occur while there are open generators. It is the user's responsibility to make sure that dynamic reordering does not occur. As long as new nodes are not created during generation, and dynamic reordering is not called explicitly, dynamic reordering will not occur. Alternatively, it is sufficient to disable dynamic reordering. It is a mistake to dispose of a diagram on which generation is ongoing.
Cudd_ForeachNode
Cudd_FirstCube
Cudd_NextCube
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_AutodynDisable
cudd.h
( )
CAUTION: It is assumed that dynamic reordering will not occur while there are open generators. It is the user's responsibility to make sure that dynamic reordering does not occur. As long as new nodes are not created during generation, and dynamic reordering is not called explicitly, dynamic reordering will not occur. Alternatively, it is sufficient to disable dynamic reordering. It is a mistake to dispose of a diagram on which generation is ongoing.
Cudd_ForeachCube
Cudd_FirstNode
Cudd_NextNode
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_AutodynDisable
cudd.h
( )
CAUTION: It is assumed that dynamic reordering will not occur while there are open generators. It is the user's responsibility to make sure that dynamic reordering does not occur. As long as new nodes are not created during generation, and dynamic reordering is not called explicitly, dynamic reordering will not occur. Alternatively, it is sufficient to disable dynamic reordering. It is a mistake to dispose of a diagram on which generation is ongoing.
Cudd_zddFirstPath
Cudd_zddNextPath
Cudd_GenFree
Cudd_IsGenEmpty
Cudd_AutodynDisable
cudd.h
( )
CAUTION: It is a mistake to change a diagram on which generation is ongoing.
Cudd_ForeachCube
Cudd_FirstPrime
Cudd_NextPrime
Cudd_GenFree
Cudd_IsGenEmpty
cudd.h
( )
cuddInt.h
( )
cuddRotateRight
cuddTable.c
( )
cuddRotateLeft
cuddTable.c
( )
Cudd_Regular
Cudd_Complement
cudd.h
( )
cuddInt.h
( )
cudd.h
( )
Cudd_IsConstant
cuddInt.h
( )
DD_ONE
Cudd_Not
DD_PLUS_INFINITY
DD_MINUS_INFINITY
cuddInt.h
( )
cuddGenetic.c
( )
Cudd_Regular
Cudd_IsComplement
cudd.h
( )
DD_ZERO
DD_PLUS_INFINITY
DD_MINUS_INFINITY
cuddInt.h
( )
Cudd_ReadPerm
cudd.h
( )
node is a constant node, the result is unpredictable.
The pointer passed to cuddE must be regular.
Cudd_E
cuddInt.h
( )
node is a constant node, the result is unpredictable.
Cudd_T
Cudd_V
cudd.h
( )
bitVectorSet
cuddEssent.c
( )
DD_ONE
DD_ZERO
DD_PLUS_INFINITY
cuddInt.h
( )
DD_ONE
DD_ZERO
DD_MINUS_INFINITY
cuddInt.h
( )
Cudd_Complement
Cudd_IsComplement
cudd.h
( )
node is a constant node, the result is unpredictable.
The pointer passed to cuddT must be regular.
Cudd_T
cuddInt.h
( )
node is a constant node, the result is unpredictable.
Cudd_E
Cudd_V
cudd.h
( )
node is an internal node, the result is unpredictable.
The pointer passed to cuddV must be regular.
Cudd_V
cuddInt.h
( )
node is an internal node, the result is unpredictable.
Cudd_T
Cudd_E
cudd.h
( )
cuddSatInc
cuddInt.h
( )
cuddSatDec
cuddInt.h
( )
bitVectorRead
cuddEssent.c