src/bdd/dsd/dsdInt.h File Reference

#include "extra.h"
#include "dsd.h"
Include dependency graph for dsdInt.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures

struct  Dsd_Manager_t_
struct  Dsd_Node_t_

Defines

#define MAXINPUTS   1000

Typedefs

typedef unsigned char byte

Functions

void Dsd_CheckCacheAllocate (int nEntries)
void Dsd_CheckCacheDeallocate ()
void Dsd_CheckCacheClear ()
int Dsd_CheckRootFunctionIdentity (DdManager *dd, DdNode *bF1, DdNode *bF2, DdNode *bC1, DdNode *bC2)
Dsd_Node_t * Dsd_TreeNodeCreate (int Type, int nDecs, int BlockNum)
void Dsd_TreeNodeDelete (DdManager *dd, Dsd_Node_t *pNode)
void Dsd_TreeUnmark (Dsd_Manager_t *dMan)
DdNode * Dsd_TreeGetPrimeFunctionOld (DdManager *dd, Dsd_Node_t *pNode, int fRemap)

Define Documentation

#define MAXINPUTS   1000

MACRO DEFINITIONS ///

Definition at line 65 of file dsdInt.h.

Typedef Documentation

typedef unsigned char byte

CFile****************************************************************

FileName [dsdInt.h]

PackageName [DSD: Disjoint-support decomposition package.]

Synopsis [Internal declarations of the package.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 8.0. Started - September 22, 2003.]

Revision [

Id
dsdInt.h,v 1.0 2002/22/09 00:00:00 alanmi Exp

] TYPEDEF DEFINITIONS ///

Definition at line 29 of file dsdInt.h.

Function Documentation

void Dsd_CheckCacheAllocate ( int  nEntries  ) 

PARAMETERS /// FUNCTION DECLARATIONS ///

FUNCTION DEFINITIONS ///Function********************************************************************

Synopsis [(Re)allocates the local cache.]

Description []

SideEffects []

SeeAlso []

Definition at line 60 of file dsdCheck.c.

00061 {
00062         int nRequested;
00063 
00064     pCache = ALLOC( Dds_Cache_t, 1 );
00065     memset( pCache, 0, sizeof(Dds_Cache_t) );
00066 
00067         // check what is the size of the current cache
00068     nRequested = Cudd_Prime( nEntries );
00069         if ( pCache->nTableSize != nRequested )
00070         { // the current size is different
00071                 // deallocate the old, allocate the new
00072                 if ( pCache->nTableSize )
00073                         Dsd_CheckCacheDeallocate();
00074                 // allocate memory for the hash table
00075                 pCache->nTableSize = nRequested;
00076                 pCache->pTable = ALLOC( Dsd_Entry_t, nRequested );
00077         }
00078         // otherwise, there is no need to allocate, just clean
00079         Dsd_CheckCacheClear();
00080 //      printf( "\nThe number of allocated cache entries = %d.\n\n", pCache->nTableSize );
00081 }

void Dsd_CheckCacheClear (  ) 

Function********************************************************************

Synopsis [Clears the local cache.]

Description []

SideEffects []

SeeAlso []

Definition at line 111 of file dsdCheck.c.

00112 {
00113         int i;
00114         for ( i = 0; i < pCache->nTableSize; i++ )
00115                 pCache->pTable[0].bX[0] = NULL;
00116 }

void Dsd_CheckCacheDeallocate (  ) 

Function********************************************************************

Synopsis [Deallocates the local cache.]

Description []

SideEffects []

SeeAlso []

Definition at line 94 of file dsdCheck.c.

00095 {
00096         free( pCache->pTable );
00097     free( pCache );
00098 }

int Dsd_CheckRootFunctionIdentity ( DdManager *  dd,
DdNode *  bF1,
DdNode *  bF2,
DdNode *  bC1,
DdNode *  bC2 
)

Function********************************************************************

Synopsis [Checks whether it is true that bF1(bC1=0) == bF2(bC2=0).]

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file dsdCheck.c.

00131 {
00132         int RetValue;
00133 //      pCache->nSuccess = 0;
00134 //      pCache->nFailure = 0;
00135         RetValue = Dsd_CheckRootFunctionIdentity_rec(dd, bF1, bF2, bC1, bC2);
00136 //      printf( "Cache success = %d. Cache failure = %d.\n", pCache->nSuccess, pCache->nFailure );
00137         return RetValue;
00138 }

DdNode* Dsd_TreeGetPrimeFunctionOld ( DdManager *  dd,
Dsd_Node_t *  pNode,
int  fRemap 
)

Function*************************************************************

Synopsis [Retuns the function of one node of the decomposition tree.]

Description [This is the old procedure. It is now superceded by the procedure Dsd_TreeGetPrimeFunction() found in "dsdLocal.c".]

SideEffects []

SeeAlso []

Definition at line 1008 of file dsdTree.c.

