cuddgencof.c

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

    topc = cuddI(dd,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) {
	/* We know that c is not constant because f is not. */
	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;
    }

    resT = cuddBddLICMarkEdges(dd, Fv, Cv, table, cache);
    if (resT == CUDD_OUT_OF_MEM) {
	FREE(key);
	return(CUDD_OUT_OF_MEM);
    }
    resE = cuddBddLICMarkEdges(dd, Fnv, Cnv, table, cache);
    if (resE == CUDD_OUT_OF_MEM) {
	FREE(key);
	return(CUDD_OUT_OF_MEM);
    }

    /* Update edge markings. */
    if (topf <= topc) {
	retval = st_find_or_add(table, (char *)f, (char ***)&slot);
	if (retval == 0) {
	    *slot = (char *) (ptrint)((resT << 2) | resE);
	} else if (retval == 1) {
	    *slot = (char *) (ptrint)((int)((ptrint) *slot) | (resT << 2) | resE);
	} else {
	    FREE(key);
	    return(CUDD_OUT_OF_MEM);
	}
    }

    /* Cache result. */
    res = resT | resE;
    if (st_insert(cache, (char *)key, (char *)(ptrint)res) == ST_OUT_OF_MEM) {
	FREE(key);
	return(CUDD_OUT_OF_MEM);
    }

    /* Take into account possible complementation. */
    if (comple) {
	if (res == DD_LIC_0) res = DD_LIC_1;
	else if (res == DD_LIC_1) res = DD_LIC_0;
    }
    return(res);

} /* end of cuddBddLICMarkEdges */


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

  Synopsis    [Builds the result of Cudd_bddLICompaction.]

  Description [Builds the results of Cudd_bddLICompaction.
  Returns a pointer to the minimized BDD if successful; otherwise NULL.]

  SideEffects [None]

  SeeAlso     [Cudd_bddLICompaction cuddBddLICMarkEdges]

******************************************************************************/
static DdNode *
cuddBddLICBuildResult(
  DdManager * dd,
  DdNode * f,
  st_table * cache,
  st_table * table)
{
    DdNode *Fv, *Fnv, *r, *t, *e;
    DdNode *one, *zero;
    unsigned int topf;
    int	index;
    int comple;
    int markT, markE, markings;

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

    if (Cudd_IsConstant(f)) return(f);
    /* Make canonical to increase the utilization of the cache. */
    comple = Cudd_IsComplement(f);
    f = Cudd_Regular(f);

    /* Check the cache. */
    if (st_lookup(cache, (char *)f, (char **)&r)) {
	return(Cudd_NotCond(r,comple));
    }

    /* Retrieve the edge markings. */
    if (st_lookup(table, (char *)f, (char **)&markings) == 0)
	return(NULL);
    markT = markings >> 2;
    markE = markings & 3;

    topf = dd->perm[f->index];
    index = f->index;
    Fv = cuddT(f); Fnv = cuddE(f);

    if (markT == DD_LIC_NL) {
	t = cuddBddLICBuildResult(dd,Fv,cache,table);
	if (t == NULL) {
	    return(NULL);
	}
    } else if (markT == DD_LIC_1) {
	t = one;
    } else {
	t = zero;
    }
    cuddRef(t);
    if (markE == DD_LIC_NL) {
	e = cuddBddLICBuildResult(dd,Fnv,cache,table);
	if (e == NULL) {
	    Cudd_IterDerefBdd(dd,t);
	    return(NULL);
	}
    } else if (markE == DD_LIC_1) {
	e = one;
    } else {
	e = zero;
    }
    cuddRef(e);

    if (markT == DD_LIC_DC && markE != DD_LIC_DC) {
	r = e;
    } else if (markT != DD_LIC_DC && markE == DD_LIC_DC) {
	r = t;
    } else {
	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);

    if (st_insert(cache, (char *)f, (char *)r) == ST_OUT_OF_MEM) {
	cuddRef(r);
	Cudd_IterDerefBdd(dd,r);
	return(NULL);
    }

    return(Cudd_NotCond(r,comple));

} /* end of cuddBddLICBuildResult */


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

  Synopsis    [Hash function for the computed table of cuddBddLICMarkEdges.]

  Description [Hash function for the computed table of
  cuddBddLICMarkEdges.  Returns the bucket number.]

  SideEffects [None]

  SeeAlso     [Cudd_bddLICompaction]

