src/cuBdd/cuddZddPort.c File Reference

#include "util.h"
#include "cuddInt.h"
Include dependency graph for cuddZddPort.c:

Go to the source code of this file.

Functions

static DdNode * zddPortFromBddStep (DdManager *dd, DdNode *B, int expected)
static DdNode * zddPortToBddStep (DdManager *dd, DdNode *f, int depth)
DdNode * Cudd_zddPortFromBdd (DdManager *dd, DdNode *B)
DdNode * Cudd_zddPortToBdd (DdManager *dd, DdNode *f)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddZddPort.c,v 1.13 2004/08/13 18:04:53 fabio Exp $"

Function Documentation

DdNode* Cudd_zddPortFromBdd ( DdManager *  dd,
DdNode *  B 
)

AutomaticEnd Function********************************************************************

Synopsis [Converts a BDD into a ZDD.]

Description [Converts a BDD into a ZDD. This function assumes that there is a one-to-one correspondence between the BDD variables and the ZDD variables, and that the variable order is the same for both types of variables. These conditions are established if the ZDD variables are created by one call to Cudd_zddVarsFromBddVars with multiplicity = 1. Returns a pointer to the resulting ZDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_zddVarsFromBddVars]

Definition at line 127 of file cuddZddPort.c.

00130 {
00131     DdNode *res;
00132 
00133     do {
00134         dd->reordered = 0;
00135         res = zddPortFromBddStep(dd,B,0);
00136     } while (dd->reordered == 1);
00137 
00138     return(res);
00139 
00140 } /* end of Cudd_zddPortFromBdd */

DdNode* Cudd_zddPortToBdd ( DdManager *  dd,
DdNode *  f 
)

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

Synopsis [Converts a ZDD into a BDD.]

Description [Converts a ZDD into a BDD. Returns a pointer to the resulting ZDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_zddPortFromBdd]

Definition at line 156 of file cuddZddPort.c.

00159 {
00160     DdNode *res;
00161 
00162     do {
00163         dd->reordered = 0;
00164         res = zddPortToBddStep(dd,f,0);
00165     } while (dd->reordered == 1);
00166 
00167     return(res);
00168 
00169 } /* end of Cudd_zddPortToBdd */

static DdNode * zddPortFromBddStep ( DdManager *  dd,
DdNode *  B,
int  expected 
) [static]

AutomaticStart

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

