abc/src/bdd/cudd/cuddTable.c
/**Function********************************************************************

  Synopsis    [Checks the unique table for the existence of an internal
  ZDD node.]

  Description [Checks the unique table for the existence of an internal
  ZDD node. If it does not exist, it creates a new one.  Does not
  modify the reference count of whatever is returned.  A newly created
  internal node comes back with a reference count 0.  For a newly
  created node, increments the reference counts of what T and E point
  to.  Returns a pointer to the new node if successful; NULL if memory
  is exhausted or if reordering took place.]

  SideEffects [None]

  SeeAlso     [cuddUniqueInter]

******************************************************************************/
Function
Synopsis    [Checks the unique table for the existence of an internal
ZDD node.]

Description [Checks the unique table for the existence of an internal
ZDD node. If it does not exist, it creates a new one.  Does not
modify the reference count of whatever is returned.  A newly created
internal node comes back with a reference count 0.  For a newly
created node, increments the reference counts of what T and E point
to.  Returns a pointer to the new node if successful; NULL if memory
is exhausted or if reordering took place.]




Function Synopsis [ Checks the unique table for the existence of an internal ZDD node . ] Description [ Checks the unique table for the existence of an internal ZDD node . If it does not exist it creates a new one . Does not modify the reference count of whatever is returned . A newly created internal node comes back with a reference count 0 . For a newly created node increments the reference counts of what T and E point to . Returns a pointer to the new node if successful ; NULL if memory is exhausted or if reordering took place . ]
DdNode *
cuddUniqueInterZdd(
  DdManager * unique,
  int  index,
  DdNode * T,
  DdNode * E)
{
    int pos;
    unsigned int level;
    int retval;
    DdNodePtr *nodelist;
    DdNode *looking;
    DdSubtable *subtable;
#ifdef DD_UNIQUE_PROFILE
    unique->uniqueLookUps++;
#endif
    if (index >= unique->sizeZ) {
        if (!cuddResizeTableZdd(unique,index)) return(NULL);
    }
    level = unique->permZ[index];
    subtable = &(unique->subtableZ[level]);
#ifdef DD_DEBUG
    assert(level < (unsigned) cuddIZ(unique,T->index));
    assert(level < (unsigned) cuddIZ(unique,Cudd_Regular(E)->index));
#endif
    if (subtable->keys > subtable->maxKeys) {
        if (unique->gcEnabled && ((unique->deadZ > unique->minDead) ||
        (10 * subtable->dead > 9 * subtable->keys))) {  
            (void) cuddGarbageCollect(unique,1);
        } else {
            ddRehashZdd(unique,(int)level);
        }
    }
    pos = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift);
    nodelist = subtable->nodelist;
    looking = nodelist[pos];
    while (looking != NULL) {
        if (cuddT(looking) == T && cuddE(looking) == E) {
            if (looking->ref == 0) {
                cuddReclaimZdd(unique,looking);
            }
            return(looking);
        }
        looking = looking->next;
#ifdef DD_UNIQUE_PROFILE
        unique->uniqueLinks++;
#endif
    }
    if (unique->autoDynZ &&
    unique->keysZ - (unique->deadZ & unique->countDead) >= unique->nextDyn) {
#ifdef DD_DEBUG
        retval = Cudd_DebugCheck(unique);
        if (retval != 0) return(NULL);
        retval = Cudd_CheckKeys(unique);
        if (retval != 0) return(NULL);
#endif
        retval = Cudd_zddReduceHeap(unique,unique->autoMethodZ,10); 
        if (retval == 0) unique->reordered = 2;
#ifdef DD_DEBUG
        retval = Cudd_DebugCheck(unique);
        if (retval != 0) unique->reordered = 2;
        retval = Cudd_CheckKeys(unique);
        if (retval != 0) unique->reordered = 2;
#endif
        return(NULL);
    }
    unique->keysZ++;
    subtable->keys++;
    looking = cuddAllocNode(unique);
    if (looking == NULL) return(NULL);
    looking->index = index;
    cuddT(looking) = T;
    cuddE(looking) = E;
    looking->next = nodelist[pos];
    nodelist[pos] = looking;
    cuddRef(T);
    cuddRef(E);
    return(looking);
}
DdNode * cuddUniqueInterZdd ( DdManager * unique , int index , DdNode * T , DdNode * E ) { int pos ; unsigned int level ; int retval ; DdNodePtr * nodelist ; DdNode * looking ; DdSubtable * subtable ; #ifdef DD_UNIQUE_PROFILE unique -> uniqueLookUps ++ ; #endif if ( index >= unique -> sizeZ ) { if ( ! cuddResizeTableZdd ( unique , index ) ) return ( NULL ) ; } level = unique -> permZ [ index ] ; subtable = & ( unique -> subtableZ [ level ] ) ; #ifdef DD_DEBUG assert ( level < ( unsigned ) cuddIZ ( unique , T -> index ) ) ; assert ( level < ( unsigned ) cuddIZ ( unique , Cudd_Regular ( E ) -> index ) ) ; #endif if ( subtable -> keys > subtable -> maxKeys ) { if ( unique -> gcEnabled && ( ( unique -> deadZ > unique -> minDead ) || ( 10 * subtable -> dead > 9 * subtable -> keys ) ) ) { ( void ) cuddGarbageCollect ( unique , 1 ) ; } else { ddRehashZdd ( unique , ( int ) level ) ; } } pos = ddHash ( cuddF2L ( T ) , cuddF2L ( E ) , subtable -> shift ) ; nodelist = subtable -> nodelist ; looking = nodelist [ pos ] ; while ( looking != NULL ) { if ( cuddT ( looking ) == T && cuddE ( looking ) == E ) { if ( looking -> ref == 0 ) { cuddReclaimZdd ( unique , looking ) ; } return ( looking ) ; } looking = looking -> next ; #ifdef DD_UNIQUE_PROFILE unique -> uniqueLinks ++ ; #endif } if ( unique -> autoDynZ && unique -> keysZ - ( unique -> deadZ & unique -> countDead ) >= unique -> nextDyn ) { #ifdef DD_DEBUG retval = Cudd_DebugCheck ( unique ) ; if ( retval != 0 ) return ( NULL ) ; retval = Cudd_CheckKeys ( unique ) ; if ( retval != 0 ) return ( NULL ) ; #endif retval = Cudd_zddReduceHeap ( unique , unique -> autoMethodZ , 10 ) ; if ( retval == 0 ) unique -> reordered = 2 ; #ifdef DD_DEBUG retval = Cudd_DebugCheck ( unique ) ; if ( retval != 0 ) unique -> reordered = 2 ; retval = Cudd_CheckKeys ( unique ) ; if ( retval != 0 ) unique -> reordered = 2 ; #endif return ( NULL ) ; } unique -> keysZ ++ ; subtable -> keys ++ ; looking = cuddAllocNode ( unique ) ; if ( looking == NULL ) return ( NULL ) ; looking -> index = index ; cuddT ( looking ) = T ; cuddE ( looking ) = E ; looking -> next = nodelist [ pos ] ; nodelist [ pos ] = looking ; cuddRef ( T ) ; cuddRef ( E ) ; return ( looking ) ; }
Function
Synopsis    [Checks the unique table for the existence of an internal
ZDD node.]
Function Synopsis [ Checks the unique table for the existence of an internal ZDD node . ]
/* too many dead */ /* countDead is 0 if deads should be counted and ~0 if they should not. */ /* 10 = whatever */