text: /**CFile****************************************************************
  
    FileName    [exorList.c]
  
    SystemName  [ABC: Logic synthesis and verification system.]
  
    PackageName [Exclusive sum-of-product minimization.]
  
    Synopsis    [Cube lists.]
  
    Author      [Alan Mishchenko]
    
    Affiliation [UC Berkeley]
  
    Date        [Ver. 1.0. Started - June 20, 2005.]
  
    Revision    [$Id: exorList.c,v 1.0 2005/06/20 00:00:00 alanmi Exp $]
  
  ***********************************************************************/
  
  ////////////////////////////////////////////////////////////////////////
  ///                                                                  ///
  ///                  Implementation of EXORCISM - 4                  ///
  ///              An Exclusive Sum-of-Product Minimizer               ///
  ///                                                                  ///
  ///               Alan Mishchenko  <alanmi@ee.pdx.edu>               ///
  ///                                                                  ///
  ////////////////////////////////////////////////////////////////////////
  ///                                                                  ///
  ///                 Iterative Cube Set Minimization                  ///
  ///                  Iterative ExorLink Procedure                    ///
  ///                  Support of Cube Pair Queques                    ///
  ///                                                                  ///
  ///  Ver. 1.0. Started - July 18, 2000. Last update - July 20, 2000  ///
  ///  Ver. 1.1. Started - July 24, 2000. Last update - July 29, 2000  ///
  ///  Ver. 1.2. Started - July 30, 2000. Last update - July 31, 2000  ///
  ///  Ver. 1.4. Started -  Aug 10, 2000. Last update -  Aug 26, 2000  ///
  ///  Ver. 1.5. Started -  Aug 30, 2000. Last update -  Aug 30, 2000  ///
  ///  Ver. 1.6. Started -  Sep 11, 2000. Last update -  Sep 15, 2000  ///
  ///  Ver. 1.7. Started -  Sep 20, 2000. Last update -  Sep 23, 2000  ///
  ///                                                                  ///
  ////////////////////////////////////////////////////////////////////////
  ///   This software was tested with the BDD package "CUDD", v.2.3.0  ///
  ///                          by Fabio Somenzi                        ///
  ///                  http://vlsi.colorado.edu/~fabio/                ///
  ////////////////////////////////////////////////////////////////////////
  
  #include "exor.h"
  
  ABC_NAMESPACE_IMPL_START
  
  ////////////////////////////////////////////////////////////////////////
  ///                       EXTERNAL VARIABLES                         ///
  ////////////////////////////////////////////////////////////////////////
  
  // information about options and the cover
  extern cinfo g_CoverInfo;
  
  // the look-up table for the number of 1's in unsigned short
  extern unsigned char BitCount[];
  
  ////////////////////////////////////////////////////////////////////////
  ///                       EXTERNAL FUNCTIONS                         ///
  ////////////////////////////////////////////////////////////////////////
  
  extern int GetDistance( Cube* pC1, Cube* pC2 );
  // distance computation for two cubes
  extern int GetDistancePlus( Cube* pC1, Cube* pC2 );
  
  extern void ExorVar( Cube* pC, int Var, varvalue Val );
  
  extern void AddToFreeCubes( Cube* pC );
  // returns a simplified cube back into the free list
  
  //extern void PrintCube( ostream& DebugStream, Cube* pC );
  // debug output for cubes
  
  extern Cube* GetFreeCube();
  
  ////////////////////////////////////////////////////////////////////////
  /// ExorLink Functions
  extern int ExorLinkCubeIteratorStart( Cube** pGroup, Cube* pC1, Cube* pC2, cubedist Dist );
  // this function starts the Exor-Link IteratorCubePair, which iterates
  // through the cube groups starting from the group with min literals
  // returns 1 on success, returns 0 if the cubes have wrong distance
  
  extern int ExorLinkCubeIteratorNext( Cube** pGroup );
  // give the next group in the decreasing order of sum of literals
  // returns 1 on success, returns 0 if there are no more groups
  
  extern int ExorLinkCubeIteratorPick( Cube** pGroup, int g );
  // gives the group #g in the order in which the groups were given
  // during iteration
  // returns 1 on success, returns 0 if something g is too large
  
  extern void ExorLinkCubeIteratorCleanUp( int fTakeLastGroup );
  // removes the cubes from the store back into the list of free cubes
  // if fTakeLastGroup is 0, removes all cubes
  // if fTakeLastGroup is 1, does not store the last group
  
  ////////////////////////////////////////////////////////////////////////
  ///                    FUNCTIONS OF THIS MODULE                      ///
  ////////////////////////////////////////////////////////////////////////
  
  // iterative ExorLink
  int IterativelyApplyExorLink2( char fDistEnable );   
  int IterativelyApplyExorLink3( char fDistEnable );   
  int IterativelyApplyExorLink4( char fDistEnable );   
  
  // function which performs distance computation and simplifes on the fly
  // it is also called from the Pseudo-Kronecker module when cubes are added
  int CheckForCloseCubes( Cube* p, int fAddCube );
  int CheckAndInsert( Cube* p );
  
  // this function changes the cube back after it was DIST-1 transformed
  void UndoRecentChanges();
  
  ////////////////////////////////////////////////////////////////////////
  // iterating through adjucency pair queques (with authomatic garbage collection)
  
  // start an iterator through cubes of dist CubeDist,
  // the resulting pointers are written into ppC1 and ppC2
  int IteratorCubePairStart( cubedist Dist, Cube** ppC1, Cube** ppC2 );
  // gives the next VALID cube pair (the previous one is automatically dequequed)
  int IteratorCubePairNext();
  
  ////////////////////////////////////////////////////////////////////////
  // the cube storage
  
  // cube storage allocation/delocation
  int AllocateCubeSets( int nVarsIn, int nVarsOut );
  void DelocateCubeSets();
  
  // insert/extract a cube into/from the storage
  void CubeInsert( Cube* p );
  Cube* CubeExtract( Cube* p );
  
  ////////////////////////////////////////////////////////////////////////
  // Cube Set Iterator
  Cube* IterCubeSetStart();
  // starts an iterator that traverses all the cubes in the ring
  Cube* IterCubeSetNext();
  // returns the next cube in the ring
  // to use it again after it has returned NULL, call IterCubeSetStart() first
  
  ////////////////////////////////////////////////////////////////////////
  // cube adjacency queques
  
  // adjacency queque allocation/delocation procedures
  int AllocateQueques( int nPlaces );
  void DelocateQueques();
  
  // conditional adding cube pairs to queques
  // reset temporarily stored new range of cube pairs
  static void NewRangeReset();
  // add temporarily stored new range of cube pairs to the queque
  static void NewRangeAdd();
  // insert one cube pair into the new range
  static void NewRangeInsertCubePair( cubedist Dist, Cube* p1, Cube* p2 );
  
  static void MarkSet();
  static void MarkRewind();
  
  void PrintQuequeStats();
  int GetQuequeStats( cubedist Dist );
  
  // iterating through the queque (with authomatic garbage collection)
  // start an iterator through cubes of dist CubeDist,
  // the resulting pointers are written into ppC1 and ppC2
  int IteratorCubePairStart( cubedist Dist, Cube** ppC1, Cube** ppC2 );
  // gives the next VALID cube pair (the previous one is automatically dequequed)
  int IteratorCubePairNext();
  
  ////////////////////////////////////////////////////////////////////////
  ///                      EXPORTED VARIABLES                          ///
  ////////////////////////////////////////////////////////////////////////`
  
  // the number of allocated places
  int s_nPosAlloc;
  // the maximum number of occupied places
  int s_nPosMax[3];
  
  ////////////////////////////////////////////////////////////////////////
  ///                      Minimization Strategy                       ///
  ////////////////////////////////////////////////////////////////////////
  
  // 1) check that ExorLink for this cube pair can be performed
  //    (it may happen that the group is outdated due to recent reshaping)
  // 2) find out what is the improvement achieved by each cube group
  // 3) depending on the distance, do the following:
  //    a) if ( Dist == 2 ) 
  //           try both cube groups, 
  //           if one of them leads to improvement, take the cube group right away
  //           if none of them leads to improment
  //              - take the last one (because it reshapes)
  //              - take the last one only in case it does not increase literals
  //    b) if ( Dist == 3 )
  //           try groups one by one
  //           if one of them leads to improvement, take the group right away
  //           if none of them leads to improvement
  //              - take the group which reshapes
  //              - take the reshaping group only in case it does not increase literals
  //           if none of them leads to reshaping, do not take any of them
  //    c) if ( Dist == 4 )
  //           try groups one by one
  //           if one of the leads to reshaping, take it right away
  //           if none of them leads to reshaping, do not take any of them
  
  ////////////////////////////////////////////////////////////////////////
  ///                       STATIC VARIABLES                           ///
  ////////////////////////////////////////////////////////////////////////
  
  // Cube set is a list of cubes
  static Cube* s_List;
  
  ///////////////////////////////////////////////////////////////////////////
  // undo information
  ///////////////////////////////////////////////////////////////////////////
  static struct
  {
      int fInput;   // 1 if the input was changed
      Cube* p;      // the pointer to the modified cube
      int PrevQa;
      int PrevPa;
      int PrevQq;
      int PrevPq;
      int PrevPz;
      int Var;      // the number of variable that was changed
      int Value;    // the value what was there
      int PrevID;   // the previous ID of the removed cube
  } s_ChangeStore;
  ///////////////////////////////////////////////////////////////////////////
  
  // enable pair accumulation
  // from the begginning (while the starting cover is generated)
  // only the distance 2 accumulation is enabled
  static int s_fDistEnable2 = 1;
  static int s_fDistEnable3;
  static int s_fDistEnable4;
  
  // temporary storage for cubes generated by the ExorLink iterator
  static Cube* s_CubeGroup[5];
  // the marks telling whether the given cube is inserted
  static int s_fInserted[5];
  
  // enable selection only those Dist2 and Dist3 that do not increase literals
  int s_fDecreaseLiterals = 0;
  
  // the counters for display
  static int s_cEnquequed;
  static int s_cAttempts;
  static int s_cReshapes;
  
  // the number of cubes before ExorLink starts
  static int s_nCubesBefore;
  // the distance code specific for each ExorLink
  static cubedist s_Dist;
  
  // other variables
  static int s_Gain;
  static int s_GainTotal;
  static int s_GroupCounter;
  static int s_GroupBest;
  static Cube *s_pC1, *s_pC2;
  
  ////////////////////////////////////////////////////////////////////////
  ///                  Iterative ExorLink Operation                    ///
  ////////////////////////////////////////////////////////////////////////
  
  int CheckAndInsert( Cube* p )
  {
  //  return CheckForCloseCubes( p, 1 );
      CubeInsert( p );
      return 0;
  }
  
  int IterativelyApplyExorLink2( char fDistEnable )   
  // MEMO: instead of inserting the cubes that have already been checked
  // by running CheckForCloseCubes again, try inserting them without checking
  // and observe the difference (it will save 50% of checking time)
  {
      int z;
  
      // this var is specific to ExorLink-2
      s_Dist = (cubedist)0;
  
      // enable pair accumulation
      s_fDistEnable2 = fDistEnable & 1;
      s_fDistEnable3 = fDistEnable & 2;
      s_fDistEnable4 = fDistEnable & 4;
  
      // initialize counters
      s_cEnquequed = GetQuequeStats( s_Dist );
      s_cAttempts  = 0;
      s_cReshapes  = 0;
  
      // remember the number of cubes before minimization
      s_nCubesBefore = g_CoverInfo.nCubesInUse;
  
      for ( z = IteratorCubePairStart( s_Dist, &s_pC1, &s_pC2 ); z; z = IteratorCubePairNext() )
      {
          s_cAttempts++;
          // start ExorLink of the given Distance
          if ( ExorLinkCubeIteratorStart( s_CubeGroup, s_pC1, s_pC2, s_Dist ) )
          {
              // extract old cubes from storage (to prevent EXORing with their derivitives)
              CubeExtract( s_pC1 );
              CubeExtract( s_pC2 );
  
              // mark the current position in the cube pair queques
              MarkSet();
  
              // check the first group (generated by ExorLinkCubeIteratorStart())
              if ( CheckForCloseCubes( s_CubeGroup[0], 0 ) ) 
              {  // the first cube leads to improvement - it is already inserted
                  CheckForCloseCubes( s_CubeGroup[1], 1 ); // insert the second cube
                  goto SUCCESS;
              }
              if ( CheckForCloseCubes( s_CubeGroup[1], 0 ) ) 
              {  // the second cube leads to improvement - it is already inserted
                  CheckForCloseCubes( s_CubeGroup[0], 1 ); // insert the first cube
  //              CheckAndInsert( s_CubeGroup[0] );
                  goto SUCCESS;
              }
              // the first group does not lead to improvement
  
              // rewind to the previously marked position in the cube pair queques
              MarkRewind();
  
              // generate the second group
              ExorLinkCubeIteratorNext( s_CubeGroup );
  
              // check the second group
              if ( CheckForCloseCubes( s_CubeGroup[0], 0 ) ) 
              { // the first cube leads to improvement - it is already inserted
                  CheckForCloseCubes( s_CubeGroup[1], 1 ); // insert the second cube
                  goto SUCCESS;
              }
              if ( CheckForCloseCubes( s_CubeGroup[1], 0 ) ) 
              { // the second cube leads to improvement - it is already inserted
                  CheckForCloseCubes( s_CubeGroup[0], 1 ); // insert the first cube
  //              CheckAndInsert( s_CubeGroup[0] );
                  goto SUCCESS;
              }
              // the second group does not lead to improvement
  
              // decide whether to accept the second group, depending on literals
              if ( s_fDecreaseLiterals )
              {
                  if ( g_CoverInfo.fUseQCost ? 
                       s_CubeGroup[0]->q + s_CubeGroup[1]->q >= s_pC1->q + s_pC2->q :
                       s_CubeGroup[0]->a + s_CubeGroup[1]->a >= s_pC1->a + s_pC2->a ) 
                  // the group increases literals
                  { // do not take the last group
                              
                      // rewind to the previously marked position in the cube pair queques
                      MarkRewind();
  
                      // return the old cubes back to storage
                      CubeInsert( s_pC1 );
                      CubeInsert( s_pC2 );
                      // clean the results of generating ExorLinked cubes
                      ExorLinkCubeIteratorCleanUp( 0 );
                      continue;
                  }
              }
  
              // take the last group
              // there is no need to test these cubes again,
              // because they have been tested and did not yield any improvement
              CubeInsert( s_CubeGroup[0] );
              CubeInsert( s_CubeGroup[1] );
  //          CheckForCloseCubes( s_CubeGroup[0], 1 ); 
  //          CheckForCloseCubes( s_CubeGroup[1], 1 ); 
  
  SUCCESS:
              // clean the results of generating ExorLinked cubes
              ExorLinkCubeIteratorCleanUp( 1 ); // take the last group
              // free old cubes
              AddToFreeCubes( s_pC1 );
              AddToFreeCubes( s_pC2 );
              // increate the counter
              s_cReshapes++;
          }
      }
      // print the report
      if ( g_CoverInfo.Verbosity == 2 )
      {
      printf( "ExLink-%d", 2 );
      printf( ": Que= %5d", s_cEnquequed );
      printf( "  Att= %4d", s_cAttempts );
      printf( "  Resh= %4d", s_cReshapes );
      printf( "  NoResh= %4d", s_cAttempts - s_cReshapes );
      printf( "  Cubes= %3d", g_CoverInfo.nCubesInUse );
      printf( "  (%d)", s_nCubesBefore - g_CoverInfo.nCubesInUse );
      printf( "  Lits= %5d", CountLiterals() );
      printf( "  QCost = %6d", CountQCost() );
      printf( "\n" );
      }
  
      // return the number of cubes gained in the process
      return s_nCubesBefore - g_CoverInfo.nCubesInUse;
  }
  
  int IterativelyApplyExorLink3( char fDistEnable )   
  {
      int z, c, d;
      // this var is specific to ExorLink-3
      s_Dist = (cubedist)1;
  
      // enable pair accumulation
      s_fDistEnable2 = fDistEnable & 1;
      s_fDistEnable3 = fDistEnable & 2;
      s_fDistEnable4 = fDistEnable & 4;
  
      // initialize counters
      s_cEnquequed = GetQuequeStats( s_Dist );
      s_cAttempts  = 0;
      s_cReshapes  = 0;
  
      // remember the number of cubes before minimization
      s_nCubesBefore = g_CoverInfo.nCubesInUse;
  
      for ( z = IteratorCubePairStart( s_Dist, &s_pC1, &s_pC2 ); z; z = IteratorCubePairNext() )
      {
          s_cAttempts++;
          // start ExorLink of the given Distance
          if ( ExorLinkCubeIteratorStart( s_CubeGroup, s_pC1, s_pC2, s_Dist ) )
          {
              // extract old cubes from storage (to prevent EXORing with their derivitives)
              CubeExtract( s_pC1 );
              CubeExtract( s_pC2 );
  
              // mark the current position in the cube pair queques
              MarkSet();
  
              // check cube groups one by one
              s_GroupCounter = 0;
              do  
              {   // check the cubes of this group one by one
                  for ( c = 0; c < 3; c++ )
                  if ( !s_CubeGroup[c]->fMark ) // this cube has not yet been checked
                  {
                      s_Gain = CheckForCloseCubes( s_CubeGroup[c], 0 ); // do not insert the cube, by default
                      if ( s_Gain ) 
                      { // this cube leads to improvement or reshaping - it is already inserted
  
                          // decide whether to accept this group based on literal count
                          if ( s_fDecreaseLiterals && s_Gain == 1 )
                          if ( g_CoverInfo.fUseQCost ?
                               s_CubeGroup[0]->q + s_CubeGroup[1]->q + s_CubeGroup[2]->q > s_pC1->q + s_pC2->q + s_ChangeStore.PrevQq :
                               s_CubeGroup[0]->a + s_CubeGroup[1]->a + s_CubeGroup[2]->a > s_pC1->a + s_pC2->a + s_ChangeStore.PrevQa 
                             ) // the group increases literals
                          { // do not take this group
                              // remember the group
                              s_GroupBest = s_GroupCounter;
                              // undo changes to be able to continue checking other groups
                              UndoRecentChanges();
                              break;
                          }
  
                          // take this group
                          for ( d = 0; d < 3; d++ ) // insert other cubes
                              if ( d != c )
                              {
                                  CheckForCloseCubes( s_CubeGroup[d], 1 ); 
  //                              if ( s_CubeGroup[d]->fMark )
  //                                  CheckAndInsert( s_CubeGroup[d] );
  //                                  CheckOnlyOneCube( s_CubeGroup[d] );
  //                                  CheckForCloseCubes( s_CubeGroup[d], 1 ); 
  //                              else
  //                                  CheckForCloseCubes( s_CubeGroup[d], 1 ); 
                              }
  
                          // clean the results of generating ExorLinked cubes
                          ExorLinkCubeIteratorCleanUp( 1 ); // take the last group
                          // free old cubes
                          AddToFreeCubes( s_pC1 );
                          AddToFreeCubes( s_pC2 );
                          // update the counter
                          s_cReshapes++;
                          goto END_OF_LOOP;
                      }
                      else // mark the cube as checked
                          s_CubeGroup[c]->fMark = 1;
                  }
                  // the group is not taken - find the new group
                  s_GroupCounter++;
                                          
                  // rewind to the previously marked position in the cube pair queques
                  MarkRewind();
              } 
              while ( ExorLinkCubeIteratorNext( s_CubeGroup ) );
              // none of the groups leads to improvement
  
              // return the old cubes back to storage
              CubeInsert( s_pC1 );
              CubeInsert( s_pC2 );
              // clean the results of generating ExorLinked cubes
              ExorLinkCubeIteratorCleanUp( 0 );
          }
  END_OF_LOOP: {}
      }
  
      // print the report
      if ( g_CoverInfo.Verbosity == 2 )
      {
      printf( "ExLink-%d", 3 );
      printf( ": Que= %5d", s_cEnquequed );
      printf( "  Att= %4d", s_cAttempts );
      printf( "  Resh= %4d", s_cReshapes );
      printf( "  NoResh= %4d", s_cAttempts - s_cReshapes );
      printf( "  Cubes= %3d", g_CoverInfo.nCubesInUse );
      printf( "  (%d)", s_nCubesBefore - g_CoverInfo.nCubesInUse );
      printf( "  Lits= %5d", CountLiterals() );
      printf( "  QCost = %6d", CountQCost() );
      printf( "\n" );
      }
  
      // return the number of cubes gained in the process
      return s_nCubesBefore - g_CoverInfo.nCubesInUse;
  }
  
  int IterativelyApplyExorLink4( char fDistEnable )   
  {
      int z, c;
      // this var is specific to ExorLink-4
      s_Dist = (cubedist)2;
  
      // enable pair accumulation
      s_fDistEnable2 = fDistEnable & 1;
      s_fDistEnable3 = fDistEnable & 2;
      s_fDistEnable4 = fDistEnable & 4;
  
      // initialize counters
      s_cEnquequed = GetQuequeStats( s_Dist );
      s_cAttempts  = 0;
      s_cReshapes  = 0;
  
      // remember the number of cubes before minimization
      s_nCubesBefore = g_CoverInfo.nCubesInUse;
  
      for ( z = IteratorCubePairStart( s_Dist, &s_pC1, &s_pC2 ); z; z = IteratorCubePairNext() )
      {
          s_cAttempts++;
          // start ExorLink of the given Distance
          if ( ExorLinkCubeIteratorStart( s_CubeGroup, s_pC1, s_pC2, s_Dist ) )
          {
              // extract old cubes from storage (to prevent EXORing with their derivitives)
              CubeExtract( s_pC1 );
              CubeExtract( s_pC2 );
  
              // mark the current position in the cube pair queques
              MarkSet();
  
              // check cube groups one by one
              do  
              {   // check the cubes of this group one by one
                  s_GainTotal = 0;
                  for ( c = 0; c < 4; c++ )
                  if ( !s_CubeGroup[c]->fMark ) // this cube has not yet been checked
                  {
                      s_Gain = CheckForCloseCubes( s_CubeGroup[c], 0 ); // do not insert the cube, by default
                      // if the cube leads to gain, it is already inserted
                      s_fInserted[c] = (int)(s_Gain>0);
                      // increment the total gain
                      s_GainTotal += s_Gain;
                  }
                  else
                      s_fInserted[c] = 0; // the cube has already been checked - it is not inserted
  
                  if ( s_GainTotal == 0 ) // the group does not lead to any gain
                  { // mark the cubes
                      for ( c = 0; c < 4; c++ )
                          s_CubeGroup[c]->fMark = 1;
                  }
                  else if ( s_GainTotal == 1 ) // the group does not lead to substantial gain, too
                  { 
                      // undo changes to be able to continue checking groups
                      UndoRecentChanges();
                      // mark those cubes that were not inserted
                      for ( c = 0; c < 4; c++ )
                          s_CubeGroup[c]->fMark = !s_fInserted[c];
                  }
                  else // if ( s_GainTotal > 1 ) // the group reshapes or improves
                  { // accept the group
                      for ( c = 0; c < 4; c++ ) // insert other cubes
                          if ( !s_fInserted[c] )
                              CheckForCloseCubes( s_CubeGroup[c], 1 ); 
  //                          CheckAndInsert( s_CubeGroup[c] );
                      // clean the results of generating ExorLinked cubes
                      ExorLinkCubeIteratorCleanUp( 1 ); // take the last group
                      // free old cubes
                      AddToFreeCubes( s_pC1 );
                      AddToFreeCubes( s_pC2 );
                      // update the counter
                      s_cReshapes++;
                      goto END_OF_LOOP;
                  }
                                          
                  // rewind to the previously marked position in the cube pair queques
                  MarkRewind();
              } 
              while ( ExorLinkCubeIteratorNext( s_CubeGroup ) );
              // none of the groups leads to improvement
  
              // return the old cubes back to storage
              CubeInsert( s_pC1 );
              CubeInsert( s_pC2 );
              // clean the results of generating ExorLinked cubes
              ExorLinkCubeIteratorCleanUp( 0 );
          }
  END_OF_LOOP: {}
      }
  
      // print the report
      if ( g_CoverInfo.Verbosity == 2 )
      {
      printf( "ExLink-%d", 4 );
      printf( ": Que= %5d", s_cEnquequed );
      printf( "  Att= %4d", s_cAttempts );
      printf( "  Resh= %4d", s_cReshapes );
      printf( "  NoResh= %4d", s_cAttempts - s_cReshapes );
      printf( "  Cubes= %3d", g_CoverInfo.nCubesInUse );
      printf( "  (%d)", s_nCubesBefore - g_CoverInfo.nCubesInUse );
      printf( "  Lits= %5d", CountLiterals() );
      printf( "  QCost = %6d", CountQCost() );
      printf( "\n" );
      }
  
      // return the number of cubes gained in the process
      return s_nCubesBefore - g_CoverInfo.nCubesInUse;
  }
  
  // local static variables
  Cube* s_q;
  int s_Distance;
  int s_DiffVarNum;
  int s_DiffVarValueP_old;
  int s_DiffVarValueP_new;
  int s_DiffVarValueQ;
  
  int CheckForCloseCubes( Cube* p, int fAddCube )
  // checks the cube storage for a cube that is dist-0 and dist-1 removed 
  // from the given one (p) if such a cube is found, extracts it from the data 
  // structure, EXORs it with the given cube, adds the resultant cube
  // to the data structure and performed the same check for the resultant cube;
  // returns the number of cubes gained in the process of reduction;
  // if an adjacent cube is not found, inserts the cube only if (fAddCube==1)!!!
  {
      // start the new range
      NewRangeReset();
  
      for ( s_q = s_List; s_q; s_q = s_q->Next )
      {
          s_Distance = GetDistancePlus( p, s_q );
          if ( s_Distance > 4 )
          {
          }
          else if ( s_Distance == 4 )
          {
              if ( s_fDistEnable4 ) 
                  NewRangeInsertCubePair( DIST4, p, s_q );
          }
          else if ( s_Distance == 3 )
          {
              if ( s_fDistEnable3 ) 
                  NewRangeInsertCubePair( DIST3, p, s_q );
          }
          else if ( s_Distance == 2 )
          { 
              if ( s_fDistEnable2 ) 
                  NewRangeInsertCubePair( DIST2, p, s_q );
          }
          else if ( s_Distance == 1 )
          {   // extract the cube from the data structure
  
              //////////////////////////////////////////////////////////
              // store the changes
              s_ChangeStore.fInput = (s_DiffVarNum != -1);
              s_ChangeStore.p      = p;
              s_ChangeStore.PrevQa = s_q->a;
              s_ChangeStore.PrevPa = p->a;
              s_ChangeStore.PrevQq = s_q->q;
              s_ChangeStore.PrevPq = p->q;
              s_ChangeStore.PrevPz = p->z;
              s_ChangeStore.Var    = s_DiffVarNum;
              s_ChangeStore.Value  = s_DiffVarValueQ;
              s_ChangeStore.PrevID = s_q->ID;
              //////////////////////////////////////////////////////////
  
              CubeExtract( s_q );
              // perform the EXOR of the two cubes and write the result into p
  
              // it is important that the resultant cube is written into p!!!
  
              if ( s_DiffVarNum == -1 )
              {
                  int i;
                  // exor the output part
                  p->z = 0;
                  for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
                  {
                      p->pCubeDataOut[i] ^= s_q->pCubeDataOut[i];
                      p->z += BIT_COUNT(p->pCubeDataOut[i]);
                  }
              }
              else
              {
                  // the cube has already been updated by GetDistancePlus()
  
                  // modify the parameters of the number of literals in the new cube
  //              p->a += s_UpdateLiterals[ s_DiffVarValueP ][ s_DiffVarValueQ ];
                  if ( s_DiffVarValueP_old == VAR_NEG || s_DiffVarValueP_old == VAR_POS )
                      p->a--;
                  if ( s_DiffVarValueP_new == VAR_NEG || s_DiffVarValueP_new == VAR_POS )
                      p->a++;
                  p->q = ComputeQCostBits(p);
              }
  
              // move q to the free cube list
              AddToFreeCubes( s_q );
  
              // make sure that nobody with use the pairs created so far
  //          NewRangeReset();
              // call the function again for the new cube
              return 1 + CheckForCloseCubes( p, 1 );
          }
          else // if ( Distance == 0 )
          {   // extract the second cube from the data structure and add them both to the free list
              AddToFreeCubes( p );
              AddToFreeCubes( CubeExtract( s_q ) );
  
              // make sure that nobody with use the pairs created so far
              NewRangeReset();
              return 2;
          }
      }
      
      // add the cube to the data structure if needed
      if ( fAddCube )
          CubeInsert( p );
  
      // add temporarily stored new range of cube pairs to the queque
      NewRangeAdd();
  
      return 0;
  }
  
  void UndoRecentChanges()
  {
      Cube * p, * q;
      // get back cube q that was deleted
      q = GetFreeCube();
      // restore the ID
      q->ID = s_ChangeStore.PrevID;
      // insert the cube into storage again
      CubeInsert( q );
  
      // extract cube p
      p = CubeExtract( s_ChangeStore.p );
  
      // modify it back
      if ( s_ChangeStore.fInput ) // the input has changed
      {
          ExorVar( p, s_ChangeStore.Var, (varvalue)s_ChangeStore.Value );
          p->a = s_ChangeStore.PrevPa;
          p->q = s_ChangeStore.PrevPq;
          // p->z did not change
      }
      else // if ( s_ChangeStore.fInput ) // the output has changed
      {
          int i;
          for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
              p->pCubeDataOut[i] ^= q->pCubeDataOut[i];
          p->z = s_ChangeStore.PrevPz;
          // p->a did not change
      }
  }
  
  ///////////////////////////////////////////////////////////////////
  ///               CUBE SET MANIPULATION PROCEDURES              ///
  ///////////////////////////////////////////////////////////////////
  
  // Cube set is a list of cubes
  //static Cube* s_List;
  
  ///////////////////////////////////////////////////////////////////
  ///                 Memory Allocation/Delocation                ///
  ///////////////////////////////////////////////////////////////////
  
  int AllocateCubeSets( int nVarsIn, int nVarsOut )
  {
      s_List = NULL;
  
      // clean other data
      s_fDistEnable2 = 1;
      s_fDistEnable3 = 0;
      s_fDistEnable4 = 0;
      memset( s_CubeGroup, 0, sizeof(void *) * 5 );
      memset( s_fInserted, 0, sizeof(int) * 5 );
      s_fDecreaseLiterals = 0;
      s_cEnquequed = 0;
      s_cAttempts = 0;
      s_cReshapes = 0;
      s_nCubesBefore = 0;
      s_Gain = 0;
      s_GainTotal = 0;
      s_GroupCounter = 0;
      s_GroupBest = 0;
      s_pC1 = s_pC2 = NULL;
  
      return 4;
  }
  
  void DelocateCubeSets()
  {
  }
  
  ///////////////////////////////////////////////////////////////////
  ///                     Insertion Operators                     ///
  ///////////////////////////////////////////////////////////////////
  
  void CubeInsert( Cube* p )
  // inserts the cube into storage (puts it at the beginning of the list)
  {
      assert( p->Prev == NULL && p->Next == NULL );
      assert( p->ID );
  
      if ( s_List == NULL )
          s_List = p;
      else
      {
          p->Next = s_List;
  
          s_List->Prev = p;
          s_List = p;
      }
  
      g_CoverInfo.nCubesInUse++;
  }
  
  Cube* CubeExtract( Cube* p )
  // extracts the cube from storage
  {
  //  assert( p->Prev && p->Next ); // can be done only with rings
      assert( p->ID );
  
  //  if ( s_List == p )
  //      s_List = p->Next;
  //  if ( p->Prev )
  //      p->Prev->Next = p->Next;
  
      if ( s_List == p )
          s_List = p->Next;
      else
          p->Prev->Next = p->Next;
  
      if ( p->Next )
          p->Next->Prev = p->Prev;
  
      p->Prev = NULL;
      p->Next = NULL;
  
      g_CoverInfo.nCubesInUse--;
      return p;
  }
  
  ///////////////////////////////////////////////////////////////////
  ///                       CUBE ITERATOR                         ///
  ///////////////////////////////////////////////////////////////////
  
  // the iterator starts from the Head and stops when it sees NULL
  Cube* s_pCubeLast;
  
  ///////////////////////////////////////////////////////////////////
  ///                     Cube Set Iterator                       ///
  ///////////////////////////////////////////////////////////////////
  
  Cube* IterCubeSetStart()
  // starts an iterator that traverses all the cubes in the ring
  {
      assert( s_pCubeLast == NULL );
  
      // check whether the List has cubes
      if ( s_List == NULL )
          return NULL;
  
      return ( s_pCubeLast = s_List );
  }
  
  Cube* IterCubeSetNext()
  // returns the next cube in the cube set
  // to use it again after it has returned NULL, first call IterCubeSetStart()
  {
      assert( s_pCubeLast );
      return ( s_pCubeLast = s_pCubeLast->Next );
  }
  
  ///////////////////////////////////////////////////////////////////
  ////                      ADJACENCY QUEQUES                  //////
  ///////////////////////////////////////////////////////////////////
  
  typedef struct
  {
      Cube** pC1;      // the pointer to the first cube
      Cube** pC2;      // the pointer to the second cube
      byte*  ID1;      // the ID of the first cube
      byte*  ID2;      // the ID of the second cube
      int  PosOut;     // extract position
      int  PosIn;      // insert position
      int  PosCur;     // temporary insert position
      int  PosMark;    // the marked position
      int  fEmpty;     // this flag is 1 if there is nothing in the queque
  } que;
  
  static que s_Que[3];  // Dist-2, Dist-3, Dist-4 queques
  
  // the number of allocated places
  //int s_nPosAlloc;
  // the maximum number of occupied places
  //int s_nPosMax[3];
  
  //////////////////////////////////////////////////////////////////////
  //            Conditional Adding Cube Pairs To Queques              //
  //////////////////////////////////////////////////////////////////////
  
  int GetPosDiff( int PosBeg, int PosEnd )
  {
      return (PosEnd - PosBeg + s_nPosAlloc) % s_nPosAlloc;
  }
  
  void MarkSet()
  // sets marks in the cube pair queques
  {
      s_Que[0].PosMark = s_Que[0].PosIn;
      s_Que[1].PosMark = s_Que[1].PosIn;
      s_Que[2].PosMark = s_Que[2].PosIn;
  }
  
  void MarkRewind()
  // rewinds the queques to the previously set marks
  {
      s_Que[0].PosIn = s_Que[0].PosMark;
      s_Que[1].PosIn = s_Que[1].PosMark;
      s_Que[2].PosIn = s_Que[2].PosMark;
  }
  
  void NewRangeReset()
  // resets temporarily stored new range of cube pairs
  {
      s_Que[0].PosCur = s_Que[0].PosIn;
      s_Que[1].PosCur = s_Que[1].PosIn;
      s_Que[2].PosCur = s_Que[2].PosIn;
  }
  
  void NewRangeAdd()
  // adds temporarily stored new range of cube pairs to the queque
  {
      s_Que[0].PosIn = s_Que[0].PosCur;
      s_Que[1].PosIn = s_Que[1].PosCur;
      s_Que[2].PosIn = s_Que[2].PosCur;
  }
  
  void NewRangeInsertCubePair( cubedist Dist, Cube* p1, Cube* p2 )
  // insert one cube pair into the new range
  {
      que* p = &s_Que[Dist];
      int Pos = p->PosCur;
  
      if ( p->fEmpty || Pos != p->PosOut )
      {
          p->pC1[Pos] = p1;
          p->pC2[Pos] = p2;
          p->ID1[Pos] = p1->ID;
          p->ID2[Pos] = p2->ID;
  
          p->PosCur = (p->PosCur+1)%s_nPosAlloc;
      }
      else
          assert(0);
  //      cout << endl << "DIST-" << (int)(Dist+2) << ": Have run out of queque space!" << endl;
  }
  
  void PrintQuequeStats()
  {
  /*
      cout << endl << "Queque statistics: ";
      cout << " Alloc = " << s_nPosAlloc;
      cout << "   DIST2 = " << GetPosDiff( s_Que[0].PosOut, s_Que[0].PosIn );
      cout << "   DIST3 = " << GetPosDiff( s_Que[1].PosOut, s_Que[1].PosIn );
      cout << "   DIST4 = " << GetPosDiff( s_Que[2].PosOut, s_Que[2].PosIn );
      cout << endl;
      cout << endl;
  */
  }
  
  int GetQuequeStats( cubedist Dist )
  {
      return GetPosDiff( s_Que[Dist].PosOut, s_Que[Dist].PosIn );
  }
  
  //////////////////////////////////////////////////////////////////////
  //                       Queque Iterators                           //
  //////////////////////////////////////////////////////////////////////
  
  // iterating through the queque (with authomatic garbage collection)
  // only one iterator can be active at a time
  static struct
  {
      int fStarted;    // status of the iterator (1 if working)
      cubedist Dist;   // the currently iterated queque
      Cube** ppC1;     // the position where the first cube pointer goes
      Cube** ppC2;     // the position where the second cube pointer goes
      int PosStop;     // the stop position (to prevent the iterator from
                       // choking when new pairs are added during iteration)
      int CutValue;    // the number of literals below which the cubes are not used
  } s_Iter;
  
  static que* pQ;
  static Cube *p1, *p2;
  
  int IteratorCubePairStart( cubedist CubeDist, Cube** ppC1, Cube** ppC2 )
  // start an iterator through cubes of dist CubeDist,
  // the resulting pointers are written into ppC1 and ppC2
  // returns 1 if the first cube pair is found
  {
      int fEntryFound;
  
      assert( s_Iter.fStarted == 0 );
      assert( CubeDist >= 0 && CubeDist <= 2 );
  
      s_Iter.fStarted = 1;
      s_Iter.Dist = CubeDist;
      s_Iter.ppC1 = ppC1;
      s_Iter.ppC2 = ppC2;
  
      s_Iter.PosStop = s_Que[ CubeDist ].PosIn;
  
      // determine the cut value
  //  s_Iter.CutValue = s_nLiteralsInUse/s_nCubesInUse/2;
      s_Iter.CutValue = -1;
  
      fEntryFound = 0;
      // go through the entries while there is something in the queque
      for ( pQ = &s_Que[ CubeDist ]; pQ->PosOut != s_Iter.PosStop; pQ->PosOut = (pQ->PosOut+1)%s_nPosAlloc )
      {
          p1 = pQ->pC1[ pQ->PosOut ];
          p2 = pQ->pC2[ pQ->PosOut ];
  
          // check whether the entry is valid
          if ( p1->ID == pQ->ID1[ pQ->PosOut ] && 
               p2->ID == pQ->ID2[ pQ->PosOut ] ) //&&
               //p1->x + p1->y + p2->x + p2->y > s_Iter.CutValue )
          {
               fEntryFound = 1;
               break;
          }
      }
  
      if ( fEntryFound )
      { // write the result into the pick-up place
          *ppC1 = pQ->pC1[ pQ->PosOut ];
          *ppC2 = pQ->pC2[ pQ->PosOut ];
  
          pQ->PosOut = (pQ->PosOut+1)%s_nPosAlloc;
      }
      else
          s_Iter.fStarted = 0;
      return fEntryFound;
  }
  
  int IteratorCubePairNext()
  // gives the next VALID cube pair (the previous one is automatically dequequed)
  {
      int fEntryFound = 0;
      assert( s_Iter.fStarted );
  
      // go through the entries while there is something in the queque
      for ( pQ = &s_Que[ s_Iter.Dist ]; pQ->PosOut != s_Iter.PosStop; pQ->PosOut = (pQ->PosOut+1)%s_nPosAlloc )
      {
          p1 = pQ->pC1[ pQ->PosOut ];
          p2 = pQ->pC2[ pQ->PosOut ];
  
          // check whether the entry is valid
          if ( p1->ID == pQ->ID1[ pQ->PosOut ] && 
               p2->ID == pQ->ID2[ pQ->PosOut ] ) //&&
               //p1->x + p1->y + p2->x + p2->y > s_Iter.CutValue )
          {
               fEntryFound = 1;
               break;
          }
      }
  
      if ( fEntryFound )
      { // write the result into the pick-up place
          *(s_Iter.ppC1) = pQ->pC1[ pQ->PosOut ];
          *(s_Iter.ppC2) = pQ->pC2[ pQ->PosOut ];
  
          pQ->PosOut = (pQ->PosOut+1)%s_nPosAlloc;
      }
      else // iteration has finished
          s_Iter.fStarted = 0;
  
      return fEntryFound;
  }
  
  //////////////////////////////////////////////////////////////////////
  //                     Allocation/Delocation                        //
  //////////////////////////////////////////////////////////////////////
  
  int AllocateQueques( int nPlaces )
  // nPlaces should be approximately nCubes*nCubes/10
  // allocates memory for cube pair queques
  {
      int i;
      s_nPosAlloc  = nPlaces;
  
      for ( i = 0; i < 3; i++ )
      {
          // clean data
          memset( &s_Que[i], 0, sizeof(que) );
  
          s_Que[i].pC1 = (Cube**) ABC_ALLOC( Cube*, nPlaces );
          s_Que[i].pC2 = (Cube**) ABC_ALLOC( Cube*, nPlaces );
          s_Que[i].ID1 = (byte*) ABC_ALLOC( byte, nPlaces );
          s_Que[i].ID2 = (byte*) ABC_ALLOC( byte, nPlaces );
  
          if ( s_Que[i].pC1==NULL || s_Que[i].pC2==NULL || s_Que[i].ID1==NULL || s_Que[i].ID2==NULL )
              return 0;
  
          s_nPosMax[i] = 0;
          s_Que[i].fEmpty = 1;
      }
  
      return nPlaces * (sizeof(Cube*) + sizeof(Cube*) + 2*sizeof(byte) );
  }
  
  void DelocateQueques()
  {
      int i;
      for ( i = 0; i < 3; i++ )
      {
          ABC_FREE( s_Que[i].pC1 );
          ABC_FREE( s_Que[i].pC2 );
          ABC_FREE( s_Que[i].ID1 );
          ABC_FREE( s_Que[i].ID2 );
      }
  }
  
  ///////////////////////////////////////////////////////////////////
  ////////////              End of File             /////////////////
  ///////////////////////////////////////////////////////////////////
  
  
  ABC_NAMESPACE_IMPL_END
  