cudddecomp.c

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

	}
    } else if  (pairValue2 == BOTH_G) {
	/* g and h are  found in the g table */
	factors->g = g2;
	factors->h = h2;
	if (h2 != one) {
	    value = 3;
	    if (st_insert(ghTable, (char *)Cudd_Regular(h2),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		*outOfMem = 1;
		FREE(factors);
		return(NULL);
	    }
	}
    } else if (pairValue2 == H_ST) { 
	/* h exists in the table, g is not found in either table */
	factors->g = g2;
	factors->h = h2;
	if (g2 != one) {
	    value = 1;
	    if (st_insert(ghTable, (char *)Cudd_Regular(g2),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		*outOfMem = 1;
		FREE(factors);
		return(NULL);
	    }
	}
    } else if (pairValue2 == BOTH_H) {
	/* g and h are  found in the h table */
	factors->g = g2;
	factors->h = h2;
	if (g2 != one) {
	    value = 3;
	    if (st_insert(ghTable, (char *)Cudd_Regular(g2),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		*outOfMem = 1;
		FREE(factors);
		return(NULL);
	    }
	}
    } else if (pairValue1 == G_CR) {
	/* g found in h table and h in none */
	factors->g = h1;
	factors->h = g1;
	if (h1 != one) {
	    value = 1;
	    if (st_insert(ghTable, (char *)Cudd_Regular(h1),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		*outOfMem = 1;
		FREE(factors);
		return(NULL);
	    }
	}
    } else if (pairValue1 == H_CR) {
	/* h found in g table and g in none */
	factors->g = h1;
	factors->h = g1;
	if (g1 != one) {
	    value = 2;
	    if (st_insert(ghTable, (char *)Cudd_Regular(g1),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		*outOfMem = 1;
		FREE(factors);
		return(NULL);
	    }
	}
    } else if (pairValue2 == G_CR) {
	/* g found in h table and h in none */
	factors->g = h2;
	factors->h = g2;
	if (h2 != one) {
	    value = 1;
	    if (st_insert(ghTable, (char *)Cudd_Regular(h2),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		*outOfMem = 1;
		FREE(factors);
		return(NULL);
	    }
	}
    } else if (pairValue2 == H_CR) {
	/* h found in g table and g in none */
	factors->g = h2;
	factors->h = g2;
	if (g2 != one) {
	    value = 2;
	    if (st_insert(ghTable, (char *)Cudd_Regular(g2),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		*outOfMem = 1;
		FREE(factors);
		return(NULL);
	    }
	}
    }
    
    /* Store factors in cache table for later use. */
    if (st_insert(cacheTable, (char *)node, (char *)factors) ==
	    ST_OUT_OF_MEM) {
	*outOfMem = 1;
	FREE(factors);
	return(NULL);
    }
    return factors;
} /* end of CheckInTables */



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

  Synopsis    [If one child is zero, do explicitly what Restrict does or better]

  Description [If one child is zero, do explicitly what Restrict does or better.
  First separate a variable and its child in the base case. In case of a cube
  times a function, separate the cube and function. As a last resort, look in
  tables.]

  SideEffects [Frees the BDDs in factorsNv. factorsNv itself is not freed
  because it is freed above.]

  SeeAlso     [BuildConjuncts]

******************************************************************************/
static Conjuncts *
ZeroCase(
  DdManager * dd,
  DdNode * node,
  Conjuncts * factorsNv,
  st_table * ghTable,
  st_table * cacheTable,
  int switched)
{
    int topid;
    DdNode *g, *h, *g1, *g2, *h1, *h2, *x, *N, *G, *H, *Gv, *Gnv;
    DdNode *Hv, *Hnv;
    int value;
    int outOfMem;
    Conjuncts *factors;
    
    /* get var at this node */
    N = Cudd_Regular(node);
    topid = N->index;
    x = dd->vars[topid];
    x = (switched) ? Cudd_Not(x): x;
    cuddRef(x);

    /* Seprate variable and child */
    if (factorsNv->g == one) {
	Cudd_RecursiveDeref(dd, factorsNv->g);
	factors = ALLOC(Conjuncts, 1);
	if (factors == NULL) {
	    dd->errorCode = CUDD_MEMORY_OUT;
	    Cudd_RecursiveDeref(dd, factorsNv->h);
	    Cudd_RecursiveDeref(dd, x);
	    return(NULL);
	}
	factors->g = x;
	factors->h = factorsNv->h;
	/* cache the result*/
	if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
	    dd->errorCode = CUDD_MEMORY_OUT;
	    Cudd_RecursiveDeref(dd, factorsNv->h); 
	    Cudd_RecursiveDeref(dd, x);
	    FREE(factors);
	    return NULL;
	}
	
	/* store  x in g table, the other node is already in the table */
	if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
	    value |= 1;
	} else {
	    value = 1;
	}
	if (st_insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == ST_OUT_OF_MEM) {
	    dd->errorCode = CUDD_MEMORY_OUT;
	    return NULL;
	}
	return(factors);
    }
    
    /* Seprate variable and child */
    if (factorsNv->h == one) {
	Cudd_RecursiveDeref(dd, factorsNv->h);
	factors = ALLOC(Conjuncts, 1);
	if (factors == NULL) {
	    dd->errorCode = CUDD_MEMORY_OUT;
	    Cudd_RecursiveDeref(dd, factorsNv->g);
	    Cudd_RecursiveDeref(dd, x);
	    return(NULL);
	}
	factors->g = factorsNv->g;
	factors->h = x;
	/* cache the result. */
 	if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
	    dd->errorCode = CUDD_MEMORY_OUT;
	    Cudd_RecursiveDeref(dd, factorsNv->g);
	    Cudd_RecursiveDeref(dd, x);
	    FREE(factors);
	    return(NULL);
	}
	/* store x in h table,  the other node is already in the table */
	if (st_lookup_int(ghTable, (char *)Cudd_Regular(x), &value)) {
	    value |= 2;
	} else {
	    value = 2;
	}
	if (st_insert(ghTable, (char *)Cudd_Regular(x), (char *)(long)value) == ST_OUT_OF_MEM) {
	    dd->errorCode = CUDD_MEMORY_OUT;
	    return NULL;
	}
	return(factors);
    }

    G = Cudd_Regular(factorsNv->g);
    Gv = cuddT(G);
    Gnv = cuddE(G);
    Gv = Cudd_NotCond(Gv, Cudd_IsComplement(node));
    Gnv = Cudd_NotCond(Gnv, Cudd_IsComplement(node));
    /* if the child below is a variable */
    if ((Gv == zero) || (Gnv == zero)) {
	h = factorsNv->h;
	g = cuddBddAndRecur(dd, x, factorsNv->g);
	if (g != NULL) 	cuddRef(g);
	Cudd_RecursiveDeref(dd, factorsNv->g); 
	Cudd_RecursiveDeref(dd, x);
	if (g == NULL) {
	    Cudd_RecursiveDeref(dd, factorsNv->h); 
	    return NULL;
	}
	/* CheckTablesCacheAndReturn responsible for allocating
	 * factors structure., g,h referenced for cache store  the
	 */
	factors = CheckTablesCacheAndReturn(node,
					    g,
					    h,
					    ghTable,
					    cacheTable);
	if (factors == NULL) {
	    dd->errorCode = CUDD_MEMORY_OUT;
	    Cudd_RecursiveDeref(dd, g);
	    Cudd_RecursiveDeref(dd, h);
	}
	return(factors); 
    }

    H = Cudd_Regular(factorsNv->h);
    Hv = cuddT(H);
    Hnv = cuddE(H);
    Hv = Cudd_NotCond(Hv, Cudd_IsComplement(node));
    Hnv = Cudd_NotCond(Hnv, Cudd_IsComplement(node));
    /* if the child below is a variable */
    if ((Hv == zero) || (Hnv == zero)) {
	g = factorsNv->g;
	h = cuddBddAndRecur(dd, x, factorsNv->h);
	if (h!= NULL) cuddRef(h);
	Cudd_RecursiveDeref(dd, factorsNv->h);
	Cudd_RecursiveDeref(dd, x);
	if (h == NULL) {
	    Cudd_RecursiveDeref(dd, factorsNv->g);
	    return NULL;
	}
	/* CheckTablesCacheAndReturn responsible for allocating
	 * factors structure.g,h referenced for table store 
	 */
	factors = CheckTablesCacheAndReturn(node,
					    g,
					    h,
					    ghTable,
					    cacheTable);
	if (factors == NULL) {
	    dd->errorCode = CUDD_MEMORY_OUT;
	    Cudd_RecursiveDeref(dd, g);
	    Cudd_RecursiveDeref(dd, h);
	}
	return(factors); 
    }

    /* build g1 = x*g; h1 = h */
    /* build g2 = g; h2 = x*h */
    Cudd_RecursiveDeref(dd, x);
    h1 = factorsNv->h;
    g1 = cuddBddAndRecur(dd, x, factorsNv->g);
    if (g1 != NULL) cuddRef(g1);
    if (g1 == NULL) {
	Cudd_RecursiveDeref(dd, factorsNv->g); 
	Cudd_RecursiveDeref(dd, factorsNv->h);
	return NULL;
    }
    
    g2 = factorsNv->g;
    h2 = cuddBddAndRecur(dd, x, factorsNv->h);
    if (h2 != NULL) cuddRef(h2);
    if (h2 == NULL) {
	Cudd_RecursiveDeref(dd, factorsNv->h);
	Cudd_RecursiveDeref(dd, factorsNv->g);
	return NULL;
    }

    /* check whether any pair is in tables */
    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;
    }

    /* check for each pair in tables and choose one */
    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 ZeroCase */


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

  Synopsis    [Builds the conjuncts recursively, bottom up.]

  Description [Builds the conjuncts recursively, bottom up. Constants
  are returned as (f, f). The cache is checked for previously computed
  result. The decomposition points are determined by the local
  reference count of this node and the longest distance from the
  constant. At the decomposition point, the factors returned are (f,
  1). Recur on the two children. The order is determined by the
  heavier branch. Combine the factors of the two children and pick the
  one that already occurs in the gh table. Occurence in g is indicated
  by value 1, occurence in h by 2, occurence in both 3.]

  SideEffects []

  SeeAlso     [cuddConjunctsAux]

******************************************************************************/
static Conjuncts *
BuildConjuncts(
  DdManager * dd,
  DdNode * node,
  st_table * distanceTable,
  st_table * cacheTable,
  int approxDistance,
  int maxLocalRef,
  st_table * ghTable,
  st_table * mintermTable)
{
    int topid, distance;
    Conjuncts *factorsNv, *factorsNnv, *factors;
    Conjuncts *dummy;
    DdNode *N, *Nv, *Nnv, *temp, *g1, *g2, *h1, *h2, *topv;
    double minNv = 0.0, minNnv = 0.0;
    double *doubleDummy;
    int switched =0;
    int outOfMem;
    int freeNv = 0, freeNnv = 0, freeTemp;
    NodeStat *nodeStat;
    int value;

    /* if f is constant, return (f,f) */
    if (Cudd_IsConstant(node)) {
	factors = ALLOC(Conjuncts, 1);
	if (factors == NULL) {
	    dd->errorCode = CUDD_MEMORY_OUT;
	    return(NULL);
	}
	factors->g = node;
	factors->h = node;
	return(FactorsComplement(factors));
    }

    /* If result (a pair of conjuncts) in cache, return the factors. */
    if (st_lookup(cacheTable, (char *)node, (char **)&dummy)) {
	factors = dummy;
	return(factors);
    }
    
    /* check distance and local reference count of this node */
    N = Cudd_Regular(node);
    if (!st_lookup(distanceTable, (char *)N, (char **)&nodeStat)) {
	(void) fprintf(dd->err, "Not in table, Something wrong\n");
	dd->errorCode = CUDD_INTERNAL_ERROR;
	return(NULL);
    }
    distance = nodeStat->distance;

    /* at or below decomposition point, return (f, 1) */
    if (((nodeStat->localRef > maxLocalRef*2/3) &&
	 (distance < approxDistance*2/3)) ||
	    (distance <= approxDistance/4)) {
	factors = ALLOC(Conjuncts, 1);
	if (factors == NULL) {
	    dd->errorCode = CUDD_MEMORY_OUT;
	    return(NULL);
	}
	/* alternate assigning (f,1) */
	value = 0;
	if (st_lookup_int(ghTable, (char *)Cudd_Regular(node), &value)) {
	    if (value == 3) {
		if (!lastTimeG) {
		    factors->g = node;
		    factors->h = one;
		    lastTimeG = 1;
		} else {
		    factors->g = one;
		    factors->h = node;
		    lastTimeG = 0; 
		}