******************************************************************************/
static int
MarkCacheHash(
  char * ptr,
  int  modulus)
{
    int val = 0;
    MarkCacheKey *entry;

    entry = (MarkCacheKey *) ptr;

    val = (int) (ptrint) entry->f;
    val = val * 997 + (int) (ptrint) entry->c;

    return ((val < 0) ? -val : val) % modulus;

} /* end of MarkCacheHash */


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

  Synopsis    [Comparison function for the computed table of
  cuddBddLICMarkEdges.]

  Description [Comparison function for the computed table of
  cuddBddLICMarkEdges. Returns 0 if the two nodes of the key are equal; 1
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddLICompaction]

******************************************************************************/
static int
MarkCacheCompare(
  const char * ptr1,
  const char * ptr2)
{
    MarkCacheKey *entry1, *entry2;

    entry1 = (MarkCacheKey *) ptr1;
    entry2 = (MarkCacheKey *) ptr2;
    
    return((entry1->f != entry2->f) || (entry1->c != entry2->c));

} /* end of MarkCacheCompare */



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

  Synopsis    [Frees memory associated with computed table of
  cuddBddLICMarkEdges.]

  Description [Frees memory associated with computed table of
  cuddBddLICMarkEdges. Returns ST_CONTINUE.]

  SideEffects [None]

  SeeAlso     [Cudd_bddLICompaction]

******************************************************************************/
static enum st_retval
MarkCacheCleanUp(
  char * key,
  char * value,
  char * arg)
{
    MarkCacheKey *entry;

    entry = (MarkCacheKey *) key;
    FREE(entry);
    return ST_CONTINUE;

} /* end of MarkCacheCleanUp */


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

  Synopsis    [Performs the recursive step of Cudd_bddSqueeze.]

  Description [Performs the recursive step of Cudd_bddSqueeze.  This
  procedure exploits the fact that if we complement and swap the
  bounds of the interval we obtain a valid solution by taking the
  complement of the solution to the original problem. Therefore, we
  can enforce the condition that the upper bound is always regular.
  Returns a pointer to the result if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddSqueeze]

