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

  Synopsis    [Implements the recursive step of Cudd_FindTwoLiteralClauses.]

  Description [Implements the recursive step of
  Cudd_FindTwoLiteralClauses.  The DD node is assumed to be not
  constant.  Returns a pointer to a set of clauses if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_FindTwoLiteralClauses]

******************************************************************************/
Function
Synopsis    [Implements the recursive step of Cudd_FindTwoLiteralClauses.]

Description [Implements the recursive step of
Cudd_FindTwoLiteralClauses.  The DD node is assumed to be not
constant.  Returns a pointer to a set of clauses if successful; NULL
otherwise.]




Function Synopsis [ Implements the recursive step of Cudd_FindTwoLiteralClauses . ] Description [ Implements the recursive step of Cudd_FindTwoLiteralClauses . The DD node is assumed to be not constant . Returns a pointer to a set of clauses if successful ; NULL otherwise . ]
static DdTlcInfo *
ddFindTwoLiteralClausesRecur(
  DdManager * dd,
  DdNode * f,
  st__table *table)
{
    DdNode *T, *E, *F;
    DdNode *one, *lzero, *azero;
    DdTlcInfo *res, *Tres, *Eres;
    DdHalfWord index;
    F = Cudd_Regular(f);
    assert(!cuddIsConstant(F));
    if ( st__lookup(table, (const char *)f, (char **)&res)) {
        return(res);
    }
    one = DD_ONE(dd);
    lzero = Cudd_Not(one);
    azero = DD_ZERO(dd);
    T = cuddT(F); E = cuddE(F);
    if (Cudd_IsComplement(f)) {
        T = Cudd_Not(T); E = Cudd_Not(E);
    }
    index = F->index;
    if (Cudd_IsConstant(T) && T != lzero && T != azero) {
        if (E == lzero || E == azero) {
            res = tlcInfoAlloc();
            if (res == NULL) return(NULL);
            res->vars = ABC_ALLOC(DdHalfWord,4);
            if (res->vars == NULL) {
                ABC_FREE(res);
                return(NULL);
            }
            res->phases = bitVectorAlloc(2);
            if (res->phases == NULL) {
                ABC_FREE(res->vars);
                ABC_FREE(res);
                return(NULL);
            }
            res->vars[0] = index;
            res->vars[1] = CUDD_MAXINDEX;
            res->vars[2] = 0;
            res->vars[3] = 0;
            bitVectorSet(res->phases, 0, 0); 
            bitVectorSet(res->phases, 1, 1); 
        } else if (Cudd_IsConstant(E)) {
            res = emptyClauseSet();
        } else {
            Tres = emptyClauseSet();
            if (Tres == NULL) return(NULL);
            Eres = ddFindTwoLiteralClausesRecur(dd, E, table);
            if (Eres == NULL) {
                Cudd_tlcInfoFree(Tres);
                return(NULL);
            }
            res = computeClauses(Tres, Eres, index, dd->size);
            Cudd_tlcInfoFree(Tres);
        }
    } else if (T == lzero || T == azero) {
        if (Cudd_IsConstant(E)) { 
            res = tlcInfoAlloc();
            if (res == NULL) return(NULL);
            res->vars = ABC_ALLOC(DdHalfWord,4);
            if (res->vars == NULL) {
                ABC_FREE(res);
                return(NULL);
            }
            res->phases = bitVectorAlloc(2);
            if (res->phases == NULL) {
                ABC_FREE(res->vars);
                ABC_FREE(res);
                return(NULL);
            }
            res->vars[0] = index;
            res->vars[1] = CUDD_MAXINDEX;
            res->vars[2] = 0;
            res->vars[3] = 0;
            bitVectorSet(res->phases, 0, 1); 
            bitVectorSet(res->phases, 1, 1); 
        } else { 
            Eres = ddFindTwoLiteralClausesRecur(dd, E, table);
            if (Eres == NULL) return(NULL);
            res = computeClausesWithUniverse(Eres, index, 1);
        }
    } else { 
        Tres = ddFindTwoLiteralClausesRecur(dd, T, table);
        if (Tres == NULL) return(NULL);
        if (Cudd_IsConstant(E)) {
            if (E == lzero || E == azero) {
                res = computeClausesWithUniverse(Tres, index, 0);
            } else {
                Eres = emptyClauseSet();
                if (Eres == NULL) return(NULL);
                res = computeClauses(Tres, Eres, index, dd->size);
                Cudd_tlcInfoFree(Eres);
            }
        } else {
            Eres = ddFindTwoLiteralClausesRecur(dd, E, table);
            if (Eres == NULL) return(NULL);
            res = computeClauses(Tres, Eres, index, dd->size);
        }
    }
    if ( st__add_direct(table, (char *)f, (char *)res) == st__OUT_OF_MEM) {
        ABC_FREE(res);
        return(NULL);
    }
    return(res);
}
static DdTlcInfo * ddFindTwoLiteralClausesRecur ( DdManager * dd , DdNode * f , st__table * table ) { DdNode * T , * E , * F ; DdNode * one , * lzero , * azero ; DdTlcInfo * res , * Tres , * Eres ; DdHalfWord index ; F = Cudd_Regular ( f ) ; assert ( ! cuddIsConstant ( F ) ) ; if ( st__lookup ( table , ( const char * ) f , ( char * * ) & res ) ) { return ( res ) ; } one = DD_ONE ( dd ) ; lzero = Cudd_Not ( one ) ; azero = DD_ZERO ( dd ) ; T = cuddT ( F ) ; E = cuddE ( F ) ; if ( Cudd_IsComplement ( f ) ) { T = Cudd_Not ( T ) ; E = Cudd_Not ( E ) ; } index = F -> index ; if ( Cudd_IsConstant ( T ) && T != lzero && T != azero ) { if ( E == lzero || E == azero ) { res = tlcInfoAlloc ( ) ; if ( res == NULL ) return ( NULL ) ; res -> vars = ABC_ALLOC ( DdHalfWord , 4 ) ; if ( res -> vars == NULL ) { ABC_FREE ( res ) ; return ( NULL ) ; } res -> phases = bitVectorAlloc ( 2 ) ; if ( res -> phases == NULL ) { ABC_FREE ( res -> vars ) ; ABC_FREE ( res ) ; return ( NULL ) ; } res -> vars [ 0 ] = index ; res -> vars [ 1 ] = CUDD_MAXINDEX ; res -> vars [ 2 ] = 0 ; res -> vars [ 3 ] = 0 ; bitVectorSet ( res -> phases , 0 , 0 ) ; bitVectorSet ( res -> phases , 1 , 1 ) ; } else if ( Cudd_IsConstant ( E ) ) { res = emptyClauseSet ( ) ; } else { Tres = emptyClauseSet ( ) ; if ( Tres == NULL ) return ( NULL ) ; Eres = ddFindTwoLiteralClausesRecur ( dd , E , table ) ; if ( Eres == NULL ) { Cudd_tlcInfoFree ( Tres ) ; return ( NULL ) ; } res = computeClauses ( Tres , Eres , index , dd -> size ) ; Cudd_tlcInfoFree ( Tres ) ; } } else if ( T == lzero || T == azero ) { if ( Cudd_IsConstant ( E ) ) { res = tlcInfoAlloc ( ) ; if ( res == NULL ) return ( NULL ) ; res -> vars = ABC_ALLOC ( DdHalfWord , 4 ) ; if ( res -> vars == NULL ) { ABC_FREE ( res ) ; return ( NULL ) ; } res -> phases = bitVectorAlloc ( 2 ) ; if ( res -> phases == NULL ) { ABC_FREE ( res -> vars ) ; ABC_FREE ( res ) ; return ( NULL ) ; } res -> vars [ 0 ] = index ; res -> vars [ 1 ] = CUDD_MAXINDEX ; res -> vars [ 2 ] = 0 ; res -> vars [ 3 ] = 0 ; bitVectorSet ( res -> phases , 0 , 1 ) ; bitVectorSet ( res -> phases , 1 , 1 ) ; } else { Eres = ddFindTwoLiteralClausesRecur ( dd , E , table ) ; if ( Eres == NULL ) return ( NULL ) ; res = computeClausesWithUniverse ( Eres , index , 1 ) ; } } else { Tres = ddFindTwoLiteralClausesRecur ( dd , T , table ) ; if ( Tres == NULL ) return ( NULL ) ; if ( Cudd_IsConstant ( E ) ) { if ( E == lzero || E == azero ) { res = computeClausesWithUniverse ( Tres , index , 0 ) ; } else { Eres = emptyClauseSet ( ) ; if ( Eres == NULL ) return ( NULL ) ; res = computeClauses ( Tres , Eres , index , dd -> size ) ; Cudd_tlcInfoFree ( Eres ) ; } } else { Eres = ddFindTwoLiteralClausesRecur ( dd , E , table ) ; if ( Eres == NULL ) return ( NULL ) ; res = computeClauses ( Tres , Eres , index , dd -> size ) ; } } if ( st__add_direct ( table , ( char * ) f , ( char * ) res ) == st__OUT_OF_MEM ) { ABC_FREE ( res ) ; return ( NULL ) ; } return ( res ) ; }
Function
Synopsis    [Implements the recursive step of Cudd_FindTwoLiteralClauses.]
Function Synopsis [ Implements the recursive step of Cudd_FindTwoLiteralClauses . ]
/* Check computed table.  Separate entries are necessary for
    ** a node and its complement.  We should update the counter here. */ /* Easy access to the constants for BDDs and ADDs. */ /* Find cofactors and variable labeling the top node. */ /* T is a non-zero constant.  If E is zero, then this node's index
        ** is a one-literal clause.  Otherwise, if E is a non-zero
        ** constant, there are no clauses for this node.  Finally,
        ** if E is not constant, we recursively compute its clauses, and then
        ** merge using the empty set for T. */ /* Create the clause (index + 0). */ /* positive phase */ /* negative phase */ /* If E is a non-zero constant, no clauses. */ /* E is non-constant */ /* T is zero.  If E is a non-zero constant, then the
        ** complement of this node's index is a one-literal clause.
        ** Otherwise, if E is not constant, we recursively compute its
        ** clauses, and then merge using the universal set for T. */ /* E cannot be zero here */ /* Create the clause (!index + 0). */ /* negative phase */ /* negative phase */ /* E == non-constant */ /* T == non-const */ /* Cache results. */