cudddecomp.c

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

  Synopsis    [Free factors structure]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static void
ConjunctsFree(
  DdManager * dd,
  Conjuncts * factors)
{
    Cudd_RecursiveDeref(dd, factors->g);
    Cudd_RecursiveDeref(dd, factors->h);
    FREE(factors);
    return;

} /* end of ConjunctsFree */


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

  Synopsis    [Check whether the given pair is in the tables.]

  Description [.Check whether the given pair is in the tables.  gTable
  and hTable are combined.
  absence in both is indicated by 0,
  presence in gTable is indicated by 1,
  presence in hTable by 2 and
  presence in both by 3.
  The values returned by this function are PAIR_ST,
  PAIR_CR, G_ST, G_CR, H_ST, H_CR, BOTH_G, BOTH_H, NONE.
  PAIR_ST implies g in gTable and h in hTable
  PAIR_CR implies g in hTable and h in gTable
  G_ST implies g in gTable and h not in any table
  G_CR implies g in hTable and h not in any table
  H_ST implies h in hTable and g not in any table
  H_CR implies h in gTable and g not in any table
  BOTH_G implies both in gTable
  BOTH_H implies both in hTable
  NONE implies none in table; ]

  SideEffects []

  SeeAlso     [CheckTablesCacheAndReturn CheckInTables]

******************************************************************************/
static int
PairInTables(
  DdNode * g,
  DdNode * h,
  st_table * ghTable)
{
    int valueG, valueH, gPresent, hPresent;

    valueG = valueH = gPresent = hPresent = 0;
    
    gPresent = st_lookup_int(ghTable, (char *)Cudd_Regular(g), &valueG);
    hPresent = st_lookup_int(ghTable, (char *)Cudd_Regular(h), &valueH);

    if (!gPresent && !hPresent) return(NONE);

    if (!hPresent) {
	if (valueG & 1) return(G_ST);
	if (valueG & 2) return(G_CR);
    }
    if (!gPresent) {
	if (valueH & 1) return(H_CR);
	if (valueH & 2) return(H_ST);
    }
    /* both in tables */
    if ((valueG & 1) && (valueH & 2)) return(PAIR_ST);
    if ((valueG & 2) && (valueH & 1)) return(PAIR_CR);
    
    if (valueG & 1) {
	return(BOTH_G);
    } else {
	return(BOTH_H);
    }
    
} /* end of PairInTables */


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

  Synopsis    [Check the tables for the existence of pair and return one
  combination, cache the result.]

  Description [Check the tables for the existence of pair and return
  one combination, cache the result. The assumption is that one of the
  conjuncts is already in the tables.]

  SideEffects [g and h referenced for the cache]

  SeeAlso     [ZeroCase]

******************************************************************************/
static Conjuncts *
CheckTablesCacheAndReturn(
  DdNode * node,
  DdNode * g,
  DdNode * h,
  st_table * ghTable,
  st_table * cacheTable)
{
    int pairValue;
    int value;
    Conjuncts *factors;
    
    value = 0;
    /* check tables */
    pairValue = PairInTables(g, h, ghTable);
    assert(pairValue != NONE);
    /* if both dont exist in table, we know one exists(either g or h).
     * Therefore store the other and proceed
     */
    factors = ALLOC(Conjuncts, 1);
    if (factors == NULL) return(NULL);
    if ((pairValue == BOTH_H) || (pairValue == H_ST)) {
	if (g != one) {
	    value = 0;
	    if (st_lookup_int(ghTable, (char *)Cudd_Regular(g), &value)) {
		value |= 1;
	    } else {
		value = 1;
	    }
	    if (st_insert(ghTable, (char *)Cudd_Regular(g),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		return(NULL);
	    }
	}
	factors->g = g;
	factors->h = h;
    } else  if ((pairValue == BOTH_G) || (pairValue == G_ST)) {
	if (h != one) {
	    value = 0;
	    if (st_lookup_int(ghTable, (char *)Cudd_Regular(h), &value)) {
		value |= 2;
	    } else {
		value = 2;
	    }
	    if (st_insert(ghTable, (char *)Cudd_Regular(h),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		return(NULL);
	    }
	}
	factors->g = g;
	factors->h = h;
    } else if (pairValue == H_CR) {
	if (g != one) {
	    value = 2;
	    if (st_insert(ghTable, (char *)Cudd_Regular(g),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		return(NULL);
	    }
	}
	factors->g = h;
	factors->h = g;
    } else if (pairValue == G_CR) {
	if (h != one) {
	    value = 1;
	    if (st_insert(ghTable, (char *)Cudd_Regular(h),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		return(NULL);
	    }
	}
	factors->g = h;
	factors->h = g;
    } else if (pairValue == PAIR_CR) {
    /* pair exists in table */
	factors->g = h;
	factors->h = g;
    } else if (pairValue == PAIR_ST) {
	factors->g = g;
	factors->h = h;
    }
	    
    /* cache the result for this node */
    if (st_insert(cacheTable, (char *)node, (char *)factors) == ST_OUT_OF_MEM) {
	FREE(factors);
	return(NULL);
    }

    return(factors);

} /* end of CheckTablesCacheAndReturn */
	
/**Function********************************************************************

  Synopsis    [Check the tables for the existence of pair and return one
  combination, store in cache.]

  Description [Check the tables for the existence of pair and return
  one combination, store in cache. The pair that has more pointers to
  it is picked. An approximation of the number of local pointers is
  made by taking the reference count of the pairs sent. ]

  SideEffects []

  SeeAlso     [ZeroCase BuildConjuncts]

******************************************************************************/
static Conjuncts *
PickOnePair(
  DdNode * node,
  DdNode * g1,
  DdNode * h1,
  DdNode * g2,
  DdNode * h2,
  st_table * ghTable,
  st_table * cacheTable)
{
    int value;
    Conjuncts *factors;
    int oneRef, twoRef;
    
    factors = ALLOC(Conjuncts, 1);
    if (factors == NULL) return(NULL);

    /* count the number of pointers to pair 2 */
    if (h2 == one) {
	twoRef = (Cudd_Regular(g2))->ref;
    } else if (g2 == one) {
	twoRef = (Cudd_Regular(h2))->ref;
    } else {
	twoRef = ((Cudd_Regular(g2))->ref + (Cudd_Regular(h2))->ref)/2;
    }

    /* count the number of pointers to pair 1 */
    if (h1 == one) {
	oneRef  = (Cudd_Regular(g1))->ref;
    } else if (g1 == one) {
	oneRef  = (Cudd_Regular(h1))->ref;
    } else {
	oneRef = ((Cudd_Regular(g1))->ref + (Cudd_Regular(h1))->ref)/2;
    }

    /* pick the pair with higher reference count */
    if (oneRef >= twoRef) {
	factors->g = g1;
	factors->h = h1;
    } else {
	factors->g = g2;
	factors->h = h2;
    }
    
    /*
     * Store computed factors in respective tables to encourage
     * recombination.
     */
    if (factors->g != one) {
	/* insert g in htable */
	value = 0;
	if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->g), &value)) {
	    if (value == 2) {
		value |= 1;
		if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
			      (char *)(long)value) == ST_OUT_OF_MEM) {
		    FREE(factors);
		    return(NULL);
		}
	    }
	} else {
	    value = 1;
	    if (st_insert(ghTable, (char *)Cudd_Regular(factors->g),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		FREE(factors);
		return(NULL);
	    }
	}
    }

    if (factors->h != one) {
	/* insert h in htable */
	value = 0;
	if (st_lookup_int(ghTable, (char *)Cudd_Regular(factors->h), &value)) {
	    if (value == 1) {
		value |= 2;
		if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
			      (char *)(long)value) == ST_OUT_OF_MEM) {
		    FREE(factors);
		    return(NULL);
		}
	    }	    
	} else {
	    value = 2;
	    if (st_insert(ghTable, (char *)Cudd_Regular(factors->h),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		FREE(factors);
		return(NULL);
	    }
	}
    }
    
    /* Store factors in cache table for later use. */
    if (st_insert(cacheTable, (char *)node, (char *)factors) ==
	    ST_OUT_OF_MEM) {
	FREE(factors);
	return(NULL);
    }

    return(factors);

} /* end of PickOnePair */


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

  Synopsis [Check if the two pairs exist in the table, If any of the
  conjuncts do exist, store in the cache and return the corresponding pair.]

  Description [Check if the two pairs exist in the table. If any of
  the conjuncts do exist, store in the cache and return the
  corresponding pair.]

  SideEffects []

  SeeAlso     [ZeroCase BuildConjuncts]

