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