mirror of https://github.com/YosysHQ/abc.git
1157 lines
40 KiB
C
1157 lines
40 KiB
C
/**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
|