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

  Synopsis    [Existentially Abstracts all the variables in cube from f.]

  Description [Abstracts all the variables in cube from f by summing
  over all possible values taken by the variables. Returns the
  abstracted ADD.]

  SideEffects [None]

  SeeAlso     [Cudd_addUnivAbstract Cudd_bddExistAbstract
  Cudd_addOrAbstract]

******************************************************************************/
DdNode *
Cudd_addExistAbstract(
  DdManager * manager,
  DdNode * f,
  DdNode * cube)
{
    DdNode *res;

    two = cuddUniqueConst(manager,(CUDD_VALUE_TYPE) 2);
    if (two == NULL) return(NULL);
    cuddRef(two);

    if (addCheckPositiveCube(manager, cube) == 0) {
        (void) fprintf(manager->err,"Error: Can only abstract cubes");
        return(NULL);
    }

    do {
	manager->reordered = 0;
	res = cuddAddExistAbstractRecur(manager, f, cube);
    } while (manager->reordered == 1);

    if (res == NULL) {
	Cudd_RecursiveDeref(manager,two);
	return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(manager,two);
    cuddDeref(res);

    return(res);

} /* end of Cudd_addExistAbstract */

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

  Synopsis    [Converts an ADD to a BDD.]

  Description [Converts an ADD to a BDD by replacing all
  discriminants STRICTLY greater than value with 1, and all other
  discriminants with 0. Returns a pointer to the resulting BDD if
  successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd 
  Cudd_addBddThreshold]

******************************************************************************/
DdNode *
Cudd_addBddStrictThreshold(
  DdManager * dd,
  DdNode * f,
  CUDD_VALUE_TYPE  value)
{
    DdNode *res;
    DdNode *val;
    /* NuSMV: begin add */
    abort(); /* NOT USED BY NUSMV */
    /* NuSMV: begin end */
    
    val = cuddUniqueConst(dd,value);
    if (val == NULL) return(NULL);
    cuddRef(val);

    do {
	dd->reordered = 0;
	res = addBddDoStrictThreshold(dd, f, val);
    } while (dd->reordered == 1);

    if (res == NULL) {
	Cudd_RecursiveDeref(dd, val);
	return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(dd, val);
    cuddDeref(res);
    return(res);

} /* end of Cudd_addBddStrictThreshold */

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

  Synopsis    [Computes a complement of a ZDD node.]

  Description [Computes the complement of a ZDD node. So far, since we
  couldn't find a direct way to get the complement of a ZDD cover, we first
  convert a ZDD cover to a BDD, then make the complement of the ZDD cover
  from the complement of the BDD node by using ISOP.]

  SideEffects [The result depends on current variable order.]

  SeeAlso     []

******************************************************************************/
DdNode	*
cuddZddComplement(
  DdManager * dd,
  DdNode *node)
{
    DdNode	*b, *isop, *zdd_I;

    /* Check cache */
    zdd_I = cuddCacheLookup1Zdd(dd, cuddZddComplement, node);
    if (zdd_I)
	return(zdd_I);

    b = cuddMakeBddFromZddCover(dd, node);
    if (!b)
	return(NULL);
    cuddRef(b);
    isop = cuddZddIsop(dd, Cudd_Not(b), Cudd_Not(b), &zdd_I);
    if (!isop) {
	Cudd_RecursiveDeref(dd, b);
	return(NULL);
    }
    cuddRef(isop);
    cuddRef(zdd_I);
    Cudd_RecursiveDeref(dd, b);
    Cudd_RecursiveDeref(dd, isop);

    cuddCacheInsert1(dd, cuddZddComplement, node, zdd_I);
    cuddDeref(zdd_I);
    return(zdd_I);
} /* end of cuddZddComplement */

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

  Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]

  Description [Computes the negative cofactor of a ZDD w.r.t. a
  variable. In terms of combinations, the result is the set of all
  combinations in which the variable is negated. Returns a pointer to
  the result if successful; NULL otherwise. cuddZddSubset0 performs
  the same function as Cudd_zddSubset0, but does not restart if
  reordering has taken place. Therefore it can be called from within a
  recursive procedure.]

  SideEffects [None]

  SeeAlso     [cuddZddSubset1 Cudd_zddSubset0]

******************************************************************************/
DdNode *
cuddZddSubset0(
  DdManager * dd,
  DdNode * P,
  int  var)
{
    DdNode	*zvar, *r;
    DdNode	*base, *empty;

    base = DD_TRUE(dd);
    empty = DD_FALSE(dd);

    zvar = cuddUniqueInterZdd(dd, var, base, empty);
    if (zvar == NULL) {
	return(NULL);
    } else {
	cuddRef(zvar);
	r = zdd_subset0_aux(dd, P, zvar);
	if (r == NULL) {
	    Cudd_RecursiveDerefZdd(dd, zvar);
	    return(NULL);
	}
	cuddRef(r);
	Cudd_RecursiveDerefZdd(dd, zvar);
    }

    cuddDeref(r);
    return(r);

} /* end of cuddZddSubset0 */

/**
  @brief Performs the recursive step of addScalarInverse.

  @return a pointer to the resulting %ADD in case of success. Returns
  NULL if any discriminants smaller than epsilon is encountered.

  @sideeffect None

*/
DdNode *
cuddAddScalarInverseRecur(
  DdManager * dd,
  DdNode * f,
  DdNode * epsilon)
{
    DdNode *t, *e, *res;
    CUDD_VALUE_TYPE value;

    statLine(dd);
    if (cuddIsConstant(f)) {
	if (ddAbs(cuddV(f)) < cuddV(epsilon)) return(NULL);
	value = 1.0 / cuddV(f);
	res = cuddUniqueConst(dd,value);
	return(res);
    }

    res = cuddCacheLookup2(dd,Cudd_addScalarInverse,f,epsilon);
    if (res != NULL) return(res);

    checkWhetherToGiveUp(dd);

    t = cuddAddScalarInverseRecur(dd,cuddT(f),epsilon);
    if (t == NULL) return(NULL);
    cuddRef(t);

    e = cuddAddScalarInverseRecur(dd,cuddE(f),epsilon);
    if (e == NULL) {
	Cudd_RecursiveDeref(dd, t);
	return(NULL);
    }
    cuddRef(e);

    res = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
    if (res == NULL) {
	Cudd_RecursiveDeref(dd, t);
	Cudd_RecursiveDeref(dd, e);
	return(NULL);
    }
    cuddDeref(t);
    cuddDeref(e);

    cuddCacheInsert2(dd,Cudd_addScalarInverse,f,epsilon,res);

    return(res);

} /* end of cuddAddScalarInverseRecur */

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

  Synopsis    [Implements the recursive step of Cudd_bddVarMap.]

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

  SideEffects [None]

  SeeAlso     [Cudd_bddVarMap]

******************************************************************************/
static DdNode *
cuddBddVarMapRecur(
  DdManager *manager /* DD manager */,
  DdNode *f /* BDD to be remapped */)
{
    DdNode	*F, *T, *E;
    DdNode	*res;
    int		index;

    statLine(manager);
    F = Cudd_Regular(f);

    /* Check for terminal case of constant node. */
    if (cuddIsConstant(F)) {
	return(f);
    }

    /* If problem already solved, look up answer and return. */
    if (F->ref != 1 &&
	(res = cuddCacheLookup1(manager,Cudd_bddVarMap,F)) != NULL) {
	return(Cudd_NotCond(res,F != f));
    }

    /* Split and recur on children of this node. */
    T = cuddBddVarMapRecur(manager,cuddT(F));
    if (T == NULL) return(NULL);
    cuddRef(T);
    E = cuddBddVarMapRecur(manager,cuddE(F));
    if (E == NULL) {
	Cudd_IterDerefBdd(manager, T);
	return(NULL);
    }
    cuddRef(E);

    /* Move variable that should be in this position to this position
    ** by retrieving the single var BDD for that variable, and calling
    ** cuddBddIteRecur with the T and E we just created.
    */
    index = manager->map[F->index];
    res = cuddBddIteRecur(manager,manager->vars[index],T,E);
    if (res == NULL) {
	Cudd_IterDerefBdd(manager, T);
	Cudd_IterDerefBdd(manager, E);
	return(NULL);
    }
    cuddRef(res);
    Cudd_IterDerefBdd(manager, T);
    Cudd_IterDerefBdd(manager, E);

    /* Do not keep the result if the reference count is only 1, since
    ** it will not be visited again.
    */
    if (F->ref != 1) {
	cuddCacheInsert1(manager,Cudd_bddVarMap,F,res);
    }
    cuddDeref(res);
    return(Cudd_NotCond(res,F != f));

} /* end of cuddBddVarMapRecur */

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

  Synopsis    [Performs the recursive step of Extra_bddSpaceCanonVars().]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * extraBddSpaceCanonVars( DdManager * dd, DdNode * bF )
{
	DdNode * bRes, * bFR;
	statLine( dd );

	bFR = Cudd_Regular(bF);
	if ( cuddIsConstant(bFR) )
		return bF;

    if ( (bRes = cuddCacheLookup1(dd, extraBddSpaceCanonVars, bF)) )
    	return bRes;
	else
	{
		DdNode * bF0,  * bF1;
		DdNode * bRes, * bRes0; 

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

		if ( bF0 == b0 )
		{
			bRes = extraBddSpaceCanonVars( dd, bF1 );
			if ( bRes == NULL )
				return NULL;
		}
		else if ( bF1 == b0 )
		{
			bRes = extraBddSpaceCanonVars( dd, bF0 );
			if ( bRes == NULL )
				return NULL;
		}
		else
		{
			bRes0 = extraBddSpaceCanonVars( dd, bF0 );
			if ( bRes0 == NULL )
				return NULL;
			cuddRef( bRes0 );

			bRes = cuddUniqueInter( dd, bFR->index, bRes0, b0 );
			if ( bRes == NULL ) 
			{
				Cudd_RecursiveDeref( dd,bRes0 );
				return NULL;
			}
			cuddDeref( bRes0 );
		}

		cuddCacheInsert1( dd, extraBddSpaceCanonVars, bF, bRes );
		return bRes;
	}
}

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

  Synopsis    [Performs the recursive step of Cudd_addCmpl.]

  Description [Performs the recursive step of Cudd_addCmpl. Returns a
  pointer to the resulting ADD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addCmpl]

******************************************************************************/
DdNode *
cuddAddCmplRecur(
  DdManager * dd,
  DdNode * f)
{
    DdNode *one,*zero;
    DdNode *r,*Fv,*Fnv,*t,*e;

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

    if (cuddIsConstant(f)) {
        if (f == zero) {
	    return(one);
	} else {
	    return(zero);
	}
    }
    r = cuddCacheLookup1(dd,Cudd_addCmpl,f);
    if (r != NULL) {
	return(r);
    }
    Fv = cuddT(f);
    Fnv = cuddE(f);
    t = cuddAddCmplRecur(dd,Fv);
    if (t == NULL) return(NULL);
    cuddRef(t);
    e = cuddAddCmplRecur(dd,Fnv);
    if (e == NULL) {
	Cudd_RecursiveDeref(dd,t);
	return(NULL);
    }
    cuddRef(e);
    r = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e);
    if (r == NULL) {
	Cudd_RecursiveDeref(dd, t);
	Cudd_RecursiveDeref(dd, e);
	return(NULL);
    }
    cuddDeref(t);
    cuddDeref(e);
    cuddCacheInsert1(dd,Cudd_addCmpl,f,r);
    return(r);

} /* end of cuddAddCmplRecur */

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

  Synopsis    [Recursive procedure to extract n mintems from constant 1.]

  Description [Recursive procedure to extract n mintems from constant 1.]

  SideEffects [None]

