Version abc70930

1 files changed, 0 insertions, 788 deletions

diff --git a/src/bdd/cudd/cuddAnneal.c b/src/bdd/cudd/cuddAnneal.c
deleted file mode 100644
index 3d8b56b9..00000000
--- a/src/bdd/cudd/cuddAnneal.c
+++ /dev/null
@@ -1,788 +0,0 @@
-/**CFile***********************************************************************
-
-  FileName    [cuddAnneal.c]
-
-  PackageName [cudd]
-
-  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>
-        ]
-
-  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.]
-
-******************************************************************************/
-
-#include "util_hack.h"
-#include "cuddInt.h"
-
-/*---------------------------------------------------------------------------*/
-/* Constant declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-/* Annealing parameters */
-#define BETA 0.6 
-#define ALPHA 0.90
-#define EXC_PROB 0.4 
-#define JUMP_UP_PROB 0.36
-#define MAXGEN_RATIO 15.0
-#define STOP_TEMP 1.0
-
-/*---------------------------------------------------------------------------*/
-/* Stucture declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-
-/*---------------------------------------------------------------------------*/
-/* Type declarations                                                         */
-/*---------------------------------------------------------------------------*/
-
-
-/*---------------------------------------------------------------------------*/
-/* Variable declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-#ifndef lint
-static char rcsid[] DD_UNUSED = "$Id: cuddAnneal.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $";
-#endif
-
-#ifdef DD_STATS
-extern    int    ddTotalNumberSwapping;
-extern    int    ddTotalNISwaps;
-static    int    tosses;
-static    int    acceptances;
-#endif
-
-/*---------------------------------------------------------------------------*/
-/* Macro declarations                                                        */
-/*---------------------------------------------------------------------------*/
-
-
-/**AutomaticStart*************************************************************/
-
-/*---------------------------------------------------------------------------*/
-/* 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));
-
-/**AutomaticEnd***************************************************************/
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of exported functions                                          */
-/*---------------------------------------------------------------------------*/
-
-/*---------------------------------------------------------------------------*/
-/* Definition of internal functions                                          */
-/*---------------------------------------------------------------------------*/
-
-
-/**Function********************************************************************
-
-  Synopsis    [Get new variable-order by simulated annealing algorithm.]
-
-  Description [Get x, y by random selection. Choose either
-  exchange or jump randomly. In case of jump, choose between jump_up
-  and jump_down randomly. Do exchange or jump and get optimal case.
-  Loop until there is no improvement or temperature reaches
-  minimum. Returns 1 in case of success; 0 otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-int
-cuddAnnealing(
-  DdManager * table,
-  int  lower,
-  int  upper)
-{
-    int         nvars;
-    int         size;
-    int         x,y;
-    int         result;
-    int        c1, c2, c3, c4;
-    int        BestCost;
-    int        *BestOrder;
-    double    NewTemp, temp;
-    double    rand1;
-    int         innerloop, maxGen;
-    int         ecount, ucount, dcount;
-   
-    nvars = upper - lower + 1;
-
-    result = cuddSifting(table,lower,upper);
-#ifdef DD_STATS
-    (void) fprintf(table->out,"\n");
-#endif
-    if (result == 0) return(0);
-
-    size = table->keys - table->isolated;
-
-    /* Keep track of the best order. */
-    BestCost = size;
-    BestOrder = ALLOC(int,nvars);
-    if (BestOrder == NULL) {
-    table->errorCode = CUDD_MEMORY_OUT;
-    return(0);
-    }
-    copyOrder(table,BestOrder,lower,upper);
-
-    temp = BETA * size;
-    maxGen = (int) (MAXGEN_RATIO * nvars);
-
-    c1 = size + 10;
-    c2 = c1 + 10;
-    c3 = size;
-    c4 = c2 + 10;
-    ecount = ucount = dcount = 0;
- 
-    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;
-#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++;
-#if 0
-        (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++;
-#if 0
-        (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++;
-#if 0
-        (void) fprintf(table->out,
-                   "Jump down of %d to %d: size = %d\n",
-                   x,y,table->keys - table->isolated);
-#endif
-        }
-
-        if (!result) {
-        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);
-    }
-    temp = NewTemp;                    /* control variable */
-#ifdef DD_STATS
-    (void) fprintf(table->out,"uphill = %d\taccepted = %d\n",
-               tosses,acceptances);
-    fflush(table->out);
-#endif
-    }
-
-    result = restoreOrder(table,BestOrder,lower,upper);
-    FREE(BestOrder);
-    if (!result) return(0);
-#ifdef DD_STATS
-    fprintf(table->out,"#:N_EXCHANGE %8d : total exchanges\n",ecount);
-    fprintf(table->out,"#:N_JUMPUP   %8d : total jumps up\n",ucount);
-    fprintf(table->out,"#:N_JUMPDOWN %8d : total jumps down",dcount);
-#endif
-    return(1);
-
-} /* end of cuddAnnealing */
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of static functions                                            */
-/*---------------------------------------------------------------------------*/
-
-/**Function********************************************************************
-
-  Synopsis    [Checks termination condition.]
-
-  Description [If temperature is STOP_TEMP or there is no improvement
-  then terminates. Returns 1 if the termination criterion is met; 0
-  otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static int
-stopping_criterion(
-  int  c1,
-  int  c2,
-  int  c3,
-  int  c4,
-  double  temp)
-{
-    if (STOP_TEMP < temp) {
-    return(0);
-    } else if ((c1 == c2) && (c1 == c3) && (c1 == c4)) {
-    return(1);
-    } else {
-    return(0);
-    }
-
-} /* end of stopping_criterion */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Random number generator.]
-
-  Description [Returns a double precision value between 0.0 and 1.0.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static double
-random_generator(
-   )
-{
-    return((double)(Cudd_Random() / 2147483561.0));
-
-} /* end of random_generator */
-
-
-/**Function********************************************************************
-
-  Synopsis    [This function is for exchanging two variables, x and y.]
-
-  Description [This is the same funcion as ddSwapping except for
-  comparison expression.  Use probability function, exp(-size_change/temp).]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static int
-ddExchange(
-  DdManager * table,
-  int  x,
-  int  y,
-  double  temp)
-{
-    Move       *move,*moves;
-    int        tmp;
-    int        x_ref,y_ref;
-    int        x_next,y_next;
-    int        size, result;
-    int        initial_size, limit_size;
-
-    x_ref = x;
-    y_ref = y;
-
-    x_next = cuddNextHigh(table,x);
-    y_next = cuddNextLow(table,y);
-    moves = NULL;
-    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;
-    }
-
-    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 (y_next>=x_ref) {
-        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;
-    }
-
-    /* move backward and stop at best position or accept uphill move */
-    result = siftBackwardProb(table,moves,initial_size,temp);
-    if (!result) goto ddExchangeOutOfMem;
-
-    while (moves != NULL) {
-    move = moves->next;
-    cuddDeallocNode(table, (DdNode *) moves);
-    moves = move;
-    }
-    return(1);
-
-ddExchangeOutOfMem:
-    while (moves != NULL) {
-        move = moves->next;
-        cuddDeallocNode(table,(DdNode *) moves);
-        moves = move;
-    }
-    return(0);
-
-} /* end of ddExchange */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Moves a variable to a specified position.]
-
-  Description [If x==x_low, it executes jumping_down. If x==x_high, it
-  executes jumping_up. This funcion is similar to ddSiftingAux. Returns
-  1 in case of success; 0 otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static int
-ddJumpingAux(
-  DdManager * table,
-  int  x,
-  int  x_low,
-  int  x_high,
-  double  temp)
-{
-    Move       *move;
-    Move       *moves;        /* list of moves */
-    int        initial_size;
-    int        result;
-
-    initial_size = table->keys - table->isolated;
-
-#ifdef DD_DEBUG
-    assert(table->subtables[x].keys > 0);
-#endif
-
-    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;
-    } 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;
-    } else {
-    (void) fprintf(table->err,"Unexpected condition in ddJumping\n");
-    goto ddJumpingAuxOutOfMem;
-    }
-    while (moves != NULL) {
-    move = moves->next;
-    cuddDeallocNode(table, (DdNode *) moves);
-    moves = move;
-    }
-    return(1);
-
-ddJumpingAuxOutOfMem:
-    while (moves != NULL) {
-    move = moves->next;
-    cuddDeallocNode(table, (DdNode *) moves);
-    moves = move;
-    }
-    return(0);
-
-} /* end of ddJumpingAux */
-
-
-/**Function********************************************************************
-
-  Synopsis    [This function is for jumping up.]
-
-  Description [This is a simplified version of ddSiftingUp. It does not
-  use lower bounding. Returns the set of moves in case of success; NULL
-  if memory is full.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static Move *
-ddJumpingUp(
-  DdManager * table,
-  int  x,
-  int  x_low,
-  int  initial_size)
-{
-    Move       *moves;
-    Move       *move;
-    int        y;
-    int        size;
-    int        limit_size = initial_size;
-
-    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);
-    }
-    return(moves);
-
-ddJumpingUpOutOfMem:
-    while (moves != NULL) {
-    move = moves->next;
-    cuddDeallocNode(table, (DdNode *) moves);
-    moves = move;
-    }
-    return(NULL);
-
-} /* end of ddJumpingUp */
-
-
-/**Function********************************************************************
-
-  Synopsis    [This function is for jumping down.]
-
-  Description [This is a simplified version of ddSiftingDown. It does not
-  use lower bounding. Returns the set of moves in case of success; NULL
-  if memory is full.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static Move *
-ddJumpingDown(
-  DdManager * table,
-  int  x,
-  int  x_high,
-  int  initial_size)
-{
-    Move       *moves;
-    Move       *move;
-    int        y;
-    int        size;
-    int        limit_size = initial_size;
-
-    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);
-    }
-    return(moves);
-
-ddJumpingDownOutOfMem:
-    while (moves != NULL) {
-    move = moves->next;
-    cuddDeallocNode(table, (DdNode *) moves);
-    moves = move;
-    }
-    return(NULL);
-
-} /* end of ddJumpingDown */
-
-
-/**Function********************************************************************
-
-  Synopsis [Returns the DD to the best position encountered during
-  sifting if there was improvement.]
-
-  Description [Otherwise, "tosses a coin" to decide whether to keep
-  the current configuration or return the DD to the original
-  one. Returns 1 in case of success; 0 otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static int
-siftBackwardProb(
-  DdManager * table,
-  Move * moves,
-  int  size,
-  double  temp)
-{
-    Move   *move;
-    int    res;
-    int    best_size = size;
-    double coin, threshold;
-
-    /* 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 best_size equals size, the last sifting did not produce any
-    ** improvement. We now toss a coin to decide whether to retain
-    ** this change or not.
-    */
-    if (best_size == size) {
-    coin = random_generator();
-#ifdef DD_STATS
-    tosses++;
-#endif
-    threshold = exp(-((double)(table->keys - table->isolated - size))/temp);
-    if (coin < threshold) {
-#ifdef DD_STATS
-        acceptances++;
-#endif
-        return(1);
-    }
-    }
-
-    /* Either there was improvement, or we have decided not to
-    ** accept the uphill move. Go to best position.
-    */
-    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);
-    }
-
-    return(1);
-
-} /* end of sift_backward_prob */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Copies the current variable order to array.]
-
-  Description [Copies the current variable order to array.
-  At the same time inverts the permutation.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static void
-copyOrder(
-  DdManager * table,
-  int * array,
-  int  lower,
-  int  upper)
-{
-    int i;
-    int nvars;
-
-    nvars = upper - lower + 1;
-    for (i = 0; i < nvars; i++) {
-    array[i] = table->invperm[i+lower];
-    }
-
-} /* end of copyOrder */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Restores the variable order in array by a series of sifts up.]
-
-  Description [Restores the variable order in array by a series of sifts up.
-  Returns 1 in case of success; 0 otherwise.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-static int
-restoreOrder(
-  DdManager * table,
-  int * array,
-  int  lower,
-  int  upper)
-{
-    int i, x, y, size;
-    int nvars = upper - lower + 1;
-
-    for (i = 0; i < nvars; 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);
-    }
-    }
-
-    return(1);
-
-} /* end of restoreOrder */
-