Upgrade to the latest CUDD 2.4.2.

1 files changed, 294 insertions, 265 deletions

diff --git a/src/bdd/cudd/cuddAnneal.c b/src/bdd/cudd/cuddAnneal.c
index c133cdc8..7a08b5ae 100644
--- a/src/bdd/cudd/cuddAnneal.c
+++ b/src/bdd/cudd/cuddAnneal.c
@@ -7,31 +7,58 @@
   Synopsis    [Reordering of DDs based on simulated annealing]
 
   Description [Internal procedures included in this file:
-        <ul>
-        <li> cuddAnnealing()
-        </ul>
-           Static procedures included in this file:
-        <ul>
-        <li> stopping_criterion()
-        <li> random_generator()
-        <li> ddExchange()
-        <li> ddJumpingAux()
-        <li> ddJumpingUp()
-        <li> ddJumpingDown()
-        <li> siftBackwardProb()
-        <li> copyOrder()
-        <li> restoreOrder()
-        </ul>
-        ]
+                <ul>
+                <li> cuddAnnealing()
+                </ul>
+               Static procedures included in this file:
+                <ul>
+                <li> stopping_criterion()
+                <li> random_generator()
+                <li> ddExchange()
+                <li> ddJumpingAux()
+                <li> ddJumpingUp()
+                <li> ddJumpingDown()
+                <li> siftBackwardProb()
+                <li> copyOrder()
+                <li> restoreOrder()
+                </ul>
+                ]
 
   SeeAlso     []
 
   Author      [Jae-Young Jang, Jorgen Sivesind]
 
-  Copyright [This file was created at the University of Colorado at
-  Boulder.  The University of Colorado at Boulder makes no warranty
-  about the suitability of this software for any purpose.  It is
-  presented on an AS IS basis.]
+  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
+
+  All rights reserved.
+
+  Redistribution and use in source and binary forms, with or without
+  modification, are permitted provided that the following conditions
+  are met:
+
+  Redistributions of source code must retain the above copyright
+  notice, this list of conditions and the following disclaimer.
+
+  Redistributions in binary form must reproduce the above copyright
+  notice, this list of conditions and the following disclaimer in the
+  documentation and/or other materials provided with the distribution.
+
+  Neither the name of the University of Colorado nor the names of its
+  contributors may be used to endorse or promote products derived from
+  this software without specific prior written permission.
+
+  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
+  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
+  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+  POSSIBILITY OF SUCH DAMAGE.]
 
 ******************************************************************************/
 
@@ -41,6 +68,7 @@
 ABC_NAMESPACE_IMPL_START
 
 
+
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -68,14 +96,14 @@ ABC_NAMESPACE_IMPL_START
 /*---------------------------------------------------------------------------*/
 
 #ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddAnneal.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
+static char rcsid[] DD_UNUSED = "$Id: cuddAnneal.c,v 1.14 2004/08/13 18:04:46 fabio Exp $";
 #endif
 
 #ifdef DD_STATS
-extern    int    ddTotalNumberSwapping;
-extern    int    ddTotalNISwaps;
-static    int    tosses;
-static    int    acceptances;
+extern  int     ddTotalNumberSwapping;
+extern  int     ddTotalNISwaps;
+static  int     tosses;
+static  int     acceptances;
 #endif
 
 /*---------------------------------------------------------------------------*/
@@ -89,15 +117,15 @@ static    int    acceptances;
 /* Static function prototypes                                                */
 /*---------------------------------------------------------------------------*/
 
-static int stopping_criterion ARGS((int c1, int c2, int c3, int c4, double temp));
-static double random_generator ARGS(());
-static int ddExchange ARGS((DdManager *table, int x, int y, double temp));
-static int ddJumpingAux ARGS((DdManager *table, int x, int x_low, int x_high, double temp));
-static Move * ddJumpingUp ARGS((DdManager *table, int x, int x_low, int initial_size));
-static Move * ddJumpingDown ARGS((DdManager *table, int x, int x_high, int initial_size));
-static int siftBackwardProb ARGS((DdManager *table, Move *moves, int size, double temp));
-static void copyOrder ARGS((DdManager *table, int *array, int lower, int upper));
-static int restoreOrder ARGS((DdManager *table, int *array, int lower, int upper));
+static int stopping_criterion (int c1, int c2, int c3, int c4, double temp);
+static double random_generator (void);
+static int ddExchange (DdManager *table, int x, int y, double temp);
+static int ddJumpingAux (DdManager *table, int x, int x_low, int x_high, double temp);
+static Move * ddJumpingUp (DdManager *table, int x, int x_low, int initial_size);
+static Move * ddJumpingDown (DdManager *table, int x, int x_high, int initial_size);
+static int siftBackwardProb (DdManager *table, Move *moves, int size, double temp);
+static void copyOrder (DdManager *table, int *array, int lower, int upper);
+static int restoreOrder (DdManager *table, int *array, int lower, int upper);
 
 /**AutomaticEnd***************************************************************/
 
