diff options
Diffstat (limited to 'abc70930/src/bdd/dsd/dsdMan.c')
| -rw-r--r-- | abc70930/src/bdd/dsd/dsdMan.c | 114 |
1 files changed, 114 insertions, 0 deletions
diff --git a/abc70930/src/bdd/dsd/dsdMan.c b/abc70930/src/bdd/dsd/dsdMan.c new file mode 100644 index 00000000..6e43f0f4 --- /dev/null +++ b/abc70930/src/bdd/dsd/dsdMan.c @@ -0,0 +1,114 @@ +/**CFile**************************************************************** + + FileName [dsdMan.c] + + PackageName [DSD: Disjoint-support decomposition package.] + + Synopsis [APIs of the DSD manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 8.0. Started - September 22, 2003.] + + Revision [$Id: dsdMan.c,v 1.0 2002/22/09 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dsdInt.h" + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// API OF DSD MANAGER /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the DSD manager.] + + Description [Takes the started BDD manager and the maximum support size + of the function to be DSD-decomposed. The manager should have at least as + many variables as there are variables in the support. The functions should + be expressed using the first nSuppSizeMax variables in the manager (these + may be ordered not necessarily on top of the manager).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose ) +{ + Dsd_Manager_t * dMan; + Dsd_Node_t * pNode; + int i; + + assert( nSuppMax <= dd->size ); + + dMan = ALLOC( Dsd_Manager_t, 1 ); + memset( dMan, 0, sizeof(Dsd_Manager_t) ); + dMan->dd = dd; + dMan->nInputs = nSuppMax; + dMan->fVerbose = fVerbose; + dMan->nRoots = 0; + dMan->nRootsAlloc = 50; + dMan->pRoots = (Dsd_Node_t **) malloc( dMan->nRootsAlloc * sizeof(Dsd_Node_t *) ); + dMan->pInputs = (Dsd_Node_t **) malloc( dMan->nInputs * sizeof(Dsd_Node_t *) ); + + // create the primary inputs and insert them into the table + dMan->Table = st_init_table(st_ptrcmp, st_ptrhash); + for ( i = 0; i < dMan->nInputs; i++ ) + { + pNode = Dsd_TreeNodeCreate( DSD_NODE_BUF, 1, 0 ); + pNode->G = dd->vars[i]; Cudd_Ref( pNode->G ); + pNode->S = dd->vars[i]; Cudd_Ref( pNode->S ); + st_insert( dMan->Table, (char*)dd->vars[i], (char*)pNode ); + dMan->pInputs[i] = pNode; + } + pNode = Dsd_TreeNodeCreate( DSD_NODE_CONST1, 0, 0 ); + pNode->G = b1; Cudd_Ref( pNode->G ); + pNode->S = b1; Cudd_Ref( pNode->S ); + st_insert( dMan->Table, (char*)b1, (char*)pNode ); + dMan->pConst1 = pNode; + + Dsd_CheckCacheAllocate( 5000 ); + return dMan; +} + +/**Function************************************************************* + + Synopsis [Stops the DSD manager.] + + Description [Stopping the DSD manager automatically derefereces and + deallocates all the DSD nodes that were created during the life time + of the DSD manager. As a result, the user does not need to deref or + deallocate any DSD nodes or trees that are derived and placed in + the manager while it exists.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dsd_ManagerStop( Dsd_Manager_t * dMan ) +{ + st_generator * gen; + Dsd_Node_t * pNode; + DdNode * bFunc; + // delete the nodes + st_foreach_item( dMan->Table, gen, (char**)&bFunc, (char**)&pNode ) + Dsd_TreeNodeDelete( dMan->dd, Dsd_Regular(pNode) ); + st_free_table(dMan->Table); + free( dMan->pInputs ); + free( dMan->pRoots ); + free( dMan ); + Dsd_CheckCacheDeallocate(); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// |