Merged alanmi/abc into default

6 files changed, 137 insertions, 31 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4e374e88..9e45a7da 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -40439,13 +40439,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, int fUseQCost );
+    extern int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity, int nCubesMax, 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, fUseQCost = 0, fVerbose = 0;
+    int c, Quality = 2, Verbosity = 0, nCubesMax = 20000, fUseQCost = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "QVqvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "QVCqvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -40471,6 +40471,17 @@ int Abc_CommandAbc9Exorcism( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( Verbosity < 0 )
                 goto usage;
             break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCubesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCubesMax < 0 )
+                goto usage;
+            break;
         case 'q':
             fUseQCost ^= 1;
             break;
@@ -40493,18 +40504,19 @@ 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, fUseQCost );
+    Abc_ExorcismMain( vEsop, Gia_ManCiNum(pAbc->pGia), Gia_ManCoNum(pAbc->pGia), pFileNameOut, Quality, Verbosity, nCubesMax, fUseQCost );
     Vec_WecFree( vEsop );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &exorcism [-Q N] [-V N] <file>\n" );
+    Abc_Print( -2, "usage: &exorcism [-Q N] [-V N] [-C N] -q <file>\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, "        -C N  : maximum number of cubes in startign cover [default = %d]\n", nCubesMax );
+    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 db93d034..052362e5 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,8 +146,45 @@ int ComputeQCostBits( Cube * p )
             nLits++;
     }
     nLits += nLitsN;
-    return QCost[Abc_MinInt(nLits, 7)][Abc_MinInt(nLitsN, 7)];
+    return GetQCost( nLits, nLitsN );
 }
+int ToffoliGateCount( int controls, int lines )
+{
+    switch ( controls )
+    {
+    case 0u:
+    case 1u:
+        return 0;
+        break;
+    case 2u:
+        return 1;
+        break;
+    case 3u:
+        return 4;
+        break;
+    case 4u:
+        return ( ( ( lines + 1 ) / 2 ) >= controls ) ? 8 : 10;
+        break;
+    default:
+        return ( ( ( lines + 1 ) / 2 ) >= controls ) ? 4 * ( controls - 2 ) : 8 * ( controls - 3 );
+    }
+}
+int ComputeQCostTcount( Vec_Int_t * vCube )
+{
+    return 7 * ToffoliGateCount( Vec_IntSize( vCube ), g_CoverInfo.nVarsIn + 1 );
+}
+int ComputeQCostTcountBits( Cube * p )
+{
+    extern varvalue GetVar( Cube* pC, int Var );
+    int v, nLits = 0;
+    for ( v = 0; v < g_CoverInfo.nVarsIn; v++ )
+        if ( GetVar( p, v ) != VAR_ABS )
+            nLits++;
+    return 7 * ToffoliGateCount( nLits, g_CoverInfo.nVarsIn + 1 );
+
+    /* maybe just: 7 * ToffoliGateCount( p->a, g_CoverInfo.nVarsIn + 1 ); */
+}
+
 
 /**Function*************************************************************
 
@@ -742,9 +811,9 @@ int Exorcism( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut )
     printf( "The number of cubes in the starting cover is %d\n", g_CoverInfo.nCubesBefore );
     }
 
-    if ( g_CoverInfo.nCubesBefore > 20000 )
+    if ( g_CoverInfo.nCubesBefore > g_CoverInfo.nCubesMax )
     {
-        printf( "\nThe size of the starting cover is more than 20000 cubes. Quitting...\n" );
+        printf( "\nThe size of the starting cover is more than %d cubes. Quitting...\n", g_CoverInfo.nCubesMax );
         return 0;
     }
 
@@ -825,8 +894,8 @@ int Exorcism( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut )
         char Buffer[1000];
         sprintf( Buffer, "%s", pFileNameOut ? pFileNameOut : "temp.esop" );
         WriteResultIntoFile( Buffer );
-        //if ( g_CoverInfo.Verbosity )
-        printf( "Minimized cover has been written into file <%s>\n", Buffer );
+        if ( g_CoverInfo.Verbosity )
+            printf( "Minimized cover has been written into file <%s>\n", Buffer );
     }
 
     ///////////////////////////////////////////////////////////////////////
@@ -852,12 +921,15 @@ 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 fUseQCost )
+int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity, int nCubesMax, int fUseQCost )
 {
     memset( &g_CoverInfo, 0, sizeof(cinfo) );
     g_CoverInfo.Quality = Quality;
     g_CoverInfo.Verbosity = Verbosity;
+    g_CoverInfo.nCubesMax = nCubesMax;
     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..5a727557 100644
--- a/src/base/exor/exor.h
+++ b/src/base/exor/exor.h
@@ -112,6 +112,7 @@ typedef struct cinfo_tag
 
     int Verbosity;      // verbosity level
     int Quality;        // quality
+    int nCubesMax;      // maximum number of cubes in starting cover
     int fUseQCost;      // use q-cost instead of literal count
 
     abctime TimeRead;   // reading time
@@ -167,6 +168,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( &ltime );
     TimeStr = asctime( localtime( &ltime ) );
     // 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 );