cuddzddfuncs.c

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

    }

    if (q == zero) {
	Cudd_RecursiveDerefZdd(dd, fd);
	Cudd_RecursiveDerefZdd(dd, gd);
	cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, zero);
	Cudd_Deref(q);
	return(zero);
    }

    if (gd != zero) {
	Cudd_RecursiveDerefZdd(dd, q);
	tmp = cuddZddWeakDivF(dd, fd, gd);
	if (tmp == NULL) {
	    Cudd_RecursiveDerefZdd(dd, fd);
	    Cudd_RecursiveDerefZdd(dd, gd);
	    return(NULL);
	}
	Cudd_Ref(tmp);
	Cudd_RecursiveDerefZdd(dd, fd);
	Cudd_RecursiveDerefZdd(dd, gd);
	if (q == g)
	    q = tmp;
	else {
	    q = cuddZddIntersect(dd, q, tmp);
	    if (q == NULL) {
		Cudd_RecursiveDerefZdd(dd, tmp);
		return(NULL);
	    }
	    Cudd_Ref(q);
	    Cudd_RecursiveDerefZdd(dd, tmp);
	}
    }
    else {
	Cudd_RecursiveDerefZdd(dd, fd);
	Cudd_RecursiveDerefZdd(dd, gd);
    }

    cuddCacheInsert2(dd, cuddZddWeakDivF, f, g, q);
    Cudd_Deref(q);
    return(q);

} /* end of cuddZddWeakDivF */


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

  Synopsis    [Performs the recursive step of Cudd_zddDivide.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_zddDivide]

******************************************************************************/
DdNode	*
cuddZddDivide(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    int		v;
    DdNode	*one = DD_ONE(dd);
    DdNode	*zero = DD_ZERO(dd);
    DdNode	*f0, *f1, *g0, *g1;
    DdNode	*q, *r, *tmp;
    int		flag;

    statLine(dd);
    if (g == one)
	return(f);
    if (f == zero || f == one)
	return(zero);
    if (f == g)
	return(one);

    /* Check cache. */
    r = cuddCacheLookup2Zdd(dd, cuddZddDivide, f, g);
    if (r)
	return(r);

    v = g->index;

    flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
    if (flag == 1)
	return(NULL);
    Cudd_Ref(f1);
    Cudd_Ref(f0);
    flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);	/* g1 != zero */
    if (flag == 1) {
	Cudd_RecursiveDerefZdd(dd, f1);
	Cudd_RecursiveDerefZdd(dd, f0);
	return(NULL);
    }
    Cudd_Ref(g1);
    Cudd_Ref(g0);

    r = cuddZddDivide(dd, f1, g1);
    if (r == NULL) {
	Cudd_RecursiveDerefZdd(dd, f1);
	Cudd_RecursiveDerefZdd(dd, f0);
	Cudd_RecursiveDerefZdd(dd, g1);
	Cudd_RecursiveDerefZdd(dd, g0);
	return(NULL);
    }
    Cudd_Ref(r);

    if (r != zero && g0 != zero) {
	tmp = r;
	q = cuddZddDivide(dd, f0, g0);
	if (q == NULL) {
	    Cudd_RecursiveDerefZdd(dd, f1);
	    Cudd_RecursiveDerefZdd(dd, f0);
	    Cudd_RecursiveDerefZdd(dd, g1);
	    Cudd_RecursiveDerefZdd(dd, g0);
	    return(NULL);
	}
	Cudd_Ref(q);
	r = cuddZddIntersect(dd, r, q);
	if (r == NULL) {
	    Cudd_RecursiveDerefZdd(dd, f1);
	    Cudd_RecursiveDerefZdd(dd, f0);
	    Cudd_RecursiveDerefZdd(dd, g1);
	    Cudd_RecursiveDerefZdd(dd, g0);
	    Cudd_RecursiveDerefZdd(dd, q);
	    return(NULL);
	}
	Cudd_Ref(r);
	Cudd_RecursiveDerefZdd(dd, q);
	Cudd_RecursiveDerefZdd(dd, tmp);
    }

    Cudd_RecursiveDerefZdd(dd, f1);
    Cudd_RecursiveDerefZdd(dd, f0);
    Cudd_RecursiveDerefZdd(dd, g1);
    Cudd_RecursiveDerefZdd(dd, g0);
    
    cuddCacheInsert2(dd, cuddZddDivide, f, g, r);
    Cudd_Deref(r);
    return(r);

} /* end of cuddZddDivide */


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

  Synopsis    [Performs the recursive step of Cudd_zddDivideF.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_zddDivideF]

