distr/cudd/cuddZddPort.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddZddPort.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions that translate BDDs to ZDDs.]
   8
   9   Description [External procedures included in this module:
  10                     <ul>
  11                     <li> Cudd_zddPortFromBdd()
  12                     <li> Cudd_zddPortToBdd()
  13                     </ul>
  14                Internal procedures included in this module:
  15                     <ul>
  16                     </ul>
  17                Static procedures included in this module:
  18                     <ul>
  19                     <li> zddPortFromBddStep()
  20                     <li> zddPortToBddStep()
  21                     </ul>
  22               ]
  23
  24   SeeAlso     []
  25
  26   Author      [Hyong-kyoon Shin, In-Ho Moon]
  27
  28   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  29
  30   All rights reserved.
  31
  32   Redistribution and use in source and binary forms, with or without
  33   modification, are permitted provided that the following conditions
  34   are met:
  35
  36   Redistributions of source code must retain the above copyright
  37   notice, this list of conditions and the following disclaimer.
  38
  39   Redistributions in binary form must reproduce the above copyright
  40   notice, this list of conditions and the following disclaimer in the
  41   documentation and/or other materials provided with the distribution.
  42
  43   Neither the name of the University of Colorado nor the names of its
  44   contributors may be used to endorse or promote products derived from
  45   this software without specific prior written permission.
  46
  47   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  48   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  49   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  50   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  51   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  52   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  53   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  54   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  55   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  56   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  57   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  58   POSSIBILITY OF SUCH DAMAGE.]
  59
  60 ******************************************************************************/
  61
  62 #include "util.h"
  63 #include "cuddInt.h"
  64
  65 /*---------------------------------------------------------------------------*/
  66 /* Constant declarations                                                     */
  67 /*---------------------------------------------------------------------------*/
  68
  69
  70 /*---------------------------------------------------------------------------*/
  71 /* Stucture declarations                                                     */
  72 /*---------------------------------------------------------------------------*/
  73
  74
  75 /*---------------------------------------------------------------------------*/
  76 /* Type declarations                                                         */
  77 /*---------------------------------------------------------------------------*/
  78
  79
  80 /*---------------------------------------------------------------------------*/
  81 /* Variable declarations                                                     */
  82 /*---------------------------------------------------------------------------*/
  83
  84 #ifndef lint
  85 static char rcsid[] DD_UNUSED = "$Id: cuddZddPort.c,v 1.13 2004/08/13 18:04:53 fabio Exp $";
  86 #endif
  87
  88 /*---------------------------------------------------------------------------*/
  89 /* Macro declarations                                                        */
  90 /*---------------------------------------------------------------------------*/
  91
  92
  93 /**AutomaticStart*************************************************************/
  94
  95 /*---------------------------------------------------------------------------*/
  96 /* Static function prototypes                                                */
  97 /*---------------------------------------------------------------------------*/
  98
  99 static DdNode * zddPortFromBddStep (DdManager *dd, DdNode *B, int expected);
 100 static DdNode * zddPortToBddStep (DdManager *dd, DdNode *f, int depth);
 101
 102 /**AutomaticEnd***************************************************************/
 103
 104
 105 /*---------------------------------------------------------------------------*/
 106 /* Definition of exported functions                                          */
 107 /*---------------------------------------------------------------------------*/
 108
 109
 110 /**Function********************************************************************
 111
 112   Synopsis [Converts a BDD into a ZDD.]
 113
 114   Description [Converts a BDD into a ZDD. This function assumes that
 115   there is a one-to-one correspondence between the BDD variables and the
 116   ZDD variables, and that the variable order is the same for both types
 117   of variables. These conditions are established if the ZDD variables
 118   are created by one call to Cudd_zddVarsFromBddVars with multiplicity =
 119   1. Returns a pointer to the resulting ZDD if successful; NULL otherwise.]
 120
 121   SideEffects [None]
 122
 123   SeeAlso     [Cudd_zddVarsFromBddVars]
 124
 125 ******************************************************************************/
 126 DdNode *
 127 Cudd_zddPortFromBdd(
 128   DdManager * dd,
 129   DdNode * B)
 130 {
 131     DdNode *res;
 132
 133     do {
 134         dd->reordered = 0;
 135         res = zddPortFromBddStep(dd,B,0);
 136     } while (dd->reordered == 1);
 137
 138     return(res);
 139
 140 } /* end of Cudd_zddPortFromBdd */
 141
 142
 143 /**Function********************************************************************
 144
 145   Synopsis [Converts a ZDD into a BDD.]
 146
 147   Description [Converts a ZDD into a BDD. Returns a pointer to the resulting
 148   ZDD if successful; NULL otherwise.]
 149
 150   SideEffects [None]
 151
 152   SeeAlso     [Cudd_zddPortFromBdd]
 153
 154 ******************************************************************************/
 155 DdNode *
 156 Cudd_zddPortToBdd(
 157   DdManager * dd,
 158   DdNode * f)
 159 {
 160     DdNode *res;
 161
 162     do {
 163         dd->reordered = 0;
 164         res = zddPortToBddStep(dd,f,0);
 165     } while (dd->reordered == 1);
 166
 167     return(res);
 168
 169 } /* end of Cudd_zddPortToBdd */
 170
 171
 172 /*---------------------------------------------------------------------------*/
 173 /* Definition of internal functions                                          */
 174 /*---------------------------------------------------------------------------*/
 175
 176 /*---------------------------------------------------------------------------*/
 177 /* Definition of static functions                                            */
 178 /*---------------------------------------------------------------------------*/
 179
 180
 181 /**Function********************************************************************
 182
 183   Synopsis [Performs the recursive step of Cudd_zddPortFromBdd.]
 184
 185   Description []
 186
 187   SideEffects [None]
 188
 189   SeeAlso     []
 190
 191 ******************************************************************************/
 192 static DdNode *
 193 zddPortFromBddStep(
 194   DdManager * dd,
 195   DdNode * B,
 196   int  expected)
 197 {
 198     DdNode      *res, *prevZdd, *t, *e;
 199     DdNode      *Breg, *Bt, *Be;
 200     int         id, level;
 201
 202     statLine(dd);
 203     /* Terminal cases. */
 204     if (B == Cudd_Not(DD_ONE(dd)))
 205         return(DD_ZERO(dd));
 206     if (B == DD_ONE(dd)) {
 207         if (expected >= dd->sizeZ) {
 208             return(DD_ONE(dd));
 209         } else {
 210             return(dd->univ[expected]);
 211         }
 212     }
 213
 214     Breg = Cudd_Regular(B);
 215
 216     /* Computed table look-up. */
 217     res = cuddCacheLookup1Zdd(dd,Cudd_zddPortFromBdd,B);
 218     if (res != NULL) {
 219         level = cuddI(dd,Breg->index);
 220         /* Adding DC vars. */
 221         if (expected < level) {
 222             /* Add suppressed variables. */
 223             cuddRef(res);
 224             for (level--; level >= expected; level--) {
 225                 prevZdd = res;
 226                 id = dd->invperm[level];
 227                 res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
 228                 if (res == NULL) {
 229                     Cudd_RecursiveDerefZdd(dd, prevZdd);
 230                     return(NULL);
 231                 }
 232                 cuddRef(res);
 233                 Cudd_RecursiveDerefZdd(dd, prevZdd);
 234             }
 235             cuddDeref(res);
 236         }
 237         return(res);
 238     }   /* end of cache look-up */
 239
 240     if (Cudd_IsComplement(B)) {
 241         Bt = Cudd_Not(cuddT(Breg));
 242         Be = Cudd_Not(cuddE(Breg));
 243     } else {
 244         Bt = cuddT(Breg);
 245         Be = cuddE(Breg);
 246     }
 247
 248     id = Breg->index;
 249     level = cuddI(dd,id);
 250     t = zddPortFromBddStep(dd, Bt, level+1);
 251     if (t == NULL) return(NULL);
 252     cuddRef(t);
 253     e = zddPortFromBddStep(dd, Be, level+1);
 254     if (e == NULL) {
 255         Cudd_RecursiveDerefZdd(dd, t);
 256         return(NULL);
 257     }
 258     cuddRef(e);
 259     res = cuddZddGetNode(dd, id, t, e);
 260     if (res == NULL) {
 261         Cudd_RecursiveDerefZdd(dd, t);
 262         Cudd_RecursiveDerefZdd(dd, e);
 263         return(NULL);
 264     }
 265     cuddRef(res);
 266     Cudd_RecursiveDerefZdd(dd, t);
 267     Cudd_RecursiveDerefZdd(dd, e);
 268
 269     cuddCacheInsert1(dd,Cudd_zddPortFromBdd,B,res);
 270
 271     for (level--; level >= expected; level--) {
 272         prevZdd = res;
 273         id = dd->invperm[level];
 274         res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
 275         if (res == NULL) {
 276             Cudd_RecursiveDerefZdd(dd, prevZdd);
 277             return(NULL);
 278         }
 279         cuddRef(res);
 280         Cudd_RecursiveDerefZdd(dd, prevZdd);
 281     }
 282
 283     cuddDeref(res);
 284     return(res);
 285
 286 } /* end of zddPortFromBddStep */
 287
 288
 289 /**Function********************************************************************
 290
 291   Synopsis [Performs the recursive step of Cudd_zddPortToBdd.]
 292
 293   Description []
 294
 295   SideEffects [None]
 296
 297   SeeAlso     []
 298
 299 ******************************************************************************/
 300 static DdNode *
 301 zddPortToBddStep(
 302   DdManager * dd /* manager */,
 303   DdNode * f /* ZDD to be converted */,
 304   int  depth /* recursion depth */)
 305 {
 306     DdNode *one, *zero, *T, *E, *res, *var;
 307     unsigned int index;
 308     unsigned int level;
 309
 310     statLine(dd);
 311     one = DD_ONE(dd);
 312     zero = DD_ZERO(dd);
 313     if (f == zero) return(Cudd_Not(one));
 314
 315     if (depth == dd->sizeZ) return(one);
 316
 317     index = dd->invpermZ[depth];
 318     level = cuddIZ(dd,f->index);
 319     var = cuddUniqueInter(dd,index,one,Cudd_Not(one));
 320     if (var == NULL) return(NULL);
 321     cuddRef(var);
 322
 323     if (level > (unsigned) depth) {
 324         E = zddPortToBddStep(dd,f,depth+1);
 325         if (E == NULL) {
 326             Cudd_RecursiveDeref(dd,var);
 327             return(NULL);
 328         }
 329         cuddRef(E);
 330         res = cuddBddIteRecur(dd,var,Cudd_Not(one),E);
 331         if (res == NULL) {
 332             Cudd_RecursiveDeref(dd,var);
 333             Cudd_RecursiveDeref(dd,E);
 334             return(NULL);
 335         }
 336         cuddRef(res);
 337         Cudd_RecursiveDeref(dd,var);
 338         Cudd_RecursiveDeref(dd,E);
 339         cuddDeref(res);
 340         return(res);
 341     }
 342
 343     res = cuddCacheLookup1(dd,Cudd_zddPortToBdd,f);
 344     if (res != NULL) {
 345         Cudd_RecursiveDeref(dd,var);
 346         return(res);
 347     }
 348
 349     T = zddPortToBddStep(dd,cuddT(f),depth+1);
 350     if (T == NULL) {
 351         Cudd_RecursiveDeref(dd,var);
 352         return(NULL);
 353     }
 354     cuddRef(T);
 355     E = zddPortToBddStep(dd,cuddE(f),depth+1);
 356     if (E == NULL) {
 357         Cudd_RecursiveDeref(dd,var);
 358         Cudd_RecursiveDeref(dd,T);
 359         return(NULL);
 360     }
 361     cuddRef(E);
 362
 363     res = cuddBddIteRecur(dd,var,T,E);
 364     if (res == NULL) {
 365         Cudd_RecursiveDeref(dd,var);
 366         Cudd_RecursiveDeref(dd,T);
 367         Cudd_RecursiveDeref(dd,E);
 368         return(NULL);
 369     }
 370     cuddRef(res);
 371     Cudd_RecursiveDeref(dd,var);
 372     Cudd_RecursiveDeref(dd,T);
 373     Cudd_RecursiveDeref(dd,E);
 374     cuddDeref(res);
 375
 376     cuddCacheInsert1(dd,Cudd_zddPortToBdd,f,res);
 377
 378     return(res);
 379
 380 } /* end of zddPortToBddStep */
 381