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

  Synopsis    [Performs the recursive step of Cudd_DumpFactoredForm.]

  Description [Performs the recursive step of
  Cudd_DumpFactoredForm. Traverses the BDD f and writes a factored
  form for each node to the file pointed by fp in terms of the
  factored forms of the children. Constants are propagated, and
  absorption is applied.  f is assumed to be a regular pointer and
  ddDoDumpFActoredForm guarantees this assumption in the recursive
  calls.]

  SideEffects [None]

  SeeAlso     [Cudd_DumpFactoredForm]

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

Description [Performs the recursive step of
Cudd_DumpFactoredForm. Traverses the BDD f and writes a factored
form for each node to the file pointed by fp in terms of the
factored forms of the children. Constants are propagated, and
absorption is applied.  f is assumed to be a regular pointer and
ddDoDumpFActoredForm guarantees this assumption in the recursive
calls.]




Function Synopsis [ Performs the recursive step of Cudd_DumpFactoredForm . ] Description [ Performs the recursive step of Cudd_DumpFactoredForm . Traverses the BDD f and writes a factored form for each node to the file pointed by fp in terms of the factored forms of the children . Constants are propagated and absorption is applied . f is assumed to be a regular pointer and ddDoDumpFActoredForm guarantees this assumption in the recursive calls . ]
static int
ddDoDumpFactoredForm(
  DdManager * dd,
  DdNode * f,
  FILE * fp,
  char ** names)
{
    DdNode      *T, *E;
    int         retval;
#ifdef DD_DEBUG
    assert(!Cudd_IsComplement(f));
    assert(!Cudd_IsConstant(f));
#endif
    if (f == NULL)
        return(0);
    T = cuddT(f);
    E = cuddE(f);
    if (T != DD_ZERO(dd)) {
        if (E != DD_ONE(dd)) {
            if (names != NULL) {
                retval = fprintf(fp, "%s", names[f->index]);
            } else {
#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
                retval = fprintf(fp, "x%u", f->index);
#else
                retval = fprintf(fp, "x%hu", f->index);
#endif
            }
            if (retval == EOF) return(0);
        }
        if (T != DD_ONE(dd)) {
            retval = fprintf(fp, "%s(", E != DD_ONE(dd) ? " * " : "");
            if (retval == EOF) return(0);
            retval = ddDoDumpFactoredForm(dd,T,fp,names);
            if (retval != 1) return(retval);
            retval = fprintf(fp, ")");
            if (retval == EOF) return(0);
        }
        if (E == Cudd_Not(DD_ONE(dd)) || E == DD_ZERO(dd)) return(1);
        retval = fprintf(fp, " + ");
        if (retval == EOF) return(0);
    }
    E = Cudd_Regular(E);
    if (T != DD_ONE(dd)) {
        if (names != NULL) {
            retval = fprintf(fp, "!%s", names[f->index]);
        } else {
#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
            retval = fprintf(fp, "!x%u", f->index);
#else
            retval = fprintf(fp, "!x%hu", f->index);
#endif
        }
        if (retval == EOF) return(0);
    }
    if (E != DD_ONE(dd)) {
        retval = fprintf(fp, "%s%s(", T != DD_ONE(dd) ? " * " : "",
                         E != cuddE(f) ? "!" : "");
        if (retval == EOF) return(0);
        retval = ddDoDumpFactoredForm(dd,E,fp,names);
        if (retval != 1) return(retval);
        retval = fprintf(fp, ")");
        if (retval == EOF) return(0);
    }
    return(1);
}
static int ddDoDumpFactoredForm ( DdManager * dd , DdNode * f , FILE * fp , char * * names ) { DdNode * T , * E ; int retval ; #ifdef DD_DEBUG assert ( ! Cudd_IsComplement ( f ) ) ; assert ( ! Cudd_IsConstant ( f ) ) ; #endif if ( f == NULL ) return ( 0 ) ; T = cuddT ( f ) ; E = cuddE ( f ) ; if ( T != DD_ZERO ( dd ) ) { if ( E != DD_ONE ( dd ) ) { if ( names != NULL ) { retval = fprintf ( fp , " " , names [ f -> index ] ) ; } else { #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 retval = fprintf ( fp , " " , f -> index ) ; #else retval = fprintf ( fp , " " , f -> index ) ; #endif } if ( retval == EOF ) return ( 0 ) ; } if ( T != DD_ONE ( dd ) ) { retval = fprintf ( fp , " " , E != DD_ONE ( dd ) ? " " : " " ) ; if ( retval == EOF ) return ( 0 ) ; retval = ddDoDumpFactoredForm ( dd , T , fp , names ) ; if ( retval != 1 ) return ( retval ) ; retval = fprintf ( fp , " " ) ; if ( retval == EOF ) return ( 0 ) ; } if ( E == Cudd_Not ( DD_ONE ( dd ) ) || E == DD_ZERO ( dd ) ) return ( 1 ) ; retval = fprintf ( fp , " " ) ; if ( retval == EOF ) return ( 0 ) ; } E = Cudd_Regular ( E ) ; if ( T != DD_ONE ( dd ) ) { if ( names != NULL ) { retval = fprintf ( fp , " " , names [ f -> index ] ) ; } else { #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 retval = fprintf ( fp , " " , f -> index ) ; #else retval = fprintf ( fp , " " , f -> index ) ; #endif } if ( retval == EOF ) return ( 0 ) ; } if ( E != DD_ONE ( dd ) ) { retval = fprintf ( fp , " " , T != DD_ONE ( dd ) ? " " : " " , E != cuddE ( f ) ? " " : " " ) ; if ( retval == EOF ) return ( 0 ) ; retval = ddDoDumpFactoredForm ( dd , E , fp , names ) ; if ( retval != 1 ) return ( retval ) ; retval = fprintf ( fp , " " ) ; if ( retval == EOF ) return ( 0 ) ; } return ( 1 ) ; }
Function
Synopsis    [Performs the recursive step of Cudd_DumpFactoredForm.]
Function Synopsis [ Performs the recursive step of Cudd_DumpFactoredForm . ]
/* Check for abnormal condition that should never happen. */ /* Recursive calls. */