src/bdd/cudd/cuddSolve.c File Reference

#include "util_hack.h"
#include "cuddInt.h"
Include dependency graph for cuddSolve.c:

Go to the source code of this file.

Functions

DdNode * Cudd_SolveEqn (DdManager *bdd, DdNode *F, DdNode *Y, DdNode **G, int **yIndex, int n)
DdNode * Cudd_VerifySol (DdManager *bdd, DdNode *F, DdNode **G, int *yIndex, int n)
DdNode * cuddSolveEqnRecur (DdManager *bdd, DdNode *F, DdNode *Y, DdNode **G, int n, int *yIndex, int i)
DdNode * cuddVerifySol (DdManager *bdd, DdNode *F, DdNode **G, int *yIndex, int n)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddSolve.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"

Function Documentation

DdNode* Cudd_SolveEqn ( DdManager *  bdd,
DdNode *  F,
DdNode *  Y,
DdNode **  G,
int **  yIndex,
int  n 
)

AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Implements the solution of F(x,y) = 0.]

Description [Implements the solution for F(x,y) = 0. The return value is the consistency condition. The y variables are the unknowns and the remaining variables are the parameters. Returns the consistency condition if successful; NULL otherwise. Cudd_SolveEqn allocates an array and fills it with the indices of the unknowns. This array is used by Cudd_VerifySol.]

SideEffects [The solution is returned in G; the indices of the y variables are returned in yIndex.]

SeeAlso [Cudd_VerifySol]

Definition at line 95 of file cuddSolve.c.

00102 {
00103     DdNode *res;
00104     int *temp;
00105 
00106     *yIndex = temp = ALLOC(int, n);
00107     if (temp == NULL) {
00108         bdd->errorCode = CUDD_MEMORY_OUT;
00109         (void) fprintf(bdd->out,
00110                        "Cudd_SolveEqn: Out of memory for yIndex\n");
00111         return(NULL);
00112     }
00113 
00114     do {
00115         bdd->reordered = 0;
00116         res = cuddSolveEqnRecur(bdd, F, Y, G, n, temp, 0);
00117     } while (bdd->reordered == 1);
00118 
00119     return(res);
00120 
00121 } /* end of Cudd_SolveEqn */

DdNode* Cudd_VerifySol ( DdManager *  bdd,
DdNode *  F,
DdNode **  G,
int *  yIndex,
int  n 
)

Function********************************************************************

Synopsis [Checks the solution of F(x,y) = 0.]

Description [Checks the solution of F(x,y) = 0. This procedure substitutes the solution components for the unknowns of F and returns the resulting BDD for F.]

SideEffects [Frees the memory pointed by yIndex.]

SeeAlso [Cudd_SolveEqn]

Definition at line 138 of file cuddSolve.c.

00144 {
00145     DdNode *res;
00146 
00147     do {
00148         bdd->reordered = 0;
00149         res = cuddVerifySol(bdd, F, G, yIndex, n);
00150     } while (bdd->reordered == 1);
00151 
00152     FREE(yIndex);
00153 
00154     return(res);
00155 
00156 } /* end of Cudd_VerifySol */

DdNode* cuddSolveEqnRecur ( DdManager *  bdd,
DdNode *  F,
DdNode *  Y,
DdNode **  G,
int  n,
int *  yIndex,
int  i 
)

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]

Definition at line 179 of file cuddSolve.c.

