distr/cudd/cuddLinear.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddLinear.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Functions for DD reduction by linear transformations.]
   8
   9   Description [ Internal procedures included in this module:
  10                 <ul>
  11                 <li> cuddLinearAndSifting()
  12                 <li> cuddLinearInPlace()
  13                 <li> cuddUpdateInteractionMatrix()
  14                 <li> cuddInitLinear()
  15                 <li> cuddResizeLinear()
  16                 </ul>
  17         Static procedures included in this module:
  18                 <ul>
  19                 <li> ddLinearUniqueCompare()
  20                 <li> ddLinearAndSiftingAux()
  21                 <li> ddLinearAndSiftingUp()
  22                 <li> ddLinearAndSiftingDown()
  23                 <li> ddLinearAndSiftingBackward()
  24                 <li> ddUndoMoves()
  25                 <li> cuddXorLinear()
  26                 </ul>]
  27
  28   Author      [Fabio Somenzi]
  29
  30   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  31
  32   All rights reserved.
  33
  34   Redistribution and use in source and binary forms, with or without
  35   modification, are permitted provided that the following conditions
  36   are met:
  37
  38   Redistributions of source code must retain the above copyright
  39   notice, this list of conditions and the following disclaimer.
  40
  41   Redistributions in binary form must reproduce the above copyright
  42   notice, this list of conditions and the following disclaimer in the
  43   documentation and/or other materials provided with the distribution.
  44
  45   Neither the name of the University of Colorado nor the names of its
  46   contributors may be used to endorse or promote products derived from
  47   this software without specific prior written permission.
  48
  49   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  50   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  51   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  52   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  53   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  54   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  55   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  56   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  57   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  58   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  59   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  60   POSSIBILITY OF SUCH DAMAGE.]
  61
  62 ******************************************************************************/
  63
  64 #include "util.h"
  65 #include "cuddInt.h"
  66
  67 /*---------------------------------------------------------------------------*/
  68 /* Constant declarations                                                     */
  69 /*---------------------------------------------------------------------------*/
  70
  71 #define CUDD_SWAP_MOVE 0
  72 #define CUDD_LINEAR_TRANSFORM_MOVE 1
  73 #define CUDD_INVERSE_TRANSFORM_MOVE 2
  74 #if SIZEOF_LONG == 8
  75 #define BPL 64
  76 #define LOGBPL 6
  77 #else
  78 #define BPL 32
  79 #define LOGBPL 5
  80 #endif
  81
  82 /*---------------------------------------------------------------------------*/
  83 /* Stucture declarations                                                     */
  84 /*---------------------------------------------------------------------------*/
  85
  86 /*---------------------------------------------------------------------------*/
  87 /* Type declarations                                                         */
  88 /*---------------------------------------------------------------------------*/
  89
  90 /*---------------------------------------------------------------------------*/
  91 /* Variable declarations                                                     */
  92 /*---------------------------------------------------------------------------*/
  93
  94 #ifndef lint
  95 static char rcsid[] DD_UNUSED = "$Id: cuddLinear.c,v 1.28 2009/02/19 16:21:03 fabio Exp $";
  96 #endif
  97
  98 static  int     *entry;
  99
 100 #ifdef DD_STATS
 101 extern  int     ddTotalNumberSwapping;
 102 extern  int     ddTotalNISwaps;
 103 static  int     ddTotalNumberLinearTr;
 104 #endif
 105
 106 #ifdef DD_DEBUG
 107 static  int     zero = 0;
 108 #endif
 109
 110 /*---------------------------------------------------------------------------*/
 111 /* Macro declarations                                                        */
 112 /*---------------------------------------------------------------------------*/
 113
 114 /**AutomaticStart*************************************************************/
 115
 116 /*---------------------------------------------------------------------------*/
 117 /* Static function prototypes                                                */
 118 /*---------------------------------------------------------------------------*/
 119
 120 static int ddLinearUniqueCompare (int *ptrX, int *ptrY);
 121 static int ddLinearAndSiftingAux (DdManager *table, int x, int xLow, int xHigh);
 122 static Move * ddLinearAndSiftingUp (DdManager *table, int y, int xLow, Move *prevMoves);
 123 static Move * ddLinearAndSiftingDown (DdManager *table, int x, int xHigh, Move *prevMoves);
 124 static int ddLinearAndSiftingBackward (DdManager *table, int size, Move *moves);
 125 static Move* ddUndoMoves (DdManager *table, Move *moves);
 126 static void cuddXorLinear (DdManager *table, int x, int y);
 127
 128 /**AutomaticEnd***************************************************************/
 129
 130
 131 /*---------------------------------------------------------------------------*/
 132 /* Definition of exported functions                                          */
 133 /*---------------------------------------------------------------------------*/
 134
 135
 136 /**Function********************************************************************
 137
 138   Synopsis    [Prints the linear transform matrix.]
 139
 140   Description [Prints the linear transform matrix. Returns 1 in case of
 141   success; 0 otherwise.]
 142
 143   SideEffects [none]
 144
 145   SeeAlso     []
 146
 147 ******************************************************************************/
 148 int
 149 Cudd_PrintLinear(
 150   DdManager * table)
 151 {
 152     int i,j,k;
 153     int retval;
 154     int nvars = table->linearSize;
 155     int wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
 156     long word;
 157
 158     for (i = 0; i < nvars; i++) {
 159         for (j = 0; j < wordsPerRow; j++) {
 160             word = table->linear[i*wordsPerRow + j];
 161             for (k = 0; k < BPL; k++) {
 162                 retval = fprintf(table->out,"%ld",word & 1);
 163                 if (retval == 0) return(0);
 164                 word >>= 1;
 165             }
 166         }
 167         retval = fprintf(table->out,"\n");
 168         if (retval == 0) return(0);
 169     }
 170     return(1);
 171
 172 } /* end of Cudd_PrintLinear */
 173
 174
 175 /**Function********************************************************************
 176
 177   Synopsis    [Reads an entry of the linear transform matrix.]
 178
 179   Description [Reads an entry of the linear transform matrix.]
 180
 181   SideEffects [none]
 182
 183   SeeAlso     []
 184
 185 ******************************************************************************/
 186 int
 187 Cudd_ReadLinear(
 188   DdManager * table /* CUDD manager */,
 189   int  x /* row index */,
 190   int  y /* column index */)
 191 {
 192     int nvars = table->size;
 193     int wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
 194     long word;
 195     int bit;
 196     int result;
 197
 198     assert(table->size == table->linearSize);
 199
 200     word = wordsPerRow * x + (y >> LOGBPL);
 201     bit  = y & (BPL-1);
 202     result = (int) ((table->linear[word] >> bit) & 1);
 203     return(result);
 204
 205 } /* end of Cudd_ReadLinear */
 206
 207
 208 /*---------------------------------------------------------------------------*/
 209 /* Definition of internal functions                                          */
 210 /*---------------------------------------------------------------------------*/
 211
 212
 213 /**Function********************************************************************
 214
 215   Synopsis    [BDD reduction based on combination of sifting and linear
 216   transformations.]
 217
 218   Description [BDD reduction based on combination of sifting and linear
 219   transformations.  Assumes that no dead nodes are present.
 220     <ol>
 221     <li> Order all the variables according to the number of entries
 222     in each unique table.
 223     <li> Sift the variable up and down, remembering each time the
 224     total size of the DD heap. At each position, linear transformation
 225     of the two adjacent variables is tried and is accepted if it reduces
 226     the size of the DD.
 227     <li> Select the best permutation.
 228     <li> Repeat 3 and 4 for all variables.
 229     </ol>
 230   Returns 1 if successful; 0 otherwise.]
 231
 232   SideEffects [None]
 233
 234 ******************************************************************************/
 235 int
 236 cuddLinearAndSifting(
 237   DdManager * table,
 238   int  lower,
 239   int  upper)
 240 {
 241     int         i;
 242     int         *var;
 243     int         size;
 244     int         x;
 245     int         result;
 246 #ifdef DD_STATS
 247     int         previousSize;
 248 #endif
 249
 250 #ifdef DD_STATS
 251     ddTotalNumberLinearTr = 0;
 252 #endif
 253
 254     size = table->size;
 255
 256     var = NULL;
 257     entry = NULL;
 258     if (table->linear == NULL) {
 259         result = cuddInitLinear(table);
 260         if (result == 0) goto cuddLinearAndSiftingOutOfMem;
 261 #if 0
 262         (void) fprintf(table->out,"\n");
 263         result = Cudd_PrintLinear(table);
 264         if (result == 0) goto cuddLinearAndSiftingOutOfMem;
 265 #endif
 266     } else if (table->size != table->linearSize) {
 267         result = cuddResizeLinear(table);
 268         if (result == 0) goto cuddLinearAndSiftingOutOfMem;
 269 #if 0
 270         (void) fprintf(table->out,"\n");
 271         result = Cudd_PrintLinear(table);
 272         if (result == 0) goto cuddLinearAndSiftingOutOfMem;
 273 #endif
 274     }
 275
 276     /* Find order in which to sift variables. */
 277     entry = ALLOC(int,size);
 278     if (entry == NULL) {
 279         table->errorCode = CUDD_MEMORY_OUT;
 280         goto cuddLinearAndSiftingOutOfMem;
 281     }
 282     var = ALLOC(int,size);
 283     if (var == NULL) {
 284         table->errorCode = CUDD_MEMORY_OUT;
 285         goto cuddLinearAndSiftingOutOfMem;
 286     }
 287
 288     for (i = 0; i < size; i++) {
 289         x = table->perm[i];
 290         entry[i] = table->subtables[x].keys;
 291         var[i] = i;
 292     }
 293
 294     qsort((void *)var,size,sizeof(int),(DD_QSFP)ddLinearUniqueCompare);
 295
 296     /* Now sift. */
 297     for (i = 0; i < ddMin(table->siftMaxVar,size); i++) {
 298         x = table->perm[var[i]];
 299         if (x < lower || x > upper) continue;
 300 #ifdef DD_STATS
 301         previousSize = table->keys - table->isolated;
 302 #endif
 303         result = ddLinearAndSiftingAux(table,x,lower,upper);
 304         if (!result) goto cuddLinearAndSiftingOutOfMem;
 305 #ifdef DD_STATS
 306         if (table->keys < (unsigned) previousSize + table->isolated) {
 307             (void) fprintf(table->out,"-");
 308         } else if (table->keys > (unsigned) previousSize + table->isolated) {
 309             (void) fprintf(table->out,"+");     /* should never happen */
 310             (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keys - table->isolated, var[i]);
 311         } else {
 312             (void) fprintf(table->out,"=");
 313         }
 314         fflush(table->out);
 315 #endif
 316 #ifdef DD_DEBUG
 317         (void) Cudd_DebugCheck(table);
 318 #endif
 319     }
 320
 321     FREE(var);
 322     FREE(entry);
 323
 324 #ifdef DD_STATS
 325     (void) fprintf(table->out,"\n#:L_LINSIFT %8d: linear trans.",
 326                    ddTotalNumberLinearTr);
 327 #endif
 328
 329     return(1);
 330
 331 cuddLinearAndSiftingOutOfMem:
 332
 333     if (entry != NULL) FREE(entry);
 334     if (var != NULL) FREE(var);
 335
 336     return(0);
 337
 338 } /* end of cuddLinearAndSifting */
 339
 340
 341 /**Function********************************************************************
 342
 343   Synopsis    [Linearly combines two adjacent variables.]
 344
 345   Description [Linearly combines two adjacent variables. Specifically,
 346   replaces the top variable with the exclusive nor of the two variables.
 347   It assumes that no dead nodes are present on entry to this
 348   procedure.  The procedure then guarantees that no dead nodes will be
 349   present when it terminates.  cuddLinearInPlace assumes that x &lt;
 350   y.  Returns the number of keys in the table if successful; 0
 351   otherwise.]
 352
 353   SideEffects [The two subtables corrresponding to variables x and y are
 354   modified. The global counters of the unique table are also affected.]
 355
 356   SeeAlso     [cuddSwapInPlace]
 357
 358 ******************************************************************************/
 359 int
 360 cuddLinearInPlace(
 361   DdManager * table,
 362   int  x,
 363   int  y)
 364 {
 365     DdNodePtr *xlist, *ylist;
 366     int    xindex, yindex;
 367     int    xslots, yslots;
 368     int    xshift, yshift;
 369     int    oldxkeys, oldykeys;
 370     int    newxkeys, newykeys;
 371     int    comple, newcomplement;
 372     int    i;
 373     int    posn;
 374     int    isolated;
 375     DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0;
 376     DdNode *g,*next,*last;
 377     DdNodePtr *previousP;
 378     DdNode *tmp;
 379     DdNode *sentinel = &(table->sentinel);
 380 #ifdef DD_DEBUG
 381     int    count, idcheck;
 382 #endif
 383
 384 #ifdef DD_DEBUG
 385     assert(x < y);
 386     assert(cuddNextHigh(table,x) == y);
 387     assert(table->subtables[x].keys != 0);
 388     assert(table->subtables[y].keys != 0);
 389     assert(table->subtables[x].dead == 0);
 390     assert(table->subtables[y].dead == 0);
 391 #endif
 392
 393     xindex = table->invperm[x];
 394     yindex = table->invperm[y];
 395
 396     if (cuddTestInteract(table,xindex,yindex)) {
 397 #ifdef DD_STATS
 398         ddTotalNumberLinearTr++;
 399 #endif
 400         /* Get parameters of x subtable. */
 401         xlist = table->subtables[x].nodelist;
 402         oldxkeys = table->subtables[x].keys;
 403         xslots = table->subtables[x].slots;
 404         xshift = table->subtables[x].shift;
 405
 406         /* Get parameters of y subtable. */
 407         ylist = table->subtables[y].nodelist;
 408         oldykeys = table->subtables[y].keys;
 409         yslots = table->subtables[y].slots;
 410         yshift = table->subtables[y].shift;
 411
 412         newxkeys = 0;
 413         newykeys = oldykeys;
 414
 415         /* Check whether the two projection functions involved in this
 416         ** swap are isolated. At the end, we'll be able to tell how many
 417         ** isolated projection functions are there by checking only these
 418         ** two functions again. This is done to eliminate the isolated
 419         ** projection functions from the node count.
 420         */
 421         isolated = - ((table->vars[xindex]->ref == 1) +
 422                      (table->vars[yindex]->ref == 1));
 423
 424         /* The nodes in the x layer are put in a chain.
 425         ** The chain is handled as a FIFO; g points to the beginning and
 426         ** last points to the end.
 427         */
 428         g = NULL;
 429 #ifdef DD_DEBUG
 430         last = NULL;
 431 #endif
 432         for (i = 0; i < xslots; i++) {
 433             f = xlist[i];
 434             if (f == sentinel) continue;
 435             xlist[i] = sentinel;
 436             if (g == NULL) {
 437                 g = f;
 438             } else {
 439                 last->next = f;
 440             }
 441             while ((next = f->next) != sentinel) {
 442                 f = next;
 443             } /* while there are elements in the collision chain */
 444             last = f;
 445         } /* for each slot of the x subtable */
 446 #ifdef DD_DEBUG
 447         /* last is always assigned in the for loop because there is at
 448         ** least one key */
 449         assert(last != NULL);
 450 #endif
 451         last->next = NULL;
 452
 453 #ifdef DD_COUNT
 454         table->swapSteps += oldxkeys;
 455 #endif
 456         /* Take care of the x nodes that must be re-expressed.
 457         ** They form a linked list pointed by g.
 458         */
 459         f = g;
 460         while (f != NULL) {
 461             next = f->next;
 462             /* Find f1, f0, f11, f10, f01, f00. */
 463             f1 = cuddT(f);
 464 #ifdef DD_DEBUG
 465             assert(!(Cudd_IsComplement(f1)));
 466 #endif
 467             if ((int) f1->index == yindex) {
 468                 f11 = cuddT(f1); f10 = cuddE(f1);
 469             } else {
 470                 f11 = f10 = f1;
 471             }
 472 #ifdef DD_DEBUG
 473             assert(!(Cudd_IsComplement(f11)));
 474 #endif
 475             f0 = cuddE(f);
 476             comple = Cudd_IsComplement(f0);
 477             f0 = Cudd_Regular(f0);
 478             if ((int) f0->index == yindex) {
 479                 f01 = cuddT(f0); f00 = cuddE(f0);
 480             } else {
 481                 f01 = f00 = f0;
 482             }
 483             if (comple) {
 484                 f01 = Cudd_Not(f01);
 485                 f00 = Cudd_Not(f00);
 486             }
 487             /* Decrease ref count of f1. */
 488             cuddSatDec(f1->ref);
 489             /* Create the new T child. */
 490             if (f11 == f00) {
 491                 newf1 = f11;
 492                 cuddSatInc(newf1->ref);
 493             } else {
 494                 /* Check ylist for triple (yindex,f11,f00). */
 495                 posn = ddHash(f11, f00, yshift);
 496                 /* For each element newf1 in collision list ylist[posn]. */
 497                 previousP = &(ylist[posn]);
 498                 newf1 = *previousP;
 499                 while (f11 < cuddT(newf1)) {
 500                     previousP = &(newf1->next);
 501                     newf1 = *previousP;
 502                 }
 503                 while (f11 == cuddT(newf1) && f00 < cuddE(newf1)) {
 504                     previousP = &(newf1->next);
 505                     newf1 = *previousP;
 506                 }
 507                 if (cuddT(newf1) == f11 && cuddE(newf1) == f00) {
 508                     cuddSatInc(newf1->ref);
 509                 } else { /* no match */
 510                     newf1 = cuddDynamicAllocNode(table);
 511                     if (newf1 == NULL)
 512                         goto cuddLinearOutOfMem;
 513                     newf1->index = yindex; newf1->ref = 1;
 514                     cuddT(newf1) = f11;
 515                     cuddE(newf1) = f00;
 516                     /* Insert newf1 in the collision list ylist[posn];
 517                     ** increase the ref counts of f11 and f00.
 518                     */
 519                     newykeys++;
 520                     newf1->next = *previousP;
 521                     *previousP = newf1;
 522                     cuddSatInc(f11->ref);
 523                     tmp = Cudd_Regular(f00);
 524                     cuddSatInc(tmp->ref);
 525                 }
 526             }
 527             cuddT(f) = newf1;
 528 #ifdef DD_DEBUG
 529             assert(!(Cudd_IsComplement(newf1)));
 530 #endif
 531
 532             /* Do the same for f0, keeping complement dots into account. */
 533             /* decrease ref count of f0 */
 534             tmp = Cudd_Regular(f0);
 535             cuddSatDec(tmp->ref);
 536             /* create the new E child */
 537             if (f01 == f10) {
 538                 newf0 = f01;
 539                 tmp = Cudd_Regular(newf0);
 540                 cuddSatInc(tmp->ref);
 541             } else {
 542                 /* make sure f01 is regular */
 543                 newcomplement = Cudd_IsComplement(f01);
 544                 if (newcomplement) {
 545                     f01 = Cudd_Not(f01);
 546                     f10 = Cudd_Not(f10);
 547                 }
 548                 /* Check ylist for triple (yindex,f01,f10). */
 549                 posn = ddHash(f01, f10, yshift);
 550                 /* For each element newf0 in collision list ylist[posn]. */
 551                 previousP = &(ylist[posn]);
 552                 newf0 = *previousP;
 553                 while (f01 < cuddT(newf0)) {
 554                     previousP = &(newf0->next);
 555                     newf0 = *previousP;
 556                 }
 557                 while (f01 == cuddT(newf0) && f10 < cuddE(newf0)) {
 558                     previousP = &(newf0->next);
 559                     newf0 = *previousP;
 560                 }
 561                 if (cuddT(newf0) == f01 && cuddE(newf0) == f10) {
 562                     cuddSatInc(newf0->ref);
 563                 } else { /* no match */
 564                     newf0 = cuddDynamicAllocNode(table);
 565                     if (newf0 == NULL)
 566                         goto cuddLinearOutOfMem;
 567                     newf0->index = yindex; newf0->ref = 1;
 568                     cuddT(newf0) = f01;
 569                     cuddE(newf0) = f10;
 570                     /* Insert newf0 in the collision list ylist[posn];
 571                     ** increase the ref counts of f01 and f10.
 572                     */
 573                     newykeys++;
 574                     newf0->next = *previousP;
 575                     *previousP = newf0;
 576                     cuddSatInc(f01->ref);
 577                     tmp = Cudd_Regular(f10);
 578                     cuddSatInc(tmp->ref);
 579                 }
 580                 if (newcomplement) {
 581                     newf0 = Cudd_Not(newf0);
 582                 }
 583             }
 584             cuddE(f) = newf0;
 585
 586             /* Re-insert the modified f in xlist.
 587             ** The modified f does not already exists in xlist.
 588             ** (Because of the uniqueness of the cofactors.)
 589             */
 590             posn = ddHash(newf1, newf0, xshift);
 591             newxkeys++;
 592             previousP = &(xlist[posn]);
 593             tmp = *previousP;
 594             while (newf1 < cuddT(tmp)) {
 595                 previousP = &(tmp->next);
 596                 tmp = *previousP;
 597             }
 598             while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) {
 599                 previousP = &(tmp->next);
 600                 tmp = *previousP;
 601             }
 602             f->next = *previousP;
 603             *previousP = f;
 604             f = next;
 605         } /* while f != NULL */
 606
 607         /* GC the y layer. */
 608
 609         /* For each node f in ylist. */
 610         for (i = 0; i < yslots; i++) {
 611             previousP = &(ylist[i]);
 612             f = *previousP;
 613             while (f != sentinel) {
 614                 next = f->next;
 615                 if (f->ref == 0) {
 616                     tmp = cuddT(f);
 617                     cuddSatDec(tmp->ref);
 618                     tmp = Cudd_Regular(cuddE(f));
 619                     cuddSatDec(tmp->ref);
 620                     cuddDeallocNode(table,f);
 621                     newykeys--;
 622                 } else {
 623                     *previousP = f;
 624                     previousP = &(f->next);
 625                 }
 626                 f = next;
 627             } /* while f */
 628             *previousP = sentinel;
 629         } /* for every collision list */
 630
 631 #ifdef DD_DEBUG
 632 #if 0
 633         (void) fprintf(table->out,"Linearly combining %d and %d\n",x,y);
 634 #endif
 635         count = 0;
 636         idcheck = 0;
 637         for (i = 0; i < yslots; i++) {
 638             f = ylist[i];
 639             while (f != sentinel) {
 640                 count++;
 641                 if (f->index != (DdHalfWord) yindex)
 642                     idcheck++;
 643                 f = f->next;
 644             }
 645         }
 646         if (count != newykeys) {
 647             fprintf(table->err,"Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n",oldykeys,newykeys,count);
 648         }
 649         if (idcheck != 0)
 650             fprintf(table->err,"Error in id's of ylist\twrong id's = %d\n",idcheck);
 651         count = 0;
 652         idcheck = 0;
 653         for (i = 0; i < xslots; i++) {
 654             f = xlist[i];
 655             while (f != sentinel) {
 656                 count++;
 657                 if (f->index != (DdHalfWord) xindex)
 658                     idcheck++;
 659                 f = f->next;
 660             }
 661         }
 662         if (count != newxkeys || newxkeys != oldxkeys) {
 663             fprintf(table->err,"Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n",oldxkeys,newxkeys,count);
 664         }
 665         if (idcheck != 0)
 666             fprintf(table->err,"Error in id's of xlist\twrong id's = %d\n",idcheck);
 667 #endif
 668
 669         isolated += (table->vars[xindex]->ref == 1) +
 670                     (table->vars[yindex]->ref == 1);
 671         table->isolated += isolated;
 672
 673         /* Set the appropriate fields in table. */
 674         table->subtables[y].keys = newykeys;
 675
 676         /* Here we should update the linear combination table
 677         ** to record that x <- x EXNOR y. This is done by complementing
 678         ** the (x,y) entry of the table.
 679         */
 680
 681         table->keys += newykeys - oldykeys;
 682
 683         cuddXorLinear(table,xindex,yindex);
 684     }
 685
 686 #ifdef DD_DEBUG
 687     if (zero) {
 688         (void) Cudd_DebugCheck(table);
 689     }
 690 #endif
 691
 692     return(table->keys - table->isolated);
 693
 694 cuddLinearOutOfMem:
 695     (void) fprintf(table->err,"Error: cuddLinearInPlace out of memory\n");
 696
 697     return (0);
 698
 699 } /* end of cuddLinearInPlace */
 700
 701
 702 /**Function********************************************************************
 703
 704   Synopsis    [Updates the interaction matrix.]
 705
 706   Description []
 707
 708   SideEffects [none]
 709
 710   SeeAlso     []
 711
 712 ******************************************************************************/
 713 void
 714 cuddUpdateInteractionMatrix(
 715   DdManager * table,
 716   int  xindex,
 717   int  yindex)
 718 {
 719     int i;
 720     for (i = 0; i < yindex; i++) {
 721         if (i != xindex && cuddTestInteract(table,i,yindex)) {
 722             if (i < xindex) {
 723                 cuddSetInteract(table,i,xindex);
 724             } else {
 725                 cuddSetInteract(table,xindex,i);
 726             }
 727         }
 728     }
 729     for (i = yindex+1; i < table->size; i++) {
 730         if (i != xindex && cuddTestInteract(table,yindex,i)) {
 731             if (i < xindex) {
 732                 cuddSetInteract(table,i,xindex);
 733             } else {
 734                 cuddSetInteract(table,xindex,i);
 735             }
 736         }
 737     }
 738
 739 } /* end of cuddUpdateInteractionMatrix */
 740
 741
 742 /**Function********************************************************************
 743
 744   Synopsis    [Initializes the linear transform matrix.]
 745
 746   Description [Initializes the linear transform matrix.  Returns 1 if
 747   successful; 0 otherwise.]
 748
 749   SideEffects [none]
 750
 751   SeeAlso     []
 752
 753 ******************************************************************************/
 754 int
 755 cuddInitLinear(
 756   DdManager * table)
 757 {
 758     int words;
 759     int wordsPerRow;
 760     int nvars;
 761     int word;
 762     int bit;
 763     int i;
 764     long *linear;
 765
 766     nvars = table->size;
 767     wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
 768     words = wordsPerRow * nvars;
 769     table->linear = linear = ALLOC(long,words);
 770     if (linear == NULL) {
 771         table->errorCode = CUDD_MEMORY_OUT;
 772         return(0);
 773     }
 774     table->memused += words * sizeof(long);
 775     table->linearSize = nvars;
 776     for (i = 0; i < words; i++) linear[i] = 0;
 777     for (i = 0; i < nvars; i++) {
 778         word = wordsPerRow * i + (i >> LOGBPL);
 779         bit  = i & (BPL-1);
 780         linear[word] = 1 << bit;
 781     }
 782     return(1);
 783
 784 } /* end of cuddInitLinear */
 785
 786
 787 /**Function********************************************************************
 788
 789   Synopsis    [Resizes the linear transform matrix.]
 790
 791   Description [Resizes the linear transform matrix.  Returns 1 if
 792   successful; 0 otherwise.]
 793
 794   SideEffects [none]
 795
 796   SeeAlso     []
 797
 798 ******************************************************************************/
 799 int
 800 cuddResizeLinear(
 801   DdManager * table)
 802 {
 803     int words,oldWords;
 804     int wordsPerRow,oldWordsPerRow;
 805     int nvars,oldNvars;
 806     int word,oldWord;
 807     int bit;
 808     int i,j;
 809     long *linear,*oldLinear;
 810
 811     oldNvars = table->linearSize;
 812     oldWordsPerRow = ((oldNvars - 1) >> LOGBPL) + 1;
 813     oldWords = oldWordsPerRow * oldNvars;
 814     oldLinear = table->linear;
 815
 816     nvars = table->size;
 817     wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
 818     words = wordsPerRow * nvars;
 819     table->linear = linear = ALLOC(long,words);
 820     if (linear == NULL) {
 821         table->errorCode = CUDD_MEMORY_OUT;
 822         return(0);
 823     }
 824     table->memused += (words - oldWords) * sizeof(long);
 825     for (i = 0; i < words; i++) linear[i] = 0;
 826
 827     /* Copy old matrix. */
 828     for (i = 0; i < oldNvars; i++) {
 829         for (j = 0; j < oldWordsPerRow; j++) {
 830             oldWord = oldWordsPerRow * i + j;
 831             word = wordsPerRow * i + j;
 832             linear[word] = oldLinear[oldWord];
 833         }
 834     }
 835     FREE(oldLinear);
 836
 837     /* Add elements to the diagonal. */
 838     for (i = oldNvars; i < nvars; i++) {
 839         word = wordsPerRow * i + (i >> LOGBPL);
 840         bit  = i & (BPL-1);
 841         linear[word] = 1 << bit;
 842     }
 843     table->linearSize = nvars;
 844
 845     return(1);
 846
 847 } /* end of cuddResizeLinear */
 848
 849
 850 /*---------------------------------------------------------------------------*/
 851 /* Definition of static functions                                            */
 852 /*---------------------------------------------------------------------------*/
 853
 854
 855 /**Function********************************************************************
 856
 857   Synopsis    [Comparison function used by qsort.]
 858
 859   Description [Comparison function used by qsort to order the
 860   variables according to the number of keys in the subtables.
 861   Returns the difference in number of keys between the two
 862   variables being compared.]
 863
 864   SideEffects [None]
 865
 866 ******************************************************************************/
 867 static int
 868 ddLinearUniqueCompare(
 869   int * ptrX,
 870   int * ptrY)
 871 {
 872 #if 0
 873     if (entry[*ptrY] == entry[*ptrX]) {
 874         return((*ptrX) - (*ptrY));
 875     }
 876 #endif
 877     return(entry[*ptrY] - entry[*ptrX]);
 878
 879 } /* end of ddLinearUniqueCompare */
 880
 881
 882 /**Function********************************************************************
 883
 884   Synopsis    [Given xLow <= x <= xHigh moves x up and down between the
 885   boundaries.]
 886
 887   Description [Given xLow <= x <= xHigh moves x up and down between the
 888   boundaries. At each step a linear transformation is tried, and, if it
 889   decreases the size of the DD, it is accepted. Finds the best position
 890   and does the required changes.  Returns 1 if successful; 0 otherwise.]
 891
 892   SideEffects [None]
 893
 894 ******************************************************************************/
 895 static int
 896 ddLinearAndSiftingAux(
 897   DdManager * table,
 898   int  x,
 899   int  xLow,
 900   int  xHigh)
 901 {
 902
 903     Move        *move;
 904     Move        *moveUp;                /* list of up moves */
 905     Move        *moveDown;              /* list of down moves */
 906     int         initialSize;
 907     int         result;
 908
 909     initialSize = table->keys - table->isolated;
 910
 911     moveDown = NULL;
 912     moveUp = NULL;
 913
 914     if (x == xLow) {
 915         moveDown = ddLinearAndSiftingDown(table,x,xHigh,NULL);
 916         /* At this point x --> xHigh unless bounding occurred. */
 917         if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
 918         /* Move backward and stop at best position. */
 919         result = ddLinearAndSiftingBackward(table,initialSize,moveDown);
 920         if (!result) goto ddLinearAndSiftingAuxOutOfMem;
 921
 922     } else if (x == xHigh) {
 923         moveUp = ddLinearAndSiftingUp(table,x,xLow,NULL);
 924         /* At this point x --> xLow unless bounding occurred. */
 925         if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
 926         /* Move backward and stop at best position. */
 927         result = ddLinearAndSiftingBackward(table,initialSize,moveUp);
 928         if (!result) goto ddLinearAndSiftingAuxOutOfMem;
 929
 930     } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
 931         moveDown = ddLinearAndSiftingDown(table,x,xHigh,NULL);
 932         /* At this point x --> xHigh unless bounding occurred. */
 933         if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
 934         moveUp = ddUndoMoves(table,moveDown);
 935 #ifdef DD_DEBUG
 936         assert(moveUp == NULL || moveUp->x == x);
 937 #endif
 938         moveUp = ddLinearAndSiftingUp(table,x,xLow,moveUp);
 939         if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
 940         /* Move backward and stop at best position. */
 941         result = ddLinearAndSiftingBackward(table,initialSize,moveUp);
 942         if (!result) goto ddLinearAndSiftingAuxOutOfMem;
 943
 944     } else { /* must go up first: shorter */
 945         moveUp = ddLinearAndSiftingUp(table,x,xLow,NULL);
 946         /* At this point x --> xLow unless bounding occurred. */
 947         if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
 948         moveDown = ddUndoMoves(table,moveUp);
 949 #ifdef DD_DEBUG
 950         assert(moveDown == NULL || moveDown->y == x);
 951 #endif
 952         moveDown = ddLinearAndSiftingDown(table,x,xHigh,moveDown);
 953         if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
 954         /* Move backward and stop at best position. */
 955         result = ddLinearAndSiftingBackward(table,initialSize,moveDown);
 956         if (!result) goto ddLinearAndSiftingAuxOutOfMem;
 957     }
 958
 959     while (moveDown != NULL) {
 960         move = moveDown->next;
 961         cuddDeallocMove(table, moveDown);
 962         moveDown = move;
 963     }
 964     while (moveUp != NULL) {
 965         move = moveUp->next;
 966         cuddDeallocMove(table, moveUp);
 967         moveUp = move;
 968     }
 969
 970     return(1);
 971
 972 ddLinearAndSiftingAuxOutOfMem:
 973     while (moveDown != NULL) {
 974         move = moveDown->next;
 975         cuddDeallocMove(table, moveDown);
 976         moveDown = move;
 977     }
 978     while (moveUp != NULL) {
 979         move = moveUp->next;
 980         cuddDeallocMove(table, moveUp);
 981         moveUp = move;
 982     }
 983
 984     return(0);
 985
 986 } /* end of ddLinearAndSiftingAux */
 987
 988
 989 /**Function********************************************************************
 990
 991   Synopsis    [Sifts a variable up and applies linear transformations.]
 992
 993   Description [Sifts a variable up and applies linear transformations.
 994   Moves y up until either it reaches the bound (xLow) or the size of
 995   the DD heap increases too much.  Returns the set of moves in case of
 996   success; NULL if memory is full.]
 997
 998   SideEffects [None]
 999
1000 ******************************************************************************/
1001 static Move *
1002 ddLinearAndSiftingUp(
1003   DdManager * table,
1004   int  y,
1005   int  xLow,
1006   Move * prevMoves)
1007 {
1008     Move        *moves;
1009     Move        *move;
1010     int         x;
1011     int         size, newsize;
1012     int         limitSize;
1013     int         xindex, yindex;
1014     int         isolated;
1015     int         L;      /* lower bound on DD size */
1016 #ifdef DD_DEBUG
1017     int checkL;
1018     int z;
1019     int zindex;
1020 #endif
1021
1022     moves = prevMoves;
1023     yindex = table->invperm[y];
1024
1025     /* Initialize the lower bound.
1026     ** The part of the DD below y will not change.
1027     ** The part of the DD above y that does not interact with y will not
1028     ** change. The rest may vanish in the best case, except for
1029     ** the nodes at level xLow, which will not vanish, regardless.
1030     */
1031     limitSize = L = table->keys - table->isolated;
1032     for (x = xLow + 1; x < y; x++) {
1033         xindex = table->invperm[x];
1034         if (cuddTestInteract(table,xindex,yindex)) {
1035             isolated = table->vars[xindex]->ref == 1;
1036             L -= table->subtables[x].keys - isolated;
1037         }
1038     }
1039     isolated = table->vars[yindex]->ref == 1;
1040     L -= table->subtables[y].keys - isolated;
1041
1042     x = cuddNextLow(table,y);
1043     while (x >= xLow && L <= limitSize) {
1044         xindex = table->invperm[x];
1045 #ifdef DD_DEBUG
1046         checkL = table->keys - table->isolated;
1047         for (z = xLow + 1; z < y; z++) {
1048             zindex = table->invperm[z];
1049             if (cuddTestInteract(table,zindex,yindex)) {
1050                 isolated = table->vars[zindex]->ref == 1;
1051                 checkL -= table->subtables[z].keys - isolated;
1052             }
1053         }
1054         isolated = table->vars[yindex]->ref == 1;
1055         checkL -= table->subtables[y].keys - isolated;
1056         if (L != checkL) {
1057             (void) fprintf(table->out, "checkL(%d) != L(%d)\n",checkL,L);
1058         }
1059 #endif
1060         size = cuddSwapInPlace(table,x,y);
1061         if (size == 0) goto ddLinearAndSiftingUpOutOfMem;
1062         newsize = cuddLinearInPlace(table,x,y);
1063         if (newsize == 0) goto ddLinearAndSiftingUpOutOfMem;
1064         move = (Move *) cuddDynamicAllocNode(table);
1065         if (move == NULL) goto ddLinearAndSiftingUpOutOfMem;
1066         move->x = x;
1067         move->y = y;
1068         move->next = moves;
1069         moves = move;
1070         move->flags = CUDD_SWAP_MOVE;
1071         if (newsize >= size) {
1072             /* Undo transformation. The transformation we apply is
1073             ** its own inverse. Hence, we just apply the transformation
1074             ** again.
1075             */
1076             newsize = cuddLinearInPlace(table,x,y);
1077             if (newsize == 0) goto ddLinearAndSiftingUpOutOfMem;
1078 #ifdef DD_DEBUG
1079             if (newsize != size) {
1080                 (void) fprintf(table->out,"Change in size after identity transformation! From %d to %d\n",size,newsize);
1081             }
1082 #endif
1083         } else if (cuddTestInteract(table,xindex,yindex)) {
1084             size = newsize;
1085             move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
1086             cuddUpdateInteractionMatrix(table,xindex,yindex);
1087         }
1088         move->size = size;
1089         /* Update the lower bound. */
1090         if (cuddTestInteract(table,xindex,yindex)) {
1091             isolated = table->vars[xindex]->ref == 1;
1092             L += table->subtables[y].keys - isolated;
1093         }
1094         if ((double) size > (double) limitSize * table->maxGrowth) break;
1095         if (size < limitSize) limitSize = size;
1096         y = x;
1097         x = cuddNextLow(table,y);
1098     }
1099     return(moves);
1100
1101 ddLinearAndSiftingUpOutOfMem:
1102     while (moves != NULL) {
1103         move = moves->next;
1104         cuddDeallocMove(table, moves);
1105         moves = move;
1106     }
1107     return((Move *) CUDD_OUT_OF_MEM);
1108
1109 } /* end of ddLinearAndSiftingUp */
1110
1111
1112 /**Function********************************************************************
1113
1114   Synopsis    [Sifts a variable down and applies linear transformations.]
1115
1116   Description [Sifts a variable down and applies linear
1117   transformations. Moves x down until either it reaches the bound
1118   (xHigh) or the size of the DD heap increases too much. Returns the
1119   set of moves in case of success; NULL if memory is full.]
1120
1121   SideEffects [None]
1122
1123 ******************************************************************************/
1124 static Move *
1125 ddLinearAndSiftingDown(
1126   DdManager * table,
1127   int  x,
1128   int  xHigh,
1129   Move * prevMoves)
1130 {
1131     Move        *moves;
1132     Move        *move;
1133     int         y;
1134     int         size, newsize;
1135     int         R;      /* upper bound on node decrease */
1136     int         limitSize;
1137     int         xindex, yindex;
1138     int         isolated;
1139 #ifdef DD_DEBUG
1140     int         checkR;
1141     int         z;
1142     int         zindex;
1143 #endif
1144
1145     moves = prevMoves;
1146     /* Initialize R */
1147     xindex = table->invperm[x];
1148     limitSize = size = table->keys - table->isolated;
1149     R = 0;
1150     for (y = xHigh; y > x; y--) {
1151         yindex = table->invperm[y];
1152         if (cuddTestInteract(table,xindex,yindex)) {
1153             isolated = table->vars[yindex]->ref == 1;
1154             R += table->subtables[y].keys - isolated;
1155         }
1156     }
1157
1158     y = cuddNextHigh(table,x);
1159     while (y <= xHigh && size - R < limitSize) {
1160 #ifdef DD_DEBUG
1161         checkR = 0;
1162         for (z = xHigh; z > x; z--) {
1163             zindex = table->invperm[z];
1164             if (cuddTestInteract(table,xindex,zindex)) {
1165                 isolated = table->vars[zindex]->ref == 1;
1166                 checkR += table->subtables[z].keys - isolated;
1167             }
1168         }
1169         if (R != checkR) {
1170             (void) fprintf(table->out, "checkR(%d) != R(%d)\n",checkR,R);
1171         }
1172 #endif
1173         /* Update upper bound on node decrease. */
1174         yindex = table->invperm[y];
1175         if (cuddTestInteract(table,xindex,yindex)) {
1176             isolated = table->vars[yindex]->ref == 1;
1177             R -= table->subtables[y].keys - isolated;
1178         }
1179         size = cuddSwapInPlace(table,x,y);
1180         if (size == 0) goto ddLinearAndSiftingDownOutOfMem;
1181         newsize = cuddLinearInPlace(table,x,y);
1182         if (newsize == 0) goto ddLinearAndSiftingDownOutOfMem;
1183         move = (Move *) cuddDynamicAllocNode(table);
1184         if (move == NULL) goto ddLinearAndSiftingDownOutOfMem;
1185         move->x = x;
1186         move->y = y;
1187         move->next = moves;
1188         moves = move;
1189         move->flags = CUDD_SWAP_MOVE;
1190         if (newsize >= size) {
1191             /* Undo transformation. The transformation we apply is
1192             ** its own inverse. Hence, we just apply the transformation
1193             ** again.
1194             */
1195             newsize = cuddLinearInPlace(table,x,y);
1196             if (newsize == 0) goto ddLinearAndSiftingDownOutOfMem;
1197             if (newsize != size) {
1198                 (void) fprintf(table->out,"Change in size after identity transformation! From %d to %d\n",size,newsize);
1199             }
1200         } else if (cuddTestInteract(table,xindex,yindex)) {
1201             size = newsize;
1202             move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
1203             cuddUpdateInteractionMatrix(table,xindex,yindex);
1204         }
1205         move->size = size;
1206         if ((double) size > (double) limitSize * table->maxGrowth) break;
1207         if (size < limitSize) limitSize = size;
1208         x = y;
1209         y = cuddNextHigh(table,x);
1210     }
1211     return(moves);
1212
1213 ddLinearAndSiftingDownOutOfMem:
1214     while (moves != NULL) {
1215         move = moves->next;
1216         cuddDeallocMove(table, moves);
1217         moves = move;
1218     }
1219     return((Move *) CUDD_OUT_OF_MEM);
1220
1221 } /* end of ddLinearAndSiftingDown */
1222
1223
1224 /**Function********************************************************************
1225
1226   Synopsis    [Given a set of moves, returns the DD heap to the order
1227   giving the minimum size.]
1228
1229   Description [Given a set of moves, returns the DD heap to the
1230   position giving the minimum size. In case of ties, returns to the
1231   closest position giving the minimum size. Returns 1 in case of
1232   success; 0 otherwise.]
1233
1234   SideEffects [None]
1235
1236 ******************************************************************************/
1237 static int
1238 ddLinearAndSiftingBackward(
1239   DdManager * table,
1240   int  size,
1241   Move * moves)
1242 {
1243     Move *move;
1244     int res;
1245
1246     for (move = moves; move != NULL; move = move->next) {
1247         if (move->size < size) {
1248             size = move->size;
1249         }
1250     }
1251
1252     for (move = moves; move != NULL; move = move->next) {
1253         if (move->size == size) return(1);
1254         if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
1255             res = cuddLinearInPlace(table,(int)move->x,(int)move->y);
1256             if (!res) return(0);
1257         }
1258         res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1259         if (!res) return(0);
1260         if (move->flags == CUDD_INVERSE_TRANSFORM_MOVE) {
1261             res = cuddLinearInPlace(table,(int)move->x,(int)move->y);
1262             if (!res) return(0);
1263         }
1264     }
1265
1266     return(1);
1267
1268 } /* end of ddLinearAndSiftingBackward */
1269
1270
1271 /**Function********************************************************************
1272
1273   Synopsis    [Given a set of moves, returns the DD heap to the order
1274   in effect before the moves.]
1275
1276   Description [Given a set of moves, returns the DD heap to the
1277   order in effect before the moves.  Returns 1 in case of success;
1278   0 otherwise.]
1279
1280   SideEffects [None]
1281
1282 ******************************************************************************/
1283 static Move*
1284 ddUndoMoves(
1285   DdManager * table,
1286   Move * moves)
1287 {
1288     Move *invmoves = NULL;
1289     Move *move;
1290     Move *invmove;
1291     int size;
1292
1293     for (move = moves; move != NULL; move = move->next) {
1294         invmove = (Move *) cuddDynamicAllocNode(table);
1295         if (invmove == NULL) goto ddUndoMovesOutOfMem;
1296         invmove->x = move->x;
1297         invmove->y = move->y;
1298         invmove->next = invmoves;
1299         invmoves = invmove;
1300         if (move->flags == CUDD_SWAP_MOVE) {
1301             invmove->flags = CUDD_SWAP_MOVE;
1302             size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1303             if (!size) goto ddUndoMovesOutOfMem;
1304         } else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
1305             invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE;
1306             size = cuddLinearInPlace(table,(int)move->x,(int)move->y);
1307             if (!size) goto ddUndoMovesOutOfMem;
1308             size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1309             if (!size) goto ddUndoMovesOutOfMem;
1310         } else { /* must be CUDD_INVERSE_TRANSFORM_MOVE */
1311 #ifdef DD_DEBUG
1312             (void) fprintf(table->err,"Unforseen event in ddUndoMoves!\n");
1313 #endif
1314             invmove->flags = CUDD_LINEAR_TRANSFORM_MOVE;
1315             size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1316             if (!size) goto ddUndoMovesOutOfMem;
1317             size = cuddLinearInPlace(table,(int)move->x,(int)move->y);
1318             if (!size) goto ddUndoMovesOutOfMem;
1319         }
1320         invmove->size = size;
1321     }
1322
1323     return(invmoves);
1324
1325 ddUndoMovesOutOfMem:
1326     while (invmoves != NULL) {
1327         move = invmoves->next;
1328         cuddDeallocMove(table, invmoves);
1329         invmoves = move;
1330     }
1331     return((Move *) CUDD_OUT_OF_MEM);
1332
1333 } /* end of ddUndoMoves */
1334
1335
1336 /**Function********************************************************************
1337
1338   Synopsis    [XORs two rows of the linear transform matrix.]
1339
1340   Description [XORs two rows of the linear transform matrix and replaces
1341   the first row with the result.]
1342
1343   SideEffects [none]
1344
1345   SeeAlso     []
1346
1347 ******************************************************************************/
1348 static void
1349 cuddXorLinear(
1350   DdManager * table,
1351   int  x,
1352   int  y)
1353 {
1354     int i;
1355     int nvars = table->size;
1356     int wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
1357     int xstart = wordsPerRow * x;
1358     int ystart = wordsPerRow * y;
1359     long *linear = table->linear;
1360
1361     for (i = 0; i < wordsPerRow; i++) {
1362         linear[xstart+i] ^= linear[ystart+i];
1363     }
1364
1365 } /* end of cuddXorLinear */