src/bdd/dsd/dsdMan.c

Go to the documentation of this file.

#include "dsdInt.h"



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;
}

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();
}

---