cuddzddfuncs.c

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

    tmp = cuddZddUnion(dd, term1, term2);
    if (tmp == NULL) {
	Cudd_RecursiveDerefZdd(dd, N0);
	Cudd_RecursiveDerefZdd(dd, term1);
	Cudd_RecursiveDerefZdd(dd, term2);
	Cudd_RecursiveDerefZdd(dd, term3);
	return(NULL);
    }
    Cudd_Ref(tmp);
    Cudd_RecursiveDerefZdd(dd, term1);
    Cudd_RecursiveDerefZdd(dd, term2);
    R1 = cuddZddUnion(dd, tmp, term3);
    if (R1 == NULL) {
	Cudd_RecursiveDerefZdd(dd, N0);
	Cudd_RecursiveDerefZdd(dd, term3);
	Cudd_RecursiveDerefZdd(dd, tmp);
	return(NULL);
    }
    Cudd_Ref(R1);
    Cudd_RecursiveDerefZdd(dd, tmp);
    Cudd_RecursiveDerefZdd(dd, term3);
    N1 = cuddZddGetNode(dd, pv, R1, N0); /* pv = yi */
    if (N1 == NULL) {
	Cudd_RecursiveDerefZdd(dd, N0);
	Cudd_RecursiveDerefZdd(dd, R1);
	return(NULL);
    }
    Cudd_Ref(N1);
    Cudd_RecursiveDerefZdd(dd, R1);
    Cudd_RecursiveDerefZdd(dd, N0);

    cuddCacheInsert2(dd, cuddZddProduct, f, g, N1);
    Cudd_Deref(N1);
    return(N1);

} /* end of cuddZddProduct */


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

  Synopsis    [Performs the recursive step of Cudd_zddUnateProduct.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_zddUnateProduct]

******************************************************************************/
DdNode	*
cuddZddUnateProduct(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    int		v, top_f, top_g;
    DdNode	*term1, *term2, *term3, *term4;
    DdNode	*sum1, *sum2;
    DdNode	*f0, *f1, *g0, *g1;
    DdNode	*r;
    DdNode	*one = DD_ONE(dd);
    DdNode	*zero = DD_ZERO(dd);
    int		flag;

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

    top_f = dd->permZ[f->index];
    top_g = dd->permZ[g->index];

    if (top_f > top_g)
	return(cuddZddUnateProduct(dd, g, f));

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

    v = f->index;	/* either yi or zi */
    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);
    if (flag == 1) {
	Cudd_RecursiveDerefZdd(dd, f1);
	Cudd_RecursiveDerefZdd(dd, f0);
	return(NULL);
    }
    Cudd_Ref(g1);
    Cudd_Ref(g0);

    term1 = cuddZddUnateProduct(dd, f1, g1);
    if (term1 == NULL) {
	Cudd_RecursiveDerefZdd(dd, f1);
	Cudd_RecursiveDerefZdd(dd, f0);
	Cudd_RecursiveDerefZdd(dd, g1);
	Cudd_RecursiveDerefZdd(dd, g0);
	return(NULL);
    }
    Cudd_Ref(term1);
    term2 = cuddZddUnateProduct(dd, f1, g0);
    if (term2 == NULL) {
	Cudd_RecursiveDerefZdd(dd, f1);
	Cudd_RecursiveDerefZdd(dd, f0);
	Cudd_RecursiveDerefZdd(dd, g1);
	Cudd_RecursiveDerefZdd(dd, g0);
	Cudd_RecursiveDerefZdd(dd, term1);
	return(NULL);
    }
    Cudd_Ref(term2);
    term3 = cuddZddUnateProduct(dd, f0, g1);
    if (term3 == NULL) {
	Cudd_RecursiveDerefZdd(dd, f1);
	Cudd_RecursiveDerefZdd(dd, f0);
	Cudd_RecursiveDerefZdd(dd, g1);
	Cudd_RecursiveDerefZdd(dd, g0);
	Cudd_RecursiveDerefZdd(dd, term1);
	Cudd_RecursiveDerefZdd(dd, term2);
	return(NULL);
    }
    Cudd_Ref(term3);
    term4 = cuddZddUnateProduct(dd, f0, g0);
    if (term4 == NULL) {
	Cudd_RecursiveDerefZdd(dd, f1);
	Cudd_RecursiveDerefZdd(dd, f0);
	Cudd_RecursiveDerefZdd(dd, g1);
	Cudd_RecursiveDerefZdd(dd, g0);
	Cudd_RecursiveDerefZdd(dd, term1);
	Cudd_RecursiveDerefZdd(dd, term2);
	Cudd_RecursiveDerefZdd(dd, term3);
	return(NULL);
    }
    Cudd_Ref(term4);
    Cudd_RecursiveDerefZdd(dd, f1);
    Cudd_RecursiveDerefZdd(dd, f0);
    Cudd_RecursiveDerefZdd(dd, g1);
    Cudd_RecursiveDerefZdd(dd, g0);
    sum1 = cuddZddUnion(dd, term1, term2);
    if (sum1 == NULL) {
	Cudd_RecursiveDerefZdd(dd, term1);
	Cudd_RecursiveDerefZdd(dd, term2);
	Cudd_RecursiveDerefZdd(dd, term3);
	Cudd_RecursiveDerefZdd(dd, term4);
	return(NULL);
    }
    Cudd_Ref(sum1);
    Cudd_RecursiveDerefZdd(dd, term1);
    Cudd_RecursiveDerefZdd(dd, term2);
    sum2 = cuddZddUnion(dd, sum1, term3);
    if (sum2 == NULL) {
	Cudd_RecursiveDerefZdd(dd, term3);
	Cudd_RecursiveDerefZdd(dd, term4);
	Cudd_RecursiveDerefZdd(dd, sum1);
	return(NULL);
    }
    Cudd_Ref(sum2);
    Cudd_RecursiveDerefZdd(dd, sum1);
    Cudd_RecursiveDerefZdd(dd, term3);
    r = cuddZddGetNode(dd, v, sum2, term4);
    if (r == NULL) {
	Cudd_RecursiveDerefZdd(dd, term4);
	Cudd_RecursiveDerefZdd(dd, sum2);
	return(NULL);
    }
    Cudd_Ref(r);
    Cudd_RecursiveDerefZdd(dd, sum2);
    Cudd_RecursiveDerefZdd(dd, term4);

    cuddCacheInsert2(dd, cuddZddUnateProduct, f, g, r);
    Cudd_Deref(r);
    return(r);

} /* end of cuddZddUnateProduct */


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

  Synopsis    [Performs the recursive step of Cudd_zddWeakDiv.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_zddWeakDiv]

