exorList.cpp

/**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 "eabc/exor.h"

namespace abc::exorcism {

////////////////////////////////////////////////////////////////////////
///                       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             /////////////////
///////////////////////////////////////////////////////////////////


}