01009 {
01010         DdNode * bCof0,  * bCof1, * bCube0, * bCube1, * bNewFunc, * bTemp;
01011         int i;
01012         int fAllBuffs = 1;
01013         static int Permute[MAXINPUTS];
01014 
01015         assert( pNode );
01016         assert( !Dsd_IsComplement( pNode ) );
01017         assert( pNode->Type == DSD_NODE_PRIME );
01018 
01019         // transform the function of this block to depend on inputs
01020         // corresponding to the formal inputs
01021 
01022         // first, substitute those inputs that have some blocks associated with them
01023         // second, remap the inputs to the top of the manager (then, it is easy to output them)
01024 
01025         // start the function
01026         bNewFunc = pNode->G;  Cudd_Ref( bNewFunc );
01027         // go over all primary inputs
01028         for ( i = 0; i < pNode->nDecs; i++ )
01029         if ( pNode->pDecs[i]->Type != DSD_NODE_BUF ) // remap only if it is not the buffer
01030         {
01031                 bCube0 = Extra_bddFindOneCube( dd, Cudd_Not(pNode->pDecs[i]->G) );  Cudd_Ref( bCube0 );
01032                 bCof0 = Cudd_Cofactor( dd, bNewFunc, bCube0 );                     Cudd_Ref( bCof0 );
01033                 Cudd_RecursiveDeref( dd, bCube0 );
01034 
01035                 bCube1 = Extra_bddFindOneCube( dd,          pNode->pDecs[i]->G  );  Cudd_Ref( bCube1 );
01036                 bCof1 = Cudd_Cofactor( dd, bNewFunc, bCube1 );                     Cudd_Ref( bCof1 );
01037                 Cudd_RecursiveDeref( dd, bCube1 );
01038 
01039                 Cudd_RecursiveDeref( dd, bNewFunc );
01040 
01041                 // use the variable in the i-th level of the manager
01042 //              bNewFunc = Cudd_bddIte( dd, dd->vars[dd->invperm[i]],bCof1,bCof0 );     Cudd_Ref( bNewFunc );
01043                 // use the first variale in the support of the component
01044                 bNewFunc = Cudd_bddIte( dd, dd->vars[pNode->pDecs[i]->S->index],bCof1,bCof0 );     Cudd_Ref( bNewFunc );
01045                 Cudd_RecursiveDeref( dd, bCof0 );
01046                 Cudd_RecursiveDeref( dd, bCof1 );
01047         }
01048 
01049         if ( fRemap )
01050         {
01051                 // remap the function to the top of the manager
01052                 // remap the function to the first variables of the manager
01053                 for ( i = 0; i < pNode->nDecs; i++ )
01054         //              Permute[ pNode->pDecs[i]->S->index ] = dd->invperm[i];
01055                         Permute[ pNode->pDecs[i]->S->index ] = i;
01056 
01057                 bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, Permute );   Cudd_Ref( bNewFunc );
01058                 Cudd_RecursiveDeref( dd, bTemp );
01059         }
01060 
01061         Cudd_Deref( bNewFunc );
01062         return bNewFunc;
01063 }

Dsd_Node_t* Dsd_TreeNodeCreate ( int  Type,
int  nDecs,
int  BlockNum 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Create the DSD node.]

Description []

SideEffects []

SeeAlso []

Definition at line 61 of file dsdTree.c.

00062 {
00063         // allocate memory for this node 
00064         Dsd_Node_t * p = (Dsd_Node_t *) malloc( sizeof(Dsd_Node_t) );
00065         memset( p, 0, sizeof(Dsd_Node_t) );
00066         p->Type       = Type;       // the type of this block
00067         p->nDecs      = nDecs;      // the number of decompositions
00068         if ( p->nDecs )
00069         {
00070                 p->pDecs      = (Dsd_Node_t **) malloc( p->nDecs * sizeof(Dsd_Node_t *) );
00071                 p->pDecs[0]   = NULL;
00072         }
00073         return p;
00074 }

void Dsd_TreeNodeDelete ( DdManager *  dd,
Dsd_Node_t *  pNode 
)

Function*************************************************************

Synopsis [Frees the DSD node.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file dsdTree.c.

00088 {
00089         if ( pNode->G )  Cudd_RecursiveDeref( dd, pNode->G );
00090         if ( pNode->S )  Cudd_RecursiveDeref( dd, pNode->S );
00091         FREE( pNode->pDecs );
00092         FREE( pNode );
00093 }

void Dsd_TreeUnmark ( Dsd_Manager_t *  pDsdMan  ) 

Function*************************************************************

Synopsis [Unmarks the decomposition tree.]

Description [This function assumes that originally pNode->nVisits are set to zero!]

SideEffects []

SeeAlso []

Definition at line 107 of file dsdTree.c.

00108 {
00109         int i;
00110         for ( i = 0; i < pDsdMan->nRoots; i++ )
00111                 Dsd_TreeUnmark_rec( Dsd_Regular( pDsdMan->pRoots[i] ) );
00112 }

Generated on Tue Jan 5 12:18:58 2010 for abc70930 by  doxygen 1.6.1