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

  Synopsis    [Performs the recursive step of Cuddaux_IsVarIn.]

  Description [Performs the recursive step of Cuddaux_IsVarIn. var is
  supposed to be a BDD projection function. Returns the logical one or
  zero.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode*
cuddauxIsVarInRecur(DdManager* manager, DdNode* f, DdNode* Var)
{
  DdNode *zero,*one, *F, *res;
  int topV,topF;

  one = DD_ONE(manager);
  zero = Cudd_Not(one);
  F = Cudd_Regular(f);

  if (cuddIsConstant(F)) return zero;
  if (Var==F) return(one);

  topV = Var->index;
  topF = F->index;
  if (topF == topV) return(one);
  if (cuddI(manager,topV) < cuddI(manager,topF)) return(zero);

  res = cuddCacheLookup2(manager,cuddauxIsVarInRecur, F, Var);
  if (res != NULL) return(res);
  res = cuddauxIsVarInRecur(manager,cuddT(F),Var);
  if (res==zero){
    res = cuddauxIsVarInRecur(manager,cuddE(F),Var);
  }
  cuddCacheInsert2(manager,cuddauxIsVarInRecur,F,Var,res);
  return(res);
}

DdNode*
cuddauxAddGuardOfNodeRecur(DdManager* manager, DdNode* f, DdNode* h)
{
  DdNode *one, *res, *T, *E;
  int topf, toph;

  /* Handle terminal cases */
  one = DD_ONE(manager);
  if (f==h){
    return(one);
  }
  topf = cuddI(manager,f->index);
  toph = cuddI(manager,h->index);
  if (topf >= toph){
    return Cudd_Not(one);
  }

  /* Look in the cache */
  res = cuddCacheLookup2(manager,Cuddaux_addGuardOfNode,f,h);
  if (res != NULL)
    return(res);

  T = cuddauxAddGuardOfNodeRecur(manager,cuddT(f),h);
  if (T == NULL)
    return(NULL);
  cuddRef(T);
  E = cuddauxAddGuardOfNodeRecur(manager,cuddE(f),h);
  if (E == NULL){
    Cudd_IterDerefBdd(manager, T);
    return(NULL);
  }
  cuddRef(E);
  if (T == E){
    res = T;
  }
  else {
    if (Cudd_IsComplement(T)){
      res = cuddUniqueInter(manager,f->index,Cudd_Not(T),Cudd_Not(E));
      if (res == NULL) {
	Cudd_IterDerefBdd(manager, T);
	Cudd_IterDerefBdd(manager, E);
	return(NULL);
      }
      res = Cudd_Not(res);
    }
    else {
      res = cuddUniqueInter(manager,f->index,T,E);
      if (res == NULL) {
	Cudd_IterDerefBdd(manager, T);
	Cudd_IterDerefBdd(manager, E);
	return(NULL);
      }
    }
  }
  cuddDeref(T);
  cuddDeref(E);
  cuddCacheInsert2(manager,Cuddaux_addGuardOfNode,f,h,res);
  return(res);
}

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

  Synopsis    [Determines whether f is less than or equal to g.]

  Description [Returns 1 if f is less than or equal to g; 0 otherwise.
  No new nodes are created. This procedure works for arbitrary ADDs.
  For 0-1 ADDs Cudd_addEvalConst is more efficient.]

  SideEffects [None]

  SeeAlso     [Cudd_addIteConstant Cudd_addEvalConst Cudd_bddLeq]

******************************************************************************/
int
Cudd_addLeq(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    DdNode *tmp, *fv, *fvn, *gv, *gvn;
    unsigned int topf, topg, res;

    /* Terminal cases. */
    if (f == g) return(1);

    statLine(dd);
    if (cuddIsConstant(f)) {
	if (cuddIsConstant(g)) return(cuddV(f) <= cuddV(g));
	if (f == DD_MINUS_INFINITY(dd)) return(1);
	if (f == DD_PLUS_INFINITY(dd)) return(0); /* since f != g */
    }
    if (g == DD_PLUS_INFINITY(dd)) return(1);
    if (g == DD_MINUS_INFINITY(dd)) return(0); /* since f != g */

    /* Check cache. */
    tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_addLeq,f,g);
    if (tmp != NULL) {
	return(tmp == DD_ONE(dd));
    }

    /* Compute cofactors. One of f and g is not constant. */
    topf = cuddI(dd,f->index);
    topg = cuddI(dd,g->index);
    if (topf <= topg) {
	fv = cuddT(f); fvn = cuddE(f);
    } else {
	fv = fvn = f;
    }
    if (topg <= topf) {
	gv = cuddT(g); gvn = cuddE(g);
    } else {
	gv = gvn = g;
    }

    res = Cudd_addLeq(dd,fvn,gvn) && Cudd_addLeq(dd,fv,gv);

    /* Store result in cache and return. */
    cuddCacheInsert2(dd,(DD_CTFP) Cudd_addLeq,f,g,
		     Cudd_NotCond(DD_ONE(dd),res==0));
    return(res);

} /* end of Cudd_addLeq */

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

  Synopsis    [Performs the recursive step of Cuddaux_NodesBelowLevelRecur.]

  Description [Performs the recursive step of
  Cuddaux_NodesBelowLevelRecur.  F is supposed to be a regular
  node. Returns 1 if successful, NULL otherwise.
  The background node is not put in the list if take_background==0 ]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static int
