abc/src/bool/kit/cloud.c
/**Function********************************************************************

  Synopsis    [Returns or creates a new node]

  Description [Checks the unique table for the existance of the node. If the node is 
  present, returns the node. If the node is absent, creates a new node.]
               
  SideEffects []

  SeeAlso     []

******************************************************************************/
Function
Synopsis    [Returns or creates a new node]

Description [Checks the unique table for the existance of the node. If the node is
present, returns the node. If the node is absent, creates a new node.]




Function Synopsis [ Returns or creates a new node ] Description [ Checks the unique table for the existance of the node . If the node is present returns the node . If the node is absent creates a new node . ]
CloudNode * cloudMakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e )
{
    CloudNode * entryUnique;
    CLOUD_ASSERT(t); 
    CLOUD_ASSERT(e);
    assert( ((int)v) >= 0 && ((int)v) < dd->nVars );  
    assert( v < Cloud_V(t) && v < Cloud_V(e) );       
    assert( !Cloud_IsComplement(t) );                 
    assert( t && e );
    entryUnique = dd->tUnique + cloudHashCudd3(v, t, e, dd->shiftUnique);
    while ( entryUnique->s == dd->nSignCur )
    {
        if ( entryUnique->v == v && entryUnique->t == t && entryUnique->e == e )
        { 
            dd->nUniqueHits++;
            return entryUnique;  
        }
        if ( ++entryUnique - dd->tUnique == dd->nNodesAlloc )
            entryUnique = dd->tUnique + 1;
        dd->nUniqueSteps++;
    }
    dd->nUniqueMisses++;
    if ( ++dd->nNodesCur == dd->nNodesLimit ) 
    { 
        printf( "Cloud needs restart!\n" );
        return NULL;
    }
    entryUnique->s   = dd->nSignCur;
    entryUnique->v   = v;
    entryUnique->t   = t;
    entryUnique->e   = e;
    return entryUnique;  
}
CloudNode * cloudMakeNode ( CloudManager * dd , CloudVar v , CloudNode * t , CloudNode * e ) { CloudNode * entryUnique ; CLOUD_ASSERT ( t ) ; CLOUD_ASSERT ( e ) ; assert ( ( ( int ) v ) >= 0 && ( ( int ) v ) < dd -> nVars ) ; assert ( v < Cloud_V ( t ) && v < Cloud_V ( e ) ) ; assert ( ! Cloud_IsComplement ( t ) ) ; assert ( t && e ) ; entryUnique = dd -> tUnique + cloudHashCudd3 ( v , t , e , dd -> shiftUnique ) ; while ( entryUnique -> s == dd -> nSignCur ) { if ( entryUnique -> v == v && entryUnique -> t == t && entryUnique -> e == e ) { dd -> nUniqueHits ++ ; return entryUnique ; } if ( ++ entryUnique - dd -> tUnique == dd -> nNodesAlloc ) entryUnique = dd -> tUnique + 1 ; dd -> nUniqueSteps ++ ; } dd -> nUniqueMisses ++ ; if ( ++ dd -> nNodesCur == dd -> nNodesLimit ) { printf ( " \n " ) ; return NULL ; } entryUnique -> s = dd -> nSignCur ; entryUnique -> v = v ; entryUnique -> t = t ; entryUnique -> e = e ; return entryUnique ; }
Function
Synopsis    [Returns or creates a new node]
Function Synopsis [ Returns or creates a new node ]
// the variable must be in the range // variable should be above in the order // the THEN edge must not be complemented // make sure we are not searching for the constant node // get the unique entry // compare the node // the node is found // returns the node // increment the hash value modulus the hash table size // increment the number of steps through the table // check if the new node can be created // initiate the restart //        fflush( stdout ); //        exit(1); // create the node // returns the node