cudddecomp.c

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

	    } else if (value == 1) {
		factors->g = node;
		factors->h = one;
	    } else {
		factors->g = one;
		factors->h = node;
	    }
	} else if (!lastTimeG) {
	    factors->g = node;
	    factors->h = one;
	    lastTimeG = 1;
	    value = 1;
	    if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
		dd->errorCode = CUDD_MEMORY_OUT;
		FREE(factors);
		return NULL;
	    }
	} else {
	    factors->g = one;
	    factors->h = node;
	    lastTimeG = 0;
	    value = 2;
	    if (st_insert(ghTable, (char *)Cudd_Regular(node), (char *)(long)value) == ST_OUT_OF_MEM) {
		dd->errorCode = CUDD_MEMORY_OUT;
		FREE(factors);
		return NULL;
	    }
	}
	return(FactorsComplement(factors));
    }
    
    /* get the children and recur */
    Nv = cuddT(N);
    Nnv = cuddE(N);
    Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
    Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));

    /* Choose which subproblem to solve first based on the number of
     * minterms. We go first where there are more minterms.
     */
    if (!Cudd_IsConstant(Nv)) {
	if (!st_lookup(mintermTable, (char *)Nv, (char **)&doubleDummy)) {
	    (void) fprintf(dd->err, "Not in table: Something wrong\n");
	    dd->errorCode = CUDD_INTERNAL_ERROR;
	    return(NULL);
	}
	minNv = *doubleDummy;
    }
    
    if (!Cudd_IsConstant(Nnv)) {
	if (!st_lookup(mintermTable, (char *)Nnv, (char **)&doubleDummy)) {
	    (void) fprintf(dd->err, "Not in table: Something wrong\n");
	    dd->errorCode = CUDD_INTERNAL_ERROR;
	    return(NULL);
	}
	minNnv = *doubleDummy;
    }
    
    if (minNv < minNnv) {
	temp = Nv;
	Nv = Nnv;
	Nnv = temp;
	switched = 1;
    }

    /* build gt, ht recursively */
    if (Nv != zero) {
	factorsNv = BuildConjuncts(dd, Nv, distanceTable,
				   cacheTable, approxDistance, maxLocalRef, 
				   ghTable, mintermTable);
	if (factorsNv == NULL) return(NULL);
	freeNv = FactorsNotStored(factorsNv);
	factorsNv = (freeNv) ? FactorsUncomplement(factorsNv) : factorsNv;
	cuddRef(factorsNv->g);
	cuddRef(factorsNv->h);
	
	/* Deal with the zero case */
	if (Nnv == zero) {
	    /* is responsible for freeing factorsNv */
	    factors = ZeroCase(dd, node, factorsNv, ghTable,
			       cacheTable, switched);
	    if (freeNv) FREE(factorsNv);
	    return(factors);
	}
    }

    /* build ge, he recursively */
    if (Nnv != zero) {
	factorsNnv = BuildConjuncts(dd, Nnv, distanceTable,
				    cacheTable, approxDistance, maxLocalRef,
				    ghTable, mintermTable);
	if (factorsNnv == NULL) {
	    Cudd_RecursiveDeref(dd, factorsNv->g);
	    Cudd_RecursiveDeref(dd, factorsNv->h);
	    if (freeNv) FREE(factorsNv);
	    return(NULL);
	}
	freeNnv = FactorsNotStored(factorsNnv);
	factorsNnv = (freeNnv) ? FactorsUncomplement(factorsNnv) : factorsNnv;
	cuddRef(factorsNnv->g);
	cuddRef(factorsNnv->h);
	
	/* Deal with the zero case */
	if (Nv == zero) {
	    /* is responsible for freeing factorsNv */
	    factors = ZeroCase(dd, node, factorsNnv, ghTable,
			       cacheTable, switched);
	    if (freeNnv) FREE(factorsNnv);
	    return(factors);
	}
    }

    /* construct the 2 pairs */
    /* g1 = x*gt + x'*ge; h1 = x*ht + x'*he; */
    /* g2 = x*gt + x'*he; h2 = x*ht + x'*ge */
    if (switched) {
	factors = factorsNnv;
	factorsNnv = factorsNv;
	factorsNv = factors;
	freeTemp = freeNv;
	freeNv = freeNnv;
	freeNnv = freeTemp;
    }

    /* Build the factors for this node. */
    topid = N->index;
    topv = dd->vars[topid];
    
    g1 = cuddBddIteRecur(dd, topv, factorsNv->g, factorsNnv->g);
    if (g1 == NULL) {
	Cudd_RecursiveDeref(dd, factorsNv->g);
	Cudd_RecursiveDeref(dd, factorsNv->h);
	Cudd_RecursiveDeref(dd, factorsNnv->g);
	Cudd_RecursiveDeref(dd, factorsNnv->h);
	if (freeNv) FREE(factorsNv);
	if (freeNnv) FREE(factorsNnv);
	return(NULL);
    }

    cuddRef(g1);

    h1 = cuddBddIteRecur(dd, topv, factorsNv->h, factorsNnv->h);
    if (h1 == NULL) {
	Cudd_RecursiveDeref(dd, factorsNv->g);
	Cudd_RecursiveDeref(dd, factorsNv->h);
	Cudd_RecursiveDeref(dd, factorsNnv->g);
	Cudd_RecursiveDeref(dd, factorsNnv->h);
	Cudd_RecursiveDeref(dd, g1);
	if (freeNv) FREE(factorsNv);
	if (freeNnv) FREE(factorsNnv);
	return(NULL);
    }

    cuddRef(h1);

    g2 = cuddBddIteRecur(dd, topv, factorsNv->g, factorsNnv->h);
    if (g2 == NULL) {
	Cudd_RecursiveDeref(dd, factorsNv->h);
	Cudd_RecursiveDeref(dd, factorsNv->g);
	Cudd_RecursiveDeref(dd, factorsNnv->g);
	Cudd_RecursiveDeref(dd, factorsNnv->h);
	Cudd_RecursiveDeref(dd, g1);
	Cudd_RecursiveDeref(dd, h1);
	if (freeNv) FREE(factorsNv);
	if (freeNnv) FREE(factorsNnv);
	return(NULL);
    }
    cuddRef(g2);
    Cudd_RecursiveDeref(dd, factorsNv->g);
    Cudd_RecursiveDeref(dd, factorsNnv->h);

    h2 = cuddBddIteRecur(dd, topv, factorsNv->h, factorsNnv->g);
    if (h2 == NULL) {
	Cudd_RecursiveDeref(dd, factorsNv->g);
	Cudd_RecursiveDeref(dd, factorsNv->h);
	Cudd_RecursiveDeref(dd, factorsNnv->g);
	Cudd_RecursiveDeref(dd, factorsNnv->h);
	Cudd_RecursiveDeref(dd, g1);
	Cudd_RecursiveDeref(dd, h1);
	Cudd_RecursiveDeref(dd, g2);
	if (freeNv) FREE(factorsNv);
	if (freeNnv) FREE(factorsNnv);
	return(NULL);
    }
    cuddRef(h2);
    Cudd_RecursiveDeref(dd, factorsNv->h);
    Cudd_RecursiveDeref(dd, factorsNnv->g);
    if (freeNv) FREE(factorsNv);
    if (freeNnv) FREE(factorsNnv);

    /* check for each pair in tables and choose one */
    factors = CheckInTables(node, g1, h1, g2, h2, ghTable, cacheTable, &outOfMem);
    if (outOfMem) {
	dd->errorCode = CUDD_MEMORY_OUT;
	Cudd_RecursiveDeref(dd, g1);
	Cudd_RecursiveDeref(dd, h1);
	Cudd_RecursiveDeref(dd, g2);
	Cudd_RecursiveDeref(dd, h2);
	return(NULL);
    }
    if (factors != NULL) {
	if ((factors->g == g1) || (factors->g == h1)) {
	    Cudd_RecursiveDeref(dd, g2);
	    Cudd_RecursiveDeref(dd, h2);
	} else {
	    Cudd_RecursiveDeref(dd, g1);
	    Cudd_RecursiveDeref(dd, h1);
	}
	return(factors);
    }

    /* if not in tables, pick one pair */
    factors = PickOnePair(node,g1, h1, g2, h2, ghTable, cacheTable);
    if (factors == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	Cudd_RecursiveDeref(dd, g1);
	Cudd_RecursiveDeref(dd, h1);
	Cudd_RecursiveDeref(dd, g2);
	Cudd_RecursiveDeref(dd, h2);
    } else {
	/* now free what was created and not used */
	if ((factors->g == g1) || (factors->g == h1)) {
	    Cudd_RecursiveDeref(dd, g2);
	    Cudd_RecursiveDeref(dd, h2);
	} else {
	    Cudd_RecursiveDeref(dd, g1);
	    Cudd_RecursiveDeref(dd, h1);
	}
    }
	
    return(factors);
    
} /* end of BuildConjuncts */


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

  Synopsis    [Procedure to compute two conjunctive factors of f and place in *c1 and *c2.]

  Description [Procedure to compute two conjunctive factors of f and
  place in *c1 and *c2. Sets up the required data - table of distances
  from the constant and local reference count. Also minterm table. ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
cuddConjunctsAux(
  DdManager * dd,
  DdNode * f,
  DdNode ** c1,
  DdNode ** c2)
{
    st_table *distanceTable = NULL;
    st_table *cacheTable = NULL;
    st_table *mintermTable = NULL;
    st_table *ghTable = NULL;
    st_generator *stGen;
    char *key, *value;
    Conjuncts *factors;
    int distance, approxDistance;
    double max, minterms;
    int freeFactors;
    NodeStat *nodeStat;
    int maxLocalRef;
    
    /* initialize */
    *c1 = NULL;
    *c2 = NULL;

    /* initialize distances table */
    distanceTable = st_init_table(st_ptrcmp,st_ptrhash);
    if (distanceTable == NULL) goto outOfMem;
    
    /* make the entry for the constant */
    nodeStat = ALLOC(NodeStat, 1);
    if (nodeStat == NULL) goto outOfMem;
    nodeStat->distance = 0;
    nodeStat->localRef = 1;
    if (st_insert(distanceTable, (char *)one, (char *)nodeStat) == ST_OUT_OF_MEM) {
	goto outOfMem;
    }

    /* Count node distances from constant. */
    nodeStat = CreateBotDist(f, distanceTable);
    if (nodeStat == NULL) goto outOfMem;

    /* set the distance for the decomposition points */
    approxDistance = (DEPTH < nodeStat->distance) ? nodeStat->distance : DEPTH;
    distance = nodeStat->distance;

    if (distance < approxDistance) {
	/* Too small to bother. */
	*c1 = f;
	*c2 = DD_ONE(dd);
	cuddRef(*c1); cuddRef(*c2);
	stGen = st_init_gen(distanceTable);
	if (stGen == NULL) goto outOfMem;
	while(st_gen(stGen, (char **)&key, (char **)&value)) {
	    FREE(value);
	}
	st_free_gen(stGen); stGen = NULL;
	st_free_table(distanceTable);
	return(1);
    }

    /* record the maximum local reference count */
    maxLocalRef = 0;
    stGen = st_init_gen(distanceTable);
    if (stGen == NULL) goto outOfMem;
    while(st_gen(stGen, (char **)&key, (char **)&value)) {
	nodeStat = (NodeStat *)value;
	maxLocalRef = (nodeStat->localRef > maxLocalRef) ?
	    nodeStat->localRef : maxLocalRef;
    }
    st_free_gen(stGen); stGen = NULL;

	    
    /* Count minterms for each node. */
    max = pow(2.0, (double)Cudd_SupportSize(dd,f)); /* potential overflow */
    mintermTable = st_init_table(st_ptrcmp,st_ptrhash);
    if (mintermTable == NULL) goto outOfMem;
    minterms = CountMinterms(f, max, mintermTable, dd->err);
    if (minterms == -1.0) goto outOfMem;
    
    lastTimeG = Cudd_Random() & 1;
    cacheTable = st_init_table(st_ptrcmp, st_ptrhash);
    if (cacheTable == NULL) goto outOfMem;
    ghTable = st_init_table(st_ptrcmp, st_ptrhash);
    if (ghTable == NULL) goto outOfMem;

    /* Build conjuncts. */
    factors = BuildConjuncts(dd, f, distanceTable, cacheTable,
			     approxDistance, maxLocalRef, ghTable, mintermTable);
    if (factors == NULL) goto outOfMem;

    /* free up tables */
    stGen = st_init_gen(distanceTable);
    if (stGen == NULL) goto outOfMem;
    while(st_gen(stGen, (char **)&key, (char **)&value)) {
	FREE(value);
    }
    st_free_gen(stGen); stGen = NULL;
    st_free_table(distanceTable); distanceTable = NULL;
    st_free_table(ghTable); ghTable = NULL;
    
    stGen = st_init_gen(mintermTable);
    if (stGen == NULL) goto outOfMem;
    while(st_gen(stGen, (char **)&key, (char **)&value)) {
	FREE(value);
    }
    st_free_gen(stGen); stGen = NULL;
    st_free_table(mintermTable); mintermTable = NULL;

    freeFactors = FactorsNotStored(factors);
    factors = (freeFactors) ? FactorsUncomplement(factors) : factors;
    if (factors != NULL) {
	*c1 = factors->g;
	*c2 = factors->h;
	cuddRef(*c1);
	cuddRef(*c2);
	if (freeFactors) FREE(factors);
	
#if 0    
	if ((*c1 == f) && (!Cudd_IsConstant(f))) {
	    assert(*c2 == one);
	}
	if ((*c2 == f) && (!Cudd_IsConstant(f))) {
	    assert(*c1 == one);
	}
	
	if ((*c1 != one) && (!Cudd_IsConstant(f))) {
	    assert(!Cudd_bddLeq(dd, *c2, *c1));
	}
	if ((*c2 != one) && (!Cudd_IsConstant(f))) {
	    assert(!Cudd_bddLeq(dd, *c1, *c2));
	}
#endif
    }

    stGen = st_init_gen(cacheTable);
    if (stGen == NULL) goto outOfMem;
    while(st_gen(stGen, (char **)&key, (char **)&value)) {
	ConjunctsFree(dd, (Conjuncts *)value);
    }
    st_free_gen(stGen); stGen = NULL;

    st_free_table(cacheTable); cacheTable = NULL;

    return(1);

outOfMem:
    if (distanceTable != NULL) {
	stGen = st_init_gen(distanceTable);
	if (stGen == NULL) goto outOfMem;
	while(st_gen(stGen, (char **)&key, (char **)&value)) {
	    FREE(value);
	}
	st_free_gen(stGen); stGen = NULL;
	st_free_table(distanceTable); distanceTable = NULL;
    }
    if (mintermTable != NULL) {
	stGen = st_init_gen(mintermTable);
	if (stGen == NULL) goto outOfMem;
	while(st_gen(stGen, (char **)&key, (char **)&value)) {
	    FREE(value);
	}
	st_free_gen(stGen); stGen = NULL;
	st_free_table(mintermTable); mintermTable = NULL;
    }
    if (ghTable != NULL) st_free_table(ghTable);
    if (cacheTable != NULL) {
	stGen = st_init_gen(cacheTable);
	if (stGen == NULL) goto outOfMem;
	while(st_gen(stGen, (char **)&key, (char **)&value)) {
	    ConjunctsFree(dd, (Conjuncts *)value);
	}
	st_free_gen(stGen); stGen = NULL;
	st_free_table(cacheTable); cacheTable = NULL;
    }
    dd->errorCode = CUDD_MEMORY_OUT;
    return(0);

} /* end of cuddConjunctsAux */