cuddgencof.c

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

DdNode *
Cudd_bddLICompaction(
  DdManager * dd /* manager */,
  DdNode * f /* function to be minimized */,
  DdNode * c /* constraint (care set) */)
{
    DdNode *res;

    do {
	dd->reordered = 0;
	res = cuddBddLICompaction(dd,f,c);
    } while (dd->reordered == 1);
    return(res);

} /* end of Cudd_bddLICompaction */


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

  Synopsis    [Finds a small BDD in a function interval.]

  Description [Finds a small BDD in a function interval. Given BDDs
  <code>l</code> and <code>u</code>, representing the lower bound and
  upper bound of a function interval, Cudd_bddSqueeze produces the BDD
  of a function within the interval with a small BDD.  Returns a
  pointer to the result if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddRestrict Cudd_bddLICompaction]

******************************************************************************/
DdNode *
Cudd_bddSqueeze(
  DdManager * dd /* manager */,
  DdNode * l /* lower bound */,
  DdNode * u /* upper bound */)
{
    DdNode *res;
    int sizeRes, sizeL, sizeU;

    do {
	dd->reordered = 0;
	res = cuddBddSqueeze(dd,l,u);
    } while (dd->reordered == 1);
    if (res == NULL) return(NULL);
    /* We now compare the result with the bounds and return the smallest.
    ** We first compare to u, so that in case l == 0 and u == 1, we return
    ** 0 as in other minimization algorithms. */
    sizeRes = Cudd_DagSize(res);
    sizeU = Cudd_DagSize(u);
    if (sizeU <= sizeRes) {
	cuddRef(res);
	Cudd_IterDerefBdd(dd,res);
	res = u;
	sizeRes = sizeU;
    }
    sizeL = Cudd_DagSize(l);
    if (sizeL <= sizeRes) {
	cuddRef(res);
	Cudd_IterDerefBdd(dd,res);
	res = l;
	sizeRes = sizeL;
    }
    return(res);

} /* end of Cudd_bddSqueeze */


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

  Synopsis    [Finds a small BDD that agrees with <code>f</code> over
  <code>c</code>.]

  Description [Finds a small BDD that agrees with <code>f</code> over
  <code>c</code>.  Returns a pointer to the result if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddRestrict Cudd_bddLICompaction Cudd_bddSqueeze]

******************************************************************************/
DdNode *
Cudd_bddMinimize(
  DdManager * dd,
  DdNode * f,
  DdNode * c)
{
    DdNode *cplus, *res;

    if (c == Cudd_Not(DD_ONE(dd))) return(c);
    if (Cudd_IsConstant(f)) return(f);
    if (f == c) return(DD_ONE(dd));
    if (f == Cudd_Not(c)) return(Cudd_Not(DD_ONE(dd)));

    cplus = Cudd_RemapOverApprox(dd,c,0,0,1.0);
    if (cplus == NULL) return(NULL);
    cuddRef(cplus);
    res = Cudd_bddLICompaction(dd,f,cplus);
    if (res == NULL) {
	Cudd_IterDerefBdd(dd,cplus);
	return(NULL);
    }
    cuddRef(res);
    Cudd_IterDerefBdd(dd,cplus);
    cuddDeref(res);
    return(res);

} /* end of Cudd_bddMinimize */


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

  Synopsis    [Find a dense subset of BDD <code>f</code>.]

  Description [Finds a dense subset of BDD <code>f</code>. Density is
  the ratio of number of minterms to number of nodes.  Uses several
  techniques in series. It is more expensive than other subsetting
  procedures, but often produces better results. See
  Cudd_SubsetShortPaths for a description of the threshold and nvars
  parameters.  Returns a pointer to the result if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_SubsetRemap Cudd_SubsetShortPaths Cudd_SubsetHeavyBranch
  Cudd_bddSqueeze]

******************************************************************************/
DdNode *
Cudd_SubsetCompress(
  DdManager * dd /* manager */,
  DdNode * f /* BDD whose subset is sought */,
  int  nvars /* number of variables in the support of f */,
  int  threshold /* maximum number of nodes in the subset */)
{
    DdNode *res, *tmp1, *tmp2;

    tmp1 = Cudd_SubsetShortPaths(dd, f, nvars, threshold, 0);
    if (tmp1 == NULL) return(NULL);
    cuddRef(tmp1);
    tmp2 = Cudd_RemapUnderApprox(dd,tmp1,nvars,0,1.0);
    if (tmp2 == NULL) {
	Cudd_IterDerefBdd(dd,tmp1);
	return(NULL);
    }
    cuddRef(tmp2);
    Cudd_IterDerefBdd(dd,tmp1);
    res = Cudd_bddSqueeze(dd,tmp2,f);
    if (res == NULL) {
	Cudd_IterDerefBdd(dd,tmp2);
	return(NULL);
    }
    cuddRef(res);
    Cudd_IterDerefBdd(dd,tmp2);
    cuddDeref(res);
    return(res);

} /* end of Cudd_SubsetCompress */


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

  Synopsis    [Find a dense superset of BDD <code>f</code>.]

  Description [Finds a dense superset of BDD <code>f</code>. Density is
  the ratio of number of minterms to number of nodes.  Uses several
  techniques in series. It is more expensive than other supersetting
  procedures, but often produces better results. See
  Cudd_SupersetShortPaths for a description of the threshold and nvars
  parameters.  Returns a pointer to the result if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_SubsetCompress Cudd_SupersetRemap Cudd_SupersetShortPaths
  Cudd_SupersetHeavyBranch Cudd_bddSqueeze]

