cuddpriority.c

来自「主要进行大规模的电路综合」· C语言 代码 · 共 1,476 行 · 第 1/3 页

	    return(NULL);
	}
	cuddRef(res2);
	res = cuddBddIteRecur(dd, dd->vars[index], res1, res2);
	if (res == NULL) {
	    Cudd_RecursiveDeref(dd,res1);
	    Cudd_RecursiveDeref(dd,res2);
	    return(NULL);
	}
	/* If we have reached this point, res1 and res2 are now
	** incorporated in res. cuddDeref is therefore sufficient.
	*/
	cuddDeref(res1);
	cuddDeref(res2);
    } else {
	/* Compute the cofactors of Y */
	index = y->index;
	YT = cuddT(y);
	YE = cuddE(y);
	if (y != Y) {
	    YT = Cudd_Not(YT); YE = Cudd_Not(YE);
	}
	if (YT == Cudd_Not(one)) {
	    Alpha  = Cudd_Not(dd->vars[index]);
	    Yrest = YE;
	    Ra = RE;
	    Ran = RT;
	} else {
	    Alpha = dd->vars[index];
	    Yrest = YT;
	    Ra = RT;
	    Ran = RE;
	}
	Gamma = cuddBddExistAbstractRecur(dd,Ra,cuddT(Ysupp));
	if (Gamma == NULL) return(NULL);
	if (Gamma == one) {
	    res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp));
	    if (res1 == NULL) return(NULL);
	    cuddRef(res1);
	    res = cuddBddAndRecur(dd, Alpha, res1);
	    if (res == NULL) {
		Cudd_RecursiveDeref(dd,res1);
		return(NULL);
	    }
	    cuddDeref(res1);
	} else if (Gamma == Cudd_Not(one)) {
	    res1 = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp));
	    if (res1 == NULL) return(NULL);
	    cuddRef(res1);
	    res = cuddBddAndRecur(dd, Cudd_Not(Alpha), res1);
	    if (res == NULL) {
		Cudd_RecursiveDeref(dd,res1);
		return(NULL);
	    }
	    cuddDeref(res1);
	} else {
	    cuddRef(Gamma);
	    resA = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp));
	    if (resA == NULL) {
		Cudd_RecursiveDeref(dd,Gamma);
		return(NULL);
	    }
	    cuddRef(resA);
	    res2 = cuddBddAndRecur(dd, Cudd_Not(Gamma), resA);
	    if (res2 == NULL) {
		Cudd_RecursiveDeref(dd,Gamma);
		Cudd_RecursiveDeref(dd,resA);
		return(NULL);
	    }
	    cuddRef(res2);
	    Cudd_RecursiveDeref(dd,Gamma);
	    Cudd_RecursiveDeref(dd,resA);
	    res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp));
	    if (res1 == NULL) {
		Cudd_RecursiveDeref(dd,res2);
		return(NULL);
	    }
	    cuddRef(res1);
	    res = cuddBddIteRecur(dd, Alpha, res1, res2);
	    if (res == NULL) {
		Cudd_RecursiveDeref(dd,res1);
		Cudd_RecursiveDeref(dd,res2);
		return(NULL);
	    }
	    cuddDeref(res1);
	    cuddDeref(res2);
	}
    }

    cuddCacheInsert2(dd,Cudd_CProjection,R,Y,res);

    return(res);

} /* end of cuddCProjectionRecur */


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

  Synopsis    [Performs the recursive step of Cudd_bddClosestCube.]

  Description [Performs the recursive step of Cudd_bddClosestCube.
  Returns the cube if succesful; NULL otherwise.  The procedure uses a
  four-way recursion to examine all four combinations of cofactors of
  f and g.  The most interesting feature of this function is the
  scheme used for caching the results in the global computed table.
  Since we have a cube and a distance, we combine them to form an ADD.
  The combination replaces the zero child of the top node of the cube
  with the negative of the distance.  (The use of the negative is to
  avoid ambiguity with 1.)  The degenerate cases (zero and one) are
  treated specially because the distance is known (0 for one, and
  infinity for zero).]

  SideEffects [None]

  SeeAlso     [Cudd_bddClosestCube]

