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

  Synopsis    [Performs the recursive step of addScalarInverse.]

  Description [Returns a pointer to the resulting ADD in case of
  success. Returns NULL if any discriminants smaller than epsilon is
  encountered.]

  SideEffects [None]

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

Description [Returns a pointer to the resulting ADD in case of
success. Returns NULL if any discriminants smaller than epsilon is
encountered.]


Function Synopsis [ Performs the recursive step of addScalarInverse . ] Description [ Returns a pointer to the resulting ADD in case of success . Returns NULL if any discriminants smaller than epsilon is encountered . ]
DdNode *
cuddAddScalarInverseRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * epsilon)
{
    DdNode *t, *e, *res;
    CUDD_VALUE_TYPE value;
    statLine(dd);
    if (cuddIsConstant(f)) {
        if (ddAbs(cuddV(f)) < cuddV(epsilon)) return(NULL);
        value = 1.0 / cuddV(f);
        res = cuddUniqueConst(dd,value);
        return(res);
    }
    res = cuddCacheLookup2(dd,Cudd_addScalarInverse,f,epsilon);
    if (res != NULL) return(res);
    t = cuddAddScalarInverseRecur(dd,cuddT(f),epsilon);
    if (t == NULL) return(NULL);
    cuddRef(t);
    e = cuddAddScalarInverseRecur(dd,cuddE(f),epsilon);
    if (e == NULL) {
        Cudd_RecursiveDeref(dd, t);
        return(NULL);
    }
    cuddRef(e);
    res = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
    if (res == NULL) {
        Cudd_RecursiveDeref(dd, t);
        Cudd_RecursiveDeref(dd, e);
        return(NULL);
    }
    cuddDeref(t);
    cuddDeref(e);
    cuddCacheInsert2(dd,Cudd_addScalarInverse,f,epsilon,res);
    return(res);
}
DdNode * cuddAddScalarInverseRecur ( DdManager * dd , DdNode * f , DdNode * epsilon ) { DdNode * t , * e , * res ; CUDD_VALUE_TYPE value ; statLine ( dd ) ; if ( cuddIsConstant ( f ) ) { if ( ddAbs ( cuddV ( f ) ) < cuddV ( epsilon ) ) return ( NULL ) ; value = 1.0 / cuddV ( f ) ; res = cuddUniqueConst ( dd , value ) ; return ( res ) ; } res = cuddCacheLookup2 ( dd , Cudd_addScalarInverse , f , epsilon ) ; if ( res != NULL ) return ( res ) ; t = cuddAddScalarInverseRecur ( dd , cuddT ( f ) , epsilon ) ; if ( t == NULL ) return ( NULL ) ; cuddRef ( t ) ; e = cuddAddScalarInverseRecur ( dd , cuddE ( f ) , epsilon ) ; if ( e == NULL ) { Cudd_RecursiveDeref ( dd , t ) ; return ( NULL ) ; } cuddRef ( e ) ; res = ( t == e ) ? t : cuddUniqueInter ( dd , ( int ) f -> index , t , e ) ; if ( res == NULL ) { Cudd_RecursiveDeref ( dd , t ) ; Cudd_RecursiveDeref ( dd , e ) ; return ( NULL ) ; } cuddDeref ( t ) ; cuddDeref ( e ) ; cuddCacheInsert2 ( dd , Cudd_addScalarInverse , f , epsilon , res ) ; return ( res ) ; }
Function
Synopsis    [Performs the recursive step of addScalarInverse.]
Function Synopsis [ Performs the recursive step of addScalarInverse . ]