******************************************************************************/
DdNode *
Cudd_SupersetCompress(
  DdManager * dd /* manager */,
  DdNode * f /* BDD whose superset is sought */,
  int  nvars /* number of variables in the support of f */,
  int  threshold /* maximum number of nodes in the superset */)
{
    DdNode *subset;

    subset = Cudd_SubsetCompress(dd, Cudd_Not(f),nvars,threshold);

    return(Cudd_NotCond(subset, (subset != NULL)));

} /* end of Cudd_SupersetCompress */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


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

  Synopsis    [Performs the recursive step of Cudd_bddConstrain.]

  Description [Performs the recursive step of Cudd_bddConstrain.
  Returns a pointer to the result if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddConstrain]

******************************************************************************/
DdNode *
cuddBddConstrainRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * c)
{
    DdNode       *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r;
    DdNode	 *one, *zero;
    unsigned int topf, topc;
    int		 index;
    int          comple = 0;

    statLine(dd);
    one = DD_ONE(dd);
    zero = Cudd_Not(one);

    /* Trivial cases. */
    if (c == one)		return(f);
    if (c == zero)		return(zero);
    if (Cudd_IsConstant(f))	return(f);
    if (f == c)			return(one);
    if (f == Cudd_Not(c))	return(zero);

    /* Make canonical to increase the utilization of the cache. */
    if (Cudd_IsComplement(f)) {
	f = Cudd_Not(f);
	comple = 1;
    }
    /* Now f is a regular pointer to a non-constant node; c is also
    ** non-constant, but may be complemented.
    */

    /* Check the cache. */
    r = cuddCacheLookup2(dd, Cudd_bddConstrain, f, c);
    if (r != NULL) {
	return(Cudd_NotCond(r,comple));
    }
    
    /* Recursive step. */
    topf = dd->perm[f->index];
    topc = dd->perm[Cudd_Regular(c)->index];
    if (topf <= topc) {
	index = f->index;
	Fv = cuddT(f); Fnv = cuddE(f);
    } else {
	index = Cudd_Regular(c)->index;
	Fv = Fnv = f;
    }
    if (topc <= topf) {
	Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
	if (Cudd_IsComplement(c)) {
	    Cv = Cudd_Not(Cv);
	    Cnv = Cudd_Not(Cnv);
	}
    } else {
	Cv = Cnv = c;
    }

    if (!Cudd_IsConstant(Cv)) {
	t = cuddBddConstrainRecur(dd, Fv, Cv);
	if (t == NULL)
	    return(NULL);
    } else if (Cv == one) {
	t = Fv;
    } else {		/* Cv == zero: return Fnv @ Cnv */
	if (Cnv == one) {
	    r = Fnv;
	} else {
	    r = cuddBddConstrainRecur(dd, Fnv, Cnv);
	    if (r == NULL)
		return(NULL);
	}
	return(Cudd_NotCond(r,comple));
    }
    cuddRef(t);

    if (!Cudd_IsConstant(Cnv)) {
	e = cuddBddConstrainRecur(dd, Fnv, Cnv);
	if (e == NULL) {
	    Cudd_IterDerefBdd(dd, t);
	    return(NULL);
	}
    } else if (Cnv == one) {
	e = Fnv;
    } else {		/* Cnv == zero: return Fv @ Cv previously computed */
	cuddDeref(t);
	return(Cudd_NotCond(t,comple));
    }
    cuddRef(e);

    if (Cudd_IsComplement(t)) {
	t = Cudd_Not(t);
	e = Cudd_Not(e);
	r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
	if (r == NULL) {
	    Cudd_IterDerefBdd(dd, e);
	    Cudd_IterDerefBdd(dd, t);
	    return(NULL);
	}
	r = Cudd_Not(r);
    } else {
	r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
	if (r == NULL) {
	    Cudd_IterDerefBdd(dd, e);
	    Cudd_IterDerefBdd(dd, t);
	    return(NULL);
	}
    }
    cuddDeref(t);
    cuddDeref(e);

    cuddCacheInsert2(dd, Cudd_bddConstrain, f, c, r);
    return(Cudd_NotCond(r,comple));

} /* end of cuddBddConstrainRecur */


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

  Synopsis    [Performs the recursive step of Cudd_bddRestrict.]

  Description [Performs the recursive step of Cudd_bddRestrict.
  Returns the restricted BDD if successful; otherwise NULL.]

  SideEffects [None]

  SeeAlso     [Cudd_bddRestrict]

