cuddzddisop.c

主要进行大规模的电路综合

	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 */


/**Function********************************************************************

  Synopsis [Performs the recursive step of Cudd_bddIsop.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_bddIsop]

******************************************************************************/
DdNode	*
cuddBddIsop(
  DdManager * dd,
  DdNode * L,
  DdNode * U)
{
    DdNode	*one = DD_ONE(dd);
    DdNode	*zero = Cudd_Not(one);
    int		v, top_l, top_u;
    DdNode	*Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
    DdNode	*Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
    DdNode	*Isub0, *Isub1, *Id;
    DdNode	*x;
    DdNode	*term0, *term1, *sum;
    DdNode	*Lv, *Uv, *Lnv, *Unv;
    DdNode	*r;
    int		index;

    statLine(dd);
    if (L == zero)
    	return(zero);
    if (U == one)
    	return(one);

    /* Check cache */
    r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
    if (r)
    	return(r);

    top_l = dd->perm[Cudd_Regular(L)->index];
    top_u = dd->perm[Cudd_Regular(U)->index];
    v = ddMin(top_l, top_u);

    /* Compute cofactors */
    if (top_l == v) {
	index = Cudd_Regular(L)->index;
    	Lv = Cudd_T(L);
    	Lnv = Cudd_E(L);
    	if (Cudd_IsComplement(L)) {
    	    Lv = Cudd_Not(Lv);
    	    Lnv = Cudd_Not(Lnv);
    	}
    }
    else {
	index = Cudd_Regular(U)->index;
        Lv = Lnv = L;
    }

    if (top_u == v) {
    	Uv = Cudd_T(U);
    	Unv = Cudd_E(U);
    	if (Cudd_IsComplement(U)) {
    	    Uv = Cudd_Not(Uv);
    	    Unv = Cudd_Not(Unv);
    	}
    }
    else {
        Uv = Unv = U;
    }

    Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
    if (Lsub0 == NULL)
	return(NULL);
    Cudd_Ref(Lsub0);
    Usub0 = Unv;
    Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
    if (Lsub1 == NULL) {
	Cudd_RecursiveDeref(dd, Lsub0);
	return(NULL);
    }
    Cudd_Ref(Lsub1);
    Usub1 = Uv;

    Isub0 = cuddBddIsop(dd, Lsub0, Usub0);
    if (Isub0 == NULL) {
	Cudd_RecursiveDeref(dd, Lsub0);
	Cudd_RecursiveDeref(dd, Lsub1);
	return(NULL);
    }
    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);

    x = cuddUniqueInter(dd, index, one, zero);
    if (x == NULL) {
	Cudd_RecursiveDeref(dd, Isub0);
	Cudd_RecursiveDeref(dd, Isub1);
	Cudd_RecursiveDeref(dd, Id);
	return(NULL);
    }
    Cudd_Ref(x);
    term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
    if (term0 == NULL) {
	Cudd_RecursiveDeref(dd, Isub0);
	Cudd_RecursiveDeref(dd, Isub1);
	Cudd_RecursiveDeref(dd, Id);
	Cudd_RecursiveDeref(dd, x);
	return(NULL);
    }
    Cudd_Ref(term0);
    Cudd_RecursiveDeref(dd, Isub0);
    term1 = cuddBddAndRecur(dd, x, Isub1);
    if (term1 == NULL) {
	Cudd_RecursiveDeref(dd, Isub1);
	Cudd_RecursiveDeref(dd, 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));
    sum = Cudd_NotCond(sum, sum != NULL);
    if (sum == NULL) {
	Cudd_RecursiveDeref(dd, Id);
	Cudd_RecursiveDeref(dd, term0);
	Cudd_RecursiveDeref(dd, term1);
	return(NULL);
    }
    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_RecursiveDeref(dd, Id);
	Cudd_RecursiveDeref(dd, sum);
	return(NULL);
    }
    Cudd_Ref(r);
    Cudd_RecursiveDeref(dd, sum);
    Cudd_RecursiveDeref(dd, Id);

    cuddCacheInsert2(dd, cuddBddIsop, L, U, r);

    Cudd_Deref(r);
    return(r);

} /* end of cuddBddIsop */


/**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_RecursiveDerefZdd(dd, fd);
	T = b1;
	E = b0;
    }

    if (Cudd_IsComplement(T)) {
	neW = cuddUniqueInterIVO(dd, v / 2, Cudd_Not(T), Cudd_Not(E));
	if (!neW) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
	neW = Cudd_Not(neW);
    }
    else {
	neW = cuddUniqueInterIVO(dd, v / 2, T, E);
	if (!neW) {
	    Cudd_RecursiveDeref(dd, T);
	    Cudd_RecursiveDeref(dd, E);
	    return(NULL);
	}
    }
    Cudd_Ref(neW);
    Cudd_RecursiveDeref(dd, T);
    Cudd_RecursiveDeref(dd, E);

    cuddCacheInsert1(dd, cuddMakeBddFromZddCover, node, neW);
    Cudd_Deref(neW);
    return(neW);

} /* end of cuddMakeBddFromZddCover */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/