distr/dddmp/dddmpNodeAdd.c

   1 /**CFile**********************************************************************
   2
   3   FileName     [dddmpNodeAdd.c]
   4
   5   PackageName  [dddmp]
   6
   7   Synopsis     [Functions to handle ADD node infos and numbering]
   8
   9   Description  [Functions to handle ADD 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 NumberNodeRecurAdd(DdNode *f, int id);
  54 static void RemoveFromUniqueRecurAdd(DdManager *ddMgr, DdNode *f);
  55 static void RestoreInUniqueRecurAdd(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     [RemoveFromUniqueRecurAdd (), NumberNodeRecurAdd (),
  80     DddmpUnnumberDdNodesAdd ()]
  81
  82 ******************************************************************************/
  83
  84 int
  85 DddmpNumberAddNodes (
  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     RemoveFromUniqueRecurAdd (ddMgr, f[i]);
  95   }
  96
  97   for (i=0; i<n; i++) {
  98     id = NumberNodeRecurAdd (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      [DddmpNumberDdNodeAdd ()]
 116
 117 ******************************************************************************/
 118
 119 void
 120 DddmpUnnumberAddNodes (
 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     RestoreInUniqueRecurAdd (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      [DddmpReadNodeIndexAdd (), DddmpSetVisitedAdd (),
 147     DddmpVisitedAdd ()]
 148
 149 ******************************************************************************/
 150
 151 void
 152 DddmpWriteNodeIndexAdd (
 153   DdNode *f   /* IN: BDD node */,
 154   int id      /* IN: index to be written */
 155   )
 156 {
 157   if (1 || !Cudd_IsConstant (f)) {
 158     f->next = (struct DdNode *)((ptruint)((id)<<1));
 159   }
 160
 161   return;
 162 }
 163
 164 /**Function********************************************************************
 165
 166   Synopsis     [Reads the index of a node]
 167
 168   Description  [Reads the index of a node. LSB is skipped (used as visited
 169     flag).
 170     ]
 171
 172   SideEffects  [None]
 173
 174   SeeAlso      [DddmpWriteNodeIndexAdd (), DddmpSetVisitedAdd  (),
 175     DddmpVisitedAdd ()]
 176
 177 ******************************************************************************/
 178
 179 int
 180 DddmpReadNodeIndexAdd (
 181   DdNode *f    /* IN: BDD node */
 182   )
 183 {
 184   if (1 || !Cudd_IsConstant (f)) {
 185     return ((int)(((ptruint)(f->next))>>1));
 186   } else {
 187     return (1);
 188   }
 189 }
 190
 191 /**Function********************************************************************
 192
 193   Synopsis     [Returns true if node is visited]
 194
 195   Description  [Returns true if node is visited]
 196
 197   SideEffects  [None]
 198
 199   SeeAlso      [DddmpSetVisitedAdd (), DddmpClearVisitedAdd ()]
 200
 201 ******************************************************************************/
 202
 203 int
 204 DddmpVisitedAdd (
 205   DdNode *f    /* IN: BDD node to be tested */
 206   )
 207 {
 208   f = Cudd_Regular(f);
 209   return ((int)((ptruint)(f->next)) & (01));
 210 }
 211
 212 /**Function********************************************************************
 213
 214   Synopsis     [Marks a node as visited]
 215
 216   Description  [Marks a node as visited]
 217
 218   SideEffects  [None]
 219
 220   SeeAlso      [DddmpVisitedAdd (), DddmpClearVisitedAdd ()]
 221
 222 ******************************************************************************/
 223
 224 void
 225 DddmpSetVisitedAdd (
 226   DdNode *f   /* IN: BDD node to be marked (as visited) */
 227   )
 228 {
 229   f = Cudd_Regular(f);
 230
 231   f->next = (DdNode *)(ptruint)((int)((ptruint)(f->next))|01);
 232
 233   return;
 234 }
 235
 236 /**Function********************************************************************
 237
 238   Synopsis     [Marks a node as not visited]
 239
 240   Description  [Marks a node as not visited]
 241
 242   SideEffects  [None]
 243
 244   SeeAlso      [DddmpVisitedAdd (), DddmpSetVisitedAdd ()]
 245
 246 ******************************************************************************/
 247
 248 void
 249 DddmpClearVisitedAdd (
 250   DdNode *f    /* IN: BDD node to be marked (as not visited) */
 251   )
 252 {
 253   f = Cudd_Regular (f);
 254
 255   f->next = (DdNode *)(ptruint)((int)((ptruint)(f->next)) & (~01));
 256
 257   return;
 258 }
 259
 260 /*---------------------------------------------------------------------------*/
 261 /* Definition of static functions                                            */
 262 /*---------------------------------------------------------------------------*/
 263
 264 /**Function********************************************************************
 265
 266   Synopsis     [Number nodes recursively in post-order]
 267
 268   Description  [Number nodes recursively in post-order.
 269     The "visited" flag is used with inverse polarity, because all nodes
 270     were set "visited" when removing them from unique.
 271     ]
 272
 273   SideEffects  ["visited" flags are reset.]
 274
 275   SeeAlso      []
 276
 277 ******************************************************************************/
 278
 279 static int
 280 NumberNodeRecurAdd (
 281   DdNode *f  /*  IN: root of the BDD to be numbered */,
 282   int id     /* IN/OUT: index to be assigned to the node */
 283   )
 284 {
 285   f = Cudd_Regular(f);
 286
 287   if (!DddmpVisitedAdd (f)) {
 288     return (id);
 289   }
 290
 291   if (!cuddIsConstant (f)) {
 292     id = NumberNodeRecurAdd (cuddT (f), id);
 293     id = NumberNodeRecurAdd (cuddE (f), id);
 294   }
 295
 296   DddmpWriteNodeIndexAdd (f, ++id);
 297   DddmpClearVisitedAdd (f);
 298
 299   return (id);
 300 }
 301
 302 /**Function********************************************************************
 303
 304   Synopsis    [Removes a node from unique table]
 305
 306   Description [Removes a node from the unique table by locating the proper
 307     subtable and unlinking the node from it. It recurs on the
 308     children of the node. Constants remain untouched.
 309     ]
 310
 311   SideEffects [Nodes are left with the "visited" flag true.]
 312
 313   SeeAlso     [RestoreInUniqueRecurAdd ()]
 314
 315 ******************************************************************************/
 316
 317 static void
 318 RemoveFromUniqueRecurAdd (
 319   DdManager *ddMgr  /*  IN: DD Manager */,
 320   DdNode *f         /*  IN: root of the BDD to be extracted */
 321   )
 322 {
 323   DdNode *node, *last, *next;
 324   DdNode *sentinel = &(ddMgr->sentinel);
 325   DdNodePtr *nodelist;
 326   DdSubtable *subtable;
 327   int pos, level;
 328
 329   f = Cudd_Regular (f);
 330
 331   if (DddmpVisitedAdd (f)) {
 332     return;
 333   }
 334
 335   if (!cuddIsConstant (f)) {
 336
 337     RemoveFromUniqueRecurAdd (ddMgr, cuddT (f));
 338     RemoveFromUniqueRecurAdd (ddMgr, cuddE (f));
 339
 340     level = ddMgr->perm[f->index];
 341     subtable = &(ddMgr->subtables[level]);
 342
 343     nodelist = subtable->nodelist;
 344
 345     pos = ddHash (cuddT (f), cuddE (f), subtable->shift);
 346     node = nodelist[pos];
 347     last = NULL;
 348     while (node != sentinel) {
 349       next = node->next;
 350       if (node == f) {
 351         if (last != NULL)
 352           last->next = next;
 353         else
 354           nodelist[pos] = next;
 355         break;
 356       } else {
 357         last = node;
 358         node = next;
 359       }
 360     }
 361
 362     f->next = NULL;
 363
 364   }
 365
 366   DddmpSetVisitedAdd (f);
 367
 368   return;
 369 }
 370
 371 /**Function********************************************************************
 372
 373   Synopsis     [Restores a node in unique table]
 374
 375   Description  [Restores a node in unique table (recursively)]
 376
 377   SideEffects  [Nodes are not restored in the same order as before removal]
 378
 379   SeeAlso      [RemoveFromUniqueAdd ()]
 380
 381 ******************************************************************************/
 382
 383 static void
 384 RestoreInUniqueRecurAdd (
 385   DdManager *ddMgr /*  IN: DD Manager */,
 386   DdNode *f        /*  IN: root of the BDD to be restored */
 387   )
 388 {
 389   DdNodePtr *nodelist;
 390   DdNode *T, *E, *looking;
 391   DdNodePtr *previousP;
 392   DdSubtable *subtable;
 393   int pos, level;
 394 #ifdef DDDMP_DEBUG
 395   DdNode *node;
 396   DdNode *sentinel = &(ddMgr->sentinel);
 397 #endif
 398
 399   f = Cudd_Regular(f);
 400
 401   if (!Cudd_IsComplement (f->next)) {
 402     return;
 403   }
 404
 405   if (cuddIsConstant (f)) {
 406     /* StQ 11.02.2004:
 407        Bug fixed --> restore NULL within the next field */
 408     /*DddmpClearVisitedAdd (f);*/
 409     f->next = NULL;
 410
 411     return;
 412   }
 413
 414   RestoreInUniqueRecurAdd (ddMgr, cuddT (f));
 415   RestoreInUniqueRecurAdd (ddMgr, cuddE (f));
 416
 417   level = ddMgr->perm[f->index];
 418   subtable = &(ddMgr->subtables[level]);
 419
 420   nodelist = subtable->nodelist;
 421
 422   pos = ddHash (cuddT (f), cuddE (f), subtable->shift);
 423
 424 #ifdef DDDMP_DEBUG
 425   /* verify uniqueness to avoid duplicate nodes in unique table */
 426   for (node=nodelist[pos]; node != sentinel; node=node->next)
 427     assert(node!=f);
 428 #endif
 429
 430   T = cuddT (f);
 431   E = cuddE (f);
 432   previousP = &(nodelist[pos]);
 433   looking = *previousP;
 434
 435   while (T < cuddT (looking)) {
 436     previousP = &(looking->next);
 437     looking = *previousP;
 438   }
 439
 440   while (T == cuddT (looking) && E < cuddE (looking)) {
 441     previousP = &(looking->next);
 442     looking = *previousP;
 443   }
 444
 445   f->next = *previousP;
 446   *previousP = f;
 447
 448   return;
 449 }
 450
 451