******************************************************************************/
static DdNode *
cuddBddSqueeze(
  DdManager * dd,
  DdNode * l,
  DdNode * u)
{
    DdNode *one, *zero, *r, *lt, *le, *ut, *ue, *t, *e;
#if 0
    DdNode *ar;
#endif
    int comple = 0;
    unsigned int topu, topl;
    int index;

    statLine(dd);
    if (l == u) {
	return(l);
    }
    one = DD_ONE(dd);
    zero = Cudd_Not(one);
    /* The only case when l == zero && u == one is at the top level,
    ** where returning either one or zero is OK. In all other cases
    ** the procedure will detect such a case and will perform
    ** remapping. Therefore the order in which we test l and u at this
    ** point is immaterial. */
    if (l == zero) return(l);
    if (u == one)  return(u);

    /* Make canonical to increase the utilization of the cache. */
    if (Cudd_IsComplement(u)) {
	DdNode *temp;
	temp = Cudd_Not(l);
	l = Cudd_Not(u);
	u = temp;
	comple = 1;
    }
    /* At this point u is regular and non-constant; l is non-constant, but
    ** may be complemented. */

    /* Here we could check the relative sizes. */

    /* Check the cache. */
    r = cuddCacheLookup2(dd, Cudd_bddSqueeze, l, u);
    if (r != NULL) {
	return(Cudd_NotCond(r,comple));
    }

    /* Recursive step. */
    topu = dd->perm[u->index];
    topl = dd->perm[Cudd_Regular(l)->index];
    if (topu <= topl) {
	index = u->index;
	ut = cuddT(u); ue = cuddE(u);
    } else {
	index = Cudd_Regular(l)->index;
	ut = ue = u;
    }
    if (topl <= topu) {
	lt = cuddT(Cudd_Regular(l)); le = cuddE(Cudd_Regular(l));
	if (Cudd_IsComplement(l)) {
	    lt = Cudd_Not(lt);
	    le = Cudd_Not(le);
	}
    } else {
	lt = le = l;
    }

    /* If one interval is contained in the other, use the smaller
    ** interval. This corresponds to one-sided matching. */
    if ((lt == zero || Cudd_bddLeq(dd,lt,le)) &&
	(ut == one  || Cudd_bddLeq(dd,ue,ut))) { /* remap */
	r = cuddBddSqueeze(dd, le, ue);
	if (r == NULL)
	    return(NULL);
	return(Cudd_NotCond(r,comple));
    } else if ((le == zero || Cudd_bddLeq(dd,le,lt)) &&
	       (ue == one  || Cudd_bddLeq(dd,ut,ue))) { /* remap */
	r = cuddBddSqueeze(dd, lt, ut);
	if (r == NULL)
	    return(NULL);
	return(Cudd_NotCond(r,comple));
    } else if ((le == zero || Cudd_bddLeq(dd,le,Cudd_Not(ut))) &&
	       (ue == one  || Cudd_bddLeq(dd,Cudd_Not(lt),ue))) { /* c-remap */
	t = cuddBddSqueeze(dd, lt, ut);
	cuddRef(t);
	if (Cudd_IsComplement(t)) {
	    r = cuddUniqueInter(dd, index, Cudd_Not(t), t);
	    if (r == NULL) {
		Cudd_IterDerefBdd(dd, t);
		return(NULL);
	    }
	    r = Cudd_Not(r);
	} else {
	    r = cuddUniqueInter(dd, index, t, Cudd_Not(t));
	    if (r == NULL) {
		Cudd_IterDerefBdd(dd, t);
		return(NULL);
	    }
	}
	cuddDeref(t);
	if (r == NULL)
	    return(NULL);
	cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
	return(Cudd_NotCond(r,comple));
    } else if ((lt == zero || Cudd_bddLeq(dd,lt,Cudd_Not(ue))) &&
	       (ut == one  || Cudd_bddLeq(dd,Cudd_Not(le),ut))) { /* c-remap */
	e = cuddBddSqueeze(dd, le, ue);
	cuddRef(e);
	if (Cudd_IsComplement(e)) {
	    r = cuddUniqueInter(dd, index, Cudd_Not(e), e);
	    if (r == NULL) {
		Cudd_IterDerefBdd(dd, e);
		return(NULL);
	    }
	} else {
	    r = cuddUniqueInter(dd, index, e, Cudd_Not(e));
	    if (r == NULL) {
		Cudd_IterDerefBdd(dd, e);
		return(NULL);
	    }
	    r = Cudd_Not(r);
	}
	cuddDeref(e);
	if (r == NULL)
	    return(NULL);
	cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
	return(Cudd_NotCond(r,comple));
    }

#if 0
    /* If the two intervals intersect, take a solution from
    ** the intersection of the intervals. This guarantees that the
    ** splitting variable will not appear in the result.
    ** This approach corresponds to two-sided matching, and is very
    ** expensive. */
    if (Cudd_bddLeq(dd,lt,ue) && Cudd_bddLeq(dd,le,ut)) {
	DdNode *au, *al;
	au = cuddBddAndRecur(dd,ut,ue);
	if (au == NULL)
	    return(NULL);
	cuddRef(au);
	al = cuddBddAndRecur(dd,Cudd_Not(lt),Cudd_Not(le));
	if (al == NULL) {
	    Cudd_IterDerefBdd(dd,au);
	    return(NULL);
	}
	cuddRef(al);
	al = Cudd_Not(al);
	ar = cuddBddSqueeze(dd, al, au);
	if (ar == NULL) {
	    Cudd_IterDerefBdd(dd,au);
	    Cudd_IterDerefBdd(dd,al);
	    return(NULL);
	}
	cuddRef(ar);
	Cudd_IterDerefBdd(dd,au);
	Cudd_IterDerefBdd(dd,al);
    } else {
	ar = NULL;
    }
#endif

    t = cuddBddSqueeze(dd, lt, ut);
    if (t == NULL) {
	return(NULL);
    }
    cuddRef(t);
    e = cuddBddSqueeze(dd, le, ue);
    if (e == NULL) {
	Cudd_IterDerefBdd(dd,t);
	return(NULL);
    }
    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);

#if 0
    /* Check whether there is a result obtained by abstraction and whether
    ** it is better than the one obtained by recursion. */
    cuddRef(r);
    if (ar != NULL) {
	if (Cudd_DagSize(ar) <= Cudd_DagSize(r)) {
	    Cudd_IterDerefBdd(dd, r);
	    r = ar;
	} else {
	    Cudd_IterDerefBdd(dd, ar);
	}
    }
    cuddDeref(r);
#endif

    cuddCacheInsert2(dd, Cudd_bddSqueeze, l, u, r);
    return(Cudd_NotCond(r,comple));

} /* end of cuddBddSqueeze */