cuddauxNodesBelowLevelRecur(DdManager* manager, DdNode* F, int level,
			    cuddaux_list_t** plist, st_table* visited,
			    size_t max, size_t* psize,
			    bool take_background)
{
  int topF,res;

  if ((!take_background && F==DD_BACKGROUND(manager)) || st_is_member(visited, (char *) F) == 1){
    return 1;
  }
  topF = cuddI(manager,F->index);
  if (topF < level){
    res = cuddauxNodesBelowLevelRecur(manager, Cudd_Regular(cuddT(F)), level, plist, visited, max, psize, take_background);
    if (res==0) return 0;
    if (max == 0 || *psize<max){
      res = cuddauxNodesBelowLevelRecur(manager, Cudd_Regular(cuddE(F)), level, plist, visited, max, psize, take_background);
      if (res==0) return 0;
    }
  }
  else {
    res = cuddaux_list_add(plist,F);
    (*psize)++;
    if (res==0) return 0;
  }
  if (st_add_direct(visited, (char *) F, NULL) == ST_OUT_OF_MEM){
    cuddaux_list_free(*plist);
    return 0;
  }
  return 1;
}

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

  Synopsis [Computes the fraction of minterms in the on-set of all the
  positive cofactors of a BDD or ADD.]

  Description [Computes the fraction of minterms in the on-set of all
  the positive cofactors of DD. Returns the pointer to an array of
  doubles if successful; NULL otherwise. The array hs as many
  positions as there are BDD variables in the manager plus one. The
  last position of the array contains the fraction of the minterms in
  the ON-set of the function represented by the BDD or ADD. The other
  positions of the array hold the variable signatures.]

  SideEffects [None]

