cuddutil.c

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

	}

	while (isSame) {
	    isSame = 0;
	    for (j = savePoint; j < i; j++) {
		if (strcmp(string[i], string[j]) == 0) {
		    isSame = 1;
		    break;
		}
	    }
	    if (isSame) {
		strcpy(string[i], saveString);
		/* Randomize choice for don't cares. */
		for (j = 0; j < n; j++) {
		    if (string[i][indices[j]] == '2') 
			string[i][indices[j]] = (Cudd_Random() & 0x20) ?
			    '1' : '0';
		}
	    }
	}

	old[i] = Cudd_ReadOne(dd);
	cuddRef(old[i]);

	for (j = 0; j < n; j++) {
	    if (string[i][indices[j]] == '0') {
		neW = Cudd_bddAnd(dd,old[i],Cudd_Not(vars[j]));
	    } else {
		neW = Cudd_bddAnd(dd,old[i],vars[j]);
	    }
	    if (neW == NULL) {
		FREE(saveString);
		for (l = 0; l < k; l++)
		    FREE(string[l]);
		FREE(string);
		FREE(indices);
		for (l = 0; l <= i; l++)
		    Cudd_RecursiveDeref(dd,old[l]);
		FREE(old);
		return(NULL);
	    }
	    cuddRef(neW);
	    Cudd_RecursiveDeref(dd,old[i]);
	    old[i] = neW;
	}

	/* Test. */
	if (!Cudd_bddLeq(dd,old[i],f)) {
	    FREE(saveString);
	    for (l = 0; l < k; l++)
		FREE(string[l]);
	    FREE(string);
	    FREE(indices);
	    for (l = 0; l <= i; l++)
		Cudd_RecursiveDeref(dd,old[l]);
	    FREE(old);
	    return(NULL);
	}
    }

    FREE(saveString);
    for (i = 0; i < k; i++) {
	cuddDeref(old[i]);
	FREE(string[i]);
    }
    FREE(string);
    FREE(indices);
    return(old);

}  /* end of Cudd_bddPickArbitraryMinterms */


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

  Synopsis    [Extracts a subset from a BDD.]

  Description [Extracts a subset from a BDD in the following procedure.
  1. Compute the weight for each mask variable by counting the number of
     minterms for both positive and negative cofactors of the BDD with
     respect to each mask variable. (weight = #positive - #negative)
  2. Find a representative cube of the BDD by using the weight. From the
     top variable of the BDD, for each variable, if the weight is greater
     than 0.0, choose THEN branch, othereise ELSE branch, until meeting
     the constant 1.
  3. Quantify out the variables not in maskVars from the representative
     cube and if a variable in maskVars is don't care, replace the
     variable with a constant(1 or 0) depending on the weight.
  4. Make a subset of the BDD by multiplying with the modified cube.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode *
Cudd_SubsetWithMaskVars(
  DdManager * dd /* manager */,
  DdNode * f /* function from which to pick a cube */,
  DdNode ** vars /* array of variables */,
  int  nvars /* size of <code>vars</code> */,
  DdNode ** maskVars /* array of variables */,
  int  mvars /* size of <code>maskVars</code> */)
{
    double	*weight;
    char	*string;
    int		i, size;
    int		*indices, *mask;
    int		result;
    DdNode	*zero, *cube, *newCube, *subset;
    DdNode	*cof;

    DdNode	*support;
    support = Cudd_Support(dd,f);
    cuddRef(support);
    Cudd_RecursiveDeref(dd,support);

    zero = Cudd_Not(dd->one);
    size = dd->size;
    
    weight = ALLOC(double,size);
    if (weight == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }
    for (i = 0; i < size; i++) {
        weight[i] = 0.0;
    }
    for (i = 0; i < mvars; i++) {
	cof = Cudd_Cofactor(dd, f, maskVars[i]);
	cuddRef(cof);
	weight[i] = Cudd_CountMinterm(dd, cof, nvars);
	Cudd_RecursiveDeref(dd,cof);

	cof = Cudd_Cofactor(dd, f, Cudd_Not(maskVars[i]));
	cuddRef(cof);
	weight[i] -= Cudd_CountMinterm(dd, cof, nvars);
	Cudd_RecursiveDeref(dd,cof);
    }

    string = ALLOC(char, size + 1);
    if (string == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }
    mask = ALLOC(int, size);
    if (mask == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	FREE(string);
	return(NULL);
    }
    for (i = 0; i < size; i++) {
	string[i] = '2';
	mask[i] = 0;
    }
    string[size] = '\0';
    indices = ALLOC(int,nvars);
    if (indices == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	FREE(string);
	FREE(mask);
	return(NULL);
    }
    for (i = 0; i < nvars; i++) {
        indices[i] = vars[i]->index;
    }

    result = ddPickRepresentativeCube(dd,f,nvars,weight,string);
    if (result == 0) {
	FREE(string);
	FREE(mask);
	FREE(indices);
	return(NULL);
    }

    cube = Cudd_ReadOne(dd);
    cuddRef(cube);
    zero = Cudd_Not(Cudd_ReadOne(dd));
    for (i = 0; i < nvars; i++) {
	if (string[indices[i]] == '0') {
	    newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
	} else if (string[indices[i]] == '1') {
	    newCube = Cudd_bddIte(dd,cube,vars[i],zero);
	} else
	    continue;
	if (newCube == NULL) {
	    FREE(string);
	    FREE(mask);
	    FREE(indices);
	    Cudd_RecursiveDeref(dd,cube);
	    return(NULL);
	}
	cuddRef(newCube);
	Cudd_RecursiveDeref(dd,cube);
	cube = newCube;
    }
    Cudd_RecursiveDeref(dd,cube);

    for (i = 0; i < mvars; i++) {
	mask[maskVars[i]->index] = 1;
    }
    for (i = 0; i < nvars; i++) {
	if (mask[indices[i]]) {
	    if (string[indices[i]] == '2') {
		if (weight[indices[i]] >= 0.0)
		    string[indices[i]] = '1';
		else
		    string[indices[i]] = '0';
	    }
	} else {
	    string[indices[i]] = '2';
	}
    }

    cube = Cudd_ReadOne(dd);
    cuddRef(cube);
    zero = Cudd_Not(Cudd_ReadOne(dd));

    /* Build result BDD. */
    for (i = 0; i < nvars; i++) {
	if (string[indices[i]] == '0') {
	    newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero);
	} else if (string[indices[i]] == '1') {
	    newCube = Cudd_bddIte(dd,cube,vars[i],zero);
	} else
	    continue;
	if (newCube == NULL) {
	    FREE(string);
	    FREE(mask);
	    FREE(indices);
	    Cudd_RecursiveDeref(dd,cube);
	    return(NULL);
	}
	cuddRef(newCube);
	Cudd_RecursiveDeref(dd,cube);
	cube = newCube;
    }

    subset = Cudd_bddAnd(dd,f,cube);
    cuddRef(subset);
    Cudd_RecursiveDeref(dd,cube);

    /* Test. */
    if (Cudd_bddLeq(dd,subset,f)) {
	cuddDeref(subset);
    } else {
	Cudd_RecursiveDeref(dd,subset);
	subset = NULL;
    }

    FREE(string);
    FREE(mask);
    FREE(indices);
    FREE(weight);
    return(subset);

} /* end of Cudd_SubsetWithMaskVars */


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

  Synopsis    [Finds the first cube of a decision diagram.]

  Description [Defines an iterator on the onset of a decision diagram
  and finds its first cube. Returns a generator that contains the
  information necessary to continue the enumeration if successful; NULL
  otherwise.<p>
  A cube is represented as an array of literals, which are integers in
  {0, 1, 2}; 0 represents a complemented literal, 1 represents an
  uncomplemented literal, and 2 stands for don't care. The enumeration
  produces a disjoint cover of the function associated with the diagram.
  The size of the array equals the number of variables in the manager at
  the time Cudd_FirstCube is called.<p>
  For each cube, a value is also returned. This value is always 1 for a
  BDD, while it may be different from 1 for an ADD.
  For BDDs, the offset is the set of cubes whose value is the logical zero.
  For ADDs, the offset is the set of cubes whose value is the
  background value. The cubes of the offset are not enumerated.]

  SideEffects [The first cube and its value are returned as side effects.]

  SeeAlso     [Cudd_ForeachCube Cudd_NextCube Cudd_GenFree Cudd_IsGenEmpty
  Cudd_FirstNode]

******************************************************************************/
DdGen *
Cudd_FirstCube(
  DdManager * dd,
  DdNode * f,
  int ** cube,
  CUDD_VALUE_TYPE * value)
{
    DdGen *gen;
    DdNode *top, *treg, *next, *nreg, *prev, *preg;
    int i;
    int nvars;

    /* Sanity Check. */
    if (dd == NULL || f == NULL) return(NULL);

    /* Allocate generator an initialize it. */
    gen = ALLOC(DdGen,1);
    if (gen == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }

    gen->manager = dd;
    gen->type = CUDD_GEN_CUBES;
    gen->status = CUDD_GEN_EMPTY;
    gen->gen.cubes.cube = NULL;
    gen->gen.cubes.value = DD_ZERO_VAL;
    gen->stack.sp = 0;
    gen->stack.stack = NULL;
    gen->node = NULL;

    nvars = dd->size;
    gen->gen.cubes.cube = ALLOC(int,nvars);
    if (gen->gen.cubes.cube == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	FREE(gen);
	return(NULL);
    }
    for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;

    /* The maximum stack depth is one plus the number of variables.
    ** because a path may have nodes at all levels, including the
    ** constant level.
    */
    gen->stack.stack = ALLOC(DdNode *, nvars+1);
    if (gen->stack.stack == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	FREE(gen->gen.cubes.cube);
	FREE(gen);
	return(NULL);
    }
    for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;

    /* Find the first cube of the onset. */
    gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++;

    while (1) {
	top = gen->stack.stack[gen->stack.sp-1];
	treg = Cudd_Regular(top);
	if (!cuddIsConstant(treg)) {
	    /* Take the else branch first. */
	    gen->gen.cubes.cube[treg->index] = 0;
	    next = cuddE(treg);
	    if (top != treg) next = Cudd_Not(next);
	    gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
	} else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
	    /* Backtrack */
	    while (1) {
		if (gen->stack.sp == 1) {
		    /* The current node has no predecessor. */
		    gen->status = CUDD_GEN_EMPTY;
		    gen->stack.sp--;
		    goto done;
		}
		prev = gen->stack.stack[gen->stack.sp-2];
		preg = Cudd_Regular(prev);
		nreg = cuddT(preg);
		if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
		if (next != top) { /* follow the then branch next */
		    gen->gen.cubes.cube[preg->index] = 1;
		    gen->stack.stack[gen->stack.sp-1] = next;
		    break;
		}
		/* Pop the stack and try again. */
		gen->gen.cubes.cube[preg->index] = 2;
		gen->stack.sp--;
		top = gen->stack.stack[gen->stack.sp-1];
		treg = Cudd_Regular(top);
	    }
	} else {
	    gen->status = CUDD_GEN_NONEMPTY;
	    gen->gen.cubes.value = cuddV(top);
	    goto done;
	}
    }

done:
    *cube = gen->gen.cubes.cube;
    *value = gen->gen.cubes.value;
    return(gen);

} /* end of Cudd_FirstCube */


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

  Synopsis    [Generates the next cube of a decision diagram onset.]

  Description [Generates the next cube of a decision diagram onset,
  using generator gen. Returns 0 if the enumeration is completed; 1
  otherwise.]

  SideEffects [The cube and its value are returned as side effects. The
  generator is modified.]

  SeeAlso     [Cudd_ForeachCube Cudd_FirstCube Cudd_GenFree Cudd_IsGenEmpty
  Cudd_NextNode]

