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

  Synopsis    [Performs safe minimization of a BDD.]

  Description [Performs safe minimization of a BDD. Given the BDD
  <code>f</code> of a function to be minimized and a BDD
  <code>c</code> representing the care set, Cudd_bddLICompaction
  produces the BDD of a function that agrees with <code>f</code>
  wherever <code>c</code> is 1.  Safe minimization means that the size
  of the result is guaranteed not to exceed the size of
  <code>f</code>. This function is based on the DAC97 paper by Hong et
  al..  Returns a pointer to the result if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddLICompaction]

******************************************************************************/
Function
Synopsis    [Performs safe minimization of a BDD.]

Description [Performs safe minimization of a BDD. Given the BDD
f of a function to be minimized and a BDD
c representing the care set, Cudd_bddLICompaction
produces the BDD of a function that agrees with f
wherever c is 1.  Safe minimization means that the size
of the result is guaranteed not to exceed the size of
f. This function is based on the DAC97 paper by Hong et
al..  Returns a pointer to the result if successful; NULL
otherwise.]




Function Synopsis [ Performs safe minimization of a BDD . ] Description [ Performs safe minimization of a BDD . Given the BDD f of a function to be minimized and a BDD c representing the care set Cudd_bddLICompaction produces the BDD of a function that agrees with f wherever c is 1 . Safe minimization means that the size of the result is guaranteed not to exceed the size of f . This function is based on the DAC97 paper by Hong et al .. Returns a pointer to the result if successful ; NULL otherwise . ]
DdNode *
cuddBddLICompaction(
  DdManager * dd ,
  DdNode * f ,
  DdNode * c )
{
    st__table *marktable, *markcache, *buildcache;
    DdNode *res, *zero;
    zero = Cudd_Not(DD_ONE(dd));
    if (c == zero) return(zero);
    marktable = st__init_table( st__ptrcmp, st__ptrhash);
    if (marktable == NULL) {
        return(NULL);
    }
    markcache = st__init_table(MarkCacheCompare,MarkCacheHash);
    if (markcache == NULL) {
        st__free_table(marktable);
        return(NULL);
    }
    if (cuddBddLICMarkEdges(dd,f,c,marktable,markcache) == CUDD_OUT_OF_MEM) {
        st__foreach(markcache, MarkCacheCleanUp, NULL);
        st__free_table(marktable);
        st__free_table(markcache);
        return(NULL);
    }
    st__foreach(markcache, MarkCacheCleanUp, NULL);
    st__free_table(markcache);
    buildcache = st__init_table( st__ptrcmp, st__ptrhash);
    if (buildcache == NULL) {
        st__free_table(marktable);
        return(NULL);
    }
    res = cuddBddLICBuildResult(dd,f,buildcache,marktable);
    st__free_table(buildcache);
    st__free_table(marktable);
    return(res);
}
DdNode * cuddBddLICompaction ( DdManager * dd , DdNode * f , DdNode * c ) { st__table * marktable , * markcache , * buildcache ; DdNode * res , * zero ; zero = Cudd_Not ( DD_ONE ( dd ) ) ; if ( c == zero ) return ( zero ) ; marktable = st__init_table ( st__ptrcmp , st__ptrhash ) ; if ( marktable == NULL ) { return ( NULL ) ; } markcache = st__init_table ( MarkCacheCompare , MarkCacheHash ) ; if ( markcache == NULL ) { st__free_table ( marktable ) ; return ( NULL ) ; } if ( cuddBddLICMarkEdges ( dd , f , c , marktable , markcache ) == CUDD_OUT_OF_MEM ) { st__foreach ( markcache , MarkCacheCleanUp , NULL ) ; st__free_table ( marktable ) ; st__free_table ( markcache ) ; return ( NULL ) ; } st__foreach ( markcache , MarkCacheCleanUp , NULL ) ; st__free_table ( markcache ) ; buildcache = st__init_table ( st__ptrcmp , st__ptrhash ) ; if ( buildcache == NULL ) { st__free_table ( marktable ) ; return ( NULL ) ; } res = cuddBddLICBuildResult ( dd , f , buildcache , marktable ) ; st__free_table ( buildcache ) ; st__free_table ( marktable ) ; return ( res ) ; }
Function
Synopsis    [Performs safe minimization of a BDD.]
Function Synopsis [ Performs safe minimization of a BDD . ]
/* manager */ /* function to be minimized */ /* constraint (care set) */ /* We need to use local caches for both steps of this operation.
    ** The results of the edge marking step are only valid as long as the
    ** edge markings themselves are available. However, the edge markings
    ** are lost at the end of one invocation of Cudd_bddLICompaction.
    ** Hence, the cache entries for the edge marking step must be
    ** invalidated at the end of this function.
    ** For the result of the building step we argue as follows. The result
    ** for a node and a given constrain depends on the BDD in which the node
    ** appears. Hence, the same node and constrain may give different results
    ** in successive invocations.
    */