******************************************************************************/
static DdNode *
mintermsFromUniverse(
  DdManager * manager,
  DdNode ** vars,
  int  numVars,
  double  n,
  int  index)
{
    DdNode *one, *zero;
    DdNode *q, *result;
    double max, max2;
    
    statLine(manager);
    one = DD_ONE(manager);
    zero = Cudd_Not(one);

    max = pow(2.0, (double)numVars);
    max2 = max / 2.0;

    if (n == max)
	return(one);
    if (n == 0.0)
	return(zero);
    /* if n == 2^(numVars-1), return a single variable */
    if (n == max2)
	return vars[index];
    else if (n > max2) {
	/* When n > 2^(numVars-1), a single variable vars[index]
	** contains 2^(numVars-1) minterms. The rest are extracted
	** from a constant with 1 less variable.
	*/
	q = mintermsFromUniverse(manager,vars,numVars-1,(n-max2),index+1);
	if (q == NULL)
	    return(NULL);
	cuddRef(q);
	result = cuddBddIteRecur(manager,vars[index],one,q);
    } else {
	/* When n < 2^(numVars-1), a literal of variable vars[index]
	** is selected. The required n minterms are extracted from a
	** constant with 1 less variable.
	*/
	q = mintermsFromUniverse(manager,vars,numVars-1,n,index+1);
	if (q == NULL)
	    return(NULL);
	cuddRef(q);
	result = cuddBddAndRecur(manager,vars[index],q);
    }
    
    if (result == NULL) {
	Cudd_RecursiveDeref(manager,q);
	return(NULL);
    }
    cuddRef(result);
    Cudd_RecursiveDeref(manager,q);
    cuddDeref(result);
    return(result);

} /* end of mintermsFromUniverse */

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

  Synopsis    [Performs the recursive step of Extra_zddSelectOneSubset.]

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode * extraZddSelectOneSubset( 
  DdManager * dd, 
  DdNode * zS )