******************************************************************************/
int
Cudd_NextCube(
  DdGen * gen,
  int ** cube,
  CUDD_VALUE_TYPE * value)
{
    DdNode *top, *treg, *next, *nreg, *prev, *preg;
    DdManager *dd = gen->manager;

    /* Backtrack from previously reached terminal node. */
    while (1) {
	if (gen->stack.sp == 1) {
	    /* The current node has no predecessor. */
	    gen->status = CUDD_GEN_EMPTY;
	    gen->stack.sp--;
	    goto done;
	}
	top = gen->stack.stack[gen->stack.sp-1];
	treg = Cudd_Regular(top);
	prev = gen->stack.stack[gen->stack.sp-2];
	preg = Cudd_Regular(prev);
	nreg = cuddT(preg);
	if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
	if (next != top) { /* follow the then branch next */
	    gen->gen.cubes.cube[preg->index] = 1;
	    gen->stack.stack[gen->stack.sp-1] = next;
	    break;
	}
	/* Pop the stack and try again. */
	gen->gen.cubes.cube[preg->index] = 2;
	gen->stack.sp--;
    }

    while (1) {
	top = gen->stack.stack[gen->stack.sp-1];
	treg = Cudd_Regular(top);
	if (!cuddIsConstant(treg)) {
	    /* Take the else branch first. */
	    gen->gen.cubes.cube[treg->index] = 0;
	    next = cuddE(treg);
	    if (top != treg) next = Cudd_Not(next);
	    gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
	} else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) {
	    /* Backtrack */
	    while (1) {
		if (gen->stack.sp == 1) {
		    /* The current node has no predecessor. */
		    gen->status = CUDD_GEN_EMPTY;
		    gen->stack.sp--;
		    goto done;
		}
		prev = gen->stack.stack[gen->stack.sp-2];
		preg = Cudd_Regular(prev);
		nreg = cuddT(preg);
		if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;}
		if (next != top) { /* follow the then branch next */
		    gen->gen.cubes.cube[preg->index] = 1;
		    gen->stack.stack[gen->stack.sp-1] = next;
		    break;
		}
		/* Pop the stack and try again. */
		gen->gen.cubes.cube[preg->index] = 2;
		gen->stack.sp--;
		top = gen->stack.stack[gen->stack.sp-1];
		treg = Cudd_Regular(top);
	    }
	} else {
	    gen->status = CUDD_GEN_NONEMPTY;
	    gen->gen.cubes.value = cuddV(top);
	    goto done;
	}
    }

done:
    if (gen->status == CUDD_GEN_EMPTY) return(0);
    *cube = gen->gen.cubes.cube;
    *value = gen->gen.cubes.value;
    return(1);

} /* end of Cudd_NextCube */


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