distr/dddmp/dddmpDdNodeBdd.c

   1 /**CFile**********************************************************************
   2
   3   FileName     [dddmpDdNodeBdd.c]
   4
   5   PackageName  [dddmp]
   6
   7   Synopsis     [Functions to handle BDD node infos and numbering]
   8
   9   Description  [Functions to handle BDD node infos and numbering.
  10     ]
  11
  12   Author       [Gianpiero Cabodi and Stefano Quer]
  13
  14   Copyright    [
  15     Copyright (c) 2004 by Politecnico di Torino.
  16     All Rights Reserved. This software is for educational purposes only.
  17     Permission is given to academic institutions to use, copy, and modify
  18     this software and its documentation provided that this introductory
  19     message is not removed, that this software and its documentation is
  20     used for the institutions' internal research and educational purposes,
  21     and that no monies are exchanged. No guarantee is expressed or implied
  22     by the distribution of this code.
  23     Send bug-reports and/or questions to:
  24     {gianpiero.cabodi,stefano.quer}@polito.it.
  25     ]
  26
  27 ******************************************************************************/
  28
  29 #include "dddmpInt.h"
  30
  31 /*---------------------------------------------------------------------------*/
  32 /* Stucture declarations                                                     */
  33 /*---------------------------------------------------------------------------*/
  34
  35 /*---------------------------------------------------------------------------*/
  36 /* Type declarations                                                         */
  37 /*---------------------------------------------------------------------------*/
  38
  39 /*---------------------------------------------------------------------------*/
  40 /* Variable declarations                                                     */
  41 /*---------------------------------------------------------------------------*/
  42
  43 /*---------------------------------------------------------------------------*/
  44 /* Macro declarations                                                        */
  45 /*---------------------------------------------------------------------------*/
  46
  47 /**AutomaticStart*************************************************************/
  48
  49 /*---------------------------------------------------------------------------*/
  50 /* Static function prototypes                                                */
  51 /*---------------------------------------------------------------------------*/
  52
  53 static int NumberNodeRecur(DdNode *f, int id);
  54 static void RemoveFromUniqueRecur(DdManager *ddMgr, DdNode *f);
  55 static void RestoreInUniqueRecur(DdManager *ddMgr, DdNode *f);
  56
  57 /**AutomaticEnd***************************************************************/
  58
  59 /*---------------------------------------------------------------------------*/
  60 /* Definition of exported functions                                          */
  61 /*---------------------------------------------------------------------------*/
  62
  63 /*---------------------------------------------------------------------------*/
  64 /* Definition of internal functions                                          */
  65 /*---------------------------------------------------------------------------*/
  66
  67 /**Function********************************************************************
  68
  69   Synopsis    [Removes nodes from unique table and number them]
  70
  71   Description [Node numbering is required to convert pointers to integers.
  72     Since nodes are removed from unique table, no new nodes should
  73     be generated before re-inserting nodes in the unique table
  74     (DddmpUnnumberDdNodes()).
  75     ]
  76
  77   SideEffects [Nodes are temporarily removed from unique table]
  78
  79   SeeAlso     [RemoveFromUniqueRecur(), NumberNodeRecur(),
  80     DddmpUnnumberDdNodes()]
  81
  82 ******************************************************************************/
  83
  84 int
  85 DddmpNumberDdNodes (
  86   DdManager *ddMgr  /* IN: DD Manager */,
  87   DdNode **f        /* IN: array of BDDs */,
  88   int n             /* IN: number of BDD roots in the array of BDDs */
  89   )
  90 {
  91   int id=0, i;
  92
  93   for (i=0; i<n; i++) {
  94     RemoveFromUniqueRecur (ddMgr, f[i]);
  95   }
  96
  97   for (i=0; i<n; i++) {
  98     id = NumberNodeRecur (f[i], id);
  99   }
 100
 101   return (id);
 102 }
 103
 104
 105 /**Function********************************************************************
 106
 107   Synopsis     [Restores nodes in unique table, loosing numbering]
 108
 109   Description  [Node indexes are no more needed. Nodes are re-linked in the
 110     unique table.
 111     ]
 112
 113   SideEffects  [None]
 114
 115   SeeAlso      [DddmpNumberDdNode()]
 116
 117 ******************************************************************************/
 118
 119 void
 120 DddmpUnnumberDdNodes(
 121   DdManager *ddMgr  /* IN: DD Manager */,
 122   DdNode **f        /* IN: array of BDDs */,
 123   int n             /* IN: number of BDD roots in the array of BDDs */
 124   )
 125 {
 126   int i;
 127
 128   for (i=0; i<n; i++) {
 129     RestoreInUniqueRecur (ddMgr, f[i]);
 130   }
 131
 132   return;
 133 }
 134
 135 /**Function********************************************************************
 136
 137   Synopsis     [Write index to node]
 138
 139   Description  [The index of the node is written in the "next" field of
 140     a DdNode struct. LSB is not used (set to 0). It is used as
 141     "visited" flag in DD traversals.
 142     ]
 143
 144   SideEffects  [None]
 145
 146   SeeAlso      [DddmpReadNodeIndex(), DddmpSetVisited (), DddmpVisited ()]
 147
 148 ******************************************************************************/
 149
 150 void
 151 DddmpWriteNodeIndex (
 152   DdNode *f   /* IN: BDD node */,
 153   int id       /* IN: index to be written */
 154   )
 155 {
 156 #if 0
 157   if (1 || !Cudd_IsConstant (f)) {
 158 #else
 159   if (!Cudd_IsConstant (f)) {
 160 #endif
 161     f->next = (struct DdNode *)((ptruint)((id)<<1));
 162   }
 163
 164   return;
 165 }
 166
 167 /**Function********************************************************************
 168
 169   Synopsis     [Reads the index of a node]
 170
 171   Description  [Reads the index of a node. LSB is skipped (used as visited
 172     flag).
 173     ]
 174
 175   SideEffects  [None]
 176
 177   SeeAlso      [DddmpWriteNodeIndex(), DddmpSetVisited (), DddmpVisited ()]
 178
 179 ******************************************************************************/
 180
 181 int
 182 DddmpReadNodeIndex (
 183   DdNode *f    /* IN: BDD node */
 184   )
 185 {
 186
 187 #if 0
 188   if (1 || !Cudd_IsConstant (f)) {
 189 #else
 190   if (!Cudd_IsConstant (f)) {
 191 #endif
 192     return ((int)(((ptruint)(f->next))>>1));
 193   } else {
 194     return (1);
 195   }
 196 }
 197
 198 /**Function********************************************************************
 199
 200   Synopsis     [Returns true if node is visited]
 201
 202   Description  [Returns true if node is visited]
 203
 204   SideEffects  [None]
 205
 206   SeeAlso      [DddmpSetVisited (), DddmpClearVisited ()]
 207
 208 ******************************************************************************/
 209
 210 int
 211 DddmpVisited (
 212   DdNode *f    /* IN: BDD node to be tested */
 213   )
 214 {
 215   f = Cudd_Regular(f);
 216   return ((int)((ptruint)(f->next)) & (01));
 217 }
 218
 219 /**Function********************************************************************
 220
 221   Synopsis     [Marks a node as visited]
 222
 223   Description  [Marks a node as visited]
 224
 225   SideEffects  [None]
 226
 227   SeeAlso      [DddmpVisited (), DddmpClearVisited ()]
 228
 229 ******************************************************************************/
 230
 231 void
 232 DddmpSetVisited (
 233   DdNode *f   /* IN: BDD node to be marked (as visited) */
 234   )
 235 {
 236   f = Cudd_Regular(f);
 237
 238   f->next = (DdNode *)(ptruint)((int)((ptruint)(f->next))|01);
 239
 240   return;
 241 }
 242
 243 /**Function********************************************************************
 244
 245   Synopsis     [Marks a node as not visited]
 246
 247   Description  [Marks a node as not visited]
 248
 249   SideEffects  [None]
 250
 251   SeeAlso      [DddmpVisited (), DddmpSetVisited ()]
 252
 253 ******************************************************************************/
 254
 255 void
 256 DddmpClearVisited (
 257   DdNode *f    /* IN: BDD node to be marked (as not visited) */
 258   )
 259 {
 260   f = Cudd_Regular (f);
 261
 262   f->next = (DdNode *)(ptruint)((int)((ptruint)(f->next)) & (~01));
 263
 264   return;
 265 }
 266
 267 /*---------------------------------------------------------------------------*/
 268 /* Definition of static functions                                            */
 269 /*---------------------------------------------------------------------------*/
 270
 271 /**Function********************************************************************
 272
 273   Synopsis     [Number nodes recursively in post-order]
 274
 275   Description  [Number nodes recursively in post-order.
 276     The "visited" flag is used with inverse polarity, because all nodes
 277     were set "visited" when removing them from unique.
 278     ]
 279
 280   SideEffects  ["visited" flags are reset.]
 281
 282   SeeAlso      []
 283
 284 ******************************************************************************/
 285
 286 static int
 287 NumberNodeRecur(
 288   DdNode *f  /*  IN: root of the BDD to be numbered */,
 289   int id     /* IN/OUT: index to be assigned to the node */
 290   )
 291 {
 292   f = Cudd_Regular(f);
 293
 294   if (!DddmpVisited (f)) {
 295     return (id);
 296   }
 297
 298   if (!cuddIsConstant (f)) {
 299     id = NumberNodeRecur (cuddT (f), id);
 300     id = NumberNodeRecur (cuddE (f), id);
 301   }
 302
 303   DddmpWriteNodeIndex (f, ++id);
 304   DddmpClearVisited (f);
 305
 306   return (id);
 307 }
 308
 309 /**Function********************************************************************
 310
 311   Synopsis    [Removes a node from unique table]
 312
 313   Description [Removes a node from the unique table by locating the proper
 314     subtable and unlinking the node from it. It recurs on the
 315     children of the node.
 316     ]
 317
 318   SideEffects [Nodes are left with the "visited" flag true.]
 319
 320   SeeAlso     [RestoreInUniqueRecur()]
 321
 322 ******************************************************************************/
 323
 324 static void
 325 RemoveFromUniqueRecur (
 326   DdManager *ddMgr  /*  IN: DD Manager */,
 327   DdNode *f         /*  IN: root of the BDD to be extracted */
 328   )
 329 {
 330   DdNode *node, *last, *next;
 331   DdNode *sentinel = &(ddMgr->sentinel);
 332   DdNodePtr *nodelist;
 333   DdSubtable *subtable;
 334   int pos, level;
 335
 336   f = Cudd_Regular (f);
 337
 338   if (DddmpVisited (f)) {
 339     return;
 340   }
 341
 342   if (!cuddIsConstant (f)) {
 343
 344     RemoveFromUniqueRecur (ddMgr, cuddT (f));
 345     RemoveFromUniqueRecur (ddMgr, cuddE (f));
 346
 347     level = ddMgr->perm[f->index];
 348     subtable = &(ddMgr->subtables[level]);
 349
 350     nodelist = subtable->nodelist;
 351
 352     pos = ddHash (cuddT (f), cuddE (f), subtable->shift);
 353     node = nodelist[pos];
 354     last = NULL;
 355     while (node != sentinel) {
 356       next = node->next;
 357       if (node == f) {
 358         if (last != NULL)
 359           last->next = next;
 360         else
 361           nodelist[pos] = next;
 362         break;
 363       } else {
 364         last = node;
 365         node = next;
 366       }
 367     }
 368
 369     f->next = NULL;
 370
 371   }
 372
 373   DddmpSetVisited (f);
 374
 375   return;
 376 }
 377
 378 /**Function********************************************************************
 379
 380   Synopsis     [Restores a node in unique table]
 381
 382   Description  [Restores a node in unique table (recursively)]
 383
 384   SideEffects  [Nodes are not restored in the same order as before removal]
 385
 386   SeeAlso      [RemoveFromUnique()]
 387
 388 ******************************************************************************/
 389
 390 static void
 391 RestoreInUniqueRecur (
 392   DdManager *ddMgr /*  IN: DD Manager */,
 393   DdNode *f        /*  IN: root of the BDD to be restored */
 394   )
 395 {
 396   DdNodePtr *nodelist;
 397   DdNode *T, *E, *looking;
 398   DdNodePtr *previousP;
 399   DdSubtable *subtable;
 400   int pos, level;
 401 #ifdef DDDMP_DEBUG
 402   DdNode *node;
 403   DdNode *sentinel = &(ddMgr->sentinel);
 404 #endif
 405
 406   f = Cudd_Regular(f);
 407
 408   if (!Cudd_IsComplement (f->next)) {
 409     return;
 410   }
 411
 412   if (cuddIsConstant (f)) {
 413     DddmpClearVisited (f);
 414     /*f->next = NULL;*/
 415     return;
 416   }
 417
 418   RestoreInUniqueRecur (ddMgr, cuddT (f));
 419   RestoreInUniqueRecur (ddMgr, cuddE (f));
 420
 421   level = ddMgr->perm[f->index];
 422   subtable = &(ddMgr->subtables[level]);
 423
 424   nodelist = subtable->nodelist;
 425
 426   pos = ddHash (cuddT (f), cuddE (f), subtable->shift);
 427
 428 #ifdef DDDMP_DEBUG
 429   /* verify uniqueness to avoid duplicate nodes in unique table */
 430   for (node=nodelist[pos]; node != sentinel; node=node->next)
 431     assert(node!=f);
 432 #endif
 433
 434   T = cuddT (f);
 435   E = cuddE (f);
 436   previousP = &(nodelist[pos]);
 437   looking = *previousP;
 438
 439   while (T < cuddT (looking)) {
 440     previousP = &(looking->next);
 441     looking = *previousP;
 442   }
 443
 444   while (T == cuddT (looking) && E < cuddE (looking)) {
 445     previousP = &(looking->next);
 446     looking = *previousP;
 447   }
 448
 449   f->next = *previousP;
 450   *previousP = f;
 451
 452   return;
 453 }
 454
 455