******************************************************************************/
DdNode	*
cuddZddDivideF(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    int		v;
    DdNode	*one = DD_ONE(dd);
    DdNode	*zero = DD_ZERO(dd);
    DdNode	*f0, *f1, *g0, *g1;
    DdNode	*q, *r, *tmp;
    int		flag;

    statLine(dd);
    if (g == one)
	return(f);
    if (f == zero || f == one)
	return(zero);
    if (f == g)
	return(one);

    /* Check cache. */
    r = cuddCacheLookup2Zdd(dd, cuddZddDivideF, f, g);
    if (r)
	return(r);

    v = g->index;

    flag = cuddZddGetCofactors2(dd, f, v, &f1, &f0);
    if (flag == 1)
	return(NULL);
    Cudd_Ref(f1);
    Cudd_Ref(f0);
    flag = cuddZddGetCofactors2(dd, g, v, &g1, &g0);	/* g1 != zero */
    if (flag == 1) {
	Cudd_RecursiveDerefZdd(dd, f1);
	Cudd_RecursiveDerefZdd(dd, f0);
	return(NULL);
    }
    Cudd_Ref(g1);
    Cudd_Ref(g0);

    r = cuddZddDivideF(dd, f1, g1);
    if (r == NULL) {
	Cudd_RecursiveDerefZdd(dd, f1);
	Cudd_RecursiveDerefZdd(dd, f0);
	Cudd_RecursiveDerefZdd(dd, g1);
	Cudd_RecursiveDerefZdd(dd, g0);
	return(NULL);
    }
    Cudd_Ref(r);

    if (r != zero && g0 != zero) {
	tmp = r;
	q = cuddZddDivideF(dd, f0, g0);
	if (q == NULL) {
	    Cudd_RecursiveDerefZdd(dd, f1);
	    Cudd_RecursiveDerefZdd(dd, f0);
	    Cudd_RecursiveDerefZdd(dd, g1);
	    Cudd_RecursiveDerefZdd(dd, g0);
	    return(NULL);
	}
	Cudd_Ref(q);
	r = cuddZddIntersect(dd, r, q);
	if (r == NULL) {
	    Cudd_RecursiveDerefZdd(dd, f1);
	    Cudd_RecursiveDerefZdd(dd, f0);
	    Cudd_RecursiveDerefZdd(dd, g1);
	    Cudd_RecursiveDerefZdd(dd, g0);
	    Cudd_RecursiveDerefZdd(dd, q);
	    return(NULL);
	}
	Cudd_Ref(r);
	Cudd_RecursiveDerefZdd(dd, q);
	Cudd_RecursiveDerefZdd(dd, tmp);
    }

    Cudd_RecursiveDerefZdd(dd, f1);
    Cudd_RecursiveDerefZdd(dd, f0);
    Cudd_RecursiveDerefZdd(dd, g1);
    Cudd_RecursiveDerefZdd(dd, g0);
    
    cuddCacheInsert2(dd, cuddZddDivideF, f, g, r);
    Cudd_Deref(r);
    return(r);

} /* end of cuddZddDivideF */


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

  Synopsis    [Computes the three-way decomposition of f w.r.t. v.]

  Description [Computes the three-way decomposition of function f (represented
  by a ZDD) wit respect to variable v.]

  SideEffects [The results are returned in f1, f0, and fd.]

  SeeAlso     [cuddZddGetCofactors2]

******************************************************************************/
int
cuddZddGetCofactors3(
  DdManager * dd,
  DdNode * f,
  int  v,
  DdNode ** f1,
  DdNode ** f0,
  DdNode ** fd)
{
    DdNode	*pc, *nc;
    DdNode	*zero = DD_ZERO(dd);
    int		top, hv, ht, pv, nv;
    int		level;

    top = dd->permZ[f->index];
    level = dd->permZ[v];
    hv = level >> 1;
    ht = top >> 1;

    if (hv < ht) {
	*f1 = zero;
	*f0 = zero;
	*fd = f;
    }
    else {
	pv = cuddZddGetPosVarIndex(dd, v);
	nv = cuddZddGetNegVarIndex(dd, v);

	/* not to create intermediate ZDD node */
	if (cuddZddGetPosVarLevel(dd, v) < cuddZddGetNegVarLevel(dd, v)) {
	    pc = cuddZddSubset1(dd, f, pv);
	    if (pc == NULL)
		return(1);
	    Cudd_Ref(pc);
	    nc = cuddZddSubset0(dd, f, pv);
	    if (nc == NULL) {
		Cudd_RecursiveDerefZdd(dd, pc);
		return(1);
	    }
	    Cudd_Ref(nc);

	    *f1 = cuddZddSubset0(dd, pc, nv);
	    if (*f1 == NULL) {
		Cudd_RecursiveDerefZdd(dd, pc);
		Cudd_RecursiveDerefZdd(dd, nc);
		return(1);
	    }
	    Cudd_Ref(*f1);
	    *f0 = cuddZddSubset1(dd, nc, nv);
	    if (*f0 == NULL) {
		Cudd_RecursiveDerefZdd(dd, pc);
		Cudd_RecursiveDerefZdd(dd, nc);
		Cudd_RecursiveDerefZdd(dd, *f1);
		return(1);
	    }
	    Cudd_Ref(*f0);

	    *fd = cuddZddSubset0(dd, nc, nv);
	    if (*fd == NULL) {
		Cudd_RecursiveDerefZdd(dd, pc);
		Cudd_RecursiveDerefZdd(dd, nc);
		Cudd_RecursiveDerefZdd(dd, *f1);
		Cudd_RecursiveDerefZdd(dd, *f0);
		return(1);
	    }
	    Cudd_Ref(*fd);
	} else {
	    pc = cuddZddSubset1(dd, f, nv);
	    if (pc == NULL)
		return(1);
	    Cudd_Ref(pc);
	    nc = cuddZddSubset0(dd, f, nv);
	    if (nc == NULL) {
		Cudd_RecursiveDerefZdd(dd, pc);
		return(1);
	    }
	    Cudd_Ref(nc);

	    *f0 = cuddZddSubset0(dd, pc, pv);
	    if (*f0 == NULL) {
		Cudd_RecursiveDerefZdd(dd, pc);
		Cudd_RecursiveDerefZdd(dd, nc);
		return(1);
	    }
	    Cudd_Ref(*f0);
	    *f1 = cuddZddSubset1(dd, nc, pv);
	    if (*f1 == NULL) {
		Cudd_RecursiveDerefZdd(dd, pc);
		Cudd_RecursiveDerefZdd(dd, nc);
		Cudd_RecursiveDerefZdd(dd, *f1);
		return(1);
	    }
	    Cudd_Ref(*f1);

	    *fd = cuddZddSubset0(dd, nc, pv);
	    if (*fd == NULL) {
		Cudd_RecursiveDerefZdd(dd, pc);
		Cudd_RecursiveDerefZdd(dd, nc);
		Cudd_RecursiveDerefZdd(dd, *f1);
		Cudd_RecursiveDerefZdd(dd, *f0);
		return(1);
	    }
	    Cudd_Ref(*fd);
	}

	Cudd_RecursiveDerefZdd(dd, pc);
	Cudd_RecursiveDerefZdd(dd, nc);
	Cudd_Deref(*f1);
	Cudd_Deref(*f0);
	Cudd_Deref(*fd);
    }
    return(0);

} /* end of cuddZddGetCofactors3 */


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

  Synopsis    [Computes the two-way decomposition of f w.r.t. v.]

  Description []

  SideEffects [The results are returned in f1 and f0.]

  SeeAlso     [cuddZddGetCofactors3]