******************************************************************************/
double *
Cudd_CofMinterm(
  DdManager * dd,
  DdNode * node)
{
    st_table	*table;
    double	*values;
    double	*result = NULL;
    int		i, firstLevel;

#ifdef DD_STATS
    long startTime;
    startTime = util_cpu_time();
    num_calls = 0;
    table_mem = sizeof(st_table);
#endif

    table = st_init_table(st_ptrcmp, st_ptrhash);
    if (table == NULL) {
	(void) fprintf(stdout,"out-of-memory, couldn't measure DD cofactors.\n");
	return(NULL);
    }
    size = dd->size;
    values = ddCofMintermAux(dd, node, table);
    if (values != NULL) {
	result = ALLOC(double,size + 1);
	if (result != NULL) {
#ifdef DD_STATS
	    table_mem += (size + 1) * sizeof(double);
#endif
	    if (Cudd_IsConstant(node))
		firstLevel = 1;
	    else
		firstLevel = cuddI(dd,Cudd_Regular(node)->index);
	    for (i = 0; i < size; i++) {
		if (i >= cuddI(dd,Cudd_Regular(node)->index)) {
		    result[dd->invperm[i]] = values[i - firstLevel];
		} else {
		    result[dd->invperm[i]] = values[size - firstLevel];
		}
	    }
	    result[size] = values[size - firstLevel];
	} else {
	    dd->errorCode = CUDD_MEMORY_OUT;
	}
    }

/**
 * Internal function
 */
double recurse_getNofSatisfyingAssignments(DdManager *dd, DdNode *orig, DdNode *cube, std::map<DdNode*,double> &buffer) {

	// Normalize the cube
	DdNode *cubeNext;
	if (Cudd_Regular(cube)==cube) {
		cubeNext = cuddT(cube);
	} else {
		if (!Cudd_IsConstant(cube)) {
			cube = Cudd_Regular(cube);
			cubeNext = (DdNode*)(((size_t)(cuddE(cube)) ^ 0x1));
		} else {
			// Constant
			return (orig==dd->one)?1:0;
		}
	}

	if (buffer.count(orig)>0) return buffer[orig];
	if (Cudd_IsConstant(orig)) {
		if (Cudd_IsConstant(cube)) {
			return (orig==dd->one)?1:0;
		} else {
			return 2*recurse_getNofSatisfyingAssignments(dd,orig,cubeNext,buffer);
		}
	}

	size_t xoring = (Cudd_Regular(orig)==orig?0:1);
	DdNode *reference = Cudd_Regular(orig);

	if (Cudd_IsConstant(cube)) return std::numeric_limits<double>::quiet_NaN(); // Missing variable!
	int i1 = cuddI(dd,cube->index);
	int i2 = cuddI(dd,reference->index);

	if (i1<i2) {
		double value = 2*recurse_getNofSatisfyingAssignments(dd,(DdNode*)((size_t)reference ^ xoring),cubeNext,buffer);
		buffer[orig] = value;
		return value;
	} else if (i1>i2) {
		return std::numeric_limits<double>::quiet_NaN();
	} else {
		double value = recurse_getNofSatisfyingAssignments(dd,(DdNode*)((size_t)(cuddT(reference)) ^ xoring),cubeNext,buffer)
			+ recurse_getNofSatisfyingAssignments(dd,(DdNode*)((size_t)(cuddE(reference)) ^ xoring),cubeNext,buffer);

		buffer[orig] = value;
		return value;
	}
}

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

  Synopsis    [Performs the recursive steps of Cudd_bddBoleanDiff.]

  Description [Performs the recursive steps of Cudd_bddBoleanDiff.
  Returns the BDD obtained by XORing the cofactors of f with respect to
  var if successful; NULL otherwise. Exploits the fact that dF/dx =
  dF'/dx.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode *
cuddBddBooleanDiffRecur(
  DdManager * manager,
  DdNode * f,
  DdNode * var)
{
    DdNode *T, *E, *res, *res1, *res2;

    statLine(manager);
    if (cuddI(manager,f->index) > manager->perm[var->index]) {
	/* f does not depend on var. */
	return(Cudd_Not(DD_ONE(manager)));
    }

    /* From now on, f is non-constant. */

    /* If the two indices are the same, so are their levels. */
    if (f->index == var->index) {
	res = cuddBddXorRecur(manager, cuddT(f), cuddE(f));
        return(res);
    }

    /* From now on, cuddI(manager,f->index) < cuddI(manager,cube->index). */

    /* Check the cache. */
    res = cuddCacheLookup2(manager, cuddBddBooleanDiffRecur, f, var);
    if (res != NULL) {
	return(res);
    }

    /* Compute the cofactors of f. */
    T = cuddT(f); E = cuddE(f);

    res1 = cuddBddBooleanDiffRecur(manager, T, var);
    if (res1 == NULL) return(NULL);
    cuddRef(res1);
    res2 = cuddBddBooleanDiffRecur(manager, Cudd_Regular(E), var);
    if (res2 == NULL) {
	Cudd_IterDerefBdd(manager, res1);
	return(NULL);
    }
    cuddRef(res2);
    /* ITE takes care of possible complementation of res1 and of the
    ** case in which res1 == res2. */
    res = cuddBddIteRecur(manager, manager->vars[f->index], res1, res2);
    if (res == NULL) {
	Cudd_IterDerefBdd(manager, res1);
	Cudd_IterDerefBdd(manager, res2);
	return(NULL);
    }
    cuddDeref(res1);
    cuddDeref(res2);
    cuddCacheInsert2(manager, cuddBddBooleanDiffRecur, f, var, res);
    return(res);

} /* end of cuddBddBooleanDiffRecur */

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

  Synopsis    [Performs the recursive step of Cudd_addMonadicApply.]

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

  SideEffects [None]

  SeeAlso     [cuddAddApplyRecur]

******************************************************************************/
DdNode *
cuddAddMonadicApplyRecur(
  DdManager * dd,
  DdNode * (*op)(DdManager *, DdNode *),
  DdNode * f)
{
    DdNode *res, *ft, *fe, *T, *E;
    unsigned int ford;
    unsigned int index;

    /* Check terminal cases. */
    statLine(dd);
    res = (*op)(dd,f);
    if (res != NULL) return(res);

    /* Check cache. */
    res = cuddCacheLookup1(dd,op,f);
    if (res != NULL) return(res);

    /* Recursive step. */
    ford = cuddI(dd,f->index);
    index = f->index;
    ft = cuddT(f);
    fe = cuddE(f);

    T = cuddAddMonadicApplyRecur(dd,op,ft);
    if (T == NULL) return(NULL);
    cuddRef(T);

    E = cuddAddMonadicApplyRecur(dd,op,fe);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd,T);
	return(NULL);
    }
    cuddRef(E);

    res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
    if (res == NULL) {
	Cudd_RecursiveDeref(dd, T);
	Cudd_RecursiveDeref(dd, E);
	return(NULL);
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert1(dd,op,f,res);

    return(res);

} /* end of cuddAddMonadicApplyRecur */

/**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 */

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

  Synopsis [Picks unique member from equiv expressions.]

  Description [Reduces 2 variable expressions to canonical form.]

  SideEffects [None]

  SeeAlso     [bddVarToConst bddVarToCanonicalSimple]

******************************************************************************/
static int
bddVarToCanonical(
  DdManager * dd,
  DdNode ** fp,
  DdNode ** gp,
  DdNode ** hp,
  unsigned int * topfp,
  unsigned int * topgp,
  unsigned int * tophp)
{
    register DdNode             *F, *G, *H, *r, *f, *g, *h;
    register unsigned int       topf, topg, toph;
    DdNode                      *one = dd->one;
    int                         comple, change;

    f = *fp;
    g = *gp;
    h = *hp;
    F = Cudd_Regular(f);
    G = Cudd_Regular(g);
    H = Cudd_Regular(h);
    topf = cuddI(dd,F->index);
    topg = cuddI(dd,G->index);
    toph = cuddI(dd,H->index);

    change = 0;

    if (G == one) {                     /* ITE(F,c,H) */
        if ((topf > toph) || (topf == toph && cuddF2L(f) > cuddF2L(h))) {
            r = h;
            h = f;
            f = r;                      /* ITE(F,1,H) = ITE(H,1,F) */
            if (g != one) {     /* g == zero */
                f = Cudd_Not(f);                /* ITE(F,0,H) = ITE(!H,0,!F) */
                h = Cudd_Not(h);
            }
            change = 1;
        }
    } else if (H == one) {              /* ITE(F,G,c) */
        if ((topf > topg) || (topf == topg && cuddF2L(f) > cuddF2L(g))) {
            r = g;
            g = f;
            f = r;                      /* ITE(F,G,0) = ITE(G,F,0) */
            if (h == one) {
                f = Cudd_Not(f);                /* ITE(F,G,1) = ITE(!G,!F,1) */
                g = Cudd_Not(g);
            }
            change = 1;
        }
    } else if (g == Cudd_Not(h)) {      /* ITE(F,G,!G) = ITE(G,F,!F) */
        if ((topf > topg) || (topf == topg && cuddF2L(f) > cuddF2L(g))) {
            r = f;
            f = g;
            g = r;
            h = Cudd_Not(r);
            change = 1;
        }
    }
    /* adjust pointers so that the first 2 arguments to ITE are regular */
    if (Cudd_IsComplement(f) != 0) {    /* ITE(!F,G,H) = ITE(F,H,G) */
        f = Cudd_Not(f);
        r = g;
        g = h;
        h = r;
        change = 1;
    }
    comple = 0;
    if (Cudd_IsComplement(g) != 0) {    /* ITE(F,!G,H) = !ITE(F,G,!H) */
        g = Cudd_Not(g);
        h = Cudd_Not(h);
        change = 1;
        comple = 1;
    }
    if (change != 0) {
        *fp = f;
        *gp = g;
        *hp = h;
    }
    *topfp = cuddI(dd,f->index);
    *topgp = cuddI(dd,g->index);
    *tophp = cuddI(dd,Cudd_Regular(h)->index);

    return(comple);

} /* end of bddVarToCanonical */

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

  Synopsis    [Performs the recursive step of Cudd_addApply.]

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

  SideEffects [None]

  SeeAlso     [cuddAddMonadicApplyRecur]

******************************************************************************/
DdNode *
cuddAddApplyRecur(
  DdManager * dd,
  DdNode * (*op)(DdManager *, DdNode **, DdNode **),
  DdNode * f,
  DdNode * g)
{
    DdNode *res,
	   *fv, *fvn, *gv, *gvn,
	   *T, *E;
    unsigned int ford, gord;
    unsigned int index;
    DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);

    /* Check terminal cases. Op may swap f and g to increase the
     * cache hit rate.
     */
    statLine(dd);
    res = (*op)(dd,&f,&g);
    if (res != NULL) return(res);

    /* Check cache. */
    cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *)) op;
    res = cuddCacheLookup2(dd,cacheOp,f,g);
    if (res != NULL) return(res);

    /* Recursive step. */
    ford = cuddI(dd,f->index);
    gord = cuddI(dd,g->index);
    if (ford <= gord) {
	index = f->index;
	fv = cuddT(f);
	fvn = cuddE(f);
    } else {
	index = g->index;
	fv = fvn = f;
    }
    if (gord <= ford) {
	gv = cuddT(g);
	gvn = cuddE(g);
    } else {
	gv = gvn = g;
    }

    T = cuddAddApplyRecur(dd,op,fv,gv);
    if (T == NULL) return(NULL);
    cuddRef(T);

    E = cuddAddApplyRecur(dd,op,fvn,gvn);
    if (E == NULL) {
	Cudd_RecursiveDeref(dd,T);
	return(NULL);
    }
    cuddRef(E);

    res = (T == E) ? T : cuddUniqueInter(dd,(int)index,T,E);
    if (res == NULL) {
	Cudd_RecursiveDeref(dd, T);
	Cudd_RecursiveDeref(dd, E);
	return(NULL);
    }
    cuddDeref(T);
    cuddDeref(E);

    /* Store result. */
    cuddCacheInsert2(dd,cacheOp,f,g,res);

    return(res);

} /* end of cuddAddApplyRecur */

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

  Synopsis    [Performs the recursive step of
  Cudd_bddLiteralSetIntersection.]

  Description [Performs the recursive step of
  Cudd_bddLiteralSetIntersection. Scans the cubes for common variables,
  and checks whether they agree in phase.  Returns a pointer to the
  resulting cube if successful; NULL otherwise.]

  SideEffects [None]

