From 118eea846560750b60f69f11a9e546378a7c9bc7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 17 Aug 2016 21:26:16 +0900 Subject: Changes to report quantum cost in Exorcism. --- src/aig/gia/giaEsop.c | 2 +- src/base/abci/abc.c | 4 ++-- src/base/exor/exor.c | 48 +++++++++++++++++++++++++++++++++++++++++------- src/base/exor/exor.h | 6 ++++++ src/base/exor/exorLink.c | 20 +++++++++++--------- src/base/exor/exorList.c | 7 +++++++ src/base/exor/exorUtil.c | 14 ++++++++++---- 7 files changed, 78 insertions(+), 23 deletions(-) diff --git a/src/aig/gia/giaEsop.c b/src/aig/gia/giaEsop.c index db69bf02..13627c0c 100644 --- a/src/aig/gia/giaEsop.c +++ b/src/aig/gia/giaEsop.c @@ -167,7 +167,7 @@ Vec_Wec_t * Eso_ManCoverDerive( Eso_Man_t * p, Vec_Ptr_t * vCover ) } } } - assert( Vec_WecSize(vRes) == Vec_WecCap(vRes) ); + assert( Abc_MaxInt(Vec_WecSize(vRes), 8) == Vec_WecCap(vRes) ); return vRes; } Gia_Man_t * Eso_ManCoverConvert( Eso_Man_t * p, Vec_Ptr_t * vCover ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2dab60c9..8032a426 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -40460,13 +40460,13 @@ int Abc_CommandAbc9Exorcism( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &exorcism [-Q N] [-V N] \n" ); + Abc_Print( -2, "usage: &exorcism [-Q N] [-V N] [-q] \n" ); Abc_Print( -2, " performs heuristic exclusive sum-of-project minimization\n" ); Abc_Print( -2, " -Q N : minimization quality [default = %d]\n", Quality); Abc_Print( -2, " increasing this number improves quality and adds to runtime\n"); Abc_Print( -2, " -V N : verbosity level [default = %d]\n", Verbosity); Abc_Print( -2, " 0 = no output; 1 = outline; 2 = verbose\n"); -// Abc_Print( -2, " -q : toggle using quantum cost [default = %s]\n", fUseQCost? "yes": "no" ); + Abc_Print( -2, " -q : toggle using quantum cost [default = %s]\n", fUseQCost? "yes": "no" ); Abc_Print( -2, " : the output file name in ESOP-PLA format\n"); Abc_Print( -2, "\n" ); return 1; diff --git a/src/base/exor/exor.c b/src/base/exor/exor.c index db93d034..2b8f0903 100644 --- a/src/base/exor/exor.c +++ b/src/base/exor/exor.c @@ -90,16 +90,48 @@ static int QCost[16][16] = { 56, 56, 56, 56, 58, 60, 62, 64}, // 7 { 0 } }; -int CountNegLits( Vec_Int_t * vCube ) +int GetQCost( int nVars, int nNegs ) { - int i, Entry, nLits = 0; - Vec_IntForEachEntry( vCube, Entry, i ) - nLits += Abc_LitIsCompl(Entry); - return nLits; + int Extra; + assert( nVars >= nNegs ); + if ( nVars == 0 ) + return 1; + if ( nVars == 1 ) + { + if ( nNegs == 0 ) return 1; + if ( nNegs == 1 ) return 2; + } + if ( nVars == 2 ) + { + if ( nNegs <= 1 ) return 5; + if ( nNegs == 2 ) return 6; + } + if ( nVars == 3 ) + { + if ( nNegs <= 1 ) return 14; + if ( nNegs == 2 ) return 16; + if ( nNegs == 3 ) return 18; + } + Extra = nNegs - nVars/2; + return 20 + 12 * (nVars - 4) + (Extra > 0 ? 2 * Extra : 0); + +} +void GetQCostTest() +{ + int i, k, Limit = 10; + for ( i = 0; i < Limit; i++ ) + { + for ( k = 0; k <= i; k++ ) + printf( "%4d ", GetQCost(i, k) ); + printf( "\n" ); + } } int ComputeQCost( Vec_Int_t * vCube ) { - return QCost[Abc_MinInt(Vec_IntSize(vCube), 7)][Abc_MinInt(CountNegLits(vCube), 7)]; + int i, Entry, nLitsN = 0; + Vec_IntForEachEntry( vCube, Entry, i ) + nLitsN += Abc_LitIsCompl(Entry); + return GetQCost( Vec_IntSize(vCube), nLitsN ); } int ComputeQCostBits( Cube * p ) { @@ -114,7 +146,7 @@ int ComputeQCostBits( Cube * p ) nLits++; } nLits += nLitsN; - return QCost[Abc_MinInt(nLits, 7)][Abc_MinInt(nLitsN, 7)]; + return GetQCost( nLits, nLitsN ); } /**Function************************************************************* @@ -858,6 +890,8 @@ int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOu g_CoverInfo.Quality = Quality; g_CoverInfo.Verbosity = Verbosity; g_CoverInfo.fUseQCost = fUseQCost; + if ( fUseQCost ) + s_fDecreaseLiterals = 1; if ( g_CoverInfo.Verbosity ) { printf( "\nEXORCISM, Ver.4.7: Exclusive Sum-of-Product Minimizer\n" ); diff --git a/src/base/exor/exor.h b/src/base/exor/exor.h index 15a62bbe..019b66c5 100644 --- a/src/base/exor/exor.h +++ b/src/base/exor/exor.h @@ -167,6 +167,12 @@ extern int FindDiffVars( int *pDiffVars, Cube* pC1, Cube* pC2 ); // determines the variables that are different in cubes pC1 and pC2 // returns the number of variables +extern int ComputeQCost( Vec_Int_t * vCube ); +extern int ComputeQCostBits( Cube * p ); + +extern int CountLiterals(); +extern int CountQCost(); + //////////////////////////////////////////////////////////////////////// /// VARVALUE and CUBEDIST enum typedefs /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/exor/exorLink.c b/src/base/exor/exorLink.c index fef0d4ca..2d260a27 100644 --- a/src/base/exor/exorLink.c +++ b/src/base/exor/exorLink.c @@ -335,7 +335,6 @@ static int DiffVarBits[5]; static drow MaskLiterals; // the base for counting literals static int StartingLiterals; -static int StartingQCost; // the number of literals in each cube static int CubeLiterals[32]; static int BitShift; @@ -525,9 +524,6 @@ int ExorLinkCubeIteratorStart( Cube** pGroup, Cube* pC1, Cube* pC2, cubedist Dis NewZ += BIT_COUNT(Temp); } } - // set the number of literals - ELCubes[CubeNum]->a = StartingLiterals + CubeLiterals[CubeNum]; - ELCubes[CubeNum]->z = NewZ; // set the variables that should be there for ( i = 0; i < nDiffVarsIn; i++ ) @@ -536,6 +532,11 @@ int ExorLinkCubeIteratorStart( Cube** pGroup, Cube* pC1, Cube* pC2, cubedist Dis ELCubes[CubeNum]->pCubeDataIn[ DiffVarWords[i] ] |= ( Value << DiffVarBits[i] ); } + // set the number of literals + ELCubes[CubeNum]->a = StartingLiterals + CubeLiterals[CubeNum]; + ELCubes[CubeNum]->z = NewZ; + ELCubes[CubeNum]->q = ComputeQCostBits( ELCubes[CubeNum] ); + // assign the ID ELCubes[CubeNum]->ID = g_CoverInfo.cIDs++; // skip through zero-ID @@ -645,11 +646,6 @@ int ExorLinkCubeIteratorNext( Cube** pGroup ) NewZ += BIT_COUNT(Temp); } } - // set the number of literals and output ones - ELCubes[CubeNum]->a = StartingLiterals + CubeLiterals[CubeNum]; - ELCubes[CubeNum]->z = NewZ; - - assert( NewZ != 255 ); // set the variables that should be there for ( i = 0; i < nDiffVarsIn; i++ ) @@ -658,6 +654,12 @@ int ExorLinkCubeIteratorNext( Cube** pGroup ) ELCubes[CubeNum]->pCubeDataIn[ DiffVarWords[i] ] |= ( Value << DiffVarBits[i] ); } + // set the number of literals and output ones + ELCubes[CubeNum]->a = StartingLiterals + CubeLiterals[CubeNum]; + ELCubes[CubeNum]->z = NewZ; + ELCubes[CubeNum]->q = ComputeQCostBits( ELCubes[CubeNum] ); + assert( NewZ != 255 ); + // assign the ID ELCubes[CubeNum]->ID = g_CoverInfo.cIDs++; // skip through zero-ID diff --git a/src/base/exor/exorList.c b/src/base/exor/exorList.c index 6dc9f231..18b11c6f 100644 --- a/src/base/exor/exorList.c +++ b/src/base/exor/exorList.c @@ -393,6 +393,8 @@ SUCCESS: 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" ); } @@ -510,6 +512,8 @@ END_OF_LOOP: {} 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" ); } @@ -619,6 +623,8 @@ END_OF_LOOP: {} 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" ); } @@ -709,6 +715,7 @@ int CheckForCloseCubes( Cube* p, int fAddCube ) 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 diff --git a/src/base/exor/exorUtil.c b/src/base/exor/exorUtil.c index 45c9542b..105a6490 100644 --- a/src/base/exor/exorUtil.c +++ b/src/base/exor/exorUtil.c @@ -75,7 +75,15 @@ extern varvalue GetVar( Cube* pC, int Var ); /////////////////////////////////////////////////////////////////// int CountLiterals() -// nCubesAlloc is the number of allocated cubes +{ + Cube* p; + int LitCounter = 0; + for ( p = IterCubeSetStart( ); p; p = IterCubeSetNext() ) + LitCounter += p->a; + return LitCounter; +} + +int CountLiteralsCheck() { Cube* p; int Value, v; @@ -109,9 +117,7 @@ int CountLiterals() } int CountQCost() -// nCubesAlloc is the number of allocated cubes { - extern int ComputeQCostBits( Cube * p ); Cube* p; int QCost = 0; int QCostControl = 0; @@ -191,7 +197,7 @@ int WriteResultIntoFile( char * pFileName ) time( <ime ); TimeStr = asctime( localtime( <ime ) ); // get the number of literals - g_CoverInfo.nLiteralsAfter = CountLiterals(); + g_CoverInfo.nLiteralsAfter = CountLiteralsCheck(); g_CoverInfo.QCostAfter = CountQCost(); fprintf( pFile, "# EXORCISM-4 output for command line arguments: " ); fprintf( pFile, "\"-Q %d -V %d\"\n", g_CoverInfo.Quality, g_CoverInfo.Verbosity ); -- cgit v1.2.3