cuddcompose.c

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

	} else {
	    topindex = F->index;
	    f1 = cuddT(F);
	    f0 = cuddE(F);
	}
	if (topg > topf) {
	    g1 = g0 = g;
	} else {
	    g1 = cuddT(G);
	    g0 = cuddE(G);
	    if (g != G) {
		g1 = Cudd_Not(g1);
		g0 = Cudd_Not(g0);
	    }
	}
	/* Recursive step. */
	t = cuddBddComposeRecur(dd, f1, g1, proj);
	if (t == NULL) return(NULL);
	cuddRef(t);
	e = cuddBddComposeRecur(dd, f0, g0, proj);
	if (e == NULL) {
	    Cudd_IterDerefBdd(dd, t);
	    return(NULL);
	}
	cuddRef(e);

	r = cuddBddIteRecur(dd, dd->vars[topindex], t, e);
	if (r == NULL) {
	    Cudd_IterDerefBdd(dd, t);
	    Cudd_IterDerefBdd(dd, e);
	    return(NULL);
	}
	cuddRef(r);
	Cudd_IterDerefBdd(dd, t); /* t & e not necessarily part of r */
	Cudd_IterDerefBdd(dd, e);
	cuddDeref(r);
    }

    cuddCacheInsert(dd,DD_BDD_COMPOSE_RECUR_TAG,F,g,proj,r);

    return(Cudd_NotCond(r,comple));

} /* end of cuddBddComposeRecur */


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

  Synopsis    [Performs the recursive step of Cudd_addCompose.]

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

  SideEffects [None]

  SeeAlso     [Cudd_addCompose]

******************************************************************************/
DdNode *
cuddAddComposeRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * g,
  DdNode * proj)
{
    DdNode *f1, *f0, *g1, *g0, *r, *t, *e;
    unsigned int v, topf, topg, topindex;

    statLine(dd);
    v = dd->perm[proj->index];
    topf = cuddI(dd,f->index);

    /* Terminal case. Subsumes the test for constant f. */
    if (topf > v) return(f);

    /* Check cache. */
    r = cuddCacheLookup(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj);
    if (r != NULL) {
	return(r);
    }

    if (topf == v) {
	/* Compose. */
	f1 = cuddT(f);
	f0 = cuddE(f);
	r = cuddAddIteRecur(dd, g, f1, f0);
	if (r == NULL) return(NULL);
    } else {
	/* Compute cofactors of f and g. Remember the index of the top
	** variable.
	*/
	topg = cuddI(dd,g->index);
	if (topf > topg) {
	    topindex = g->index;
	    f1 = f0 = f;
	} else {
	    topindex = f->index;
	    f1 = cuddT(f);
	    f0 = cuddE(f);
	}
	if (topg > topf) {
	    g1 = g0 = g;
	} else {
	    g1 = cuddT(g);
	    g0 = cuddE(g);
	}
	/* Recursive step. */
	t = cuddAddComposeRecur(dd, f1, g1, proj);
	if (t == NULL) return(NULL);
	cuddRef(t);
	e = cuddAddComposeRecur(dd, f0, g0, proj);
	if (e == NULL) {
	    Cudd_RecursiveDeref(dd, t);
	    return(NULL);
	}
	cuddRef(e);

	if (t == e) {
	    r = t;
	} else {
	    r = cuddUniqueInter(dd, (int) topindex, t, e);
	    if (r == NULL) {
		Cudd_RecursiveDeref(dd, t);
		Cudd_RecursiveDeref(dd, e);
		return(NULL);
	    }
	}
	cuddDeref(t);
	cuddDeref(e);
    }

    cuddCacheInsert(dd,DD_ADD_COMPOSE_RECUR_TAG,f,g,proj,r);

    return(r);

} /* end of cuddAddComposeRecur */


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


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

  Synopsis    [Implements the recursive step of Cudd_addPermute.]

  Description [ Recursively puts the ADD in the order given in the
  array permut. Checks for trivial cases to terminate recursion, then
  splits on the children of this node.  Once the solutions for the
  children are obtained, it puts into the current position the node
  from the rest of the ADD that should be here. Then returns this ADD.
  The key here is that the node being visited is NOT put in its proper
  place by this instance, but rather is switched when its proper
  position is reached in the recursion tree.<p>
  The DdNode * that is returned is the same ADD as passed in as node,
  but in the new order.]

  SideEffects [None]

  SeeAlso     [Cudd_addPermute cuddBddPermuteRecur]