******************************************************************************/
DdNode *
cuddBddLiteralSetIntersectionRecur(
    DdManager * dd,
    DdNode * f,
    DdNode * g)
{
    DdNode *res, *tmp;
    DdNode *F, *G;
    DdNode *fc, *gc;
    DdNode *one;
    DdNode *zero;
    unsigned int topf, topg, comple;
    int phasef, phaseg;

    statLine(dd);
    if (f == g) return(f);

    F = Cudd_Regular(f);
    G = Cudd_Regular(g);
    one = DD_ONE(dd);

    /* Here f != g. If F == G, then f and g are complementary.
    ** Since they are two cubes, this case only occurs when f == v,
    ** g == v', and v is a variable or its complement.
    */
    if (F == G) return(one);

    zero = Cudd_Not(one);
    topf = cuddI(dd,F->index);
    topg = cuddI(dd,G->index);
    /* Look for a variable common to both cubes. If there are none, this
    ** loop will stop when the constant node is reached in both cubes.
    */
    while (topf != topg) {
        if (topf < topg) {	/* move down on f */
            comple = f != F;
            f = cuddT(F);
            if (comple) f = Cudd_Not(f);
            if (f == zero) {
                f = cuddE(F);
                if (comple) f = Cudd_Not(f);
            }
            F = Cudd_Regular(f);
            topf = cuddI(dd,F->index);
        } else if (topg < topf) {
            comple = g != G;
            g = cuddT(G);
            if (comple) g = Cudd_Not(g);
            if (g == zero) {
                g = cuddE(G);
                if (comple) g = Cudd_Not(g);
            }
            G = Cudd_Regular(g);
            topg = cuddI(dd,G->index);
        }
    }

    /* At this point, f == one <=> g == 1. It suffices to test one of them. */
    if (f == one) return(one);

    res = cuddCacheLookup2(dd,Cudd_bddLiteralSetIntersection,f,g);
    if (res != NULL) {
        return(res);
    }

    /* Here f and g are both non constant and have the same top variable. */
    comple = f != F;
    fc = cuddT(F);
    phasef = 1;
    if (comple) fc = Cudd_Not(fc);
    if (fc == zero) {
        fc = cuddE(F);
        phasef = 0;
        if (comple) fc = Cudd_Not(fc);
    }
    comple = g != G;
    gc = cuddT(G);
    phaseg = 1;
    if (comple) gc = Cudd_Not(gc);
    if (gc == zero) {
        gc = cuddE(G);
        phaseg = 0;
        if (comple) gc = Cudd_Not(gc);
    }

    tmp = cuddBddLiteralSetIntersectionRecur(dd,fc,gc);
    if (tmp == NULL) {
//.........这里部分代码省略.........

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

  Synopsis    [Checks whether ADD g is constant whenever ADD f is 1.]

  Description [Checks whether ADD g is constant whenever ADD f is 1.  f
  must be a 0-1 ADD.  Returns a pointer to the resulting ADD (which may
  or may not be constant) or DD_NON_CONSTANT. If f is identically 0,
  the check is assumed to be successful, and the background value is
  returned. No new nodes are created.]

  SideEffects [None]

  SeeAlso     [Cudd_addIteConstant Cudd_addLeq]

******************************************************************************/
DdNode *
Cudd_addEvalConst(
  DdManager * dd,
  DdNode * f,
  DdNode * g)
{
    DdNode *zero;
    DdNode *Fv,*Fnv,*Gv,*Gnv,*r,*t,*e;
    unsigned int topf,topg;

#ifdef DD_DEBUG
    assert(!Cudd_IsComplement(f));
#endif

    statLine(dd);
    /* Terminal cases. */
    if (f == DD_ONE(dd) || cuddIsConstant(g)) {
        return(g);
    }
    if (f == (zero = DD_ZERO(dd))) {
        return(dd->background);
    }

#ifdef DD_DEBUG
    assert(!cuddIsConstant(f));
#endif
    /* From now on, f and g are known not to be constants. */

    topf = cuddI(dd,f->index);
    topg = cuddI(dd,g->index);

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

    /* Compute cofactors. */
    if (topf <= topg) {
        Fv = cuddT(f); Fnv = cuddE(f);
    } else {
        Fv = Fnv = f;
    }
    if (topg <= topf) {
        Gv = cuddT(g); Gnv = cuddE(g);
    } else {
        Gv = Gnv = g;
    }
    
    /* Recursive step. */
    if (Fv != zero) {
	t = Cudd_addEvalConst(dd,Fv,Gv);
	if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) {
	    cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
	    return(DD_NON_CONSTANT);
	}
	if (Fnv != zero) {
	    e = Cudd_addEvalConst(dd,Fnv,Gnv);
	    if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) {
		cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT);
		return(DD_NON_CONSTANT);
	    }
	}
	cuddCacheInsert2(dd,Cudd_addEvalConst,f,g,t);
	return(t);
    } else { /* Fnv must be != zero */
	e = Cudd_addEvalConst(dd,Fnv,Gnv);
	cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, e);
	return(e);
    }

} /* end of Cudd_addEvalConst */

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

  Synopsis    [Performs the reordering-sensitive step of Extra_zddTupleFromBdd().]

  Description [Generates in a bottom-up fashion ZDD for all combinations
               composed of k variables out of variables belonging to Support.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode* extraZddTuplesFromBdd( 
  DdManager * dd,   /* the DD manager */
  DdNode * bVarsK,   /* the number of variables in tuples */
  DdNode * bVarsN)   /* the set of all variables */
{
    DdNode *zRes, *zRes0, *zRes1;
    statLine(dd); 

    /* terminal cases */
/*  if ( k < 0 || k > n )
 *      return dd->zero;
 *  if ( n == 0 )
 *      return dd->one; 
 */
    if ( cuddI( dd, bVarsK->index ) < cuddI( dd, bVarsN->index ) )
        return z0;
    if ( bVarsN == b1 )
        return z1;

    /* check cache */
    zRes = cuddCacheLookup2Zdd(dd, extraZddTuplesFromBdd, bVarsK, bVarsN);
    if (zRes)
        return(zRes);

    /* ZDD in which this variable is 0 */
/*  zRes0 = extraZddTuplesFromBdd( dd, k,     n-1 ); */
    zRes0 = extraZddTuplesFromBdd( dd, bVarsK, cuddT(bVarsN) );
    if ( zRes0 == NULL ) 
        return NULL;
    cuddRef( zRes0 );

    /* ZDD in which this variable is 1 */
/*  zRes1 = extraZddTuplesFromBdd( dd, k-1,          n-1 ); */
    if ( bVarsK == b1 )
    {
        zRes1 = z0;
        cuddRef( zRes1 );
    }
    else
    {
        zRes1 = extraZddTuplesFromBdd( dd, cuddT(bVarsK), cuddT(bVarsN) );
        if ( zRes1 == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes0 );
            return NULL;
        }
        cuddRef( zRes1 );
    }

    /* compose Res0 and Res1 with the given ZDD variable */
    zRes = cuddZddGetNode( dd, 2*bVarsN->index, zRes1, zRes0 );
    if ( zRes == NULL ) 
    {
        Cudd_RecursiveDerefZdd( dd, zRes0 );
        Cudd_RecursiveDerefZdd( dd, zRes1 );
        return NULL;
    }
    cuddDeref( zRes0 );
    cuddDeref( zRes1 );

    /* insert the result into cache */
    cuddCacheInsert2(dd, extraZddTuplesFromBdd, bVarsK, bVarsN, zRes);
    return zRes;

} /* end of extraZddTuplesFromBdd */

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

  Synopsis    [Implements the recursive step of Cudd_addIte(f,g,h).]

  Description [Implements the recursive step of Cudd_addIte(f,g,h).
  Returns a pointer to the resulting ADD if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addIte]

