Changes to report quantum cost in Exorcism.

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, "        <file>: 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( &ltime ) );
     // 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) );