00187 {
00188     DdNode *Fn, *Fm1, *Fv, *Fvbar, *T, *w, *nextY, *one;
00189     DdNodePtr *variables;
00190 
00191     int j;
00192 
00193     statLine(bdd);
00194     variables = bdd->vars;
00195     one = DD_ONE(bdd);
00196 
00197     /* Base condition. */
00198     if (Y == one) {
00199         return F;
00200     }
00201 
00202     /* Cofactor of Y. */
00203     yIndex[i] = Y->index;
00204     nextY = Cudd_T(Y);
00205 
00206     /* Universal abstraction of F with respect to the top variable index. */
00207     Fm1 = cuddBddExistAbstractRecur(bdd, Cudd_Not(F), variables[yIndex[i]]);
00208     if (Fm1) {
00209         Fm1 = Cudd_Not(Fm1);
00210         cuddRef(Fm1);
00211     } else {
00212         return(NULL);
00213     }
00214 
00215     Fn = cuddSolveEqnRecur(bdd, Fm1, nextY, G, n, yIndex, i+1);
00216     if (Fn) {
00217         cuddRef(Fn);
00218     } else {
00219         Cudd_RecursiveDeref(bdd, Fm1);
00220         return(NULL);
00221     }
00222 
00223     Fv = cuddCofactorRecur(bdd, F, variables[yIndex[i]]);
00224     if (Fv) {
00225         cuddRef(Fv);
00226     } else {
00227         Cudd_RecursiveDeref(bdd, Fm1);
00228         Cudd_RecursiveDeref(bdd, Fn);
00229         return(NULL);
00230     }
00231 
00232     Fvbar = cuddCofactorRecur(bdd, F, Cudd_Not(variables[yIndex[i]]));
00233     if (Fvbar) {
00234         cuddRef(Fvbar);
00235     } else {
00236         Cudd_RecursiveDeref(bdd, Fm1);
00237         Cudd_RecursiveDeref(bdd, Fn);
00238         Cudd_RecursiveDeref(bdd, Fv);
00239         return(NULL);
00240     }
00241 
00242     /* Build i-th component of the solution. */
00243     w = cuddBddIteRecur(bdd, variables[yIndex[i]], Cudd_Not(Fv), Fvbar);
00244     if (w) {
00245         cuddRef(w);
00246     } else {
00247         Cudd_RecursiveDeref(bdd, Fm1);
00248         Cudd_RecursiveDeref(bdd, Fn);
00249         Cudd_RecursiveDeref(bdd, Fv);
00250         Cudd_RecursiveDeref(bdd, Fvbar);
00251         return(NULL);
00252     }
00253 
00254     T = cuddBddRestrictRecur(bdd, w, Cudd_Not(Fm1));
00255     if(T) {
00256         cuddRef(T);
00257     } else {
00258         Cudd_RecursiveDeref(bdd, Fm1);
00259         Cudd_RecursiveDeref(bdd, Fn);
00260         Cudd_RecursiveDeref(bdd, Fv);
00261         Cudd_RecursiveDeref(bdd, Fvbar);
00262         Cudd_RecursiveDeref(bdd, w);
00263         return(NULL);
00264     }
00265 
00266     Cudd_RecursiveDeref(bdd,Fm1);
00267     Cudd_RecursiveDeref(bdd,w);
00268     Cudd_RecursiveDeref(bdd,Fv);
00269     Cudd_RecursiveDeref(bdd,Fvbar);
00270 
00271     /* Substitute components of solution already found into solution. */
00272     for (j = n-1; j > i; j--) {
00273         w = cuddBddComposeRecur(bdd,T, G[j], variables[yIndex[j]]);
00274         if(w) {
00275             cuddRef(w);
00276         } else {
00277             Cudd_RecursiveDeref(bdd, Fn);
00278             Cudd_RecursiveDeref(bdd, T);
00279             return(NULL);
00280         }
00281         Cudd_RecursiveDeref(bdd,T);
00282         T = w;
00283     }
00284     G[i] = T;
00285 
00286     Cudd_Deref(Fn);
00287 
00288     return(Fn);
00289 
00290 } /* end of cuddSolveEqnRecur */

DdNode* cuddVerifySol ( DdManager *  bdd,
DdNode *  F,
DdNode **  G,
int *  yIndex,
int  n 
)

Function********************************************************************

Synopsis [Implements the recursive step of Cudd_VerifySol. ]

Description []

SideEffects [none]

SeeAlso [Cudd_VerifySol]

Definition at line 305 of file cuddSolve.c.

00311 {
00312     DdNode *w, *R;
00313 
00314     int j;
00315 
00316     R = F;
00317     cuddRef(R);
00318     for(j = n - 1; j >= 0; j--) {
00319          w = Cudd_bddCompose(bdd, R, G[j], yIndex[j]);
00320         if (w) {
00321             cuddRef(w);
00322         } else {
00323             return(NULL); 
00324         }
00325         Cudd_RecursiveDeref(bdd,R);
00326         R = w;
00327     }
00328 
00329     cuddDeref(R);
00330 
00331     return(R);
00332 
00333 } /* end of cuddVerifySol */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddSolve.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $" [static]

CFile***********************************************************************

FileName [cuddSolve.c]

PackageName [cudd]

Synopsis [Boolean equation solver and related functions.]

Description [External functions included in this modoule:

Internal functions included in this module:

]

SeeAlso []

Author [Balakrishna Kumthekar]

Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 54 of file cuddSolve.c.

Generated on Tue Jan 5 12:18:56 2010 for abc70930 by  doxygen 1.6.1