// selects one subset from the ZDD zS
// returns z0 if and only if zS is an empty set of cubes
{
    DdNode * zRes;

    if ( zS == z0 )    return z0;
    if ( zS == z1 )    return z1;
    
    // check cache
    if ( (zRes = cuddCacheLookup1Zdd( dd, extraZddSelectOneSubset, zS )) )
        return zRes;
    else
    {
        DdNode * zS0, * zS1, * zTemp; 

        zS0 = cuddE(zS);
        zS1 = cuddT(zS);

        if ( zS0 != z0 )
        {
            zRes = extraZddSelectOneSubset( dd, zS0 );
            if ( zRes == NULL )
                return NULL;
        }
        else // if ( zS0 == z0 )
        {
            assert( zS1 != z0 );
            zRes = extraZddSelectOneSubset( dd, zS1 );
            if ( zRes == NULL )
                return NULL;
            cuddRef( zRes );

            zRes = cuddZddGetNode( dd, zS->index, zTemp = zRes, z0 );
            if ( zRes == NULL ) 
            {
                Cudd_RecursiveDerefZdd( dd, zTemp );
                return NULL;
            }
            cuddDeref( zTemp );
        }

        // insert the result into cache
        cuddCacheInsert1( dd, extraZddSelectOneSubset, zS, zRes );
        return zRes;
    }       
} /* end of extraZddSelectOneSubset */

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

  Synopsis    [Generates a BDD for the function x > y.]

  Description [This function generates a BDD for the function x > y.
  Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and
  y\[0\] y\[1\] ...  y\[N-1\], with 0 the most significant bit.
  The BDD is built bottom-up.
  It has 3*N-1 internal nodes, if the variables are ordered as follows: 
  x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\].
  Argument z is not used by Cudd_Xgty: it is included to make it
  call-compatible to Cudd_Dxygtdxz and Cudd_Dxygtdyz.]

  SideEffects [None]

  SeeAlso     [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Dxygtdyz]