******************************************************************************/
DdNode *
cuddBddClosestCube(
  DdManager *dd,
  DdNode *f,
  DdNode *g,
  CUDD_VALUE_TYPE bound)
{
    DdNode *res, *F, *G, *ft, *fe, *gt, *ge, *tt, *ee;
    DdNode *ctt, *cee, *cte, *cet;
    CUDD_VALUE_TYPE minD, dtt, dee, dte, det;
    DdNode *one = DD_ONE(dd);
    DdNode *lzero = Cudd_Not(one);
    DdNode *azero = DD_ZERO(dd);
    unsigned int topf, topg, index;

    statLine(dd);
    if (bound < (f == Cudd_Not(g))) return(azero);
    /* Terminal cases. */
    if (g == lzero || f == lzero) return(azero);
    if (f == one && g == one) return(one);

    /* Check cache. */
    F = Cudd_Regular(f);
    G = Cudd_Regular(g);
    if (F->ref != 1 || G->ref != 1) {
	res = cuddCacheLookup2(dd,(DdNode * (*)(DdManager *, DdNode *,
			       DdNode *)) Cudd_bddClosestCube, f, g);
	if (res != NULL) return(res);
    }

    topf = cuddI(dd,F->index);
    topg = cuddI(dd,G->index);

    /* Compute cofactors. */
    if (topf <= topg) {
	index = F->index;
	ft = cuddT(F);
	fe = cuddE(F);
	if (Cudd_IsComplement(f)) {
	    ft = Cudd_Not(ft);
	    fe = Cudd_Not(fe);
	}
    } else {
	index = G->index;
	ft = fe = f;
    }

    if (topg <= topf) {
	gt = cuddT(G);
	ge = cuddE(G);
	if (Cudd_IsComplement(g)) {
	    gt = Cudd_Not(gt);
	    ge = Cudd_Not(ge);
	}
    } else {
	gt = ge = g;
    }

    tt = cuddBddClosestCube(dd,ft,gt,bound);
    if (tt == NULL) return(NULL);
    cuddRef(tt);
    ctt = separateCube(dd,tt,&dtt);
    if (ctt == NULL) {
	Cudd_RecursiveDeref(dd, tt);
	return(NULL);
    }
    cuddRef(ctt);
    Cudd_RecursiveDeref(dd, tt);
    minD = dtt;
    bound = ddMin(bound,minD);

    ee = cuddBddClosestCube(dd,fe,ge,bound);
    if (ee == NULL) {
	Cudd_RecursiveDeref(dd, ctt);
	return(NULL);
    }
    cuddRef(ee);
    cee = separateCube(dd,ee,&dee);
    if (cee == NULL) {
	Cudd_RecursiveDeref(dd, ctt);
	Cudd_RecursiveDeref(dd, ee);
	return(NULL);
    }
    cuddRef(cee);
    Cudd_RecursiveDeref(dd, ee);
    minD = ddMin(dtt, dee);
    bound = ddMin(bound,minD-1);

    if (minD > 0 && topf == topg) {
	DdNode *te = cuddBddClosestCube(dd,ft,ge,bound-1);
	if (te == NULL) {
	    Cudd_RecursiveDeref(dd, ctt);
	    Cudd_RecursiveDeref(dd, cee);
	    return(NULL);
	}
	cuddRef(te);
	cte = separateCube(dd,te,&dte);
	if (cte == NULL) {
	    Cudd_RecursiveDeref(dd, ctt);
	    Cudd_RecursiveDeref(dd, cee);
	    Cudd_RecursiveDeref(dd, te);
	    return(NULL);
	}
	cuddRef(cte);
	Cudd_RecursiveDeref(dd, te);
	dte += 1.0;
	minD = ddMin(minD, dte);
    } else {
	cte = azero;
	cuddRef(cte);
	dte = CUDD_CONST_INDEX + 1.0;
    }
    bound = ddMin(bound,minD-1);

    if (minD > 0 && topf == topg) {
	DdNode *et = cuddBddClosestCube(dd,fe,gt,bound-1);
	if (et == NULL) {
	    Cudd_RecursiveDeref(dd, ctt);
	    Cudd_RecursiveDeref(dd, cee);
	    Cudd_RecursiveDeref(dd, cte);
	    return(NULL);
	}
	cuddRef(et);
	cet = separateCube(dd,et,&det);
	if (cet == NULL) {
	    Cudd_RecursiveDeref(dd, ctt);
	    Cudd_RecursiveDeref(dd, cee);
	    Cudd_RecursiveDeref(dd, cte);
	    Cudd_RecursiveDeref(dd, et);
	    return(NULL);
	}
	cuddRef(cet);
	Cudd_RecursiveDeref(dd, et);
	det += 1.0;
	minD = ddMin(minD, det);
    } else {
	cet = azero;
	cuddRef(cet);
	det = CUDD_CONST_INDEX + 1.0;
    }

    if (minD == dtt) {
	if (dtt == dee && ctt == cee) {
	    res = createResult(dd,CUDD_CONST_INDEX,1,ctt,dtt);
	} else {
	    res = createResult(dd,index,1,ctt,dtt);
	}
    } else if (minD == dee) {
	res = createResult(dd,index,0,cee,dee);
    } else if (minD == dte) {
	res = createResult(dd,index,(topf <= topg),cte,dte);
    } else {
	res = createResult(dd,index,(topf > topg),cet,det);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(dd, ctt);
    Cudd_RecursiveDeref(dd, cee);
    Cudd_RecursiveDeref(dd, cte);
    Cudd_RecursiveDeref(dd, cet);

    if (F->ref != 1 || G->ref != 1)
	cuddCacheInsert2(dd,(DdNode * (*)(DdManager *, DdNode *,
			 DdNode *)) Cudd_bddClosestCube, f, g, res);

    cuddDeref(res);
    return(res);

} /* end of cuddBddClosestCube */


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


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

  Synopsis    [Performs the recursive step of Cudd_MinHammingDist.]

  Description [Performs the recursive step of Cudd_MinHammingDist.
  It is based on the following identity. Let H(f) be the
  minimum Hamming distance of the minterms of f from the reference
  minterm. Then:
  <xmp>
    H(f) = min(H(f0)+h0,H(f1)+h1)
  </xmp>
  where f0 and f1 are the two cofactors of f with respect to its top
  variable; h0 is 1 if the minterm assigns 1 to the top variable of f;
  h1 is 1 if the minterm assigns 0 to the top variable of f.
  The upper bound on the distance is used to bound the depth of the
  recursion.
  Returns the minimum distance unless it exceeds the upper bound or
  computation fails.]

  SideEffects [None]

  SeeAlso     [Cudd_MinHammingDist]

******************************************************************************/
static int
cuddMinHammingDistRecur(
  DdNode * f,
  int *minterm,
  DdHashTable * table,
  int upperBound)
{
    DdNode	*F, *Ft, *Fe;
    double	h, hT, hE;
    DdNode	*zero, *res;
    DdManager	*dd = table->manager;

    statLine(dd);
    if (upperBound == 0) return(0);

    F = Cudd_Regular(f);

    if (cuddIsConstant(F)) {
	zero = Cudd_Not(DD_ONE(dd));
	if (f == dd->background || f == zero) {
	    return(upperBound);
	} else {
	    return(0);
	}
    }
    if ((res = cuddHashTableLookup1(table,f)) != NULL) {
	h = cuddV(res);
	if (res->ref == 0) {
	    dd->dead++;
	    dd->constants.dead++;
	}
	return((int) h);
    }

    Ft = cuddT(F); Fe = cuddE(F);
    if (Cudd_IsComplement(f)) {
	Ft = Cudd_Not(Ft); Fe = Cudd_Not(Fe);
    }
    if (minterm[F->index] == 0) {
	DdNode *temp = Ft;
	Ft = Fe; Fe = temp;
    }

    hT = cuddMinHammingDistRecur(Ft,minterm,table,upperBound);
    if (hT == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
    if (hT == 0) {
	hE = upperBound;
    } else {
	hE = cuddMinHammingDistRecur(Fe,minterm,table,upperBound - 1);
	if (hE == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM);
    }
    h = ddMin(hT, hE + 1);

    if (F->ref != 1) {
	ptrint fanout = (ptrint) F->ref;
	cuddSatDec(fanout);
	res = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) h);
	if (!cuddHashTableInsert1(table,f,res,fanout)) {
	    cuddRef(res); Cudd_RecursiveDeref(dd, res);
	    return(CUDD_OUT_OF_MEM);
	}
    }

    return((int) h);

} /* end of cuddMinHammingDistRecur */


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

  Synopsis    [Separates cube from distance.]

  Description [Separates cube from distance.  Returns the cube if
  successful; NULL otherwise.]

  SideEffects [The distance is returned as a side effect.]

  SeeAlso     [cuddBddClosestCube createResult]