******************************************************************************/
DdNode	*
cuddZddWeakDiv(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    int		v;
    DdNode	*one = DD_ONE(dd);
    DdNode	*zero = DD_ZERO(dd);
    DdNode	*f0, *f1, *fd, *g0, *g1, *gd;
    DdNode	*q, *tmp;
    DdNode	*r;
    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, cuddZddWeakDiv, f, g);
    if (r)
	return(r);

    v = g->index;

    flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
    if (flag == 1)
	return(NULL);
    Cudd_Ref(f1);
    Cudd_Ref(f0);
    Cudd_Ref(fd);
    flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
    if (flag == 1) {
	Cudd_RecursiveDerefZdd(dd, f1);
	Cudd_RecursiveDerefZdd(dd, f0);
	Cudd_RecursiveDerefZdd(dd, fd);
	return(NULL);
    }
    Cudd_Ref(g1);
    Cudd_Ref(g0);
    Cudd_Ref(gd);

    q = g;

    if (g0 != zero) {
	q = cuddZddWeakDiv(dd, f0, g0);
	if (q == NULL) {
	    Cudd_RecursiveDerefZdd(dd, f1);
	    Cudd_RecursiveDerefZdd(dd, f0);
	    Cudd_RecursiveDerefZdd(dd, fd);
	    Cudd_RecursiveDerefZdd(dd, g1);
	    Cudd_RecursiveDerefZdd(dd, g0);
	    Cudd_RecursiveDerefZdd(dd, gd);
	    return(NULL);
	}
	Cudd_Ref(q);
    }
    else
	Cudd_Ref(q);
    Cudd_RecursiveDerefZdd(dd, f0);
    Cudd_RecursiveDerefZdd(dd, g0);

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

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

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

    if (gd != zero) {
	Cudd_RecursiveDerefZdd(dd, q);
	tmp = cuddZddWeakDiv(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, cuddZddWeakDiv, f, g, q);
    Cudd_Deref(q);
    return(q);

} /* end of cuddZddWeakDiv */


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

  Synopsis    [Performs the recursive step of Cudd_zddWeakDivF.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_zddWeakDivF]

