distr/cudd/cuddInteract.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddInteract.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions to manipulate the variable interaction matrix.]
   8
   9   Description [Internal procedures included in this file:
  10         <ul>
  11         <li> cuddSetInteract()
  12         <li> cuddTestInteract()
  13         <li> cuddInitInteract()
  14         </ul>
  15   Static procedures included in this file:
  16         <ul>
  17         <li> ddSuppInteract()
  18         <li> ddClearLocal()
  19         <li> ddUpdateInteract()
  20         <li> ddClearGlobal()
  21         </ul>
  22   The interaction matrix tells whether two variables are
  23   both in the support of some function of the DD. The main use of the
  24   interaction matrix is in the in-place swapping. Indeed, if two
  25   variables do not interact, there is no arc connecting the two layers;
  26   therefore, the swap can be performed in constant time, without
  27   scanning the subtables. Another use of the interaction matrix is in
  28   the computation of the lower bounds for sifting. Finally, the
  29   interaction matrix can be used to speed up aggregation checks in
  30   symmetric and group sifting.<p>
  31   The computation of the interaction matrix is done with a series of
  32   depth-first searches. The searches start from those nodes that have
  33   only external references. The matrix is stored as a packed array of bits;
  34   since it is symmetric, only the upper triangle is kept in memory.
  35   As a final remark, we note that there may be variables that do
  36   intercat, but that for a given variable order have no arc connecting
  37   their layers when they are adjacent.]
  38
  39   SeeAlso     []
  40
  41   Author      [Fabio Somenzi]
  42
  43   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  44
  45   All rights reserved.
  46
  47   Redistribution and use in source and binary forms, with or without
  48   modification, are permitted provided that the following conditions
  49   are met:
  50
  51   Redistributions of source code must retain the above copyright
  52   notice, this list of conditions and the following disclaimer.
  53
  54   Redistributions in binary form must reproduce the above copyright
  55   notice, this list of conditions and the following disclaimer in the
  56   documentation and/or other materials provided with the distribution.
  57
  58   Neither the name of the University of Colorado nor the names of its
  59   contributors may be used to endorse or promote products derived from
  60   this software without specific prior written permission.
  61
  62   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  63   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  64   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  65   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  66   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  67   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  68   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  69   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  70   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  71   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  72   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  73   POSSIBILITY OF SUCH DAMAGE.]
  74
  75 ******************************************************************************/
  76
  77 #include "util.h"
  78 #include "cuddInt.h"
  79
  80 /*---------------------------------------------------------------------------*/
  81 /* Constant declarations                                                     */
  82 /*---------------------------------------------------------------------------*/
  83
  84 #if SIZEOF_LONG == 8
  85 #define BPL 64
  86 #define LOGBPL 6
  87 #else
  88 #define BPL 32
  89 #define LOGBPL 5
  90 #endif
  91
  92 /*---------------------------------------------------------------------------*/
  93 /* Stucture declarations                                                     */
  94 /*---------------------------------------------------------------------------*/
  95
  96
  97 /*---------------------------------------------------------------------------*/
  98 /* Type declarations                                                         */
  99 /*---------------------------------------------------------------------------*/
 100
 101
 102 /*---------------------------------------------------------------------------*/
 103 /* Variable declarations                                                     */
 104 /*---------------------------------------------------------------------------*/
 105
 106 #ifndef lint
 107 static char rcsid[] DD_UNUSED = "$Id: cuddInteract.c,v 1.12 2004/08/13 18:04:49 fabio Exp $";
 108 #endif
 109
 110 /*---------------------------------------------------------------------------*/
 111 /* Macro declarations                                                        */
 112 /*---------------------------------------------------------------------------*/
 113
 114
 115 /**AutomaticStart*************************************************************/
 116
 117 /*---------------------------------------------------------------------------*/
 118 /* Static function prototypes                                                */
 119 /*---------------------------------------------------------------------------*/
 120
 121 static void ddSuppInteract (DdNode *f, int *support);
 122 static void ddClearLocal (DdNode *f);
 123 static void ddUpdateInteract (DdManager *table, int *support);
 124 static void ddClearGlobal (DdManager *table);
 125
 126 /**AutomaticEnd***************************************************************/
 127
 128
 129 /*---------------------------------------------------------------------------*/
 130 /* Definition of exported functions                                          */
 131 /*---------------------------------------------------------------------------*/
 132
 133
 134 /*---------------------------------------------------------------------------*/
 135 /* Definition of internal functions                                          */
 136 /*---------------------------------------------------------------------------*/
 137
 138
 139 /**Function********************************************************************
 140
 141   Synopsis    [Set interaction matrix entries.]
 142
 143   Description [Given a pair of variables 0 <= x < y < table->size,
 144   sets the corresponding bit of the interaction matrix to 1.]
 145
 146   SideEffects [None]
 147
 148   SeeAlso     []
 149
 150 ******************************************************************************/
 151 void
 152 cuddSetInteract(
 153   DdManager * table,
 154   int  x,
 155   int  y)
 156 {
 157     int posn, word, bit;
 158
 159 #ifdef DD_DEBUG
 160     assert(x < y);
 161     assert(y < table->size);
 162     assert(x >= 0);
 163 #endif
 164
 165     posn = ((((table->size << 1) - x - 3) * x) >> 1) + y - 1;
 166     word = posn >> LOGBPL;
 167     bit = posn & (BPL-1);
 168     table->interact[word] |= 1L << bit;
 169
 170 } /* end of cuddSetInteract */
 171
 172
 173 /**Function********************************************************************
 174
 175   Synopsis    [Test interaction matrix entries.]
 176
 177   Description [Given a pair of variables 0 <= x < y < table->size,
 178   tests whether the corresponding bit of the interaction matrix is 1.
 179   Returns the value of the bit.]
 180
 181   SideEffects [None]
 182
 183   SeeAlso     []
 184
 185 ******************************************************************************/
 186 int
 187 cuddTestInteract(
 188   DdManager * table,
 189   int  x,
 190   int  y)
 191 {
 192     int posn, word, bit, result;
 193
 194     if (x > y) {
 195         int tmp = x;
 196         x = y;
 197         y = tmp;
 198     }
 199 #ifdef DD_DEBUG
 200     assert(x < y);
 201     assert(y < table->size);
 202     assert(x >= 0);
 203 #endif
 204
 205     posn = ((((table->size << 1) - x - 3) * x) >> 1) + y - 1;
 206     word = posn >> LOGBPL;
 207     bit = posn & (BPL-1);
 208     result = (table->interact[word] >> bit) & 1L;
 209     return(result);
 210
 211 } /* end of cuddTestInteract */
 212
 213
 214 /**Function********************************************************************
 215
 216   Synopsis    [Initializes the interaction matrix.]
 217
 218   Description [Initializes the interaction matrix. The interaction
 219   matrix is implemented as a bit vector storing the upper triangle of
 220   the symmetric interaction matrix. The bit vector is kept in an array
 221   of long integers. The computation is based on a series of depth-first
 222   searches, one for each root of the DAG. Two flags are needed: The
 223   local visited flag uses the LSB of the then pointer. The global
 224   visited flag uses the LSB of the next pointer.
 225   Returns 1 if successful; 0 otherwise.]
 226
 227   SideEffects [None]
 228
 229   SeeAlso     []
 230
 231 ******************************************************************************/
 232 int
 233 cuddInitInteract(
 234   DdManager * table)
 235 {
 236     int i,j,k;
 237     int words;
 238     long *interact;
 239     int *support;
 240     DdNode *f;
 241     DdNode *sentinel = &(table->sentinel);
 242     DdNodePtr *nodelist;
 243     int slots;
 244     int n = table->size;
 245
 246     words = ((n * (n-1)) >> (1 + LOGBPL)) + 1;
 247     table->interact = interact = ALLOC(long,words);
 248     if (interact == NULL) {
 249         table->errorCode = CUDD_MEMORY_OUT;
 250         return(0);
 251     }
 252     for (i = 0; i < words; i++) {
 253         interact[i] = 0;
 254     }
 255
 256     support = ALLOC(int,n);
 257     if (support == NULL) {
 258         table->errorCode = CUDD_MEMORY_OUT;
 259         FREE(interact);
 260         return(0);
 261     }
 262
 263     for (i = 0; i < n; i++) {
 264         nodelist = table->subtables[i].nodelist;
 265         slots = table->subtables[i].slots;
 266         for (j = 0; j < slots; j++) {
 267             f = nodelist[j];
 268             while (f != sentinel) {
 269                 /* A node is a root of the DAG if it cannot be
 270                 ** reached by nodes above it. If a node was never
 271                 ** reached during the previous depth-first searches,
 272                 ** then it is a root, and we start a new depth-first
 273                 ** search from it.
 274                 */
 275                 if (!Cudd_IsComplement(f->next)) {
 276                     for (k = 0; k < n; k++) {
 277                         support[k] = 0;
 278                     }
 279                     ddSuppInteract(f,support);
 280                     ddClearLocal(f);
 281                     ddUpdateInteract(table,support);
 282                 }
 283                 f = Cudd_Regular(f->next);
 284             }
 285         }
 286     }
 287     ddClearGlobal(table);
 288
 289     FREE(support);
 290     return(1);
 291
 292 } /* end of cuddInitInteract */
 293
 294
 295 /*---------------------------------------------------------------------------*/
 296 /* Definition of static functions                                            */
 297 /*---------------------------------------------------------------------------*/
 298
 299
 300 /**Function********************************************************************
 301
 302   Synopsis    [Find the support of f.]
 303
 304   Description [Performs a DFS from f. Uses the LSB of the then pointer
 305   as visited flag.]
 306
 307   SideEffects [Accumulates in support the variables on which f depends.]
 308
 309   SeeAlso     []
 310
 311 ******************************************************************************/
 312 static void
 313 ddSuppInteract(
 314   DdNode * f,
 315   int * support)
 316 {
 317     if (cuddIsConstant(f) || Cudd_IsComplement(cuddT(f))) {
 318         return;
 319     }
 320
 321     support[f->index] = 1;
 322     ddSuppInteract(cuddT(f),support);
 323     ddSuppInteract(Cudd_Regular(cuddE(f)),support);
 324     /* mark as visited */
 325     cuddT(f) = Cudd_Complement(cuddT(f));
 326     f->next = Cudd_Complement(f->next);
 327     return;
 328
 329 } /* end of ddSuppInteract */
 330
 331
 332 /**Function********************************************************************
 333
 334   Synopsis    [Performs a DFS from f, clearing the LSB of the then pointers.]
 335
 336   Description []
 337
 338   SideEffects [None]
 339
 340   SeeAlso     []
 341
 342 ******************************************************************************/
 343 static void
 344 ddClearLocal(
 345   DdNode * f)
 346 {
 347     if (cuddIsConstant(f) || !Cudd_IsComplement(cuddT(f))) {
 348         return;
 349     }
 350     /* clear visited flag */
 351     cuddT(f) = Cudd_Regular(cuddT(f));
 352     ddClearLocal(cuddT(f));
 353     ddClearLocal(Cudd_Regular(cuddE(f)));
 354     return;
 355
 356 } /* end of ddClearLocal */
 357
 358
 359 /**Function********************************************************************
 360
 361   Synopsis [Marks as interacting all pairs of variables that appear in
 362   support.]
 363
 364   Description [If support[i] == support[j] == 1, sets the (i,j) entry
 365   of the interaction matrix to 1.]
 366
 367   SideEffects [None]
 368
 369   SeeAlso     []
 370
 371 ******************************************************************************/
 372 static void
 373 ddUpdateInteract(
 374   DdManager * table,
 375   int * support)
 376 {
 377     int i,j;
 378     int n = table->size;
 379
 380     for (i = 0; i < n-1; i++) {
 381         if (support[i] == 1) {
 382             for (j = i+1; j < n; j++) {
 383                 if (support[j] == 1) {
 384                     cuddSetInteract(table,i,j);
 385                 }
 386             }
 387         }
 388     }
 389
 390 } /* end of ddUpdateInteract */
 391
 392
 393 /**Function********************************************************************
 394
 395   Synopsis    [Scans the DD and clears the LSB of the next pointers.]
 396
 397   Description [The LSB of the next pointers are used as markers to tell
 398   whether a node was reached by at least one DFS. Once the interaction
 399   matrix is built, these flags are reset.]
 400
 401   SideEffects [None]
 402
 403   SeeAlso     []
 404
 405 ******************************************************************************/
 406 static void
 407 ddClearGlobal(
 408   DdManager * table)
 409 {
 410     int i,j;
 411     DdNode *f;
 412     DdNode *sentinel = &(table->sentinel);
 413     DdNodePtr *nodelist;
 414     int slots;
 415
 416     for (i = 0; i < table->size; i++) {
 417         nodelist = table->subtables[i].nodelist;
 418         slots = table->subtables[i].slots;
 419         for (j = 0; j < slots; j++) {
 420             f = nodelist[j];
 421             while (f != sentinel) {
 422                 f->next = Cudd_Regular(f->next);
 423                 f = f->next;
 424             }
 425         }
 426     }
 427
 428 } /* end of ddClearGlobal */
 429