******************************************************************************/
static DdNode *
separateCube(
  DdManager *dd,
  DdNode *f,
  CUDD_VALUE_TYPE *distance)
{
    DdNode *cube, *t;

    /* One and zero are special cases because the distance is implied. */
    if (Cudd_IsConstant(f)) {
	*distance = (f == DD_ONE(dd)) ? 0.0 :
	    (1.0 + (CUDD_VALUE_TYPE) CUDD_CONST_INDEX);
	return(f);
    }

    /* Find out which branch points to the distance and replace the top
    ** node with one pointing to zero instead. */
    t = cuddT(f);
    if (Cudd_IsConstant(t) && cuddV(t) <= 0) {
#ifdef DD_DEBUG
	assert(!Cudd_IsConstant(cuddE(f)) || cuddE(f) == DD_ONE(dd));
#endif
	*distance = -cuddV(t);
	cube = cuddUniqueInter(dd, f->index, DD_ZERO(dd), cuddE(f));
    } else {
#ifdef DD_DEBUG
	assert(!Cudd_IsConstant(t) || t == DD_ONE(dd));
#endif
	*distance = -cuddV(cuddE(f));
	cube = cuddUniqueInter(dd, f->index, t, DD_ZERO(dd));
    }

    return(cube);

} /* end of separateCube */


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

  Synopsis    [Builds a result for cache storage.]

  Description [Builds a result for cache storage.  Returns a pointer
  to the resulting ADD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [cuddBddClosestCube separateCube]

******************************************************************************/
static DdNode *
createResult(
  DdManager *dd,
  unsigned int index,
  unsigned int phase,
  DdNode *cube,
  CUDD_VALUE_TYPE distance)
{
    DdNode *res, *constant;

    /* Special case.  The cube is either one or zero, and we do not
    ** add any variables.  Hence, the result is also one or zero,
    ** and the distance remains implied by teh value of the constant. */
    if (index == CUDD_CONST_INDEX && Cudd_IsConstant(cube)) return(cube);

    constant = cuddUniqueConst(dd,-distance);
    if (constant == NULL) return(NULL);
    cuddRef(constant);

    if (index == CUDD_CONST_INDEX) {
	/* Replace the top node. */
	if (cuddT(cube) == DD_ZERO(dd)) {
	    res = cuddUniqueInter(dd,cube->index,constant,cuddE(cube));
	} else {
	    res = cuddUniqueInter(dd,cube->index,cuddT(cube),constant);
	}
    } else {
	/* Add a new top node. */
#ifdef DD_DEBUG
	assert(cuddI(dd,index) < cuddI(dd,cube->index));
#endif
	if (phase) {
	    res = cuddUniqueInter(dd,index,cube,constant);
	} else {
	    res = cuddUniqueInter(dd,index,constant,cube);
	}
    }
    if (res == NULL) {
	Cudd_RecursiveDeref(dd, constant);
	return(NULL);
    }
    cuddDeref(constant); /* safe because constant is part of res */

    return(res);

} /* end of createResult */