******************************************************************************/
DdNode	*
cuddZddWeakDivF(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    int		v, top_f, top_g, vf, vg;
    DdNode	*one = DD_ONE(dd);
    DdNode	*zero = DD_ZERO(dd);
    DdNode	*f0, *f1, *fd, *g0, *g1, *gd;
    DdNode	*q, *tmp;
    DdNode	*r;
    DdNode	*term1, *term0, *termd;
    int		flag;
    int		pv, nv;

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

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

    top_f = dd->permZ[f->index];
    top_g = dd->permZ[g->index];
    vf = top_f >> 1;
    vg = top_g >> 1;
    v = ddMin(top_f, top_g);

    if (v == top_f && vf < vg) {
	v = f->index;
	flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
	if (flag == 1)
	    return(NULL);
	Cudd_Ref(f1);
	Cudd_Ref(f0);
	Cudd_Ref(fd);

	pv = cuddZddGetPosVarIndex(dd, v);
	nv = cuddZddGetNegVarIndex(dd, v);

	term1 = cuddZddWeakDivF(dd, f1, g);
	if (term1 == NULL) {
	    Cudd_RecursiveDerefZdd(dd, f1);
	    Cudd_RecursiveDerefZdd(dd, f0);
	    Cudd_RecursiveDerefZdd(dd, fd);
	    return(NULL);
	}
	Cudd_Ref(term1);
	Cudd_RecursiveDerefZdd(dd, f1);
	term0 = cuddZddWeakDivF(dd, f0, g);
	if (term0 == NULL) {
	    Cudd_RecursiveDerefZdd(dd, f0);
	    Cudd_RecursiveDerefZdd(dd, fd);
	    Cudd_RecursiveDerefZdd(dd, term1);
	    return(NULL);
	}
	Cudd_Ref(term0);
	Cudd_RecursiveDerefZdd(dd, f0);
	termd = cuddZddWeakDivF(dd, fd, g);
	if (termd == NULL) {
	    Cudd_RecursiveDerefZdd(dd, fd);
	    Cudd_RecursiveDerefZdd(dd, term1);
	    Cudd_RecursiveDerefZdd(dd, term0);
	    return(NULL);
	}
	Cudd_Ref(termd);
	Cudd_RecursiveDerefZdd(dd, fd);

	tmp = cuddZddGetNode(dd, nv, term0, termd); /* nv = zi */
	if (tmp == NULL) {
	    Cudd_RecursiveDerefZdd(dd, term1);
	    Cudd_RecursiveDerefZdd(dd, term0);
	    Cudd_RecursiveDerefZdd(dd, termd);
	    return(NULL);
	}
	Cudd_Ref(tmp);
	Cudd_RecursiveDerefZdd(dd, term0);
	Cudd_RecursiveDerefZdd(dd, termd);
	q = cuddZddGetNode(dd, pv, term1, tmp); /* pv = yi */
	if (q == NULL) {
	    Cudd_RecursiveDerefZdd(dd, term1);
	    Cudd_RecursiveDerefZdd(dd, tmp);
	    return(NULL);
	}
	Cudd_Ref(q);
	Cudd_RecursiveDerefZdd(dd, term1);
	Cudd_RecursiveDerefZdd(dd, tmp);

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

    if (v == top_f)
	v = f->index;
    else
	v = g->index;

    flag = cuddZddGetCofactors3(dd, f, v, &f1, &f0, &fd);
    if (flag == 1)
	return(NULL);
    Cudd_Ref(f1);
    Cudd_Ref(f0);
    Cudd_Ref(fd);
    flag = cuddZddGetCofactors3(dd, g, v, &g1, &g0, &gd);
    if (flag == 1) {
	Cudd_RecursiveDerefZdd(dd, f1);
	Cudd_RecursiveDerefZdd(dd, f0);
	Cudd_RecursiveDerefZdd(dd, fd);
	return(NULL);
    }
    Cudd_Ref(g1);
    Cudd_Ref(g0);
    Cudd_Ref(gd);

    q = g;

    if (g0 != zero) {
	q = cuddZddWeakDivF(dd, f0, g0);
	if (q == NULL) {
	    Cudd_RecursiveDerefZdd(dd, f1);
	    Cudd_RecursiveDerefZdd(dd, f0);
	    Cudd_RecursiveDerefZdd(dd, fd);
	    Cudd_RecursiveDerefZdd(dd, g1);
	    Cudd_RecursiveDerefZdd(dd, g0);
	    Cudd_RecursiveDerefZdd(dd, gd);
	    return(NULL);
	}
	Cudd_Ref(q);
    }
    else
	Cudd_Ref(q);
    Cudd_RecursiveDerefZdd(dd, f0);
    Cudd_RecursiveDerefZdd(dd, g0);

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

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