******************************************************************************/
DdNode *
cuddBddRestrictRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * c)
{
    DdNode	 *Fv, *Fnv, *Cv, *Cnv, *t, *e, *r, *one, *zero;
    unsigned int topf, topc;
    int		 index;
    int		 comple = 0;

    statLine(dd);
    one = DD_ONE(dd);
    zero = Cudd_Not(one);

    /* Trivial cases */
    if (c == one)		return(f);
    if (c == zero)		return(zero);
    if (Cudd_IsConstant(f))	return(f);
    if (f == c)			return(one);
    if (f == Cudd_Not(c))	return(zero);

    /* Make canonical to increase the utilization of the cache. */
    if (Cudd_IsComplement(f)) {
	f = Cudd_Not(f);
	comple = 1;
    }
    /* Now f is a regular pointer to a non-constant node; c is also
    ** non-constant, but may be complemented.
    */

    /* Check the cache. */
    r = cuddCacheLookup2(dd, Cudd_bddRestrict, f, c);
    if (r != NULL) {
	return(Cudd_NotCond(r,comple));
    }

    topf = dd->perm[f->index];
    topc = dd->perm[Cudd_Regular(c)->index];

    if (topc < topf) {	/* abstract top variable from c */
	DdNode *d, *s1, *s2;

	/* Find complements of cofactors of c. */
	if (Cudd_IsComplement(c)) {
	    s1 = cuddT(Cudd_Regular(c));
	    s2 = cuddE(Cudd_Regular(c));
	} else {
	    s1 = Cudd_Not(cuddT(c));
	    s2 = Cudd_Not(cuddE(c));
	}
	/* Take the OR by applying DeMorgan. */
	d = cuddBddAndRecur(dd, s1, s2);
	if (d == NULL) return(NULL);
	d = Cudd_Not(d);
	cuddRef(d);
	r = cuddBddRestrictRecur(dd, f, d);
	if (r == NULL) {
	    Cudd_IterDerefBdd(dd, d);
	    return(NULL);
	}
	cuddRef(r);
	Cudd_IterDerefBdd(dd, d);
	cuddCacheInsert2(dd, Cudd_bddRestrict, f, c, r);
	cuddDeref(r);
	return(Cudd_NotCond(r,comple));
    }

    /* Recursive step. Here topf <= topc. */
    index = f->index;
    Fv = cuddT(f); Fnv = cuddE(f);
    if (topc == topf) {
	Cv = cuddT(Cudd_Regular(c)); Cnv = cuddE(Cudd_Regular(c));
	if (Cudd_IsComplement(c)) {
	    Cv = Cudd_Not(Cv);
	    Cnv = Cudd_Not(Cnv);
	}
    } else {
	Cv = Cnv = c;
    }

    if (!Cudd_IsConstant(Cv)) {
	t = cuddBddRestrictRecur(dd, Fv, Cv);
	if (t == NULL) return(NULL);
    } else if (Cv == one) {
	t = Fv;
    } else {		/* Cv == zero: return(Fnv @ Cnv) */
	if (Cnv == one) {
	    r = Fnv;
	} else {
	    r = cuddBddRestrictRecur(dd, Fnv, Cnv);
	    if (r == NULL) return(NULL);
	}
	return(Cudd_NotCond(r,comple));
    }
    cuddRef(t);

    if (!Cudd_IsConstant(Cnv)) {
	e = cuddBddRestrictRecur(dd, Fnv, Cnv);
	if (e == NULL) {
	    Cudd_IterDerefBdd(dd, t);
	    return(NULL);
	}
    } else if (Cnv == one) {
	e = Fnv;
    } else {		/* Cnv == zero: return (Fv @ Cv) previously computed */
	cuddDeref(t);
	return(Cudd_NotCond(t,comple));
    }
    cuddRef(e);

    if (Cudd_IsComplement(t)) {
	t = Cudd_Not(t);
	e = Cudd_Not(e);
	r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
	if (r == NULL) {
	    Cudd_IterDerefBdd(dd, e);
	    Cudd_IterDerefBdd(dd, t);
	    return(NULL);
	}
	r = Cudd_Not(r);
    } else {
	r = (t == e) ? t : cuddUniqueInter(dd, index, t, e);
	if (r == NULL) {
	    Cudd_IterDerefBdd(dd, e);
	    Cudd_IterDerefBdd(dd, t);
	    return(NULL);
	}
    }
    cuddDeref(t);
    cuddDeref(e);

    cuddCacheInsert2(dd, Cudd_bddRestrict, f, c, r);
    return(Cudd_NotCond(r,comple));

} /* end of cuddBddRestrictRecur */


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

  Synopsis    [Performs the recursive step of Cudd_addConstrain.]

  Description [Performs the recursive step of Cudd_addConstrain.
  Returns a pointer to the result if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addConstrain]

******************************************************************************/
DdNode *