******************************************************************************/
int
cuddZddGetCofactors2(
  DdManager * dd,
  DdNode * f,
  int  v,
  DdNode ** f1,
  DdNode ** f0)
{
    *f1 = cuddZddSubset1(dd, f, v);
    if (*f1 == NULL)
	return(1);
    *f0 = cuddZddSubset0(dd, f, v);
    if (*f0 == NULL) {
	Cudd_RecursiveDerefZdd(dd, *f1);
	return(1);
    }
    return(0);

} /* end of cuddZddGetCofactors2 */


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

  Synopsis    [Computes a complement of a ZDD node.]

  Description [Computes the complement of a ZDD node. So far, since we
  couldn't find a direct way to get the complement of a ZDD cover, we first
  convert a ZDD cover to a BDD, then make the complement of the ZDD cover
  from the complement of the BDD node by using ISOP.]

  SideEffects [The result depends on current variable order.]

  SeeAlso     []

******************************************************************************/
DdNode	*
cuddZddComplement(
  DdManager * dd,
  DdNode *node)
{
    DdNode	*b, *isop, *zdd_I;

    /* Check cache */
    zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node);
    if (zdd_I)
	return(zdd_I);

    b = cuddMakeBddFromZddCover(dd, node);
    if (!b)
	return(NULL);
    cuddRef(b);
    isop = cuddZddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I);
    if (!isop) {
	Cudd_RecursiveDeref(dd, b);
	return(NULL);
    }
    cuddRef(isop);
    cuddRef(zdd_I);
    Cudd_RecursiveDeref(dd, b);
    Cudd_RecursiveDeref(dd, isop);

    cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I);
    cuddDeref(zdd_I);
    return(zdd_I);
} /* end of cuddZddComplement */


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

  Synopsis    [Returns the index of positive ZDD variable.]

  Description [Returns the index of positive ZDD variable.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
cuddZddGetPosVarIndex(
  DdManager * dd,
  int index)
{
    int	pv = (index >> 1) << 1;
    return(pv);
} /* end of cuddZddGetPosVarIndex */


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

  Synopsis    [Returns the index of negative ZDD variable.]

  Description [Returns the index of negative ZDD variable.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
cuddZddGetNegVarIndex(
  DdManager * dd,
  int index)
{
    int	nv = index | 0x1;
    return(nv);
} /* end of cuddZddGetPosVarIndex */


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

  Synopsis    [Returns the level of positive ZDD variable.]

  Description [Returns the level of positive ZDD variable.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
cuddZddGetPosVarLevel(
  DdManager * dd,
  int index)
{
    int	pv = cuddZddGetPosVarIndex(dd, index);
    return(dd->permZ[pv]);
} /* end of cuddZddGetPosVarLevel */


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

  Synopsis    [Returns the level of negative ZDD variable.]

  Description [Returns the level of negative ZDD variable.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
cuddZddGetNegVarLevel(
  DdManager * dd,
  int index)
{
    int	nv = cuddZddGetNegVarIndex(dd, index);
    return(dd->permZ[nv]);
} /* end of cuddZddGetNegVarLevel */