******************************************************************************/
static Conjuncts *
CheckInTables(
  DdNode * node,
  DdNode * g1,
  DdNode * h1,
  DdNode * g2,
  DdNode * h2,
  st_table * ghTable,
  st_table * cacheTable,
  int * outOfMem)
{
    int pairValue1,  pairValue2;
    Conjuncts *factors;
    int value;
    
    *outOfMem = 0;

    /* check existence of pair in table */
    pairValue1 = PairInTables(g1, h1, ghTable);
    pairValue2 = PairInTables(g2, h2, ghTable);

    /* if none of the 4 exist in the gh tables, return NULL */
    if ((pairValue1 == NONE) && (pairValue2 == NONE)) {
	return NULL;
    }
    
    factors = ALLOC(Conjuncts, 1);
    if (factors == NULL) {
	*outOfMem = 1;
	return NULL;
    }

    /* pairs that already exist in the table get preference. */
    if (pairValue1 == PAIR_ST) {
	factors->g = g1;
	factors->h = h1;
    } else if (pairValue2 == PAIR_ST) {
	factors->g = g2;
	factors->h = h2;
    } else if (pairValue1 == PAIR_CR) {
	factors->g = h1;
	factors->h = g1;
    } else if (pairValue2 == PAIR_CR) {
	factors->g = h2;
	factors->h = g2;
    } else if (pairValue1 == G_ST) {
	/* g exists in the table, h is not found in either table */
	factors->g = g1;
	factors->h = h1;
	if (h1 != one) {
	    value = 2;
	    if (st_insert(ghTable, (char *)Cudd_Regular(h1),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		*outOfMem = 1;
		FREE(factors);
		return(NULL);
	    }
	}
    } else if (pairValue1 == BOTH_G) {
	/* g and h are  found in the g table */
	factors->g = g1;
	factors->h = h1;
	if (h1 != one) {
	    value = 3;
	    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_ST) {
	/* h exists in the table, g is not found in either table */
	factors->g = g1;
	factors->h = h1;
	if (g1 != one) {
	    value = 1;
	    if (st_insert(ghTable, (char *)Cudd_Regular(g1),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		*outOfMem = 1;
		FREE(factors);
		return(NULL);
	    }
	}
    } else if (pairValue1 == BOTH_H) {
	/* g and h are  found in the h table */
	factors->g = g1;
	factors->h = h1;
	if (g1 != one) {
	    value = 3;
	    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_ST) {
	/* g exists in the table, h is not found in either table */
	factors->g = g2;
	factors->h = h2;
	if (h2 != one) {
	    value = 2;
	    if (st_insert(ghTable, (char *)Cudd_Regular(h2),
			  (char *)(long)value) == ST_OUT_OF_MEM) {
		*outOfMem = 1;
		FREE(factors);
		return(NULL);
	    }