******************************************************************************/
static DdNode *
cuddAddPermuteRecur(
  DdManager * manager /* DD manager */,
  DdHashTable * table /* computed table */,
  DdNode * node /* ADD to be reordered */,
  int * permut /* permutation array */)
{
    DdNode	*T,*E;
    DdNode	*res,*var;
    int		index;
    
    statLine(manager);
    /* Check for terminal case of constant node. */
    if (cuddIsConstant(node)) {
	return(node);
    }

    /* If problem already solved, look up answer and return. */
    if (node->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) {
#ifdef DD_DEBUG
	addPermuteRecurHits++;
#endif
	return(res);
    }

    /* Split and recur on children of this node. */
    T = cuddAddPermuteRecur(manager,table,cuddT(node),permut);
    if (T == NULL) return(NULL);
    cuddRef(T);
    E = cuddAddPermuteRecur(manager,table,cuddE(node),permut);
    if (E == NULL) {
	Cudd_RecursiveDeref(manager, T);
	return(NULL);
    }
    cuddRef(E);

    /* Move variable that should be in this position to this position
    ** by creating a single var ADD for that variable, and calling
    ** cuddAddIteRecur with the T and E we just created.
    */
    index = permut[node->index];
    var = cuddUniqueInter(manager,index,DD_ONE(manager),DD_ZERO(manager));
    if (var == NULL) return(NULL);
    cuddRef(var);
    res = cuddAddIteRecur(manager,var,T,E);
    if (res == NULL) {
	Cudd_RecursiveDeref(manager,var);
	Cudd_RecursiveDeref(manager, T);
	Cudd_RecursiveDeref(manager, E);
	return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(manager,var);
    Cudd_RecursiveDeref(manager, T);
    Cudd_RecursiveDeref(manager, E);

    /* Do not keep the result if the reference count is only 1, since
    ** it will not be visited again.
    */
    if (node->ref != 1) {
	ptrint fanout = (ptrint) node->ref;
	cuddSatDec(fanout);
	if (!cuddHashTableInsert1(table,node,res,fanout)) {
	    Cudd_RecursiveDeref(manager, res);
	    return(NULL);
	}
    }
    cuddDeref(res);
    return(res);

} /* end of cuddAddPermuteRecur */


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

  Synopsis    [Implements the recursive step of Cudd_bddPermute.]

  Description [ Recursively puts the BDD in the order given in the array permut.
  Checks for trivial cases to terminate recursion, then splits on the
  children of this node.  Once the solutions for the children are
  obtained, it puts into the current position the node from the rest of
  the BDD that should be here. Then returns this BDD.
  The key here is that the node being visited is NOT put in its proper
  place by this instance, but rather is switched when its proper position
  is reached in the recursion tree.<p>
  The DdNode * that is returned is the same BDD as passed in as node,
  but in the new order.]

  SideEffects [None]

  SeeAlso     [Cudd_bddPermute cuddAddPermuteRecur]

******************************************************************************/
static DdNode *
cuddBddPermuteRecur(
  DdManager * manager /* DD manager */,
  DdHashTable * table /* computed table */,
  DdNode * node /* BDD to be reordered */,
  int * permut /* permutation array */)
{
    DdNode	*N,*T,*E;
    DdNode	*res;
    int		index;

    statLine(manager);
    N = Cudd_Regular(node);

    /* Check for terminal case of constant node. */
    if (cuddIsConstant(N)) {
	return(node);
    }

    /* If problem already solved, look up answer and return. */
    if (N->ref != 1 && (res = cuddHashTableLookup1(table,N)) != NULL) {
#ifdef DD_DEBUG
	bddPermuteRecurHits++;
#endif
	return(Cudd_NotCond(res,N != node));
    }

    /* Split and recur on children of this node. */
    T = cuddBddPermuteRecur(manager,table,cuddT(N),permut);
    if (T == NULL) return(NULL);
    cuddRef(T);
    E = cuddBddPermuteRecur(manager,table,cuddE(N),permut);
    if (E == NULL) {
	Cudd_IterDerefBdd(manager, T);
	return(NULL);
    }
    cuddRef(E);

    /* Move variable that should be in this position to this position
    ** by retrieving the single var BDD for that variable, and calling
    ** cuddBddIteRecur with the T and E we just created.
    */
    index = permut[N->index];
    res = cuddBddIteRecur(manager,manager->vars[index],T,E);
    if (res == NULL) {
	Cudd_IterDerefBdd(manager, T);
	Cudd_IterDerefBdd(manager, E);
	return(NULL);
    }
    cuddRef(res);
    Cudd_IterDerefBdd(manager, T);
    Cudd_IterDerefBdd(manager, E);

    /* Do not keep the result if the reference count is only 1, since
    ** it will not be visited again.
    */
    if (N->ref != 1) {
	ptrint fanout = (ptrint) N->ref;
	cuddSatDec(fanout);
	if (!cuddHashTableInsert1(table,N,res,fanout)) {
	    Cudd_IterDerefBdd(manager, res);
	    return(NULL);
	}
    }
    cuddDeref(res);
    return(Cudd_NotCond(res,N != node));

} /* end of cuddBddPermuteRecur */


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

  Synopsis    [Implements the recursive step of Cudd_bddVarMap.]

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

  SideEffects [None]

  SeeAlso     [Cudd_bddVarMap]

******************************************************************************/
static DdNode *
cuddBddVarMapRecur(
  DdManager *manager /* DD manager */,
  DdNode *f /* BDD to be remapped */)
{
    DdNode	*F, *T, *E;
    DdNode	*res;
    int		index;

    statLine(manager);
    F = Cudd_Regular(f);

    /* Check for terminal case of constant node. */
    if (cuddIsConstant(F)) {
	return(f);
    }

    /* If problem already solved, look up answer and return. */
    if (F->ref != 1 &&
	(res = cuddCacheLookup1(manager,Cudd_bddVarMap,F)) != NULL) {
	return(Cudd_NotCond(res,F != f));
    }

    /* Split and recur on children of this node. */
    T = cuddBddVarMapRecur(manager,cuddT(F));
    if (T == NULL) return(NULL);
    cuddRef(T);
    E = cuddBddVarMapRecur(manager,cuddE(F));
    if (E == NULL) {
	Cudd_IterDerefBdd(manager, T);
	return(NULL);
    }
    cuddRef(E);

    /* Move variable that should be in this position to this position
    ** by retrieving the single var BDD for that variable, and calling
    ** cuddBddIteRecur with the T and E we just created.
    */
    index = manager->map[F->index];
    res = cuddBddIteRecur(manager,manager->vars[index],T,E);
    if (res == NULL) {
	Cudd_IterDerefBdd(manager, T);
	Cudd_IterDerefBdd(manager, E);
	return(NULL);
    }
    cuddRef(res);
    Cudd_IterDerefBdd(manager, T);
    Cudd_IterDerefBdd(manager, E);

    /* Do not keep the result if the reference count is only 1, since
    ** it will not be visited again.
    */
    if (F->ref != 1) {
	cuddCacheInsert1(manager,Cudd_bddVarMap,F,res);
    }
    cuddDeref(res);
    return(Cudd_NotCond(res,F != f));

} /* end of cuddBddVarMapRecur */


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

  Synopsis    [Performs the recursive step of Cudd_addVectorCompose.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
cuddAddVectorComposeRecur(
  DdManager * dd /* DD manager */,
  DdHashTable * table /* computed table */,
  DdNode * f /* ADD in which to compose */,
  DdNode ** vector /* functions to substitute */,
  int  deepest /* depth of deepest substitution */)
{
    DdNode	*T,*E;
    DdNode	*res;

    statLine(dd);
    /* If we are past the deepest substitution, return f. */
    if (cuddI(dd,f->index) > deepest) {
	return(f);
    }

    if ((res = cuddHashTableLookup1(table,f)) != NULL) {
#ifdef DD_DEBUG
	addVectorComposeHits++;
#endif
	return(res);