******************************************************************************/
DdNode *
Cudd_Xgty(
  DdManager * dd /* DD manager */,
  int  N /* number of x and y variables */,
  DdNode ** z /* array of z variables: unused */,
  DdNode ** x /* array of x variables */,
  DdNode ** y /* array of y variables */)
{
    DdNode *u, *v, *w;
    int     i;

    /* Build bottom part of BDD outside loop. */
    u = Cudd_bddAnd(dd, x[N-1], Cudd_Not(y[N-1]));
    if (u == NULL) return(NULL);
    cuddRef(u);

    /* Loop to build the rest of the BDD. */
    for (i = N-2; i >= 0; i--) {
	v = Cudd_bddAnd(dd, y[i], Cudd_Not(u));
	if (v == NULL) {
	    Cudd_RecursiveDeref(dd, u);
	    return(NULL);
	}
	cuddRef(v);
	w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u);
	if (w == NULL) {
	    Cudd_RecursiveDeref(dd, u);
	    Cudd_RecursiveDeref(dd, v);
	    return(NULL);
	}
	cuddRef(w);
	Cudd_RecursiveDeref(dd, u);
	u = Cudd_bddIte(dd, x[i], Cudd_Not(v), w);
	if (u == NULL) {
	    Cudd_RecursiveDeref(dd, v);
	    Cudd_RecursiveDeref(dd, w);
	    return(NULL);
	}
	cuddRef(u);
	Cudd_RecursiveDeref(dd, v);
	Cudd_RecursiveDeref(dd, w);

    }
    cuddDeref(u);
    return(u);

} /* end of Cudd_Xgty */

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

  Synopsis    [Performs a recursive step of Extra_zddGetSingletons.]

  Description [Returns the set of ZDD singletons, containing those positive 
  polarity ZDD variables that correspond to the BDD variables in bVars.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * extraZddGetSingletons( 
  DdManager * dd,    /* the DD manager */
  DdNode * bVars)    /* the set of variables */
{
    DdNode * zRes;

    if ( bVars == b1 )
//    if ( bVars == b0 )  // bug fixed by Jin Zhang, Jan 23, 2004
        return z1;

    if ( (zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletons, bVars)) )
        return zRes;
    else
    {
        DdNode * zTemp, * zPlus;          

        // solve subproblem
        zRes = extraZddGetSingletons( dd, cuddT(bVars) );
        if ( zRes == NULL ) 
            return NULL;
        cuddRef( zRes );
        
        zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 );
        if ( zPlus == NULL ) 
        {
            Cudd_RecursiveDerefZdd( dd, zRes );
            return NULL;
        }
        cuddRef( zPlus );

        // add these to the result
        zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
        if ( zRes == NULL )
        {
            Cudd_RecursiveDerefZdd( dd, zTemp );
            Cudd_RecursiveDerefZdd( dd, zPlus );
            return NULL;
        }
        cuddRef( zRes );
        Cudd_RecursiveDerefZdd( dd, zTemp );
        Cudd_RecursiveDerefZdd( dd, zPlus );
        cuddDeref( zRes );

        cuddCacheInsert1( dd, extraZddGetSingletons, bVars, zRes );
        return zRes;
    }
}   /* end of extraZddGetSingletons */

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

  Synopsis    [Converts an ADD to a BDD.]

  Description [Converts an ADD to a BDD by replacing all
  discriminants greater than or equal to lower and less than or equal to
  upper with 1, and all other discriminants with 0. Returns a pointer to
  the resulting BDD if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_addBddThreshold Cudd_addBddStrictThreshold 
  Cudd_addBddPattern Cudd_BddToAdd]