Synopsis [Performs the recursive step of Cudd_zddPortFromBdd.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 193 of file cuddZddPort.c.

00197 {
00198     DdNode      *res, *prevZdd, *t, *e;
00199     DdNode      *Breg, *Bt, *Be;
00200     int         id, level;
00201 
00202     statLine(dd);
00203     /* Terminal cases. */
00204     if (B == Cudd_Not(DD_ONE(dd)))
00205         return(DD_ZERO(dd));
00206     if (B == DD_ONE(dd)) {
00207         if (expected >= dd->sizeZ) {
00208             return(DD_ONE(dd));
00209         } else {
00210             return(dd->univ[expected]);
00211         }
00212     }
00213 
00214     Breg = Cudd_Regular(B);
00215 
00216     /* Computed table look-up. */
00217     res = cuddCacheLookup1Zdd(dd,Cudd_zddPortFromBdd,B);
00218     if (res != NULL) {
00219         level = cuddI(dd,Breg->index);
00220         /* Adding DC vars. */
00221         if (expected < level) {
00222             /* Add suppressed variables. */
00223             cuddRef(res);
00224             for (level--; level >= expected; level--) {
00225                 prevZdd = res;
00226                 id = dd->invperm[level];
00227                 res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
00228                 if (res == NULL) {
00229                     Cudd_RecursiveDerefZdd(dd, prevZdd);
00230                     return(NULL);
00231                 }
00232                 cuddRef(res);
00233                 Cudd_RecursiveDerefZdd(dd, prevZdd);
00234             }
00235             cuddDeref(res);
00236         }
00237         return(res);
00238     }   /* end of cache look-up */
00239 
00240     if (Cudd_IsComplement(B)) {
00241         Bt = Cudd_Not(cuddT(Breg));
00242         Be = Cudd_Not(cuddE(Breg));
00243     } else {
00244         Bt = cuddT(Breg);
00245         Be = cuddE(Breg);
00246     }
00247 
00248     id = Breg->index;
00249     level = cuddI(dd,id);
00250     t = zddPortFromBddStep(dd, Bt, level+1);
00251     if (t == NULL) return(NULL);
00252     cuddRef(t);
00253     e = zddPortFromBddStep(dd, Be, level+1);
00254     if (e == NULL) {
00255         Cudd_RecursiveDerefZdd(dd, t);
00256         return(NULL);
00257     }
00258     cuddRef(e);
00259     res = cuddZddGetNode(dd, id, t, e);
00260     if (res == NULL) {
00261         Cudd_RecursiveDerefZdd(dd, t);
00262         Cudd_RecursiveDerefZdd(dd, e);
00263         return(NULL);
00264     }
00265     cuddRef(res);
00266     Cudd_RecursiveDerefZdd(dd, t);
00267     Cudd_RecursiveDerefZdd(dd, e);
00268 
00269     cuddCacheInsert1(dd,Cudd_zddPortFromBdd,B,res);
00270 
00271     for (level--; level >= expected; level--) {
00272         prevZdd = res;
00273         id = dd->invperm[level];
00274         res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
00275         if (res == NULL) {
00276             Cudd_RecursiveDerefZdd(dd, prevZdd);
00277             return(NULL);
00278         }
00279         cuddRef(res);
00280         Cudd_RecursiveDerefZdd(dd, prevZdd);
00281     }
00282 
00283     cuddDeref(res);
00284     return(res);
00285 
00286 } /* end of zddPortFromBddStep */

static DdNode * zddPortToBddStep ( DdManager *  dd,
DdNode *  f,
int  depth 
) [static]

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

Synopsis [Performs the recursive step of Cudd_zddPortToBdd.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 301 of file cuddZddPort.c.

00305 {
00306     DdNode *one, *zero, *T, *E, *res, *var;
00307     unsigned int index;
00308     unsigned int level;
00309 
00310     statLine(dd);
00311     one = DD_ONE(dd);
00312     zero = DD_ZERO(dd);
00313     if (f == zero) return(Cudd_Not(one));
00314 
00315     if (depth == dd->sizeZ) return(one);
00316 
00317     index = dd->invpermZ[depth];
00318     level = cuddIZ(dd,f->index);
00319     var = cuddUniqueInter(dd,index,one,Cudd_Not(one));
00320     if (var == NULL) return(NULL);
00321     cuddRef(var);
00322 
00323     if (level > (unsigned) depth) {
00324         E = zddPortToBddStep(dd,f,depth+1);
00325         if (E == NULL) {
00326             Cudd_RecursiveDeref(dd,var);
00327             return(NULL);
00328         }
00329         cuddRef(E);
00330         res = cuddBddIteRecur(dd,var,Cudd_Not(one),E);
00331         if (res == NULL) {
00332             Cudd_RecursiveDeref(dd,var);
00333             Cudd_RecursiveDeref(dd,E);
00334             return(NULL);
00335         }
00336         cuddRef(res);
00337         Cudd_RecursiveDeref(dd,var);
00338         Cudd_RecursiveDeref(dd,E);
00339         cuddDeref(res);
00340         return(res);
00341     }
00342 
00343     res = cuddCacheLookup1(dd,Cudd_zddPortToBdd,f);
00344     if (res != NULL) {
00345         Cudd_RecursiveDeref(dd,var);
00346         return(res);
00347     }
00348 
00349     T = zddPortToBddStep(dd,cuddT(f),depth+1);
00350     if (T == NULL) {
00351         Cudd_RecursiveDeref(dd,var);
00352         return(NULL);
00353     }
00354     cuddRef(T);
00355     E = zddPortToBddStep(dd,cuddE(f),depth+1);
00356     if (E == NULL) {
00357         Cudd_RecursiveDeref(dd,var);
00358         Cudd_RecursiveDeref(dd,T);
00359         return(NULL);
00360     }
00361     cuddRef(E);
00362 
00363     res = cuddBddIteRecur(dd,var,T,E);
00364     if (res == NULL) {
00365         Cudd_RecursiveDeref(dd,var);
00366         Cudd_RecursiveDeref(dd,T);
00367         Cudd_RecursiveDeref(dd,E);
00368         return(NULL);
00369     }
00370     cuddRef(res);
00371     Cudd_RecursiveDeref(dd,var);
00372     Cudd_RecursiveDeref(dd,T);
00373     Cudd_RecursiveDeref(dd,E);
00374     cuddDeref(res);
00375 
00376     cuddCacheInsert1(dd,Cudd_zddPortToBdd,f,res);
00377 
00378     return(res);
00379 
00380 } /* end of zddPortToBddStep */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddZddPort.c,v 1.13 2004/08/13 18:04:53 fabio Exp $" [static]

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

FileName [cuddZddPort.c]

PackageName [cudd]

Synopsis [Functions that translate BDDs to ZDDs.]

Description [External procedures included in this module:

Internal procedures included in this module:

procedures included in this module:

]

SeeAlso []

Author [Hyong-kyoon Shin, In-Ho Moon]

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 85 of file cuddZddPort.c.

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