src/cuBdd/cuddSolve.c File Reference

#include "util.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.12 2004/08/13 18:04:51 fabio 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 122 of file cuddSolve.c.

00129 {
00130     DdNode *res;
00131     int *temp;
00132 
00133     *yIndex = temp = ALLOC(int, n);
00134     if (temp == NULL) {
00135         bdd->errorCode = CUDD_MEMORY_OUT;
00136         (void) fprintf(bdd->out,
00137                        "Cudd_SolveEqn: Out of memory for yIndex\n");
00138         return(NULL);
00139     }
00140 
00141     do {
00142         bdd->reordered = 0;
00143         res = cuddSolveEqnRecur(bdd, F, Y, G, n, temp, 0);
00144     } while (bdd->reordered == 1);
00145 
00146     return(res);
00147 
00148 } /* 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 165 of file cuddSolve.c.

00171 {
00172     DdNode *res;
00173 
00174     do {
00175         bdd->reordered = 0;
00176         res = cuddVerifySol(bdd, F, G, yIndex, n);
00177     } while (bdd->reordered == 1);
00178 
00179     FREE(yIndex);
00180 
00181     return(res);
00182 
00183 } /* 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 206 of file cuddSolve.c.

00214 {
00215     DdNode *Fn, *Fm1, *Fv, *Fvbar, *T, *w, *nextY, *one;
00216     DdNodePtr *variables;
00217 
00218     int j;
00219 
00220     statLine(bdd);
00221     variables = bdd->vars;
00222     one = DD_ONE(bdd);
00223 
00224     /* Base condition. */
00225     if (Y == one) {
00226         return F;
00227     }
00228 
00229     /* Cofactor of Y. */
00230     yIndex[i] = Y->index;
00231     nextY = Cudd_T(Y);
00232 
00233     /* Universal abstraction of F with respect to the top variable index. */
00234     Fm1 = cuddBddExistAbstractRecur(bdd, Cudd_Not(F), variables[yIndex[i]]);
00235     if (Fm1) {
00236         Fm1 = Cudd_Not(Fm1);
00237         cuddRef(Fm1);
00238     } else {
00239         return(NULL);
00240     }
00241 
00242     Fn = cuddSolveEqnRecur(bdd, Fm1, nextY, G, n, yIndex, i+1);
00243     if (Fn) {
00244         cuddRef(Fn);
00245     } else {
00246         Cudd_RecursiveDeref(bdd, Fm1);
00247         return(NULL);
00248     }
00249 
00250     Fv = cuddCofactorRecur(bdd, F, variables[yIndex[i]]);
00251     if (Fv) {
00252         cuddRef(Fv);
00253     } else {
00254         Cudd_RecursiveDeref(bdd, Fm1);
00255         Cudd_RecursiveDeref(bdd, Fn);
00256         return(NULL);
00257     }
00258 
00259     Fvbar = cuddCofactorRecur(bdd, F, Cudd_Not(variables[yIndex[i]]));
00260     if (Fvbar) {
00261         cuddRef(Fvbar);
00262     } else {
00263         Cudd_RecursiveDeref(bdd, Fm1);
00264         Cudd_RecursiveDeref(bdd, Fn);
00265         Cudd_RecursiveDeref(bdd, Fv);
00266         return(NULL);
00267     }
00268 
00269     /* Build i-th component of the solution. */
00270     w = cuddBddIteRecur(bdd, variables[yIndex[i]], Cudd_Not(Fv), Fvbar);
00271     if (w) {
00272         cuddRef(w);
00273     } else {
00274         Cudd_RecursiveDeref(bdd, Fm1);
00275         Cudd_RecursiveDeref(bdd, Fn);
00276         Cudd_RecursiveDeref(bdd, Fv);
00277         Cudd_RecursiveDeref(bdd, Fvbar);
00278         return(NULL);
00279     }
00280 
00281     T = cuddBddRestrictRecur(bdd, w, Cudd_Not(Fm1));
00282     if(T) {
00283         cuddRef(T);
00284     } else {
00285         Cudd_RecursiveDeref(bdd, Fm1);
00286         Cudd_RecursiveDeref(bdd, Fn);
00287         Cudd_RecursiveDeref(bdd, Fv);
00288         Cudd_RecursiveDeref(bdd, Fvbar);
00289         Cudd_RecursiveDeref(bdd, w);
00290         return(NULL);
00291     }
00292 
00293     Cudd_RecursiveDeref(bdd,Fm1);
00294     Cudd_RecursiveDeref(bdd,w);
00295     Cudd_RecursiveDeref(bdd,Fv);
00296     Cudd_RecursiveDeref(bdd,Fvbar);
00297 
00298     /* Substitute components of solution already found into solution. */
00299     for (j = n-1; j > i; j--) {
00300         w = cuddBddComposeRecur(bdd,T, G[j], variables[yIndex[j]]);
00301         if(w) {
00302             cuddRef(w);
00303         } else {
00304             Cudd_RecursiveDeref(bdd, Fn);
00305             Cudd_RecursiveDeref(bdd, T);
00306             return(NULL);
00307         }
00308         Cudd_RecursiveDeref(bdd,T);
00309         T = w;
00310     }
00311     G[i] = T;
00312 
00313     Cudd_Deref(Fn);
00314 
00315     return(Fn);
00316 
00317 } /* 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 332 of file cuddSolve.c.

00338 {
00339     DdNode *w, *R;
00340 
00341     int j;
00342 
00343     R = F;
00344     cuddRef(R);
00345     for(j = n - 1; j >= 0; j--) {
00346          w = Cudd_bddCompose(bdd, R, G[j], yIndex[j]);
00347         if (w) {
00348             cuddRef(w);
00349         } else {
00350             return(NULL); 
00351         }
00352         Cudd_RecursiveDeref(bdd,R);
00353         R = w;
00354     }
00355 
00356     cuddDeref(R);
00357 
00358     return(R);
00359 
00360 } /* end of cuddVerifySol */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddSolve.c,v 1.12 2004/08/13 18:04:51 fabio 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 [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 81 of file cuddSolve.c.

Generated on Tue Jan 12 13:57:21 2010 for glu-2.2 by  doxygen 1.6.1