From 21435aa6e317481f23b510a011e102bd148c7deb Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 10 Aug 2016 14:18:39 -0700 Subject: Bug fix in 'edge -m'. --- src/aig/gia/giaSatLE.c | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/src/aig/gia/giaSatLE.c b/src/aig/gia/giaSatLE.c index d541804a..e6049322 100644 --- a/src/aig/gia/giaSatLE.c +++ b/src/aig/gia/giaSatLE.c @@ -867,25 +867,31 @@ int Sle_ManAddEdgeConstraints( Sle_Man_t * p, int nEdges ) ***********************************************************************/ void Sle_ManDeriveResult( Sle_Man_t * p, Vec_Int_t * vEdge2, Vec_Int_t * vMapping ) { + Vec_Int_t * vMapTemp; int iObj; // create mapping Vec_IntFill( vMapping, Gia_ManObjNum(p->pGia), 0 ); Gia_ManForEachAndId( p->pGia, iObj ) { int i, iCut, iCutVar0 = Vec_IntEntry( p->vCutFirst, iObj ); - int * pCut, * pList = Sle_ManList( p, iObj ); + int * pCut, * pCutThis = NULL, * pList = Sle_ManList( p, iObj ); if ( !sat_solver_var_value(p->pSat, iObj) ) continue; Sle_ForEachCut( pList, pCut, iCut ) if ( sat_solver_var_value(p->pSat, iCutVar0 + iCut) ) - break; - assert( iCut < Sle_ListCutNum(pList) ); + { + assert( pCutThis == NULL ); + pCutThis = pCut; + } + assert( pCutThis != NULL ); Vec_IntWriteEntry( vMapping, iObj, Vec_IntSize(vMapping) ); - Vec_IntPush( vMapping, Sle_CutSize(pCut) ); - for ( i = 0; i < Sle_CutSize(pCut); i++ ) - Vec_IntPush( vMapping, Sle_CutLeaves(pCut)[i] ); + Vec_IntPush( vMapping, Sle_CutSize(pCutThis) ); + for ( i = 0; i < Sle_CutSize(pCutThis); i++ ) + Vec_IntPush( vMapping, Sle_CutLeaves(pCutThis)[i] ); Vec_IntPush( vMapping, iObj ); } + vMapTemp = p->pGia->vMapping; + p->pGia->vMapping = vMapping; // collect edges Vec_IntClear( vEdge2 ); Gia_ManForEachAndId( p->pGia, iObj ) @@ -918,6 +924,7 @@ void Sle_ManDeriveResult( Sle_Man_t * p, Vec_Int_t * vEdge2, Vec_Int_t * vMappin Vec_IntPushTwo( vEdge2, iFanin, iObj ); } } + p->pGia->vMapping = vMapTemp; } /**Function************************************************************* -- cgit v1.2.3 From 9dc2f48858287f62ea801f92c685391f7f161b18 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 15 Aug 2016 08:04:36 +0800 Subject: Changes to report quantum cost in Exorcism. --- src/base/abci/abc.c | 12 ++++++---- src/base/exor/exor.c | 57 +++++++++++++++++++++++++++++++++++++++++++++++- src/base/exor/exor.h | 6 ++++- src/base/exor/exorLink.c | 1 + src/base/exor/exorList.c | 15 ++++++++++--- src/base/exor/exorUtil.c | 22 +++++++++++++++++-- 6 files changed, 102 insertions(+), 11 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 471e6eef..2dab60c9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -40401,13 +40401,13 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Exorcism( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity ); + extern int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity, int fUseQCost ); extern Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose, Vec_Wec_t ** pvRes ); Vec_Wec_t * vEsop = NULL; char * pFileNameOut = NULL; - int c, Quality = 2, Verbosity = 0, fVerbose = 0; + int c, Quality = 2, Verbosity = 0, fUseQCost = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "QVvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "QVqvh" ) ) != EOF ) { switch ( c ) { @@ -40433,6 +40433,9 @@ int Abc_CommandAbc9Exorcism( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( Verbosity < 0 ) goto usage; break; + case 'q': + fUseQCost ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -40452,7 +40455,7 @@ int Abc_CommandAbc9Exorcism( Abc_Frame_t * pAbc, int argc, char ** argv ) pFileNameOut = argv[globalUtilOptind]; // generate starting cover and run minimization Eso_ManCompute( pAbc->pGia, fVerbose, &vEsop ); - Abc_ExorcismMain( vEsop, Gia_ManCiNum(pAbc->pGia), Gia_ManCoNum(pAbc->pGia), pFileNameOut, Quality, Verbosity ); + Abc_ExorcismMain( vEsop, Gia_ManCiNum(pAbc->pGia), Gia_ManCoNum(pAbc->pGia), pFileNameOut, Quality, Verbosity, fUseQCost ); Vec_WecFree( vEsop ); return 0; @@ -40463,6 +40466,7 @@ usage: 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, " : 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 59d524f9..db93d034 100644 --- a/src/base/exor/exor.c +++ b/src/base/exor/exor.c @@ -66,6 +66,57 @@ extern int s_fDecreaseLiterals; /// FUNCTION main() /// //////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Number of negative literals.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int QCost[16][16] = +{ + { 1}, // 0 + { 1, 2}, // 1 + { 5, 5, 6}, // 2 + { 14, 14, 16, 18}, // 3 + { 20, 20, 20, 22, 24}, // 4 + { 32, 32, 32, 34, 36, 38}, // 5 + { 44, 44, 44, 44, 46, 48, 50}, // 6 + { 56, 56, 56, 56, 58, 60, 62, 64}, // 7 + { 0 } +}; +int CountNegLits( Vec_Int_t * vCube ) +{ + int i, Entry, nLits = 0; + Vec_IntForEachEntry( vCube, Entry, i ) + nLits += Abc_LitIsCompl(Entry); + return nLits; +} +int ComputeQCost( Vec_Int_t * vCube ) +{ + return QCost[Abc_MinInt(Vec_IntSize(vCube), 7)][Abc_MinInt(CountNegLits(vCube), 7)]; +} +int ComputeQCostBits( Cube * p ) +{ + extern varvalue GetVar( Cube* pC, int Var ); + int v, nLits = 0, nLitsN = 0; + for ( v = 0; v < g_CoverInfo.nVarsIn; v++ ) + { + int Value = GetVar( p, v ); + if ( Value == VAR_NEG ) + nLitsN++; + else if ( Value == VAR_POS ) + nLits++; + } + nLits += nLitsN; + return QCost[Abc_MinInt(nLits, 7)][Abc_MinInt(nLitsN, 7)]; +} + /**Function************************************************************* Synopsis [] @@ -591,6 +642,7 @@ void AddCubesToStartingCover( Vec_Wec_t * vEsop ) s_Level2Var[i] = i; g_CoverInfo.nLiteralsBefore = 0; + g_CoverInfo.QCostBefore = 0; Vec_WecForEachLevel( vEsop, vCube, c ) { // get the output of this cube @@ -622,6 +674,7 @@ void AddCubesToStartingCover( Vec_Wec_t * vEsop ) // set literal counts pNew->a = Vec_IntSize(vCube); pNew->z = 1; + pNew->q = ComputeQCost(vCube); // set the ID pNew->ID = g_CoverInfo.cIDs++; // skip through zero-ID @@ -632,6 +685,7 @@ void AddCubesToStartingCover( Vec_Wec_t * vEsop ) CheckForCloseCubes( pNew, 1 ); g_CoverInfo.nLiteralsBefore += Vec_IntSize(vCube); + g_CoverInfo.QCostBefore += ComputeQCost(vCube); } ABC_FREE( s_Level2Var ); ABC_FREE( s_LevelValues ); @@ -798,11 +852,12 @@ int Exorcism( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut ) SeeAlso [] ***********************************************************************/ -int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity ) +int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity, int fUseQCost ) { memset( &g_CoverInfo, 0, sizeof(cinfo) ); g_CoverInfo.Quality = Quality; g_CoverInfo.Verbosity = Verbosity; + g_CoverInfo.fUseQCost = fUseQCost; 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 f6bf4990..15a62bbe 100644 --- a/src/base/exor/exor.h +++ b/src/base/exor/exor.h @@ -105,11 +105,14 @@ typedef struct cinfo_tag int nCubesInUse; // number of cubes after simplification int nCubesFree; // number of free cubes int nLiteralsBefore;// number of literals before - int nLiteralsAfter; // number of literals before + int nLiteralsAfter; // number of literals after + int QCostBefore; // q-cost before + int QCostAfter; // q-cost after int cIDs; // the counter of cube IDs int Verbosity; // verbosity level int Quality; // quality + int fUseQCost; // use q-cost instead of literal count abctime TimeRead; // reading time abctime TimeStart; // starting cover computation time @@ -125,6 +128,7 @@ typedef struct cube byte ID; // (almost) unique ID of the cube short a; // the number of literals short z; // the number of 1's in the output part + short q; // user cost drow* pCubeDataIn; // a pointer to the bit string representing literals drow* pCubeDataOut; // a pointer to the bit string representing literals struct cube* Prev; // pointers to the previous/next cubes in the list/ring diff --git a/src/base/exor/exorLink.c b/src/base/exor/exorLink.c index 032ed318..fef0d4ca 100644 --- a/src/base/exor/exorLink.c +++ b/src/base/exor/exorLink.c @@ -335,6 +335,7 @@ 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; diff --git a/src/base/exor/exorList.c b/src/base/exor/exorList.c index 6388fbe3..6dc9f231 100644 --- a/src/base/exor/exorList.c +++ b/src/base/exor/exorList.c @@ -222,6 +222,8 @@ static struct 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 @@ -345,7 +347,9 @@ int IterativelyApplyExorLink2( char fDistEnable ) // decide whether to accept the second group, depending on literals if ( s_fDecreaseLiterals ) { - if ( s_CubeGroup[0]->a + s_CubeGroup[1]->a >= s_pC1->a + s_pC2->a ) + 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 @@ -441,8 +445,10 @@ int IterativelyApplyExorLink3( char fDistEnable ) // decide whether to accept this group based on literal count if ( s_fDecreaseLiterals && s_Gain == 1 ) - if ( 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 + 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; @@ -669,6 +675,8 @@ int CheckForCloseCubes( Cube* p, int fAddCube ) 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; @@ -750,6 +758,7 @@ void UndoRecentChanges() { 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 diff --git a/src/base/exor/exorUtil.c b/src/base/exor/exorUtil.c index fb0f40f3..45c9542b 100644 --- a/src/base/exor/exorUtil.c +++ b/src/base/exor/exorUtil.c @@ -108,6 +108,23 @@ int CountLiterals() return LitCounter; } +int CountQCost() +// nCubesAlloc is the number of allocated cubes +{ + extern int ComputeQCostBits( Cube * p ); + Cube* p; + int QCost = 0; + int QCostControl = 0; + for ( p = IterCubeSetStart( ); p; p = IterCubeSetNext() ) + { + QCostControl += p->q; + QCost += ComputeQCostBits( p ); + } +// if ( QCostControl != QCost ) +// printf( "Warning! The recorded number of literals (%d) differs from the actual number (%d)\n", QCostControl, QCost ); + return QCost; +} + void WriteTableIntoFile( FILE * pFile ) // nCubesAlloc is the number of allocated cubes @@ -175,13 +192,14 @@ int WriteResultIntoFile( char * pFileName ) TimeStr = asctime( localtime( <ime ) ); // get the number of literals g_CoverInfo.nLiteralsAfter = CountLiterals(); + 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 ); fprintf( pFile, "# Minimization performed %s", TimeStr ); fprintf( pFile, "# Initial statistics: " ); - fprintf( pFile, "Cubes = %d Literals = %d\n", g_CoverInfo.nCubesBefore, g_CoverInfo.nLiteralsBefore ); + fprintf( pFile, "Cubes = %d Literals = %d QCost = %d\n", g_CoverInfo.nCubesBefore, g_CoverInfo.nLiteralsBefore, g_CoverInfo.QCostBefore ); fprintf( pFile, "# Final statistics: " ); - fprintf( pFile, "Cubes = %d Literals = %d\n", g_CoverInfo.nCubesInUse, g_CoverInfo.nLiteralsAfter ); + fprintf( pFile, "Cubes = %d Literals = %d QCost = %d\n", g_CoverInfo.nCubesInUse, g_CoverInfo.nLiteralsAfter, g_CoverInfo.QCostAfter ); fprintf( pFile, "# File reading and reordering time = %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeRead) ); fprintf( pFile, "# Starting cover generation time = %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeStart) ); fprintf( pFile, "# Pure ESOP minimization time = %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeMin) ); -- cgit v1.2.3