自学教程：C++ Cudd_NotCond函数代码示例

/**Function*************************************************************  Synopsis    [Converts graph to BDD.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph ){    DdNode * bFunc, * bFunc0, * bFunc1;    Dec_Node_t * pNode;    int i;    // sanity checks    assert( Dec_GraphLeaveNum(pGraph) >= 0 );    assert( Dec_GraphLeaveNum(pGraph) <= pGraph->nSize );    // check for constant function    if ( Dec_GraphIsConst(pGraph) )        return Cudd_NotCond( b1, Dec_GraphIsComplement(pGraph) );    // check for a literal    if ( Dec_GraphIsVar(pGraph) )        return Cudd_NotCond( Cudd_bddIthVar(dd, Dec_GraphVarInt(pGraph)), Dec_GraphIsComplement(pGraph) );    // assign the elementary variables    Dec_GraphForEachLeaf( pGraph, pNode, i )        pNode->pFunc = Cudd_bddIthVar( dd, i );    // compute the function for each internal node    Dec_GraphForEachNode( pGraph, pNode, i )    {        bFunc0 = Cudd_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );         bFunc1 = Cudd_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );         pNode->pFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( pNode->pFunc );    }

/**Function********************************************************************  Synopsis    [Implements the recursive step of Cudd_bddVarMap.]  Description [Implements the recursive step of Cudd_bddVarMap.  Returns a pointer to the result if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [Cudd_bddVarMap]******************************************************************************/static DdNode *cuddBddVarMapRecur(  DdManager *manager /* DD manager */,  DdNode *f /* BDD to be remapped */){    DdNode	*F, *T, *E;    DdNode	*res;    int		index;    statLine(manager);    F = Cudd_Regular(f);    /* Check for terminal case of constant node. */    if (cuddIsConstant(F)) {	return(f);    }    /* If problem already solved, look up answer and return. */    if (F->ref != 1 &&	(res = cuddCacheLookup1(manager,Cudd_bddVarMap,F)) != NULL) {	return(Cudd_NotCond(res,F != f));    }    /* Split and recur on children of this node. */    T = cuddBddVarMapRecur(manager,cuddT(F));    if (T == NULL) return(NULL);    cuddRef(T);    E = cuddBddVarMapRecur(manager,cuddE(F));    if (E == NULL) {	Cudd_IterDerefBdd(manager, T);	return(NULL);    }    cuddRef(E);    /* Move variable that should be in this position to this position    ** by retrieving the single var BDD for that variable, and calling    ** cuddBddIteRecur with the T and E we just created.    */    index = manager->map[F->index];    res = cuddBddIteRecur(manager,manager->vars[index],T,E);    if (res == NULL) {	Cudd_IterDerefBdd(manager, T);	Cudd_IterDerefBdd(manager, E);	return(NULL);    }    cuddRef(res);    Cudd_IterDerefBdd(manager, T);    Cudd_IterDerefBdd(manager, E);    /* Do not keep the result if the reference count is only 1, since    ** it will not be visited again.    */    if (F->ref != 1) {	cuddCacheInsert1(manager,Cudd_bddVarMap,F,res);    }    cuddDeref(res);    return(Cudd_NotCond(res,F != f));} /* end of cuddBddVarMapRecur */

/**Function********************************************************************  Synopsis    [Checks whether a variable is dependent on others in a  function.]  Description [Checks whether a variable is dependent on others in a  function.  Returns 1 if the variable is dependent; 0 otherwise. No  new nodes are created.]  SideEffects [None]  SeeAlso     []******************************************************************************/intCudd_bddVarIsDependent(  DdManager *dd,		/* manager */  DdNode *f,			/* function */  DdNode *var			/* variable */){    DdNode *F, *res, *zero, *ft, *fe;    unsigned topf, level;    DD_CTFP cacheOp;    int retval;    /* NuSMV: begin add */    abort(); /* NOT USED BY NUSMV */    /* NuSMV: begin end */    zero = Cudd_Not(DD_TRUE(dd));    if (Cudd_IsConstant(f)) return(f == zero);    /* From now on f is not constant. */    F = Cudd_Regular(f);    topf = (unsigned) dd->perm[F->index];    level = (unsigned) dd->perm[var->index];    /* Check terminal case. If topf > index of var, f does not depend on var.    ** Therefore, var is not dependent in f. */    if (topf > level) {	return(0);    }    cacheOp = (DD_CTFP) Cudd_bddVarIsDependent;    res = cuddCacheLookup2(dd,cacheOp,f,var);    if (res != NULL) {	return(res != zero);    }    /* Compute cofactors. */    ft = Cudd_NotCond(cuddT(F), f != F);    fe = Cudd_NotCond(cuddE(F), f != F);    if (topf == level) {	retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe));    } else {	retval = Cudd_bddVarIsDependent(dd,ft,var) &&	    Cudd_bddVarIsDependent(dd,fe,var);    }    cuddCacheInsert2(dd,cacheOp,f,var,Cudd_NotCond(zero,retval));    return(retval);} /* Cudd_bddVarIsDependent */

ABC_NAMESPACE_IMPL_START///////////////////////////////////////////////////////////////////////////                        DECLARATIONS                              //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////                     FUNCTION DEFINITIONS                         ////////////////////////////////////////////////////////////////////////////**Function*************************************************************  Synopsis    [Converts graph to BDD.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph ){    DdNode * bFunc, * bFunc0, * bFunc1;    Dec_Node_t * pNode = NULL; // Suppress "might be used uninitialized"    int i;    // sanity checks    assert( Dec_GraphLeaveNum(pGraph) >= 0 );    assert( Dec_GraphLeaveNum(pGraph) <= pGraph->nSize );    // check for constant function    if ( Dec_GraphIsConst(pGraph) )        return Cudd_NotCond( b1, Dec_GraphIsComplement(pGraph) );    // check for a literal    if ( Dec_GraphIsVar(pGraph) )        return Cudd_NotCond( Cudd_bddIthVar(dd, Dec_GraphVarInt(pGraph)), Dec_GraphIsComplement(pGraph) );    // assign the elementary variables    Dec_GraphForEachLeaf( pGraph, pNode, i )        pNode->pFunc = Cudd_bddIthVar( dd, i );    // compute the function for each internal node    Dec_GraphForEachNode( pGraph, pNode, i )    {        bFunc0 = Cudd_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );         bFunc1 = Cudd_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );         pNode->pFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( (DdNode *)pNode->pFunc );    }