******************************************************************************/
DdNode *
Cudd_addBddInterval(
  DdManager * dd,
  DdNode * f,
  CUDD_VALUE_TYPE  lower,
  CUDD_VALUE_TYPE  upper)
{
    DdNode *res;
    DdNode *l;
    DdNode *u;

    /* NuSMV: begin add */
    abort(); /* NOT USED BY NUSMV */
    /* NuSMV: begin end */

    /* Create constant nodes for the interval bounds, so that we can use
    ** the global cache.
    */
    l = cuddUniqueConst(dd,lower);
    if (l == NULL) return(NULL);
    cuddRef(l);
    u = cuddUniqueConst(dd,upper);
    if (u == NULL) {
	Cudd_RecursiveDeref(dd,l);
	return(NULL);
    }
    cuddRef(u);

    do {
	dd->reordered = 0;
	res = addBddDoInterval(dd, f, l, u);
    } while (dd->reordered == 1);

    if (res == NULL) {
	Cudd_RecursiveDeref(dd, l);
	Cudd_RecursiveDeref(dd, u);
	return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(dd, l);
    Cudd_RecursiveDeref(dd, u);
    cuddDeref(res);
    return(res);

} /* end of Cudd_addBddInterval */

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

  Synopsis    [Computes the Hamming distance ADD.]

  Description [Computes the Hamming distance ADD. Returns an ADD that
  gives the Hamming distance between its two arguments if successful;
  NULL otherwise. The two vectors xVars and yVars identify the variables
  that form the two arguments.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode *
Cudd_addHamming(
  DdManager * dd,
  DdNode ** xVars,
  DdNode ** yVars,
  int  nVars)
{
    DdNode  *result,*tempBdd;
    DdNode  *tempAdd,*temp;
    int     i;

    result = DD_ZERO(dd);
    cuddRef(result);

    for (i = 0; i < nVars; i++) {
	tempBdd = Cudd_bddIte(dd,xVars[i],Cudd_Not(yVars[i]),yVars[i]);
	if (tempBdd == NULL) {
	    Cudd_RecursiveDeref(dd,result);
	    return(NULL);
	}
	cuddRef(tempBdd);
	tempAdd = Cudd_BddToAdd(dd,tempBdd);
	if (tempAdd == NULL) {
	    Cudd_RecursiveDeref(dd,tempBdd);
	    Cudd_RecursiveDeref(dd,result);
	    return(NULL);
	}
	cuddRef(tempAdd);
	Cudd_RecursiveDeref(dd,tempBdd);
	temp = Cudd_addApply(dd,Cudd_addPlus,tempAdd,result);
	if (temp == NULL) {
	    Cudd_RecursiveDeref(dd,tempAdd);
	    Cudd_RecursiveDeref(dd,result);
	    return(NULL);
	}
	cuddRef(temp);
	Cudd_RecursiveDeref(dd,tempAdd);
	Cudd_RecursiveDeref(dd,result);
	result = temp;
    }

    cuddDeref(result);
    return(result);

} /* end of Cudd_addHamming */

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

  Synopsis    [Initializes the ZDD universe.]

  Description [Initializes the ZDD universe. Returns 1 if successful; 0
  otherwise.]

  SideEffects [None]

  SeeAlso     [cuddZddFreeUniv]

******************************************************************************/
int
cuddZddInitUniv(
  DdManager * zdd)
{
    DdNode	*p, *res;
    int		i;

#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif
    zdd->univ = ALLOC(DdNode *, zdd->sizeZ);
#ifdef __osf__
#pragma pointer_size restore
#endif
    if (zdd->univ == NULL) {
	zdd->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }

    res = DD_ONE(zdd);
    cuddRef(res);
    for (i = zdd->sizeZ - 1; i >= 0; i--) {
	unsigned int index = zdd->invpermZ[i];
	p = res;
	res = cuddUniqueInterZdd(zdd, index, p, p);
	if (res == NULL) {
	    Cudd_RecursiveDerefZdd(zdd,p);
	    FREE(zdd->univ);
	    return(0);
	}
	cuddRef(res);
	cuddDeref(p);
	zdd->univ[i] = res;
    }

#ifdef DD_VERBOSE
    cuddZddP(zdd, zdd->univ[0]);
#endif

    return(1);

} /* end of cuddZddInitUniv */

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

  Synopsis    [Convert a BDD from a manager to another one.]

  Description [Convert a BDD from a manager to another one. Returns a
  pointer to the BDD in the destination manager if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Extra_TransferPermute]

******************************************************************************/
DdNode * extraTransferPermuteTime( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute, int TimeOut )
{
    DdNode *res;
    st_table *table = NULL;
    st_generator *gen = NULL;
    DdNode *key, *value;

    table = st_init_table( st_ptrcmp, st_ptrhash );
    if ( table == NULL )
        goto failure;
    res = extraTransferPermuteRecurTime( ddS, ddD, f, table, Permute, TimeOut );
    if ( res != NULL )
        cuddRef( res );

    /* Dereference all elements in the table and dispose of the table.
       ** This must be done also if res is NULL to avoid leaks in case of
       ** reordering. */
    gen = st_init_gen( table );
    if ( gen == NULL )
        goto failure;
    while ( st_gen( gen, ( const char ** ) &key, ( char ** ) &value ) )
    {
        Cudd_RecursiveDeref( ddD, value );
    }
    st_free_gen( gen );
    gen = NULL;
    st_free_table( table );
    table = NULL;

    if ( res != NULL )
        cuddDeref( res );
    return ( res );

  failure:
    if ( table != NULL )
        st_free_table( table );
    if ( gen != NULL )
        st_free_gen( gen );
    return ( NULL );

} /* end of extraTransferPermuteTime */

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

  Synopsis    [Convert a BDD from a manager to another one.]

  Description [Convert a BDD from a manager to another one. Returns a
  pointer to the BDD in the destination manager if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddTransfer]

******************************************************************************/
DdNode *
cuddBddTransfer(
  DdManager * ddS,
  DdManager * ddD,
  DdNode * f)
{
    DdNode *res;
    st_table *table = NULL;
    st_generator *gen = NULL;
    DdNode *key, *value;

    /* NuSMV: begin add */
    abort(); /* NOT USED BY NUSMV */
    /* NuSMV: begin end */

    table = st_init_table(st_ptrcmp,st_ptrhash);
    if (table == NULL) goto failure;
    res = cuddBddTransferRecur(ddS, ddD, f, table);
    if (res != NULL) cuddRef(res);

    /* Dereference all elements in the table and dispose of the table.
    ** This must be done also if res is NULL to avoid leaks in case of
    ** reordering. */
    gen = st_init_gen(table);
    if (gen == NULL) goto failure;
    while (st_gen(gen, &key, &value)) {
	Cudd_RecursiveDeref(ddD, value);
    }
    st_free_gen(gen); gen = NULL;
    st_free_table(table); table = NULL;

    if (res != NULL) cuddDeref(res);
    return(res);

failure:
    if (table != NULL) st_free_table(table);
    if (gen != NULL) st_free_gen(gen);
    return(NULL);

} /* end of cuddBddTransfer */

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

  Synopsis    [Computes the compatible projection of R w.r.t. cube Y.]

  Description [Computes the compatible projection of relation R with
  respect to cube Y. Returns a pointer to the c-projection if
  successful; NULL otherwise. For a comparison between Cudd_CProjection
  and Cudd_PrioritySelect, see the documentation of the latter.]

  SideEffects [None]

  SeeAlso     [Cudd_PrioritySelect]

******************************************************************************/
DdNode *
Cudd_CProjection(
  DdManager * dd,
  DdNode * R,
  DdNode * Y)
{
    DdNode *res;
    DdNode *support;

    if (cuddCheckCube(dd,Y) == 0) {
	(void) fprintf(dd->err,
	"Error: The third argument of Cudd_CProjection should be a cube\n");
	dd->errorCode = CUDD_INVALID_ARG;
	return(NULL);
    }

    /* Compute the support of Y, which is used by the abstraction step
    ** in cuddCProjectionRecur.
    */
    support = Cudd_Support(dd,Y);
    if (support == NULL) return(NULL);
    cuddRef(support);

    do {
	dd->reordered = 0;
	res = cuddCProjectionRecur(dd,R,Y,support);
    } while (dd->reordered == 1);

    if (res == NULL) {
	Cudd_RecursiveDeref(dd,support);
	return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDeref(dd,support);
    cuddDeref(res);

    return(res);

} /* end of Cudd_CProjection */

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

  Synopsis    [Composes an ADD with a vector of ADDs.]

  Description [Given a vector of ADDs, creates a new ADD by substituting the
  ADDs for the variables of the ADD f. vectorOn contains ADDs to be substituted
  for the x_v and vectorOff the ADDs to be substituted for x_v'. There should
  be an entry in vector for each variable in the manager.  If no substitution
  is sought for a given variable, the corresponding projection function should
  be specified in the vector.  This function implements simultaneous
  composition.  Returns a pointer to the resulting ADD if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso [Cudd_addVectorCompose Cudd_addNonSimCompose Cudd_addPermute
  Cudd_addCompose Cudd_bddVectorCompose]

******************************************************************************/
DdNode *
Cudd_addGeneralVectorCompose(
  DdManager * dd,
  DdNode * f,
  DdNode ** vectorOn,
  DdNode ** vectorOff)
{
    DdHashTable		*table;
    DdNode		*res;
    int			deepest;
    int                 i;

    do {
	dd->reordered = 0;
	/* Initialize local cache. */
	table = cuddHashTableInit(dd,1,2);
	if (table == NULL) return(NULL);

	/* Find deepest real substitution. */
	for (deepest = dd->size - 1; deepest >= 0; deepest--) {
	    i = dd->invperm[deepest];
	    if (!ddIsIthAddVarPair(dd,vectorOn[i],vectorOff[i],i)) {
		break;
	    }
	}

	/* Recursively solve the problem. */
	res = cuddAddGeneralVectorComposeRecur(dd,table,f,vectorOn,
					       vectorOff,deepest);
	if (res != NULL) cuddRef(res);

	/* Dispose of local cache. */
	cuddHashTableQuit(table);
    } while (dd->reordered == 1);

    if (res != NULL) cuddDeref(res);
    return(res);

} /* end of Cudd_addGeneralVectorCompose */

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

  Synopsis [Substitutes a variable with its complement in a ZDD.]

  Description [Substitutes a variable with its complement in a ZDD.
  returns a pointer to the result if successful; NULL
  otherwise. cuddZddChange performs the same function as
  Cudd_zddChange, but does not restart if reordering has taken
  place. Therefore it can be called from within a recursive
  procedure.]

  SideEffects [None]

  SeeAlso     [Cudd_zddChange]

******************************************************************************/
DdNode *
cuddZddChange(
  DdManager * dd,
  DdNode * P,
  int  var)
{
    DdNode	*zvar, *res;

    zvar = cuddUniqueInterZdd(dd, var, DD_ONE(dd), DD_ZERO(dd));
    if (zvar == NULL) return(NULL);
    cuddRef(zvar);

    res = cuddZddChangeAux(dd, P, zvar);
    if (res == NULL) {
	Cudd_RecursiveDerefZdd(dd,zvar);
	return(NULL);
    }
    cuddRef(res);
    Cudd_RecursiveDerefZdd(dd,zvar);
    cuddDeref(res);
    return(res);

} /* end of cuddZddChange */