cuddzddsetop.c

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

	e = cuddZddUnion(zdd, cuddE(P), cuddE(Q));
	if (e == NULL) {
	    Cudd_RecursiveDerefZdd(table, t);
	    return(NULL);
	}
	cuddRef(e);
	res = cuddZddGetNode(zdd, P->index, t, e);
	if (res == NULL) {
	    Cudd_RecursiveDerefZdd(table, t);
	    Cudd_RecursiveDerefZdd(table, e);
	    return(NULL);
	}
	cuddDeref(t);
	cuddDeref(e);
    }

    cuddCacheInsert2(table, cuddZddUnion, P, Q, res);

    return(res);

} /* end of cuddZddUnion */


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

  Synopsis [Performs the recursive step of Cudd_zddIntersect.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode *
cuddZddIntersect(
  DdManager * zdd,
  DdNode * P,
  DdNode * Q)
{
    int		p_top, q_top;
    DdNode	*empty = DD_ZERO(zdd), *t, *e, *res;
    DdManager	*table = zdd;

    statLine(zdd);
    if (P == empty)
	return(empty);
    if (Q == empty)
	return(empty);
    if (P == Q)
	return(P);

    /* Check cache. */
    res = cuddCacheLookup2Zdd(table, cuddZddIntersect, P, Q);
    if (res != NULL)
	return(res);

    if (cuddIsConstant(P))
	p_top = P->index;
    else
	p_top = zdd->permZ[P->index];
    if (cuddIsConstant(Q))
	q_top = Q->index;
    else
	q_top = zdd->permZ[Q->index];
    if (p_top < q_top) {
	res = cuddZddIntersect(zdd, cuddE(P), Q);
	if (res == NULL) return(NULL);
    } else if (p_top > q_top) {
	res = cuddZddIntersect(zdd, P, cuddE(Q));
	if (res == NULL) return(NULL);
    } else {
	t = cuddZddIntersect(zdd, cuddT(P), cuddT(Q));
	if (t == NULL) return(NULL);
	cuddRef(t);
	e = cuddZddIntersect(zdd, cuddE(P), cuddE(Q));
	if (e == NULL) {
	    Cudd_RecursiveDerefZdd(table, t);
	    return(NULL);
	}
	cuddRef(e);
	res = cuddZddGetNode(zdd, P->index, t, e);
	if (res == NULL) {
	    Cudd_RecursiveDerefZdd(table, t);
	    Cudd_RecursiveDerefZdd(table, e);
	    return(NULL);
	}
	cuddDeref(t);
	cuddDeref(e);
    }

    cuddCacheInsert2(table, cuddZddIntersect, P, Q, res);

    return(res);

} /* end of cuddZddIntersect */


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

  Synopsis [Performs the recursive step of Cudd_zddDiff.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode *
cuddZddDiff(
  DdManager * zdd,
  DdNode * P,
  DdNode * Q)
{
    int		p_top, q_top;
    DdNode	*empty = DD_ZERO(zdd), *t, *e, *res;
    DdManager	*table = zdd;

    statLine(zdd);
    if (P == empty)
	return(empty);
    if (Q == empty)
	return(P);
    if (P == Q)
	return(empty);

    /* Check cache.  The cache is shared by Cudd_zddDiffConst(). */
    res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
    if (res != NULL && res != DD_NON_CONSTANT)
	return(res);

    if (cuddIsConstant(P))
	p_top = P->index;
    else
	p_top = zdd->permZ[P->index];
    if (cuddIsConstant(Q))
	q_top = Q->index;
    else
	q_top = zdd->permZ[Q->index];
    if (p_top < q_top) {
	e = cuddZddDiff(zdd, cuddE(P), Q);
	if (e == NULL) return(NULL);
	cuddRef(e);
	res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
	if (res == NULL) {
	    Cudd_RecursiveDerefZdd(table, e);
	    return(NULL);
	}
	cuddDeref(e);
    } else if (p_top > q_top) {
	res = cuddZddDiff(zdd, P, cuddE(Q));
	if (res == NULL) return(NULL);
    } else {
	t = cuddZddDiff(zdd, cuddT(P), cuddT(Q));
	if (t == NULL) return(NULL);
	cuddRef(t);
	e = cuddZddDiff(zdd, cuddE(P), cuddE(Q));
	if (e == NULL) {
	    Cudd_RecursiveDerefZdd(table, t);
	    return(NULL);
	}
	cuddRef(e);
	res = cuddZddGetNode(zdd, P->index, t, e);
	if (res == NULL) {
	    Cudd_RecursiveDerefZdd(table, t);
	    Cudd_RecursiveDerefZdd(table, e);
	    return(NULL);
	}
	cuddDeref(t);
	cuddDeref(e);
    }

    cuddCacheInsert2(table, cuddZddDiff, P, Q, res);

    return(res);

} /* end of cuddZddDiff */


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

  Synopsis [Performs the recursive step of Cudd_zddChange.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode *
cuddZddChangeAux(
  DdManager * zdd,
  DdNode * P,
  DdNode * zvar)
{
    int		top_var, level;
    DdNode	*res, *t, *e;
    DdNode	*base = DD_ONE(zdd);
    DdNode	*empty = DD_ZERO(zdd);

    statLine(zdd);
    if (P == empty)
	return(empty);
    if (P == base)
	return(zvar);

    /* Check cache. */
    res = cuddCacheLookup2Zdd(zdd, cuddZddChangeAux, P, zvar);
    if (res != NULL)
	return(res);

    top_var = zdd->permZ[P->index];
    level = zdd->permZ[zvar->index];

    if (top_var > level) {
	res = cuddZddGetNode(zdd, zvar->index, P, DD_ZERO(zdd));
	if (res == NULL) return(NULL);
    } else if (top_var == level) {
	res = cuddZddGetNode(zdd, zvar->index, cuddE(P), cuddT(P));
	if (res == NULL) return(NULL);
    } else {
	t = cuddZddChangeAux(zdd, cuddT(P), zvar);
	if (t == NULL) return(NULL);
	cuddRef(t);
	e = cuddZddChangeAux(zdd, cuddE(P), zvar);
	if (e == NULL) {
	    Cudd_RecursiveDerefZdd(zdd, t);
	    return(NULL);
	}
	cuddRef(e);
	res = cuddZddGetNode(zdd, P->index, t, e);
	if (res == NULL) {
	    Cudd_RecursiveDerefZdd(zdd, t);
	    Cudd_RecursiveDerefZdd(zdd, e);
	    return(NULL);
	}
	cuddDeref(t);
	cuddDeref(e);
    }

    cuddCacheInsert2(zdd, cuddZddChangeAux, P, zvar, res);

    return(res);

} /* end of cuddZddChangeAux */


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

  Synopsis [Computes the positive cofactor of a ZDD w.r.t. a variable.]

  Description [Computes the positive cofactor of a ZDD w.r.t. a
  variable. In terms of combinations, the result is the set of all
  combinations in which the variable is asserted. Returns a pointer to
  the result if successful; NULL otherwise. cuddZddSubset1 performs
  the same function as Cudd_zddSubset1, but does not restart if
  reordering has taken place. Therefore it can be called from within a
  recursive procedure.]

  SideEffects [None]

  SeeAlso     [cuddZddSubset0 Cudd_zddSubset1]

******************************************************************************/
DdNode *
cuddZddSubset1(
  DdManager * dd,
  DdNode * P,
  int  var)
{
    DdNode	*zvar, *r;
    DdNode	*base, *empty;

    base = DD_ONE(dd);
    empty = DD_ZERO(dd);

    zvar = cuddUniqueInterZdd(dd, var, base, empty);
    if (zvar == NULL) {
	return(NULL);
    } else {
	cuddRef(zvar);
	r = zdd_subset1_aux(dd, P, zvar);
	if (r == NULL) {
	    Cudd_RecursiveDerefZdd(dd, zvar);
	    return(NULL);
	}
	cuddRef(r);
	Cudd_RecursiveDerefZdd(dd, zvar);
    }

    cuddDeref(r);
    return(r);

} /* end of cuddZddSubset1 */


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

  Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]

  Description [Computes the negative cofactor of a ZDD w.r.t. a
  variable. In terms of combinations, the result is the set of all
  combinations in which the variable is negated. Returns a pointer to
  the result if successful; NULL otherwise. cuddZddSubset0 performs
  the same function as Cudd_zddSubset0, but does not restart if
  reordering has taken place. Therefore it can be called from within a
  recursive procedure.]

  SideEffects [None]

  SeeAlso     [cuddZddSubset1 Cudd_zddSubset0]

******************************************************************************/
DdNode *
cuddZddSubset0(
  DdManager * dd,
  DdNode * P,
  int  var)
{
    DdNode	*zvar, *r;
    DdNode	*base, *empty;

    base = DD_ONE(dd);
    empty = DD_ZERO(dd);

    zvar = cuddUniqueInterZdd(dd, var, base, empty);
    if (zvar == NULL) {
	return(NULL);
    } else {
	cuddRef(zvar);
	r = zdd_subset0_aux(dd, P, zvar);
	if (r == NULL) {
	    Cudd_RecursiveDerefZdd(dd, zvar);
	    return(NULL);
	}
	cuddRef(r);
	Cudd_RecursiveDerefZdd(dd, zvar);
    }

    cuddDeref(r);
    return(r);

} /* end of cuddZddSubset0 */


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

  Synopsis [Substitutes a variable with its complement in a ZDD.]

  Description [Substitutes a variable with its complement in a ZDD.
  returns a pointer to the result if successful; NULL
  otherwise. cuddZddChange performs the same function as
  Cudd_zddChange, but does not restart if reordering has taken
  place. Therefore it can be called from within a recursive
  procedure.]

  SideEffects [None]

  SeeAlso     [Cudd_zddChange]

******************************************************************************/
DdNode *
cuddZddChange(
  DdManager * dd,
  DdNode * P,
  int  var)
{
    DdNode	*zvar, *res;

    zvar = cuddUniqueInterZdd(dd, var, DD_ONE(dd), DD_ZERO(dd));
    if (zvar == NULL) return(NULL);
    cuddRef(zvar);

    res = cuddZddChangeAux(dd, P, zvar);
    if (res == NULL) {
	Cudd_RecursiveDerefZdd(dd,zvar);
	return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDerefZdd(dd,zvar);
    cuddDeref(res);
    return(res);

} /* end of cuddZddChange */


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


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

  Synopsis [Performs the recursive step of Cudd_zddSubset1.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
zdd_subset1_aux(
  DdManager * zdd,
  DdNode * P,
  DdNode * zvar)
{
    int		top_var, level;
    DdNode	*res, *t, *e;
    DdNode	*base, *empty;

    statLine(zdd);
    base = DD_ONE(zdd);
    empty = DD_ZERO(zdd);

    /* Check cache. */
    res = cuddCacheLookup2Zdd(zdd, zdd_subset1_aux, P, zvar);
    if (res != NULL)
	return(res);

    if (cuddIsConstant(P)) {
	res = empty;
	cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
	return(res);
    }

    top_var = zdd->permZ[P->index];
    level = zdd->permZ[zvar->index];

    if (top_var > level) {
        res = empty;
    } else if (top_var == level) {
	res = cuddT(P);
    } else {
        t = zdd_subset1_aux(zdd, cuddT(P), zvar);
	if (t == NULL) return(NULL);
	cuddRef(t);
        e = zdd_subset1_aux(zdd, cuddE(P), zvar);
	if (e == NULL) {
	    Cudd_RecursiveDerefZdd(zdd, t);
	    return(NULL);
	}
	cuddRef(e);
        res = cuddZddGetNode(zdd, P->index, t, e);
	if (res == NULL) {
	    Cudd_RecursiveDerefZdd(zdd, t);
	    Cudd_RecursiveDerefZdd(zdd, e);
	    return(NULL);
	}
	cuddDeref(t);
	cuddDeref(e);
    }

    cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);

    return(res);

} /* end of zdd_subset1_aux */


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

  Synopsis [Performs the recursive step of Cudd_zddSubset0.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
zdd_subset0_aux(
  DdManager * zdd,
  DdNode * P,
  DdNode * zvar)
{
    int		top_var, level;
    DdNode	*res, *t, *e;
    DdNode	*base, *empty;

    statLine(zdd);
    base = DD_ONE(zdd);
    empty = DD_ZERO(zdd);

    /* Check cache. */
    res = cuddCacheLookup2Zdd(zdd, zdd_subset0_aux, P, zvar);
    if (res != NULL)
	return(res);

    if (cuddIsConstant(P)) {
	res = P;
	cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
	return(res);
    }

    top_var = zdd->permZ[P->index];
    level = zdd->permZ[zvar->index];

    if (top_var > level) {
        res = P;
    }
    else if (top_var == level) {
        res = cuddE(P);
    }
    else {
        t = zdd_subset0_aux(zdd, cuddT(P), zvar);
	if (t == NULL) return(NULL);
	cuddRef(t);
        e = zdd_subset0_aux(zdd, cuddE(P), zvar);
	if (e == NULL) {
	    Cudd_RecursiveDerefZdd(zdd, t);
	    return(NULL);
	}
	cuddRef(e);
        res = cuddZddGetNode(zdd, P->index, t, e);
	if (res == NULL) {
	    Cudd_RecursiveDerefZdd(zdd, t);
	    Cudd_RecursiveDerefZdd(zdd, e);
	    return(NULL);
	}
	cuddDeref(t);
	cuddDeref(e);
    }

    cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);

    return(res);

} /* end of zdd_subset0_aux */


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

  Synopsis    [Replaces variables with constants if possible (part of
  canonical form).]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static void
zddVarToConst(
  DdNode * f,
  DdNode ** gp,
  DdNode ** hp,
  DdNode * base,
  DdNode * empty)
{
    DdNode *g = *gp;
    DdNode *h = *hp;

    if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
	*gp = base;
    }

    if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
	*hp = empty;
    }

} /* end of zddVarToConst */