******************************************************************************/
DdNode *
cuddAddIteRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * g,
  DdNode * h)
{
    DdNode *one,*zero;
    DdNode *r,*Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*t,*e;
    unsigned int topf,topg,toph,v;
    int index;

    statLine(dd);
    /* Trivial cases. */

    /* One variable cases. */
    if (f == (one = DD_ONE(dd))) {	/* ITE(1,G,H) = G */
        return(g);
    }
    if (f == (zero = DD_ZERO(dd))) {	/* ITE(0,G,H) = H */
        return(h);
    }

    /* From now on, f is known to not be a constant. */
    addVarToConst(f,&g,&h,one,zero);

    /* Check remaining one variable cases. */
    if (g == h) {			/* ITE(F,G,G) = G */
        return(g);
    }

    if (g == one) {			/* ITE(F,1,0) = F */
        if (h == zero) return(f);
    }

    topf = cuddI(dd,f->index);
    topg = cuddI(dd,g->index);
    toph = cuddI(dd,h->index);
    v = ddMin(topg,toph);

    /* A shortcut: ITE(F,G,H) = (x,G,H) if F=(x,1,0), x < top(G,H). */
    if (topf < v && cuddT(f) == one && cuddE(f) == zero) {
	r = cuddUniqueInter(dd,(int)f->index,g,h);
	return(r);
    }
    if (topf < v && cuddT(f) == zero && cuddE(f) == one) {
	r = cuddUniqueInter(dd,(int)f->index,h,g);
	return(r);
    }

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

    /* Compute cofactors. */
    if (topf <= v) {
	v = ddMin(topf,v);	/* v = top_var(F,G,H) */
	index = f->index;
        Fv = cuddT(f); Fnv = cuddE(f);
    } else {
        Fv = Fnv = f;
    }
    if (topg == v) {
	index = g->index;
        Gv = cuddT(g); Gnv = cuddE(g);
    } else {
        Gv = Gnv = g;
    }
    if (toph == v) {
	index = h->index;
        Hv = cuddT(h); Hnv = cuddE(h);
    } else {
        Hv = Hnv = h;
    }
    
    /* Recursive step. */
    t = cuddAddIteRecur(dd,Fv,Gv,Hv);
    if (t == NULL) return(NULL);
    cuddRef(t);

    e = cuddAddIteRecur(dd,Fnv,Gnv,Hnv);
    if (e == NULL) {
	Cudd_RecursiveDeref(dd,t);
	return(NULL);
    }
//.........这里部分代码省略.........

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

  Synopsis [Performs the recursive step of Cudd_zddPortFromBdd.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
static DdNode *
zddPortFromBddStep(
  DdManager * dd,
  DdNode * B,
  int  expected)
{
    DdNode	*res, *prevZdd, *t, *e;
    DdNode	*Breg, *Bt, *Be;
    int		id, level;

    statLine(dd);
    /* Terminal cases. */
    if (B == Cudd_Not(DD_ONE(dd)))
	return(DD_ZERO(dd));
    if (B == DD_ONE(dd)) {
	if (expected >= dd->sizeZ) {
	    return(DD_ONE(dd));
	} else {
	    return(dd->univ[expected]);
	}
    }

    Breg = Cudd_Regular(B);

    /* Computed table look-up. */
    res = cuddCacheLookup1Zdd(dd,Cudd_zddPortFromBdd,B);
    if (res != NULL) {
	level = cuddI(dd,Breg->index);
	/* Adding DC vars. */
	if (expected < level) {
	    /* Add suppressed variables. */
	    cuddRef(res);
	    for (level--; level >= expected; level--) {
		prevZdd = res;
		id = dd->invperm[level];
		res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
		if (res == NULL) {
		    Cudd_RecursiveDerefZdd(dd, prevZdd);
		    return(NULL);
		}
		cuddRef(res);
		Cudd_RecursiveDerefZdd(dd, prevZdd);
	    }
	    cuddDeref(res);
	}
	return(res);
    }	/* end of cache look-up */

    if (Cudd_IsComplement(B)) {
	Bt = Cudd_Not(cuddT(Breg));
	Be = Cudd_Not(cuddE(Breg));
    } else {
	Bt = cuddT(Breg);
	Be = cuddE(Breg);
    }

    id = Breg->index;
    level = cuddI(dd,id);
    t = zddPortFromBddStep(dd, Bt, level+1);
    if (t == NULL) return(NULL);
    cuddRef(t);
    e = zddPortFromBddStep(dd, Be, level+1);
    if (e == NULL) {
	Cudd_RecursiveDerefZdd(dd, t);
	return(NULL);
    }
    cuddRef(e);
    res = cuddZddGetNode(dd, id, t, e);
    if (res == NULL) {
	Cudd_RecursiveDerefZdd(dd, t);
	Cudd_RecursiveDerefZdd(dd, e);
	return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDerefZdd(dd, t);
    Cudd_RecursiveDerefZdd(dd, e);

    cuddCacheInsert1(dd,Cudd_zddPortFromBdd,B,res);

    for (level--; level >= expected; level--) {
	prevZdd = res;
	id = dd->invperm[level];
	res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
	if (res == NULL) {
	    Cudd_RecursiveDerefZdd(dd, prevZdd);
	    return(NULL);
	}
	cuddRef(res);
	Cudd_RecursiveDerefZdd(dd, prevZdd);
//.........这里部分代码省略.........

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

  Synopsis    [Performs a recursive step of Extra_bddReduceVarSet.]

  Description [Returns the set of all variables in the given set that are not in the 
  support of the given function.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * extraBddReduceVarSet( 
  DdManager * dd,    /* the DD manager */
  DdNode * bVars,    /* the set of variables to be reduced */
  DdNode * bF)       /* the function whose support is used for reduction */
{
    DdNode * bRes;
    DdNode * bFR = Cudd_Regular(bF);

    if ( cuddIsConstant(bFR) || bVars == b1 )
        return bVars;

    if ( (bRes = cuddCacheLookup2(dd, extraBddReduceVarSet, bVars, bF)) )
        return bRes;
    else
    {
        DdNode * bF0, * bF1;             
        DdNode * bVarsThis, * bVarsLower, * bTemp;
        int LevelF;

        // if LevelF is below LevelV, scroll through the vars in bVars 
        LevelF = dd->perm[bFR->index];
        for ( bVarsThis = bVars; LevelF > cuddI(dd,bVarsThis->index); bVarsThis = cuddT(bVarsThis) );
        // scroll also through the current var, because it should be not be added
        if ( LevelF == cuddI(dd,bVarsThis->index) )
            bVarsLower = cuddT(bVarsThis);
        else
            bVarsLower = bVarsThis;

        // cofactor the function
        if ( bFR != bF ) // bFunc is complemented 
        {
            bF0 = Cudd_Not( cuddE(bFR) );
            bF1 = Cudd_Not( cuddT(bFR) );
        }
        else
        {
            bF0 = cuddE(bFR);
            bF1 = cuddT(bFR);
        }

        // solve subproblems
        bRes = extraBddReduceVarSet( dd, bVarsLower, bF0 );
        if ( bRes == NULL ) 
            return NULL;
        cuddRef( bRes );

        bRes = extraBddReduceVarSet( dd, bTemp = bRes, bF1 );
        if ( bRes == NULL ) 
        {
            Cudd_RecursiveDeref( dd, bTemp );
            return NULL;
        }
        cuddRef( bRes );
        Cudd_RecursiveDeref( dd, bTemp );

        // the current var should not be added
        // add the skipped vars
        if ( bVarsThis != bVars )
        {
            DdNode * bVarsExtra;

            // extract the skipped variables
            bVarsExtra = cuddBddExistAbstractRecur( dd, bVars, bVarsThis );
            if ( bVarsExtra == NULL )
            {
                Cudd_RecursiveDeref( dd, bRes );
                return NULL;
            }
            cuddRef( bVarsExtra );

            // add these variables
            bRes = cuddBddAndRecur( dd, bTemp = bRes, bVarsExtra );
            if ( bRes == NULL ) 
            {
                Cudd_RecursiveDeref( dd, bTemp );
                Cudd_RecursiveDeref( dd, bVarsExtra );
                return NULL;
            }
            cuddRef( bRes );
            Cudd_RecursiveDeref( dd, bTemp );
            Cudd_RecursiveDeref( dd, bVarsExtra );
        }
        cuddDeref( bRes );

        cuddCacheInsert2( dd, extraBddReduceVarSet, bVars, bF, bRes );
        return bRes;
    }
}   /* end of extraBddReduceVarSet */

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

  Synopsis    [Performs the recursive step of Cudd_addUnivAbstract.]

  Description [Performs the recursive step of Cudd_addUnivAbstract.
  Returns the ADD obtained by abstracting the variables of cube from f,
  if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode *
cuddAddUnivAbstractRecur(
  DdManager * manager,
  DdNode * f,
  DdNode * cube)
{
    DdNode	*T, *E, *res, *res1, *res2, *one, *zero;

    statLine(manager);
    one = DD_ONE(manager);
    zero = DD_ZERO(manager);

    /* Cube is guaranteed to be a cube at this point.
    ** zero and one are the only constatnts c such that c*c=c.
    */
    if (f == zero || f == one || cube == one) {  
	return(f);
    }

    /* Abstract a variable that does not appear in f. */
    if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
	res1 = cuddAddUnivAbstractRecur(manager, f, cuddT(cube));
	if (res1 == NULL) return(NULL);
	cuddRef(res1);
	/* Use the "internal" procedure to be alerted in case of
	** dynamic reordering. If dynamic reordering occurs, we
	** have to abort the entire abstraction.
	*/
	res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res1);
	if (res == NULL) {
	    Cudd_RecursiveDeref(manager,res1);
	    return(NULL);
	}
	cuddRef(res);
	Cudd_RecursiveDeref(manager,res1);
	cuddDeref(res);
	return(res);
    }

    if ((res = cuddCacheLookup2(manager, Cudd_addUnivAbstract, f, cube)) != NULL) {
	return(res);
    }

    T = cuddT(f);
    E = cuddE(f);

    /* If the two indices are the same, so are their levels. */
    if (f->index == cube->index) {
	res1 = cuddAddUnivAbstractRecur(manager, T, cuddT(cube));
	if (res1 == NULL) return(NULL);
        cuddRef(res1);
	res2 = cuddAddUnivAbstractRecur(manager, E, cuddT(cube));
	if (res2 == NULL) {
	    Cudd_RecursiveDeref(manager,res1);
	    return(NULL);
	}
        cuddRef(res2);
	res = cuddAddApplyRecur(manager, Cudd_addTimes, res1, res2);
	if (res == NULL) {
	    Cudd_RecursiveDeref(manager,res1);
	    Cudd_RecursiveDeref(manager,res2);
	    return(NULL);
	}
	cuddRef(res);
	Cudd_RecursiveDeref(manager,res1);
	Cudd_RecursiveDeref(manager,res2);
	cuddCacheInsert2(manager, Cudd_addUnivAbstract, f, cube, res);
	cuddDeref(res);
        return(res);
    } else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
	res1 = cuddAddUnivAbstractRecur(manager, T, cube);
	if (res1 == NULL) return(NULL);
        cuddRef(res1);
	res2 = cuddAddUnivAbstractRecur(manager, E, cube);
	if (res2 == NULL) {
	    Cudd_RecursiveDeref(manager,res1);
	    return(NULL);
	}
        cuddRef(res2);
	res = (res1 == res2) ? res1 :
	    cuddUniqueInter(manager, (int) f->index, res1, res2);
	if (res == NULL) {
	    Cudd_RecursiveDeref(manager,res1);
	    Cudd_RecursiveDeref(manager,res2);
	    return(NULL);
	}
	cuddDeref(res1);
//.........这里部分代码省略.........

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

  Synopsis    [Performs the recursive step of Cudd_bddCompose.]

  Description [Performs the recursive step of Cud