/**Function*************************************************************  Synopsis    [Derives the global BDD for one AIG node.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/DdNode * Bbr_NodeGlobalBdds_rec( DdManager * dd, Aig_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose ){    DdNode * bFunc, * bFunc0, * bFunc1;    assert( !Aig_IsComplement(pNode) );    if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )    {//        Extra_ProgressBarStop( pProgress );        if ( fVerbose )        printf( "The number of live nodes reached %d./n", nBddSizeMax );        fflush( stdout );        return NULL;    }    // if the result is available return    if ( Aig_ObjGlobalBdd(pNode) == NULL )    {        // compute the result for both branches        bFunc0 = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pNode), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose );         if ( bFunc0 == NULL )            return NULL;        Cudd_Ref( bFunc0 );        bFunc1 = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin1(pNode), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose );         if ( bFunc1 == NULL )            return NULL;        Cudd_Ref( bFunc1 );        bFunc0 = Cudd_NotCond( bFunc0, Aig_ObjFaninC0(pNode) );        bFunc1 = Cudd_NotCond( bFunc1, Aig_ObjFaninC1(pNode) );        // get the final result        bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );        Cudd_RecursiveDeref( dd, bFunc0 );        Cudd_RecursiveDeref( dd, bFunc1 );        // add the number of used nodes        (*pCounter)++;        // set the result        assert( Aig_ObjGlobalBdd(pNode) == NULL );        Aig_ObjSetGlobalBdd( pNode, bFunc );        // increment the progress bar//        if ( pProgress )//            Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );    }    // prepare the return value    bFunc = Aig_ObjGlobalBdd(pNode);    // dereference BDD at the node    if ( --pNode->nRefs == 0 && fDropInternal )    {        Cudd_Deref( bFunc );        Aig_ObjSetGlobalBdd( pNode, NULL );    }    return bFunc;}

/**Function*************************************************************  Synopsis    [Returns the array of constraint candidates.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/DdNode * Llb_ManComputeIndCase_rec( Aig_Man_t * p, Aig_Obj_t * pObj, DdManager * dd, Vec_Ptr_t * vBdds ){    DdNode * bBdd0, * bBdd1;    DdNode * bFunc = (DdNode *)Vec_PtrEntry( vBdds, Aig_ObjId(pObj) );    if ( bFunc != NULL )        return bFunc;    assert( Aig_ObjIsNode(pObj) );    bBdd0 = Llb_ManComputeIndCase_rec( p, Aig_ObjFanin0(pObj), dd, vBdds );     bBdd1 = Llb_ManComputeIndCase_rec( p, Aig_ObjFanin1(pObj), dd, vBdds );     bBdd0 = Cudd_NotCond( bBdd0, Aig_ObjFaninC0(pObj) );    bBdd1 = Cudd_NotCond( bBdd1, Aig_ObjFaninC1(pObj) );    bFunc = Cudd_bddAnd( dd, bBdd0, bBdd1 );  Cudd_Ref( bFunc );    Vec_PtrWriteEntry( vBdds, Aig_ObjId(pObj), bFunc );    return bFunc;}

/**Function********************************************************************  Synopsis    [Performs the recursive step for Cudd_addBddInterval.]  Description [Performs the recursive step for Cudd_addBddInterval.  Returns a pointer to the BDD if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [addBddDoThreshold addBddDoStrictThreshold]******************************************************************************/static DdNode *addBddDoInterval(  DdManager * dd,  DdNode * f,  DdNode * l,  DdNode * u){    DdNode *res, *T, *E;    DdNode *fv, *fvn;    int v;    statLine(dd);    /* Check terminal case. */    if (cuddIsConstant(f)) {	return(Cudd_NotCond(DD_TRUE(dd),cuddV(f) < cuddV(l) || cuddV(f) > cuddV(u)));    }    /* Check cache. */    res = cuddCacheLookup(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u);    if (res != NULL) return(res);    /* Recursive step. */    v = f->index;    fv = cuddT(f); fvn = cuddE(f);    T = addBddDoInterval(dd,fv,l,u);    if (T == NULL) return(NULL);    cuddRef(T);    E = addBddDoInterval(dd,fvn,l,u);    if (E == NULL) {	Cudd_RecursiveDeref(dd, T);	return(NULL);    }    cuddRef(E);    if (Cudd_IsComplement(T)) {	res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));	if (res == NULL) {	    Cudd_RecursiveDeref(dd, T);	    Cudd_RecursiveDeref(dd, E);	    return(NULL);	}	res = Cudd_Not(res);    } else {	res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);	if (res == NULL) {	    Cudd_RecursiveDeref(dd, T);	    Cudd_RecursiveDeref(dd, E);	    return(NULL);	}    }    cuddDeref(T);    cuddDeref(E);    /* Store result. */    cuddCacheInsert(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u,res);    return(res);} /* end of addBddDoInterval */

/**Function********************************************************************  Synopsis    [Performs the recursive step for Cudd_addBddStrictThreshold.]  Description [Performs the recursive step for Cudd_addBddStrictThreshold.  Returns a pointer to the BDD if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [addBddDoThreshold]******************************************************************************/static DdNode *addBddDoStrictThreshold(  DdManager * dd,  DdNode * f,  DdNode * val){    DdNode *res, *T, *E;    DdNode *fv, *fvn;    int v;    statLine(dd);    /* Check terminal case. */    if (cuddIsConstant(f)) {	return(Cudd_NotCond(DD_TRUE(dd),cuddV(f) <= cuddV(val)));    }    /* Check cache. */    res = cuddCacheLookup2(dd,addBddDoStrictThreshold,f,val);    if (res != NULL) return(res);    /* Recursive step. */    v = f->index;    fv = cuddT(f); fvn = cuddE(f);    T = addBddDoStrictThreshold(dd,fv,val);    if (T == NULL) return(NULL);    cuddRef(T);    E = addBddDoStrictThreshold(dd,fvn,val);    if (E == NULL) {	Cudd_RecursiveDeref(dd, T);	return(NULL);    }    cuddRef(E);    if (Cudd_IsComplement(T)) {	res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));	if (res == NULL) {	    Cudd_RecursiveDeref(dd, T);	    Cudd_RecursiveDeref(dd, E);	    return(NULL);	}	res = Cudd_Not(res);    } else {	res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);	if (res == NULL) {	    Cudd_RecursiveDeref(dd, T);	    Cudd_RecursiveDeref(dd, E);	    return(NULL);	}    }    cuddDeref(T);    cuddDeref(E);    /* Store result. */    cuddCacheInsert2(dd,addBddDoStrictThreshold,f,val,res);    return(res);} /* end of addBddDoStrictThreshold */

/**Function*************************************************************  Synopsis    [Recursively derives the truth table for the cut.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/DdNode * Fpga_TruthsCutBdd_rec( DdManager * dd, Fpga_Cut_t * pCut, Fpga_NodeVec_t * vVisited ){    DdNode * bFunc, * bFunc0, * bFunc1;    assert( !Fpga_IsComplement(pCut) );    // if the cut is visited, return the result    if ( pCut->uSign )        return (DdNode *)pCut->uSign;    // compute the functions of the children    bFunc0 = Fpga_TruthsCutBdd_rec( dd, Fpga_CutRegular(pCut->pOne), vVisited );   Cudd_Ref( bFunc0 );    bFunc0 = Cudd_NotCond( bFunc0, Fpga_CutIsComplement(pCut->pOne) );    bFunc1 = Fpga_TruthsCutBdd_rec( dd, Fpga_CutRegular(pCut->pTwo), vVisited );   Cudd_Ref( bFunc1 );    bFunc1 = Cudd_NotCond( bFunc1, Fpga_CutIsComplement(pCut->pTwo) );    // get the function of the cut    bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );    bFunc  = Cudd_NotCond( bFunc, pCut->Phase );    Cudd_RecursiveDeref( dd, bFunc0 );    Cudd_RecursiveDeref( dd, bFunc1 );    assert( pCut->uSign == 0 );    pCut->uSign = (unsigned)bFunc;    // add this cut to the visited list    Fpga_NodeVecPush( vVisited, (Fpga_Node_t *)pCut );    return bFunc;}

/**Function********************************************************************  Synopsis    [Determines whether f is less than or equal to g.]  Description [Returns 1 if f is less than or equal to g; 0 otherwise.  No new nodes are created. This procedure works for arbitrary ADDs.  For 0-1 ADDs Cudd_addEvalConst is more efficient.]  SideEffects [None]  SeeAlso     [Cudd_addIteConstant Cudd_addEvalConst Cudd_bddLeq]******************************************************************************/intCudd_addLeq(  DdManager * dd,  DdNode * f,  DdNode * g){    DdNode *tmp, *fv, *fvn, *gv, *gvn;    unsigned int topf, topg, res;    /* Terminal cases. */    if (f == g) return(1);    statLine(dd);    if (cuddIsConstant(f)) {	if (cuddIsConstant(g)) return(cuddV(f) <= cuddV(g));	if (f == DD_MINUS_INFINITY(dd)) return(1);	if (f == DD_PLUS_INFINITY(dd)) return(0); /* since f != g */    }    if (g == DD_PLUS_INFINITY(dd)) return(1);    if (g == DD_MINUS_INFINITY(dd)) return(0); /* since f != g */    /* Check cache. */    tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_addLeq,f,g);    if (tmp != NULL) {	return(tmp == DD_ONE(dd));    }    /* Compute cofactors. One of f and g is not constant. */    topf = cuddI(dd,f->index);    topg = cuddI(dd,g->index);    if (topf <= topg) {	fv = cuddT(f); fvn = cuddE(f);    } else {	fv = fvn = f;    }    if (topg <= topf) {	gv = cuddT(g); gvn = cuddE(g);    } else {	gv = gvn = g;    }    res = Cudd_addLeq(dd,fvn,gvn) && Cudd_addLeq(dd,fv,gv);    /* Store result in cache and return. */    cuddCacheInsert2(dd,(DD_CTFP) Cudd_addLeq,f,g,		     Cudd_NotCond(DD_ONE(dd),res==0));    return(res);} /* end of Cudd_addLeq */

    // construct the BDDs//    pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p) );    Aig_ManForEachCo( p, pObj, i )    {        bFunc = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pObj), nBddSizeMax, fDropInternal, pProgress, &Counter, fVerbose );        if ( bFunc == NULL )        {            if ( fVerbose )            printf( "Constructing global BDDs is aborted./n" );            Aig_ManFreeGlobalBdds( p, dd );            Cudd_Quit( dd );             // reset references            Aig_ManResetRefs( p );            return NULL;        }        bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pObj) );  Cudd_Ref( bFunc );         Aig_ObjSetGlobalBdd( pObj, bFunc );    }

