abc/src/bdd/cudd/cuddSolve.c
/**Function********************************************************************

  Synopsis    [Implements the recursive step of Cudd_SolveEqn.]

  Description [Implements the recursive step of Cudd_SolveEqn. 
  Returns NULL if the intermediate solution blows up
  or reordering occurs. The parametric solutions are
  stored in the array G.]

  SideEffects [none]

  SeeAlso     [Cudd_SolveEqn, Cudd_VerifySol]

******************************************************************************/
Function
Synopsis    [Implements the recursive step of Cudd_SolveEqn.]

Description [Implements the recursive step of Cudd_SolveEqn.
Returns NULL if the intermediate solution blows up
or reordering occurs. The parametric solutions are
stored in the array G.]




Function Synopsis [ Implements the recursive step of Cudd_SolveEqn . ] Description [ Implements the recursive step of Cudd_SolveEqn . Returns NULL if the intermediate solution blows up or reordering occurs . The parametric solutions are stored in the array G . ]
DdNode *
cuddSolveEqnRecur(
  DdManager * bdd,
  DdNode * F ,
  DdNode * Y ,
  DdNode ** G ,
  int  n ,
  int * yIndex ,
  int  i )
{
    DdNode *Fn, *Fm1, *Fv, *Fvbar, *T, *w, *nextY, *one;
    DdNodePtr *variables;
    int j;
    statLine(bdd);
    variables = bdd->vars;
    one = DD_ONE(bdd);
    if (Y == one) {
        return F;
    }
    yIndex[i] = Y->index;
    nextY = Cudd_T(Y);
    Fm1 = cuddBddExistAbstractRecur(bdd, Cudd_Not(F), variables[yIndex[i]]);
    if (Fm1) {
        Fm1 = Cudd_Not(Fm1);
        cuddRef(Fm1);
    } else {
        return(NULL);
    }
    Fn = cuddSolveEqnRecur(bdd, Fm1, nextY, G, n, yIndex, i+1);
    if (Fn) {
        cuddRef(Fn);
    } else {
        Cudd_RecursiveDeref(bdd, Fm1);
        return(NULL);
    }
    Fv = cuddCofactorRecur(bdd, F, variables[yIndex[i]]);
    if (Fv) {
        cuddRef(Fv);
    } else {
        Cudd_RecursiveDeref(bdd, Fm1);
        Cudd_RecursiveDeref(bdd, Fn);
        return(NULL);
    }
    Fvbar = cuddCofactorRecur(bdd, F, Cudd_Not(variables[yIndex[i]]));
    if (Fvbar) {
        cuddRef(Fvbar);
    } else {
        Cudd_RecursiveDeref(bdd, Fm1);
        Cudd_RecursiveDeref(bdd, Fn);
        Cudd_RecursiveDeref(bdd, Fv);
        return(NULL);
    }
    w = cuddBddIteRecur(bdd, variables[yIndex[i]], Cudd_Not(Fv), Fvbar);
    if (w) {
        cuddRef(w);
    } else {
        Cudd_RecursiveDeref(bdd, Fm1);
        Cudd_RecursiveDeref(bdd, Fn);
        Cudd_RecursiveDeref(bdd, Fv);
        Cudd_RecursiveDeref(bdd, Fvbar);
        return(NULL);
    }
    T = cuddBddRestrictRecur(bdd, w, Cudd_Not(Fm1));
    if(T) {
        cuddRef(T);
    } else {
        Cudd_RecursiveDeref(bdd, Fm1);
        Cudd_RecursiveDeref(bdd, Fn);
        Cudd_RecursiveDeref(bdd, Fv);
        Cudd_RecursiveDeref(bdd, Fvbar);
        Cudd_RecursiveDeref(bdd, w);
        return(NULL);
    }
    Cudd_RecursiveDeref(bdd,Fm1);
    Cudd_RecursiveDeref(bdd,w);
    Cudd_RecursiveDeref(bdd,Fv);
    Cudd_RecursiveDeref(bdd,Fvbar);
    for (j = n-1; j > i; j--) {
        w = cuddBddComposeRecur(bdd,T, G[j], variables[yIndex[j]]);
        if(w) {
            cuddRef(w);
        } else {
            Cudd_RecursiveDeref(bdd, Fn);
            Cudd_RecursiveDeref(bdd, T);
            return(NULL);
        }
        Cudd_RecursiveDeref(bdd,T);
        T = w;
    }
    G[i] = T;
    Cudd_Deref(Fn);
    return(Fn);
}
DdNode * cuddSolveEqnRecur ( DdManager * bdd , DdNode * F , DdNode * Y , DdNode * * G , int n , int * yIndex , int i ) { DdNode * Fn , * Fm1 , * Fv , * Fvbar , * T , * w , * nextY , * one ; DdNodePtr * variables ; int j ; statLine ( bdd ) ; variables = bdd -> vars ; one = DD_ONE ( bdd ) ; if ( Y == one ) { return F ; } yIndex [ i ] = Y -> index ; nextY = Cudd_T ( Y ) ; Fm1 = cuddBddExistAbstractRecur ( bdd , Cudd_Not ( F ) , variables [ yIndex [ i ] ] ) ; if ( Fm1 ) { Fm1 = Cudd_Not ( Fm1 ) ; cuddRef ( Fm1 ) ; } else { return ( NULL ) ; } Fn = cuddSolveEqnRecur ( bdd , Fm1 , nextY , G , n , yIndex , i + 1 ) ; if ( Fn ) { cuddRef ( Fn ) ; } else { Cudd_RecursiveDeref ( bdd , Fm1 ) ; return ( NULL ) ; } Fv = cuddCofactorRecur ( bdd , F , variables [ yIndex [ i ] ] ) ; if ( Fv ) { cuddRef ( Fv ) ; } else { Cudd_RecursiveDeref ( bdd , Fm1 ) ; Cudd_RecursiveDeref ( bdd , Fn ) ; return ( NULL ) ; } Fvbar = cuddCofactorRecur ( bdd , F , Cudd_Not ( variables [ yIndex [ i ] ] ) ) ; if ( Fvbar ) { cuddRef ( Fvbar ) ; } else { Cudd_RecursiveDeref ( bdd , Fm1 ) ; Cudd_RecursiveDeref ( bdd , Fn ) ; Cudd_RecursiveDeref ( bdd , Fv ) ; return ( NULL ) ; } w = cuddBddIteRecur ( bdd , variables [ yIndex [ i ] ] , Cudd_Not ( Fv ) , Fvbar ) ; if ( w ) { cuddRef ( w ) ; } else { Cudd_RecursiveDeref ( bdd , Fm1 ) ; Cudd_RecursiveDeref ( bdd , Fn ) ; Cudd_RecursiveDeref ( bdd , Fv ) ; Cudd_RecursiveDeref ( bdd , Fvbar ) ; return ( NULL ) ; } T = cuddBddRestrictRecur ( bdd , w , Cudd_Not ( Fm1 ) ) ; if ( T ) { cuddRef ( T ) ; } else { Cudd_RecursiveDeref ( bdd , Fm1 ) ; Cudd_RecursiveDeref ( bdd , Fn ) ; Cudd_RecursiveDeref ( bdd , Fv ) ; Cudd_RecursiveDeref ( bdd , Fvbar ) ; Cudd_RecursiveDeref ( bdd , w ) ; return ( NULL ) ; } Cudd_RecursiveDeref ( bdd , Fm1 ) ; Cudd_RecursiveDeref ( bdd , w ) ; Cudd_RecursiveDeref ( bdd , Fv ) ; Cudd_RecursiveDeref ( bdd , Fvbar ) ; for ( j = n - 1 ; j > i ; j -- ) { w = cuddBddComposeRecur ( bdd , T , G [ j ] , variables [ yIndex [ j ] ] ) ; if ( w ) { cuddRef ( w ) ; } else { Cudd_RecursiveDeref ( bdd , Fn ) ; Cudd_RecursiveDeref ( bdd , T ) ; return ( NULL ) ; } Cudd_RecursiveDeref ( bdd , T ) ; T = w ; } G [ i ] = T ; Cudd_Deref ( Fn ) ; return ( Fn ) ; }
Function
Synopsis    [Implements the recursive step of Cudd_SolveEqn.]
Function Synopsis [ Implements the recursive step of Cudd_SolveEqn . ]
/* the left-hand side of the equation */ /* the cube of remaining y variables */ /* the array of solutions */ /* number of unknowns */ /* array holding the y variable indices */ /* level of recursion */ /* Base condition. */ /* Cofactor of Y. */ /* Universal abstraction of F with respect to the top variable index. */ /* Build i-th component of the solution. */ /* Substitute components of solution already found into solution. */