@@ -136,11 +164,11 @@ cuddAnnealing(
     int         size;
     int         x,y;
     int         result;
-    int        c1, c2, c3, c4;
-    int        BestCost;
-    int        *BestOrder;
-    double    NewTemp, temp;
-    double    rand1;
+    int         c1, c2, c3, c4;
+    int         BestCost;
+    int         *BestOrder;
+    double      NewTemp, temp;
+    double      rand1;
     int         innerloop, maxGen;
     int         ecount, ucount, dcount;
    
@@ -158,8 +186,8 @@ cuddAnnealing(
     BestCost = size;
     BestOrder = ABC_ALLOC(int,nvars);
     if (BestOrder == NULL) {
-    table->errorCode = CUDD_MEMORY_OUT;
-    return(0);
+        table->errorCode = CUDD_MEMORY_OUT;
+        return(0);
     }
     copyOrder(table,BestOrder,lower,upper);
 
@@ -174,76 +202,76 @@ cuddAnnealing(
  
     while (!stopping_criterion(c1, c2, c3, c4, temp)) {
 #ifdef DD_STATS
-    (void) fprintf(table->out,"temp=%f\tsize=%d\tgen=%d\t",
-               temp,size,maxGen);
-    tosses = acceptances = 0;
+        (void) fprintf(table->out,"temp=%f\tsize=%d\tgen=%d\t",
+                       temp,size,maxGen);
+        tosses = acceptances = 0;
 #endif
-    for (innerloop = 0; innerloop < maxGen; innerloop++) {
-        /* Choose x, y  randomly. */
-        x = (int) Cudd_Random() % nvars;
-        do {
-        y = (int) Cudd_Random() % nvars;
-        } while (x == y);
-        x += lower;
-        y += lower;
-        if (x > y) {
-        int tmp = x;
-        x = y;
-        y = tmp;
-        }
-
-        /* Choose move with roulette wheel. */
-        rand1 = random_generator();
-        if (rand1 < EXC_PROB) {
-        result = ddExchange(table,x,y,temp);       /* exchange */
-        ecount++;
+        for (innerloop = 0; innerloop < maxGen; innerloop++) {
+            /* Choose x, y  randomly. */
+            x = (int) Cudd_Random() % nvars;
+            do {
+                y = (int) Cudd_Random() % nvars;
+            } while (x == y);
+            x += lower;
+            y += lower;
+            if (x > y) {
+                int tmp = x;
+                x = y;
+                y = tmp;
+            }
+
+            /* Choose move with roulette wheel. */
+            rand1 = random_generator();
+            if (rand1 < EXC_PROB) {
+                result = ddExchange(table,x,y,temp);       /* exchange */
+                ecount++;
 #if 0
-        (void) fprintf(table->out,
-                   "Exchange of %d and %d: size = %d\n",
-                   x,y,table->keys - table->isolated);
+                (void) fprintf(table->out,
+                               "Exchange of %d and %d: size = %d\n",
+                               x,y,table->keys - table->isolated);
 #endif
-        } else if (rand1 < EXC_PROB + JUMP_UP_PROB) {
-        result = ddJumpingAux(table,y,x,y,temp); /* jumping_up */
-        ucount++;
+            } else if (rand1 < EXC_PROB + JUMP_UP_PROB) {
+                result = ddJumpingAux(table,y,x,y,temp); /* jumping_up */
+                ucount++;
 #if 0
-        (void) fprintf(table->out,
-                   "Jump up of %d to %d: size = %d\n",
-                   y,x,table->keys - table->isolated);
+                (void) fprintf(table->out,
+                               "Jump up of %d to %d: size = %d\n",
+                               y,x,table->keys - table->isolated);
 #endif
-        } else {
-        result = ddJumpingAux(table,x,x,y,temp); /* jumping_down */
-        dcount++;
+            } else {
+                result = ddJumpingAux(table,x,x,y,temp); /* jumping_down */
+                dcount++;
 #if 0
-        (void) fprintf(table->out,
-                   "Jump down of %d to %d: size = %d\n",
-                   x,y,table->keys - table->isolated);
+                (void) fprintf(table->out,
+                               "Jump down of %d to %d: size = %d\n",
+                               x,y,table->keys - table->isolated);
 #endif
+            }
+
+            if (!result) {
+                ABC_FREE(BestOrder);
+                return(0);
+            }
+
+            size = table->keys - table->isolated;       /* keep current size */
+            if (size < BestCost) {                      /* update best order */
+                BestCost = size;
+                copyOrder(table,BestOrder,lower,upper);
+            }
         }
-
-        if (!result) {
-        ABC_FREE(BestOrder);
-        return(0);
-        }
-
-        size = table->keys - table->isolated;    /* keep current size */
-        if (size < BestCost) {            /* update best order */
-        BestCost = size;
-        copyOrder(table,BestOrder,lower,upper);
+        c1 = c2;
+        c2 = c3;
+        c3 = c4;
+        c4 = size;
+        NewTemp = ALPHA * temp;
+        if (NewTemp >= 1.0) {
+            maxGen = (int)(log(NewTemp) / log(temp) * maxGen);
         }
-    }
-    c1 = c2;
-    c2 = c3;
-    c3 = c4;
-    c4 = size;
-    NewTemp = ALPHA * temp;
-    if (NewTemp >= 1.0) {
-        maxGen = (int)(log(NewTemp) / log(temp) * maxGen);
-    }
-    temp = NewTemp;                    /* control variable */
+        temp = NewTemp;                 /* control variable */
 #ifdef DD_STATS
-    (void) fprintf(table->out,"uphill = %d\taccepted = %d\n",
-               tosses,acceptances);
-    fflush(table->out);
+        (void) fprintf(table->out,"uphill = %d\taccepted = %d\n",
+                       tosses,acceptances);
+        fflush(table->out);
 #endif
     }
 
@@ -286,11 +314,11 @@ stopping_criterion(
   double  temp)
 {
     if (STOP_TEMP < temp) {
-    return(0);
+        return(0);
     } else if ((c1 == c2) && (c1 == c3) && (c1 == c4)) {
-    return(1);
+        return(1);
     } else {
-    return(0);
+        return(0);
     }
 
 } /* end of stopping_criterion */
@@ -308,8 +336,7 @@ stopping_criterion(
 
 ******************************************************************************/
 static double
-random_generator(
-   )
+random_generator(void)
 {
     return((double)(Cudd_Random() / 2147483561.0));
 
@@ -351,83 +378,83 @@ ddExchange(
     initial_size = limit_size = table->keys - table->isolated;
 
     for (;;) {
-    if (x_next == y_next) {
-        size = cuddSwapInPlace(table,x,x_next);
-        if (size == 0) goto ddExchangeOutOfMem;
-        move = (Move *)cuddDynamicAllocNode(table);
-        if (move == NULL) goto ddExchangeOutOfMem;
-        move->x = x;
-        move->y = x_next;
-        move->size = size;
-        move->next = moves;
-        moves = move;
-        size = cuddSwapInPlace(table,y_next,y);
-        if (size == 0) goto ddExchangeOutOfMem;
-        move = (Move *)cuddDynamicAllocNode(table);
-        if (move == NULL) goto ddExchangeOutOfMem;
-        move->x = y_next;
-        move->y = y;
-        move->size = size;
-        move->next = moves;
-        moves = move;
-        size = cuddSwapInPlace(table,x,x_next);
-        if (size == 0) goto ddExchangeOutOfMem;
-        move = (Move *)cuddDynamicAllocNode(table);
-        if (move == NULL) goto ddExchangeOutOfMem;
-        move->x = x;
-        move->y = x_next;
-        move->size = size;
-        move->next = moves;
-        moves = move;
-
-        tmp = x;
-        x = y;
-        y = tmp;
-    } else if (x == y_next) {
-        size = cuddSwapInPlace(table,x,x_next);
-        if (size == 0) goto ddExchangeOutOfMem;
-        move = (Move *)cuddDynamicAllocNode(table);
-        if (move == NULL) goto ddExchangeOutOfMem;
-        move->x = x;
-        move->y = x_next;
-        move->size = size;
-        move->next = moves;
-        moves = move;
-        tmp = x;
-        x = y;
-        y = tmp;
-    } else {
-        size = cuddSwapInPlace(table,x,x_next);
-        if (size == 0) goto ddExchangeOutOfMem;
-        move = (Move *)cuddDynamicAllocNode(table);
-        if (move == NULL) goto ddExchangeOutOfMem;
-        move->x = x;
-        move->y = x_next;
-        move->size = size;
-        move->next = moves;
-        moves = move;
-        size = cuddSwapInPlace(table,y_next,y);
-        if (size == 0) goto ddExchangeOutOfMem;
-        move = (Move *)cuddDynamicAllocNode(table);
-        if (move == NULL) goto ddExchangeOutOfMem;
-        move->x = y_next;
-        move->y = y;
-        move->size = size;
-        move->next = moves;
-        moves = move;
-        x = x_next;
-        y = y_next;
-    }
+        if (x_next == y_next) {
+            size = cuddSwapInPlace(table,x,x_next);
+            if (size == 0) goto ddExchangeOutOfMem;
+            move = (Move *)cuddDynamicAllocNode(table);
+            if (move == NULL) goto ddExchangeOutOfMem;
+            move->x = x;
+            move->y = x_next;
+            move->size = size;
+            move->next = moves;
+            moves = move;
+            size = cuddSwapInPlace(table,y_next,y);
+            if (size == 0) goto ddExchangeOutOfMem;
+            move = (Move *)cuddDynamicAllocNode(table);
+            if (move == NULL) goto ddExchangeOutOfMem;
+            move->x = y_next;
+            move->y = y;
+            move->size = size;
+            move->next = moves;
+            moves = move;
+            size = cuddSwapInPlace(table,x,x_next);
+            if (size == 0) goto ddExchangeOutOfMem;
+            move = (Move *)cuddDynamicAllocNode(table);
+            if (move == NULL) goto ddExchangeOutOfMem;
+            move->x = x;
+            move->y = x_next;
+            move->size = size;
+            move->next = moves;
+            moves = move;
+
+            tmp = x;
+            x = y;
+            y = tmp;
+        } else if (x == y_next) {
+            size = cuddSwapInPlace(table,x,x_next);
+            if (size == 0) goto ddExchangeOutOfMem;
+            move = (Move *)cuddDynamicAllocNode(table);
+            if (move == NULL) goto ddExchangeOutOfMem;
+            move->x = x;
+            move->y = x_next;
+            move->size = size;
+            move->next = moves;
+            moves = move;
+            tmp = x;
+            x = y;
+            y = tmp;
+        } else {
+            size = cuddSwapInPlace(table,x,x_next);
+            if (size == 0) goto ddExchangeOutOfMem;
+            move = (Move *)cuddDynamicAllocNode(table);
+            if (move == NULL) goto ddExchangeOutOfMem;
+            move->x = x;
+            move->y = x_next;
+            move->size = size;
+            move->next = moves;
+            moves = move;
+            size = cuddSwapInPlace(table,y_next,y);
+            if (size == 0) goto ddExchangeOutOfMem;
+            move = (Move *)cuddDynamicAllocNode(table);
+            if (move == NULL) goto ddExchangeOutOfMem;
+            move->x = y_next;
+            move->y = y;
+            move->size = size;
+            move->next = moves;
+            moves = move;
+            x = x_next;
+            y = y_next;
+        }
 
-    x_next = cuddNextHigh(table,x);
-    y_next = cuddNextLow(table,y);
-    if (x_next > y_ref) break;
+        x_next = cuddNextHigh(table,x);
+        y_next = cuddNextLow(table,y);
+        if (x_next > y_ref) break;
 
-    if ((double) size > DD_MAX_REORDER_GROWTH * (double) limit_size) {
-        break;
-    } else if (size < limit_size) {
-        limit_size = size;
-    }
+        if ((double) size > DD_MAX_REORDER_GROWTH * (double) limit_size) {
+            break;
+        } else if (size < limit_size) {
+            limit_size = size;
+        }
     }
 
     if (y_next>=x_ref) {
@@ -447,16 +474,16 @@ ddExchange(
     if (!result) goto ddExchangeOutOfMem;
 
     while (moves != NULL) {
-    move = moves->next;
-    cuddDeallocNode(table, (DdNode *) moves);
-    moves = move;
+        move = moves->next;
+        cuddDeallocMove(table, moves);
+        moves = move;
     }
     return(1);
 
 ddExchangeOutOfMem:
     while (moves != NULL) {
         move = moves->next;
-        cuddDeallocNode(table,(DdNode *) moves);
+        cuddDeallocMove(table, moves);
         moves = move;
     }
     return(0);
@@ -499,36 +526,36 @@ ddJumpingAux(
     moves = NULL;
 
     if (cuddNextLow(table,x) < x_low) {
-    if (cuddNextHigh(table,x) > x_high) return(1);
-    moves = ddJumpingDown(table,x,x_high,initial_size);
-    /* after that point x --> x_high unless early termination */
-    if (moves == NULL) goto ddJumpingAuxOutOfMem;
-    /* move backward and stop at best position or accept uphill move */
-    result = siftBackwardProb(table,moves,initial_size,temp);
-    if (!result) goto ddJumpingAuxOutOfMem;
+        if (cuddNextHigh(table,x) > x_high) return(1);
+        moves = ddJumpingDown(table,x,x_high,initial_size);
+        /* after that point x --> x_high unless early termination */
+        if (moves == NULL) goto ddJumpingAuxOutOfMem;
+        /* move backward and stop at best position or accept uphill move */
+        result = siftBackwardProb(table,moves,initial_size,temp);
+        if (!result) goto ddJumpingAuxOutOfMem;
     } else if (cuddNextHigh(table,x) > x_high) {
-    moves = ddJumpingUp(table,x,x_low,initial_size);
-    /* after that point x --> x_low unless early termination */
-    if (moves == NULL) goto ddJumpingAuxOutOfMem;
-    /* move backward and stop at best position or accept uphill move */
-    result = siftBackwardProb(table,moves,initial_size,temp);
-    if (!result) goto ddJumpingAuxOutOfMem;
+        moves = ddJumpingUp(table,x,x_low,initial_size);
+        /* after that point x --> x_low unless early termination */
+        if (moves == NULL) goto ddJumpingAuxOutOfMem;
+        /* move backward and stop at best position or accept uphill move */
+        result = siftBackwardProb(table,moves,initial_size,temp);
+        if (!result) goto ddJumpingAuxOutOfMem;
     } else {
-    (void) fprintf(table->err,"Unexpected condition in ddJumping\n");
-    goto ddJumpingAuxOutOfMem;
+        (void) fprintf(table->err,"Unexpected condition in ddJumping\n");
+        goto ddJumpingAuxOutOfMem;
     }
     while (moves != NULL) {
-    move = moves->next;
-    cuddDeallocNode(table, (DdNode *) moves);
-    moves = move;
+        move = moves->next;
+        cuddDeallocMove(table, moves);
+        moves = move;
     }
     return(1);
 
 ddJumpingAuxOutOfMem:
     while (moves != NULL) {
-    move = moves->next;
-    cuddDeallocNode(table, (DdNode *) moves);
-    moves = move;
+        move = moves->next;
+        cuddDeallocMove(table, moves);
+        moves = move;
     }
     return(0);
 
@@ -564,30 +591,30 @@ ddJumpingUp(
     moves = NULL;
     y = cuddNextLow(table,x);
     while (y >= x_low) {
-    size = cuddSwapInPlace(table,y,x);
-    if (size == 0) goto ddJumpingUpOutOfMem;
-    move = (Move *)cuddDynamicAllocNode(table);
-    if (move == NULL) goto ddJumpingUpOutOfMem;
-    move->x = y;
-    move->y = x;
-    move->size = size;
-    move->next = moves;
-    moves = move;
-    if ((double) size > table->maxGrowth * (double) limit_size) {
-        break;
-    } else if (size < limit_size) {
-        limit_size = size;
-    }
-    x = y;
-    y = cuddNextLow(table,x);
+        size = cuddSwapInPlace(table,y,x);
+        if (size == 0) goto ddJumpingUpOutOfMem;
+        move = (Move *)cuddDynamicAllocNode(table);
+        if (move == NULL) goto ddJumpingUpOutOfMem;
+        move->x = y;
+        move->y = x;
+        move->size = size;
+        move->next = moves;
+        moves = move;
+        if ((double) size > table->maxGrowth * (double) limit_size) {
+            break;
+        } else if (size < limit_size) {
+            limit_size = size;
+        }
+        x = y;
+        y = cuddNextLow(table,x);
     }
     return(moves);
 
 ddJumpingUpOutOfMem:
     while (moves != NULL) {
-    move = moves->next;
-    cuddDeallocNode(table, (DdNode *) moves);
-    moves = move;
+        move = moves->next;
+        cuddDeallocMove(table, moves);
+        moves = move;
     }
     return(NULL);
 
@@ -623,30 +650,30 @@ ddJumpingDown(
     moves = NULL;
     y = cuddNextHigh(table,x);
     while (y <= x_high) {
-    size = cuddSwapInPlace(table,x,y);
-    if (size == 0) goto ddJumpingDownOutOfMem;
-    move = (Move *)cuddDynamicAllocNode(table);
-    if (move == NULL) goto ddJumpingDownOutOfMem;
-    move->x = x;
-    move->y = y;
-    move->size = size;
-    move->next = moves;
-    moves = move;
-    if ((double) size > table->maxGrowth * (double) limit_size) {
-        break;
-    } else if (size < limit_size) {
-        limit_size = size;
-    }
-    x = y;
-    y = cuddNextHigh(table,x);
+        size = cuddSwapInPlace(table,x,y);
+        if (size == 0) goto ddJumpingDownOutOfMem;
+        move = (Move *)cuddDynamicAllocNode(table);
+        if (move == NULL) goto ddJumpingDownOutOfMem;
+        move->x = x;
+        move->y = y;
+        move->size = size;
+        move->next = moves;
+        moves = move;
+        if ((double) size > table->maxGrowth * (double) limit_size) {
+            break;
+        } else if (size < limit_size) {
+            limit_size = size;
+        }
+        x = y;
+        y = cuddNextHigh(table,x);
     }
     return(moves);
 
 ddJumpingDownOutOfMem:
     while (moves != NULL) {
-    move = moves->next;
-    cuddDeallocNode(table, (DdNode *) moves);
-    moves = move;
+        move = moves->next;
+        cuddDeallocMove(table, moves);
+        moves = move;
     }
     return(NULL);
 
@@ -681,9 +708,9 @@ siftBackwardProb(
 
     /* Look for best size during the last sifting */
     for (move = moves; move != NULL; move = move->next) {
-    if (move->size < best_size) {
-        best_size = move->size;
-    }
+        if (move->size < best_size) {
+            best_size = move->size;
+        }
     }
     
     /* If best_size equals size, the last sifting did not produce any
@@ -691,17 +718,17 @@ siftBackwardProb(
     ** this change or not.
     */
     if (best_size == size) {
-    coin = random_generator();
+        coin = random_generator();
 #ifdef DD_STATS
-    tosses++;
+        tosses++;
 #endif
-    threshold = exp(-((double)(table->keys - table->isolated - size))/temp);
-    if (coin < threshold) {
+        threshold = exp(-((double)(table->keys - table->isolated - size))/temp);
+        if (coin < threshold) {
 #ifdef DD_STATS
-        acceptances++;
+            acceptances++;
 #endif
-        return(1);
-    }
+            return(1);
+        }
     }
 
     /* Either there was improvement, or we have decided not to
@@ -709,9 +736,9 @@ siftBackwardProb(
     */
     res = table->keys - table->isolated;
     for (move = moves; move != NULL; move = move->next) {
-    if (res == best_size) return(1);
-    res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
-    if (!res) return(0);
+        if (res == best_size) return(1);
+        res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
+        if (!res) return(0);
     }
 
     return(1);
@@ -743,7 +770,7 @@ copyOrder(
 
     nvars = upper - lower + 1;
     for (i = 0; i < nvars; i++) {
-    array[i] = table->invperm[i+lower];
+        array[i] = table->invperm[i+lower];
     }
 
 } /* end of copyOrder */
@@ -772,22 +799,24 @@ restoreOrder(
     int nvars = upper - lower + 1;
 
     for (i = 0; i < nvars; i++) {
-    x = table->perm[array[i]];
+        x = table->perm[array[i]];
 #ifdef DD_DEBUG
     assert(x >= lower && x <= upper);
 #endif
-    y = cuddNextLow(table,x);
-    while (y >= i + lower) {
-        size = cuddSwapInPlace(table,y,x);
-        if (size == 0) return(0);
-        x = y;
         y = cuddNextLow(table,x);
-    }
+        while (y >= i + lower) {
+            size = cuddSwapInPlace(table,y,x);
+            if (size == 0) return(0);
+            x = y;
+            y = cuddNextLow(table,x);
+        }
     }
 
     return(1);
 
 } /* end of restoreOrder */
 
+
 ABC_NAMESPACE_IMPL_END
 
+