/**Function********************************************************************  Synopsis    [Computes the disjunction of two BDDs f and g.]  Description [Computes the disjunction of two BDDs f and g. Returns a  pointer to the resulting BDD if successful; (uintptr_t) 0 if the intermediate  result blows up.]  SideEffects [None]  SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddNand Cudd_bddNor  Cudd_bddXor Cudd_bddXnor]******************************************************************************/DdNode *Cudd_bddOr(  DdManager * dd,  DdNode * f,  DdNode * g){    DdNode *res;    do {	dd->reordered = 0;	res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g));    } while (dd->reordered == 1);    res = Cudd_NotCond(res,res != (uintptr_t) 0);    return(res);} /* end of Cudd_bddOr */

/**Function********************************************************************  Synopsis    [Computes the NAND of two BDDs f and g.]  Description [Computes the NAND of two BDDs f and g. Returns a  pointer to the resulting BDD if successful; NULL if the intermediate  result blows up.]  SideEffects [None]  SeeAlso     [Cudd_bddIte Cudd_addApply Cudd_bddAnd Cudd_bddOr Cudd_bddNor  Cudd_bddXor Cudd_bddXnor]******************************************************************************/DdNode *Cudd_bddNand(  DdManager * dd,  DdNode * f,  DdNode * g){    DdNode *res;    do {        dd->reordered = 0;        res = cuddBddAndRecur(dd,f,g);    } while (dd->reordered == 1);    res = Cudd_NotCond(res,res != NULL);    return(res);} /* end of Cudd_bddNand */

ABC_NAMESPACE_IMPL_START///////////////////////////////////////////////////////////////////////////                        DECLARATIONS                              //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////                     FUNCTION DEFINITIONS                         ////////////////////////////////////////////////////////////////////////////**Function*************************************************************  Synopsis    [Computes the initial state and sets up the variable map.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/DdNode * Abc_NtkInitStateVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose ){    DdNode ** pbVarsX, ** pbVarsY;    DdNode * bTemp, * bProd, * bVar;    Abc_Obj_t * pLatch;    int i;    // set the variable mapping for Cudd_bddVarMap()    pbVarsX = ABC_ALLOC( DdNode *, dd->size );    pbVarsY = ABC_ALLOC( DdNode *, dd->size );    bProd = b1;         Cudd_Ref( bProd );    Abc_NtkForEachLatch( pNtk, pLatch, i )    {        pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ];        pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];        // get the initial value of the latch        bVar  = Cudd_NotCond( pbVarsX[i], !Abc_LatchIsInit1(pLatch) );        bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar );      Cudd_Ref( bProd );        Cudd_RecursiveDeref( dd, bTemp );     }

/**Function********************************************************************  Synopsis    [Computes the disjunction of two BDDs f and g.  Returns  NULL if too many nodes are required.]  Description [Computes the disjunction of two BDDs f and g. Returns a  pointer to the resulting BDD if successful; NULL if the intermediate  result blows up or more new nodes than <code>limit</code> are  required.]  SideEffects [None]  SeeAlso     [Cudd_bddOr]******************************************************************************/DdNode *Cudd_bddOrLimit(  DdManager * dd,  DdNode * f,  DdNode * g,  unsigned int limit){    DdNode *res;    unsigned int saveLimit = dd->maxLive;    dd->maxLive = (dd->keys - dd->dead) + (dd->keysZ - dd->deadZ) + limit;    do {	dd->reordered = 0;	res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(g));    } while (dd->reordered == 1);    dd->maxLive = saveLimit;    res = Cudd_NotCond(res,res != NULL);    return(res);} /* end of Cudd_bddOrLimit */

/**Function*************************************************************  Synopsis    [Derive BDD of the characteristic function.]  Description []                 SideEffects []  SeeAlso     []***********************************************************************/DdNode * Abc_ResBuildBdd( Abc_Ntk_t * pNtk, DdManager * dd ){    Vec_Ptr_t * vNodes, * vBdds, * vLocals;    Abc_Obj_t * pObj, * pFanin;    DdNode * bFunc, * bPart, * bTemp, * bVar;    int i, k;    assert( Abc_NtkIsSopLogic(pNtk) );    assert( Abc_NtkCoNum(pNtk) <= 3 );    vBdds = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );    Abc_NtkForEachCi( pNtk, pObj, i )        Vec_PtrWriteEntry( vBdds, Abc_ObjId(pObj), Cudd_bddIthVar(dd, i) );    // create internal node BDDs    vNodes = Abc_NtkDfs( pNtk, 0 );    vLocals = Vec_PtrAlloc( 6 );    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )    {        if ( Abc_ObjFaninNum(pObj) == 0 )        {            bFunc = Cudd_NotCond( Cudd_ReadOne(dd), Abc_SopIsConst0((char *)pObj->pData) );  Cudd_Ref( bFunc );            Vec_PtrWriteEntry( vBdds, Abc_ObjId(pObj), bFunc );            continue;        }        Vec_PtrClear( vLocals );        Abc_ObjForEachFanin( pObj, pFanin, k )            Vec_PtrPush( vLocals, Vec_PtrEntry(vBdds, Abc_ObjId(pFanin)) );        bFunc = Abc_ConvertSopToBdd( dd, (char *)pObj->pData, (DdNode **)Vec_PtrArray(vLocals) );  Cudd_Ref( bFunc );        Vec_PtrWriteEntry( vBdds, Abc_ObjId(pObj), bFunc );    }    Vec_PtrFree( vLocals );    // create char function    bFunc = Cudd_ReadOne( dd );  Cudd_Ref( bFunc );    Abc_NtkForEachCo( pNtk, pObj, i )    {        bVar  = Cudd_bddIthVar( dd, i + Abc_NtkCiNum(pNtk) );        bTemp = (DdNode *)Vec_PtrEntry( vBdds, Abc_ObjFaninId0(pObj) );        bPart = Cudd_bddXnor( dd, bTemp, bVar );          Cudd_Ref( bPart );        bFunc = Cudd_bddAnd( dd, bTemp = bFunc, bPart );  Cudd_Ref( bFunc );        Cudd_RecursiveDeref( dd, bTemp );        Cudd_RecursiveDeref( dd, bPart );    }

