abc/src/bdd/extrab/extraBddTime.c
/**Function********************************************************************

  Synopsis    [Performs the recursive step of Extra_TransferPermute.]

  Description [Performs the recursive step of Extra_TransferPermute.
  Returns a pointer to the result if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [extraTransferPermuteTime]

******************************************************************************/
Function
Synopsis    [Performs the recursive step of Extra_TransferPermute.]

Description [Performs the recursive step of Extra_TransferPermute.
Returns a pointer to the result if successful; NULL otherwise.]




Function Synopsis [ Performs the recursive step of Extra_TransferPermute . ] Description [ Performs the recursive step of Extra_TransferPermute . Returns a pointer to the result if successful ; NULL otherwise . ]
static DdNode * 
extraTransferPermuteRecurTime( 
  DdManager * ddS, 
  DdManager * ddD, 
  DdNode * f, 
  st__table * table, 
  int * Permute,
  int TimeOut )
{
    DdNode *ft, *fe, *t, *e, *var, *res;
    DdNode *one, *zero;
    int index;
    int comple = 0;
    statLine( ddD );
    one = DD_ONE( ddD );
    comple = Cudd_IsComplement( f );
    if ( Cudd_IsConstant( f ) )
        return ( Cudd_NotCond( one, comple ) );
    f = Cudd_NotCond( f, comple );
    if ( st__lookup( table, ( char * ) f, ( char ** ) &res ) )
        return ( Cudd_NotCond( res, comple ) );
    if ( TimeOut && Abc_Clock() > TimeOut )
        return NULL;
    if ( Permute )
        index = Permute[f->index];
    else
        index = f->index;
    ft = cuddT( f );
    fe = cuddE( f );
    t = extraTransferPermuteRecurTime( ddS, ddD, ft, table, Permute, TimeOut );
    if ( t == NULL )
    {
        return ( NULL );
    }
    cuddRef( t );
    e = extraTransferPermuteRecurTime( ddS, ddD, fe, table, Permute, TimeOut );
    if ( e == NULL )
    {
        Cudd_RecursiveDeref( ddD, t );
        return ( NULL );
    }
    cuddRef( e );
    zero = Cudd_Not(ddD->one);
    var = cuddUniqueInter( ddD, index, one, zero );
    if ( var == NULL )
    {
        Cudd_RecursiveDeref( ddD, t );
        Cudd_RecursiveDeref( ddD, e );
        return ( NULL );
    }
    res = cuddBddIteRecur( ddD, var, t, e );
    if ( res == NULL )
    {
        Cudd_RecursiveDeref( ddD, t );
        Cudd_RecursiveDeref( ddD, e );
        return ( NULL );
    }
    cuddRef( res );
    Cudd_RecursiveDeref( ddD, t );
    Cudd_RecursiveDeref( ddD, e );
    if ( st__add_direct( table, ( char * ) f, ( char * ) res ) ==
         st__OUT_OF_MEM )
    {
        Cudd_RecursiveDeref( ddD, res );
        return ( NULL );
    }
    return ( Cudd_NotCond( res, comple ) );
}
static DdNode * extraTransferPermuteRecurTime ( DdManager * ddS , DdManager * ddD , DdNode * f , st__table * table , int * Permute , int TimeOut ) { DdNode * ft , * fe , * t , * e , * var , * res ; DdNode * one , * zero ; int index ; int comple = 0 ; statLine ( ddD ) ; one = DD_ONE ( ddD ) ; comple = Cudd_IsComplement ( f ) ; if ( Cudd_IsConstant ( f ) ) return ( Cudd_NotCond ( one , comple ) ) ; f = Cudd_NotCond ( f , comple ) ; if ( st__lookup ( table , ( char * ) f , ( char * * ) & res ) ) return ( Cudd_NotCond ( res , comple ) ) ; if ( TimeOut && Abc_Clock ( ) > TimeOut ) return NULL ; if ( Permute ) index = Permute [ f -> index ] ; else index = f -> index ; ft = cuddT ( f ) ; fe = cuddE ( f ) ; t = extraTransferPermuteRecurTime ( ddS , ddD , ft , table , Permute , TimeOut ) ; if ( t == NULL ) { return ( NULL ) ; } cuddRef ( t ) ; e = extraTransferPermuteRecurTime ( ddS , ddD , fe , table , Permute , TimeOut ) ; if ( e == NULL ) { Cudd_RecursiveDeref ( ddD , t ) ; return ( NULL ) ; } cuddRef ( e ) ; zero = Cudd_Not ( ddD -> one ) ; var = cuddUniqueInter ( ddD , index , one , zero ) ; if ( var == NULL ) { Cudd_RecursiveDeref ( ddD , t ) ; Cudd_RecursiveDeref ( ddD , e ) ; return ( NULL ) ; } res = cuddBddIteRecur ( ddD , var , t , e ) ; if ( res == NULL ) { Cudd_RecursiveDeref ( ddD , t ) ; Cudd_RecursiveDeref ( ddD , e ) ; return ( NULL ) ; } cuddRef ( res ) ; Cudd_RecursiveDeref ( ddD , t ) ; Cudd_RecursiveDeref ( ddD , e ) ; if ( st__add_direct ( table , ( char * ) f , ( char * ) res ) == st__OUT_OF_MEM ) { Cudd_RecursiveDeref ( ddD , res ) ; return ( NULL ) ; } return ( Cudd_NotCond ( res , comple ) ) ; }
Function
Synopsis    [Performs the recursive step of Extra_TransferPermute.]
Function Synopsis [ Performs the recursive step of Extra_TransferPermute . ]
/* Trivial cases. */ /* Make canonical to increase the utilization of the cache. */ /* Now f is a regular pointer to a non-constant node. */ /* Check the cache. */ /* Recursive step. */