/**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.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.10 1998/06/05 09:29:40 fabio 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 */