/**Function********************************************************************  Synopsis    [Implements the recursive step of Cudd_bddIte.]  Description [Implements the recursive step of Cudd_bddIte. Returns a  pointer to the resulting BDD. NULL if the intermediate result blows  up or if reordering occurs.]  SideEffects [None]  SeeAlso     []******************************************************************************/DdNode *cuddBddIteRecur(  DdManager * dd,  DdNode * f,  DdNode * g,  DdNode * h){    DdNode       *one, *zero, *res;    DdNode       *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;    unsigned int topf, topg, toph, v;    int          index = -1;    int          comple;    statLine(dd);    /* Terminal cases. */    /* One variable cases. */    if (f == (one = DD_ONE(dd)))        /* ITE(1,G,H) = G */        return(g);        if (f == (zero = Cudd_Not(one)))    /* ITE(0,G,H) = H */        return(h);        /* From now on, f is known not to be a constant. */    if (g == one || f == g) {   /* ITE(F,F,H) = ITE(F,1,H) = F + H */        if (h == zero) {        /* ITE(F,1,0) = F */            return(f);        } else {            res = cuddBddAndRecur(dd,Cudd_Not(f),Cudd_Not(h));            return(Cudd_NotCond(res,res != NULL));        }    } else if (g == zero || f == Cudd_Not(g)) { /* ITE(F,!F,H) = ITE(F,0,H) = !F * H */        if (h == one) {         /* ITE(F,0,1) = !F */            return(Cudd_Not(f));        } else {            res = cuddBddAndRecur(dd,Cudd_Not(f),h);            return(res);        }    }    if (h == zero || f == h) {    /* ITE(F,G,F) = ITE(F,G,0) = F * G */        res = cuddBddAndRecur(dd,f,g);        return(res);    } else if (h == one || f == Cudd_Not(h)) { /* ITE(F,G,!F) = ITE(F,G,1) = !F + G */        res = cuddBddAndRecur(dd,f,Cudd_Not(g));        return(Cudd_NotCond(res,res != NULL));    }    /* Check remaining one variable case. */    if (g == h) {               /* ITE(F,G,G) = G */        return(g);    } else if (g == Cudd_Not(h)) { /* ITE(F,G,!G) = F <-> G */        res = cuddBddXorRecur(dd,f,h);        return(res);    }        /* From here, there are no constants. */    comple = bddVarToCanonicalSimple(dd, &f, &g, &h, &topf, &topg, &toph);    /* f & g are now regular pointers */    v = ddMin(topg, toph);    /* A shortcut: ITE(F,G,H) = (v,G,H) if F = (v,1,0), v < top(G,H). */    if (topf < v && cuddT(f) == one && cuddE(f) == zero) {        r = cuddUniqueInter(dd, (int) f->index, g, h);        return(Cudd_NotCond(r,comple && r != NULL));    }    /* Check cache. */    r = cuddCacheLookup(dd, DD_BDD_ITE_TAG, f, g, h);    if (r != NULL) {        return(Cudd_NotCond(r,comple));    }    /* Compute cofactors. */    if (topf <= v) {        v = ddMin(topf, v);     /* v = top_var(F,G,H) */        index = f->index;        Fv = cuddT(f); Fnv = cuddE(f);    } else {        Fv = Fnv = f;    }    if (topg == v) {        index = g->index;        Gv = cuddT(g); Gnv = cuddE(g);    } else {        Gv = Gnv = g;//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Implements the recursive step of Cudd_bddPermute.]  Description [ Recursively puts the BDD in the order given in the array permut.  Checks for trivial cases to terminate recursion, then splits on the  children of this node.  Once the solutions for the children are  obtained, it puts into the current position the node from the rest of  the BDD that should be here. Then returns this BDD.  The key here is that the node being visited is NOT put in its proper  place by this instance, but rather is switched when its proper position  is reached in the recursion tree.<p>  The DdNode * that is returned is the same BDD as passed in as node,  but in the new order.]  SideEffects [None]  SeeAlso     [Cudd_bddPermute cuddAddPermuteRecur]******************************************************************************/static DdNode *cuddBddPermuteRecur(  DdManager * manager /* DD manager */,  DdHashTable * table /* computed table */,  DdNode * node /* BDD to be reordered */,  int * permut /* permutation array */){    DdNode	*N,*T,*E;    DdNode	*res;    int		index;    statLine(manager);    N = Cudd_Regular(node);    /* Check for terminal case of constant node. */    if (cuddIsConstant(N)) {	return(node);    }    /* If problem already solved, look up answer and return. */    if (N->ref != 1 && (res = cuddHashTableLookup1(table,N)) != NULL) {#ifdef DD_DEBUG	bddPermuteRecurHits++;#endif	return(Cudd_NotCond(res,N != node));    }    /* Split and recur on children of this node. */    T = cuddBddPermuteRecur(manager,table,cuddT(N),permut);    if (T == NULL) return(NULL);    cuddRef(T);    E = cuddBddPermuteRecur(manager,table,cuddE(N),permut);    if (E == NULL) {	Cudd_IterDerefBdd(manager, T);	return(NULL);    }    cuddRef(E);    /* Move variable that should be in this position to this position    ** by retrieving the single var BDD for that variable, and calling    ** cuddBddIteRecur with the T and E we just created.    */    index = permut[N->index];    res = cuddBddIteRecur(manager,manager->vars[index],T,E);    if (res == NULL) {	Cudd_IterDerefBdd(manager, T);	Cudd_IterDerefBdd(manager, E);	return(NULL);    }    cuddRef(res);    Cudd_IterDerefBdd(manager, T);    Cudd_IterDerefBdd(manager, E);    /* Do not keep the result if the reference count is only 1, since    ** it will not be visited again.    */    if (N->ref != 1) {	ptrint fanout = (ptrint) N->ref;	cuddSatDec(fanout);	if (!cuddHashTableInsert1(table,N,res,fanout)) {	    Cudd_IterDerefBdd(manager, res);	    return(NULL);	}    }    cuddDeref(res);    return(Cudd_NotCond(res,N != node));} /* end of cuddBddPermuteRecur */

/**Function*************************************************************  Synopsis    []  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Abc_MvDecompose( Mv_Man_t * p ){    DdNode * bCofs[16], * bVarCube1, * bVarCube2, * bVarCube, * bCube, * bVar0, * bVar1;//, * bRes;    int k, i1, i2, v1, v2;//, c1, c2, Counter;    bVar0 = Cudd_bddIthVar(p->dd, 30);    bVar1 = Cudd_bddIthVar(p->dd, 31);    bCube = Cudd_bddAnd( p->dd, bVar0, bVar1 );  Cudd_Ref( bCube );    for ( k = 0; k < p->nFuncs; k++ )    {        printf( "FUNCTION %d/n", k );        for ( i1 = 0; i1 < p->nFuncs; i1++ )        for ( i2 = i1+1; i2 < p->nFuncs; i2++ )        {            Vec_Ptr_t * vCofs;            for ( v1 = 0; v1 < 4; v1++ )            {                bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i1  ), ((v1 & 1) == 0) );                bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i1-1), ((v1 & 2) == 0) );                bVarCube1 = Cudd_bddAnd( p->dd, bVar0, bVar1 );  Cudd_Ref( bVarCube1 );                for ( v2 = 0; v2 < 4; v2++ )                {                    bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i2  ), ((v2 & 1) == 0) );                    bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i2-1), ((v2 & 2) == 0) );                    bVarCube2 = Cudd_bddAnd( p->dd, bVar0, bVar1 );         Cudd_Ref( bVarCube2 );                    bVarCube = Cudd_bddAnd( p->dd, bVarCube1, bVarCube2 );  Cudd_Ref( bVarCube );                    bCofs[v1 * 4 + v2] = Cudd_Cofactor( p->dd, p->bFuncs[k], bVarCube );  Cudd_Ref( bCofs[v1 * 4 + v2] );                    Cudd_RecursiveDeref( p->dd, bVarCube );                    Cudd_RecursiveDeref( p->dd, bVarCube2 );                }                Cudd_RecursiveDeref( p->dd, bVarCube1 );            }/*            // check the compatibility of cofactors            Counter = 0;            for ( c1 = 0; c1 < 16; c1++ )            {                for ( c2 = 0; c2 <= c1; c2++ )                    printf( " " );                for ( c2 = c1+1; c2 < 16; c2++ )                {                    bRes = Cudd_bddAndAbstract( p->dd, bCofs[c1], bCofs[c2], bCube );  Cudd_Ref( bRes );                    if ( bRes == Cudd_ReadOne(p->dd) )                    {                        printf( "+" );                        Counter++;                    }                    else                    {                        printf( " " );                    }                    Cudd_RecursiveDeref( p->dd, bRes );                }                printf( "/n" );            }*/            vCofs = Vec_PtrAlloc( 16 );            for ( v1 = 0; v1 < 4; v1++ )            for ( v2 = 0; v2 < 4; v2++ )                Vec_PtrPushUnique( vCofs, bCofs[v1 * 4 + v2] );            printf( "%d ", Vec_PtrSize(vCofs) );            Vec_PtrFree( vCofs );            // free the cofactors            for ( v1 = 0; v1 < 4; v1++ )            for ( v2 = 0; v2 < 4; v2++ )                Cudd_RecursiveDeref( p->dd, bCofs[v1 * 4 + v2] );            printf( "/n" );//            printf( "%2d, %2d : %3d/n", i1, i2, Counter );        }    }    Cudd_RecursiveDeref( p->dd, bCube );}

/**Function*************************************************************  Synopsis    []  Description []                 SideEffects []  SeeAlso     []***********************************************************************/void Abc_MvRead( Mv_Man_t * p ){    FILE * pFile;    char Buffer[1000], * pLine;    DdNode * bCube, * bTemp, * bProd, * bVar0, * bVar1, * bCubeSum;    int i, v;    // start the cube    bCubeSum = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( bCubeSum );    // start the values    for ( i = 0; i < 15; i++ )    for ( v = 0; v < 4; v++ )    {        p->bValues[i][v]   = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bValues[i][v] );        p->bValueDcs[i][v] = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bValueDcs[i][v] );    }    // read the file    pFile = fopen( "input.pla", "r" );    while ( fgets( Buffer, 1000, pFile ) )    {        if ( Buffer[0] == '#' )            continue;        if ( Buffer[0] == '.' )        {            if ( Buffer[1] == 'e' )                break;            continue;        }        // get the cube         bCube = Abc_MvReadCube( p->dd, Buffer, 18 );  Cudd_Ref( bCube );        // add it to the values of the output functions        pLine = Buffer + 19;        for ( i = 0; i < 15; i++ )        {            if ( pLine[2*i] == '-' && pLine[2*i+1] == '-' )            {                for ( v = 0; v < 4; v++ )                {                    p->bValueDcs[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValueDcs[i][v], bCube );  Cudd_Ref( p->bValueDcs[i][v] );                    Cudd_RecursiveDeref( p->dd, bTemp );                }                continue;            }            else if ( pLine[2*i] == '0' && pLine[2*i+1] == '0' ) // 0                v = 0;            else if ( pLine[2*i] == '1' && pLine[2*i+1] == '0' ) // 1                v = 1;            else if ( pLine[2*i] == '0' && pLine[2*i+1] == '1' ) // 2                v = 2;            else if ( pLine[2*i] == '1' && pLine[2*i+1] == '1' ) // 3                v = 3;            else assert( 0 );            // add the value            p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], bCube );  Cudd_Ref( p->bValues[i][v] );            Cudd_RecursiveDeref( p->dd, bTemp );        }        // add the cube        bCubeSum = Cudd_bddOr( p->dd, bTemp = bCubeSum, bCube );  Cudd_Ref( bCubeSum );        Cudd_RecursiveDeref( p->dd, bTemp );        Cudd_RecursiveDeref( p->dd, bCube );    }    // add the complement of the domain to all values    for ( i = 0; i < 15; i++ )        for ( v = 0; v < 4; v++ )        {            if ( p->bValues[i][v] == Cudd_Not(Cudd_ReadOne(p->dd)) )                continue;            p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], p->bValueDcs[i][v] );  Cudd_Ref( p->bValues[i][v] );            Cudd_RecursiveDeref( p->dd, bTemp );            p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], Cudd_Not(bCubeSum) );  Cudd_Ref( p->bValues[i][v] );            Cudd_RecursiveDeref( p->dd, bTemp );        }    printf( "Domain = %5.2f %%./n", 100.0*Cudd_CountMinterm(p->dd, bCubeSum, 32)/Cudd_CountMinterm(p->dd, Cudd_ReadOne(p->dd), 32) );     Cudd_RecursiveDeref( p->dd, bCubeSum );    // create each output function    for ( i = 0; i < 15; i++ )    {        p->bFuncs[i] = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bFuncs[i] );        for ( v = 0; v < 4; v++ )        {            bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 30), ((v & 1) == 0) );            bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 31), ((v & 2) == 0) );//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_bddVectorCompose.]  Description []  SideEffects [None]  SeeAlso     []******************************************************************************/static DdNode *cuddBddVectorComposeRecur(  DdManager * dd /* DD manager */,  DdHashTable * table /* computed table */,  DdNode * f /* BDD in which to compose */,  DdNode ** vector /* functions to be composed */,  int deepest /* depth of the deepest substitution */){    DdNode	*F,*T,*E;    DdNode	*res;    statLine(dd);    F = Cudd_Regular(f);    /* If we are past the deepest substitution, return f. */    if (cuddI(dd,F->index) > deepest) {	return(f);    }    /* If problem already solved, look up answer and return. */    if ((res = cuddHashTableLookup1(table,F)) != NULL) {#ifdef DD_DEBUG	bddVectorComposeHits++;#endif	return(Cudd_NotCond(res,F != f));    }    /* Split and recur on children of this node. */    T = cuddBddVectorComposeRecur(dd,table,cuddT(F),vector, deepest);    if (T == NULL) return(NULL);    cuddRef(T);    E = cuddBddVectorComposeRecur(dd,table,cuddE(F),vector, deepest);    if (E == NULL) {	Cudd_IterDerefBdd(dd, T);	return(NULL);    }    cuddRef(E);    /* Call cuddBddIteRecur with the BDD that replaces the current top    ** variable and the T and E we just created.    */    res = cuddBddIteRecur(dd,vector[F->index],T,E);    if (res == NULL) {	Cudd_IterDerefBdd(dd, T);	Cudd_IterDerefBdd(dd, E);	return(NULL);    }    cuddRef(res);    Cudd_IterDerefBdd(dd, T);    Cudd_IterDerefBdd(dd, E);	    /* Do not keep the result if the reference count is only 1, since    ** it will not be visited again.    */    if (F->ref != 1) {	ptrint fanout = (ptrint) F->ref;	cuddSatDec(fanout);	if (!cuddHashTableInsert1(table,F,res,fanout)) {	    Cudd_IterDerefBdd(dd, res);	    return(NULL);	}    }    cuddDeref(res);    return(Cudd_NotCond(res,F != f));} /* end of cuddBddVectorComposeRecur */

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_bddCompose.]  Description [Performs the recursive step of Cudd_bddCompose.  Exploits the fact that the composition of f' with g  produces the complement of the composition of f with g to better  utilize the cache.  Returns the composed BDD if successful; NULL  otherwise.]  SideEffects [None]  SeeAlso     [Cudd_bddCompose]******************************************************************************/DdNode *cuddBddComposeRecur(  DdManager * dd,  DdNode * f,  DdNode * g,  DdNode * proj){    DdNode	*F, *G, *f1, *f0, *g1, *g0, *r, *t, *e;    unsigned int v, topf, topg, topindex;    int		comple;    statLine(dd);    v = dd->perm[proj->index];    F = Cudd_Regular(f);    topf = cuddI(dd,F->index);    /* Terminal case. Subsumes the test for constant f. */    if (topf > v) return(f);    /* We solve the problem for a regular pointer, and then complement    ** the result if the pointer was originally complemented.    */    comple = Cudd_IsComplement(f);    /* Check cache. */    r = cuddCacheLookup(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj);    if (r != NULL) {	return(Cudd_NotCond(r,comple));    }    if (topf == v) {	/* Compose. */	f1 = cuddT(F);	f0 = cuddE(F);	r = cuddBddIteRecur(dd, g, f1, f0);	if (r == NULL) return(NULL);    } else {	/* Compute cofactors of f and g. Remember the index of the top	** variable.	*/	G = Cudd_Regular(g);	topg = cuddI(dd,G->index);	if (topf > topg) {	    topindex = G->index;	    f1 = f0 = F;	} else {	    topindex = F->index;	    f1 = cuddT(F);	    f0 = cuddE(F);	}	if (topg > topf) {	    g1 = g0 = g;	} else {	    g1 = cuddT(G);	    g0 = cuddE(G);	    if (g != G) {		g1 = Cudd_Not(g1);		g0 = Cudd_Not(g0);	    }	}	/* Recursive step. */	t = cuddBddComposeRecur(dd, f1, g1, proj);	if (t == NULL) return(NULL);	cuddRef(t);	e = cuddBddComposeRecur(dd, f0, g0, proj);	if (e == NULL) {	    Cudd_IterDerefBdd(dd, t);	    return(NULL);	}	cuddRef(e);	r = cuddBddIteRecur(dd, dd->vars[topindex], t, e);	if (r == NULL) {	    Cudd_IterDerefBdd(dd, t);	    Cudd_IterDerefBdd(dd, e);	    return(NULL);	}	cuddRef(r);	Cudd_IterDerefBdd(dd, t); /* t & e not necessarily part of r */	Cudd_IterDerefBdd(dd, e);	cuddDeref(r);    }    cuddCacheInsert(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj,r);//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis [Converts a ZDD cover to a BDD graph.]  Description [Converts a ZDD cover to a BDD graph. If successful, it  returns a BDD node, otherwise it returns NULL. It is a recursive  algorithm as the following. First computes 3 cofactors of a ZDD cover;  f1, f0 and fd. Second, compute BDDs(b1, b0 and bd) of f1, f0 and fd.  Third, compute T=b1+bd and E=b0+bd. Fourth, compute ITE(v,T,E) where v  is the variable which has the index of the top node of the ZDD cover.  In this case, since the index of v can be larger than either one of T or  one of E, cuddUniqueInterIVO is called, here IVO stands for  independent variable ordering.]  SideEffects []  SeeAlso     [Cudd_MakeBddFromZddCover]******************************************************************************/DdNode	*cuddMakeBddFromZddCover(  DdManager * dd,  DdNode * node){    DdNode	*neW;    int		v;    DdNode	*f1, *f0, *fd;    DdNode	*b1, *b0, *bd;    DdNode	*T, *E;    statLine(dd);    if (node == dd->one)	return(dd->one);    if (node == dd->zero)	return(Cudd_Not(dd->one));    /* Check cache */    neW = cuddCacheLookup1(dd, cuddMakeBddFromZddCover, node);    if (neW)	return(neW);    v = Cudd_Regular(node)->index;	/* either yi or zi */    cuddZddGetCofactors3(dd, node, v, &f1, &f0, &fd);    Cudd_Ref(f1);    Cudd_Ref(f0);    Cudd_Ref(fd);    b1 = cuddMakeBddFromZddCover(dd, f1);    if (!b1) {	Cudd_RecursiveDerefZdd(dd, f1);	Cudd_RecursiveDerefZdd(dd, f0);	Cudd_RecursiveDerefZdd(dd, fd);	return(NULL);    }    Cudd_Ref(b1);    b0 = cuddMakeBddFromZddCover(dd, f0);    if (!b1) {	Cudd_RecursiveDerefZdd(dd, f1);	Cudd_RecursiveDerefZdd(dd, f0);	Cudd_RecursiveDerefZdd(dd, fd);	Cudd_RecursiveDeref(dd, b1);	return(NULL);    }    Cudd_Ref(b0);    Cudd_RecursiveDerefZdd(dd, f1);    Cudd_RecursiveDerefZdd(dd, f0);    if (fd != dd->zero) {	bd = cuddMakeBddFromZddCover(dd, fd);	if (!bd) {	    Cudd_RecursiveDerefZdd(dd, fd);	    Cudd_RecursiveDeref(dd, b1);	    Cudd_RecursiveDeref(dd, b0);	    return(NULL);	}	Cudd_Ref(bd);	Cudd_RecursiveDerefZdd(dd, fd);	T = cuddBddAndRecur(dd, Cudd_Not(b1), Cudd_Not(bd));	if (!T) {	    Cudd_RecursiveDeref(dd, b1);	    Cudd_RecursiveDeref(dd, b0);	    Cudd_RecursiveDeref(dd, bd);	    return(NULL);	}	T = Cudd_NotCond(T, T != NULL);	Cudd_Ref(T);	Cudd_RecursiveDeref(dd, b1);	E = cuddBddAndRecur(dd, Cudd_Not(b0), Cudd_Not(bd));	if (!E) {	    Cudd_RecursiveDeref(dd, b0);	    Cudd_RecursiveDeref(dd, bd);	    Cudd_RecursiveDeref(dd, T);	    return(NULL);	}	E = Cudd_NotCond(E, E != NULL);	Cudd_Ref(E);	Cudd_RecursiveDeref(dd, b0);	Cudd_RecursiveDeref(dd, bd);    }    else {//.........这里部分代码省略.........

//.........这里部分代码省略.........    }    Cudd_Ref(Isub0);    Isub1 = cuddBddIsop(dd, Lsub1, Usub1);    if (Isub1 == NULL) {	Cudd_RecursiveDeref(dd, Lsub0);	Cudd_RecursiveDeref(dd, Lsub1);	Cudd_RecursiveDeref(dd, Isub0);	return(NULL);    }    Cudd_Ref(Isub1);    Cudd_RecursiveDeref(dd, Lsub0);    Cudd_RecursiveDeref(dd, Lsub1);    Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));    if (Lsuper0 == NULL) {	Cudd_RecursiveDeref(dd, Isub0);	Cudd_RecursiveDeref(dd, Isub1);	return(NULL);    }    Cudd_Ref(Lsuper0);    Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));    if (Lsuper1 == NULL) {	Cudd_RecursiveDeref(dd, Isub0);	Cudd_RecursiveDeref(dd, Isub1);	Cudd_RecursiveDeref(dd, Lsuper0);	return(NULL);    }    Cudd_Ref(Lsuper1);    Usuper0 = Unv;    Usuper1 = Uv;    /* Ld = Lsuper0 + Lsuper1 */    Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));    Ld = Cudd_NotCond(Ld, Ld != NULL);    if (Ld == NULL) {	Cudd_RecursiveDeref(dd, Isub0);	Cudd_RecursiveDeref(dd, Isub1);	Cudd_RecursiveDeref(dd, Lsuper0);	Cudd_RecursiveDeref(dd, Lsuper1);	return(NULL);    }    Cudd_Ref(Ld);    Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);    if (Ud == NULL) {	Cudd_RecursiveDeref(dd, Isub0);	Cudd_RecursiveDeref(dd, Isub1);	Cudd_RecursiveDeref(dd, Lsuper0);	Cudd_RecursiveDeref(dd, Lsuper1);	Cudd_RecursiveDeref(dd, Ld);	return(NULL);    }    Cudd_Ref(Ud);    Cudd_RecursiveDeref(dd, Lsuper0);    Cudd_RecursiveDeref(dd, Lsuper1);    Id = cuddBddIsop(dd, Ld, Ud);    if (Id == NULL) {	Cudd_RecursiveDeref(dd, Isub0);	Cudd_RecursiveDeref(dd, Isub1);	Cudd_RecursiveDeref(dd, Ld);	Cudd_RecursiveDeref(dd, Ud);	return(NULL);    }    Cudd_Ref(Id);    Cudd_RecursiveDeref(dd, Ld);    Cudd_RecursiveDeref(dd, Ud);

//.........这里部分代码省略.........	Cudd_RecursiveDeref(dd, Id);	Cudd_RecursiveDerefZdd(dd, zdd_Id);	Cudd_RecursiveDeref(dd, x);	return(NULL);    }    Cudd_Ref(term0);    Cudd_RecursiveDeref(dd, Isub0);    /* term1 = x * Isub1 */    term1 = cuddBddAndRecur(dd, x, Isub1);    if (term1 == NULL) {	Cudd_RecursiveDerefZdd(dd, zdd_Isub0);	Cudd_RecursiveDeref(dd, Isub1);	Cudd_RecursiveDerefZdd(dd, zdd_Isub1);	Cudd_RecursiveDeref(dd, Id);	Cudd_RecursiveDerefZdd(dd, zdd_Id);	Cudd_RecursiveDeref(dd, x);	Cudd_RecursiveDeref(dd, term0);	return(NULL);    }    Cudd_Ref(term1);    Cudd_RecursiveDeref(dd, x);    Cudd_RecursiveDeref(dd, Isub1);    /* sum = term0 + term1 */    sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));    if (sum == NULL) {	Cudd_RecursiveDerefZdd(dd, zdd_Isub0);	Cudd_RecursiveDerefZdd(dd, zdd_Isub1);	Cudd_RecursiveDeref(dd, Id);	Cudd_RecursiveDerefZdd(dd, zdd_Id);	Cudd_RecursiveDeref(dd, term0);	Cudd_RecursiveDeref(dd, term1);	return(NULL);    }    sum = Cudd_Not(sum);    Cudd_Ref(sum);    Cudd_RecursiveDeref(dd, term0);    Cudd_RecursiveDeref(dd, term1);    /* r = sum + Id */    r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));    r = Cudd_NotCond(r, r != NULL);    if (r == NULL) {	Cudd_RecursiveDerefZdd(dd, zdd_Isub0);	Cudd_RecursiveDerefZdd(dd, zdd_Isub1);	Cudd_RecursiveDeref(dd, Id);	Cudd_RecursiveDerefZdd(dd, zdd_Id);	Cudd_RecursiveDeref(dd, sum);	return(NULL);    }    Cudd_Ref(r);    Cudd_RecursiveDeref(dd, sum);    Cudd_RecursiveDeref(dd, Id);    if (zdd_Isub0 != zdd_zero) {	z = cuddZddGetNodeIVO(dd, index * 2 + 1, zdd_Isub0, zdd_Id);	if (z == NULL) {	    Cudd_RecursiveDerefZdd(dd, zdd_Isub0);	    Cudd_RecursiveDerefZdd(dd, zdd_Isub1);	    Cudd_RecursiveDerefZdd(dd, zdd_Id);	    Cudd_RecursiveDeref(dd, r);	    return(NULL);	}    }    else {	z = zdd_Id;    }    Cudd_Ref(z);    if (zdd_Isub1 != zdd_zero) {	y = cuddZddGetNodeIVO(dd, index * 2, zdd_Isub1, z);	if (y == NULL) {	    Cudd_RecursiveDerefZdd(dd, zdd_Isub0);	    Cudd_RecursiveDerefZdd(dd, zdd_Isub1);	    Cudd_RecursiveDerefZdd(dd, zdd_Id);	    Cudd_RecursiveDeref(dd, r);	    Cudd_RecursiveDerefZdd(dd, z);	    return(NULL);	}    }    else	y = z;    Cudd_Ref(y);    Cudd_RecursiveDerefZdd(dd, zdd_Isub0);    Cudd_RecursiveDerefZdd(dd, zdd_Isub1);    Cudd_RecursiveDerefZdd(dd, zdd_Id);    Cudd_RecursiveDerefZdd(dd, z);    cuddCacheInsert2(dd, cuddBddIsop, L, U, r);    cuddCacheInsert2(dd, cacheOp, L, U, y);    Cudd_Deref(r);    Cudd_Deref(y);    *zdd_I = y;    /*    if (Cudd_Regular(r)->index != y->index / 2) {	printf("*** ERROR : mismatch in indices between BDD and ZDD. ***/n");    }    */    return(r);} /* end of cuddZddIsop */

/**  @brief Approximates the AND of two BDDs and simultaneously abstracts the  variables in cube.  @details The variables are existentially abstracted.  @return a pointer to the result is successful; NULL otherwise.  @sideeffect None  @see Cudd_bddClippingAndAbstract*/static DdNode *cuddBddClipAndAbsRecur(  DdManager * manager,  DdNode * f,  DdNode * g,  DdNode * cube,  int  distance,  int  direction){    DdNode *F, *ft, *fe, *G, *gt, *ge;    DdNode *one, *zero, *r, *t, *e, *Cube;    int topf, topg, topcube, top;    unsigned int index;    ptruint cacheTag;    statLine(manager);    one = DD_ONE(manager);    zero = Cudd_Not(one);    /* Terminal cases. */    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);    if (f == one && g == one)	return(one);    if (cube == one) {	return(cuddBddClippingAndRecur(manager, f, g, distance, direction));    }    if (f == one || f == g) {	return (cuddBddExistAbstractRecur(manager, g, cube));    }    if (g == one) {	return (cuddBddExistAbstractRecur(manager, f, cube));    }    if (distance == 0) return(Cudd_NotCond(one,(direction == 0)));    /* At this point f, g, and cube are not constant. */    distance--;    /* Check cache. */    if (f > g) { /* Try to increase cache efficiency. */	DdNode *tmp = f;	f = g; g = tmp;    }    F = Cudd_Regular(f);    G = Cudd_Regular(g);    cacheTag = direction ? DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG :	DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG;    if (F->ref != 1 || G->ref != 1) {	r = cuddCacheLookup(manager, cacheTag,			    f, g, cube);	if (r != NULL) {	    return(r);	}    }    checkWhetherToGiveUp(manager);    /* Here we can skip the use of cuddI, because the operands are known    ** to be non-constant.    */    topf = manager->perm[F->index];    topg = manager->perm[G->index];    top = ddMin(topf, topg);    topcube = manager->perm[cube->index];    if (topcube < top) {	return(cuddBddClipAndAbsRecur(manager, f, g, cuddT(cube),				      distance, direction));    }    /* Now, topcube >= top. */    if (topf == top) {	index = F->index;	ft = cuddT(F);	fe = cuddE(F);	if (Cudd_IsComplement(f)) {	    ft = Cudd_Not(ft);	    fe = Cudd_Not(fe);	}    } else {	index = G->index;	ft = fe = f;    }    if (topg == top) {	gt = cuddT(G);	ge = cuddE(G);	if (Cudd_IsComplement(g)) {	    gt = Cudd_Not(gt);//.........这里部分代码省略.........

/**  @brief Implements the recursive step of Cudd_bddClippingAnd.  @details Takes the conjunction of two BDDs.  @return a pointer to the result is successful; NULL otherwise.  @sideeffect None  @see cuddBddClippingAnd*/static DdNode *cuddBddClippingAndRecur(  DdManager * manager,  DdNode * f,  DdNode * g,  int  distance,  int  direction){    DdNode *F, *ft, *fe, *G, *gt, *ge;    DdNode *one, *zero, *r, *t, *e;    int topf, topg;    unsigned int index;    DD_CTFP cacheOp;    statLine(manager);    one = DD_ONE(manager);    zero = Cudd_Not(one);    /* Terminal cases. */    if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);    if (f == g || g == one) return(f);    if (f == one) return(g);    if (distance == 0) {	/* One last attempt at returning the right result. We sort of	** cheat by calling Cudd_bddLeq. */	if (Cudd_bddLeq(manager,f,g)) return(f);	if (Cudd_bddLeq(manager,g,f)) return(g);	if (direction == 1) {	    if (Cudd_bddLeq(manager,f,Cudd_Not(g)) ||		Cudd_bddLeq(manager,g,Cudd_Not(f))) return(zero);	}	return(Cudd_NotCond(one,(direction == 0)));    }    /* At this point f and g are not constant. */    distance--;    /* Check cache. Try to increase cache efficiency by sorting the    ** pointers. */    if (f > g) {	DdNode *tmp = f;	f = g; g = tmp;    }    F = Cudd_Regular(f);    G = Cudd_Regular(g);    cacheOp = (DD_CTFP)	(direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);    if (F->ref != 1 || G->ref != 1) {	r = cuddCacheLookup2(manager, cacheOp, f, g);	if (r != NULL) return(r);    }    checkWhetherToGiveUp(manager);    /* Here we can skip the use of cuddI, because the operands are known    ** to be non-constant.    */    topf = manager->perm[F->index];    topg = manager->perm[G->index];    /* Compute cofactors. */    if (topf <= topg) {	index = F->index;	ft = cuddT(F);	fe = cuddE(F);	if (Cudd_IsComplement(f)) {	    ft = Cudd_Not(ft);	    fe = Cudd_Not(fe);	}    } else {	index = G->index;	ft = fe = f;    }    if (topg <= topf) {	gt = cuddT(G);	ge = cuddE(G);	if (Cudd_IsComplement(g)) {	    gt = Cudd_Not(gt);	    ge = Cudd_Not(ge);	}    } else {	gt = ge = g;    }    t = cuddBddClippingAndRecur(manager, ft, gt, distance, direction);    if (t == NULL) return(NULL);    cuddRef(t);//.........这里部分代码省略.........

/**Function********************************************************************  Synopsis    [Performs the recursive step of Cudd_Cofactor.]  Description [Performs the recursive step of Cudd_Cofactor. Returns a  pointer to the cofactor if successful; NULL otherwise.]  SideEffects [None]  SeeAlso     [Cudd_Cofactor]******************************************************************************/DdNode *cuddCofactorRecur(  DdManager * dd,  DdNode * f,  DdNode * g){    DdNode *one,*zero,*F,*G,*g1,*g0,*f1,*f0,*t,*e,*r;    unsigned int topf,topg;    int comple;    F = Cudd_Regular(f);    if (cuddIsConstant(F)) return(f);    one = DD_ONE(dd);    /* The invariant g != 0 is true on entry to this procedure and is    ** recursively maintained by it. Therefore it suffices to test g    ** against one to make sure it is not constant.    */    if (g == one) return(f);    /* From now on, f and g are known not to be constants. */    comple = f != F;    r = cuddCacheLookup2(dd,Cudd_Cofactor,F,g);    if (r != NULL) {	return(Cudd_NotCond(r,comple));    }    topf = dd->perm[F->index];    G = Cudd_Regular(g);    topg = dd->perm[G->index];    /* We take the cofactors of F because we are going to rely on    ** the fact that the cofactors of the complement are the complements    ** of the cofactors to better utilize the cache. Variable comple    ** remembers whether we have to complement the result or not.    */    if (topf <= topg) {	f1 = cuddT(F); f0 = cuddE(F);    } else {	f1 = f0 = F;    }    if (topg <= topf) {	g1 = cuddT(G); g0 = cuddE(G);	if (g != G) { g1 = Cudd_Not(g1); g0 = Cudd_Not(g0); }    } else {	g1 = g0 = g;    }    zero = Cudd_Not(one);    if (topf >= topg) {	if (g0 == zero || g0 == DD_ZERO(dd)) {	    r = cuddCofactorRecur(dd, f1, g1);	} else if (g1 == zero || g1 == DD_ZERO(dd)) {	    r = cuddCofactorRecur(dd, f0, g0);	} else {	    (void) fprintf(stdout,"Cudd_Cofactor: Invalid restriction 2/n");	    return(NULL);	}	if (r == NULL) return(NULL);    } else /* if (topf < topg) */ {	t = cuddCofactorRecur(dd, f1, g);	if (t == NULL) return(NULL);    	cuddRef(t);    	e = cuddCofactorRecur(dd, f0, g);	if (e == NULL) {	    Cudd_RecursiveDeref(dd, t);	    return(NULL);	}	cuddRef(e);	if (t == e) {	    r = t;	} else if (Cudd_IsComplement(t)) {	    r = cuddUniqueInter(dd,(int)F->index,Cudd_Not(t),Cudd_Not(e));	    if (r != NULL)		r = Cudd_Not(r);	} else {	    r = cuddUniqueInter(dd,(int)F->index,t,e);	}	if (r == NULL) {	    Cudd_RecursiveDeref(dd ,e);	    Cudd_RecursiveDeref(dd ,t);	    return(NULL);	}	cuddDeref(t);	cuddDeref(e);    }//.........这里部分代码省略.........

/**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]******************************************************************************/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 );    /* Trivial cases. */    if ( Cudd_IsConstant( f ) )        return ( Cudd_NotCond( one, comple ) );    /* Make canonical to increase the utilization of the cache. */    f = Cudd_NotCond( f, comple );    /* Now f is a regular pointer to a non-constant node. */    /* Check the cache. */    if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) )        return ( Cudd_NotCond( res, comple ) );    if ( TimeOut && TimeOut < clock() )        return NULL;    /* Recursive step. */    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 ) );}  /* end of extraTransferPermuteRecurTime */

/**Function********************************************************************  Synopsis    [Implements ITEconstant(f,g,h).]  Description [Implements ITEconstant(f,g,h). Returns a pointer to the  resulting BDD (which may or may not be constant) or DD_NON_CONSTANT.  No new nodes are created.]  SideEffects [None]  SeeAlso     [Cudd_bddIte Cudd_bddIntersect Cudd_bddLeq Cudd_addIteConstant]******************************************************************************/DdNode *Cudd_bddIteConstant(  DdManager * dd,  DdNode * f,  DdNode * g,  DdNode * h){    DdNode       *r, *Fv, *Fnv, *Gv, *Gnv, *H, *Hv, *Hnv, *t, *e;    DdNode       *one = DD_ONE(dd);    DdNode       *zero = Cudd_Not(one);    int          comple;    unsigned int topf, topg, toph, v;    statLine(dd);    /* Trivial cases. */    if (f == one)                       /* ITE(1,G,H) => G */        return(g);        if (f == zero)                      /* ITE(0,G,H) => H */        return(h);        /* f now not a constant. */    bddVarToConst(f, &g, &h, one);      /* possibly convert g or h */                                        /* to constants */    if (g == h)                         /* ITE(F,G,G) => G */        return(g);    if (Cudd_IsConstant(g) && Cudd_IsConstant(h))         return(DD_NON_CONSTANT);        /* ITE(F,1,0) or ITE(F,0,1) */                                        /* => DD_NON_CONSTANT */        if (g == Cudd_Not(h))        return(DD_NON_CONSTANT);        /* ITE(F,G,G') => DD_NON_CONSTANT */                                        /* if F != G and F != G' */        comple = bddVarToCanonical(dd, &f, &g, &h, &topf, &topg, &toph);    /* Cache lookup. */    r = cuddConstantLookup(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h);    if (r != NULL) {        return(Cudd_NotCond(r,comple && r != DD_NON_CONSTANT));    }    v = ddMin(topg, toph);    /* ITE(F,G,H) = (v,G,H) (non constant) if F = (v,1,0), v < top(G,H). */    if (topf < v && cuddT(f) == one && cuddE(f) == zero) {        return(DD_NON_CONSTANT);    }    /* Compute cofactors. */    if (topf <= v) {        v = ddMin(topf, v);             /* v = top_var(F,G,H) */        Fv = cuddT(f); Fnv = cuddE(f);    } else {        Fv = Fnv = f;    }    if (topg == v) {        Gv = cuddT(g); Gnv = cuddE(g);    } else {        Gv = Gnv = g;    }    if (toph == v) {        H = Cudd_Regular(h);        Hv = cuddT(H); Hnv = cuddE(H);        if (Cudd_IsComplement(h)) {            Hv = Cudd_Not(Hv);            Hnv = Cudd_Not(Hnv);        }    } else {        Hv = Hnv = h;    }    /* Recursion. */    t = Cudd_bddIteConstant(dd, Fv, Gv, Hv);    if (t == DD_NON_CONSTANT || !Cudd_IsConstant(t)) {        cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);        return(DD_NON_CONSTANT);    }    e = Cudd_bddIteConstant(dd, Fnv, Gnv, Hnv);    if (e == DD_NON_CONSTANT || !Cudd_IsConstant(e) || t != e) {        cuddCacheInsert(dd, DD_BDD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT);        return(DD_NON_CONSTANT);    }//.........这里部分代码省略.........