Read and write to exact store.

2 files changed, 181 insertions, 21 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e4e78d08..4dc50ed2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -137,6 +137,7 @@ static int Abc_CommandVarMin                 ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandDetect                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExact                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBmsStart               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBmsStop                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBmsPs                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandLogic                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -780,6 +781,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "exact",         Abc_CommandExact,            1 );
 
     Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_start",  Abc_CommandBmsStart,         0 );
+    Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_stop",   Abc_CommandBmsStop,          0 );
     Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_ps",     Abc_CommandBmsPs,            0 );
 
     Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
@@ -7391,7 +7393,7 @@ usage:
     Abc_Print( -2, "usage: exact [-D <num>] [-atvh] <truth1> <truth2> ...\n" );
     Abc_Print( -2, "\t           finds optimum networks using SAT-based exact synthesis for hex truth tables <truth1> <truth2> ...\n" );
     Abc_Print( -2, "\t-D <num> : constrain maximum depth (if too low, algorithm may not terminate)\n" );
-    Abc_Print( -2, "\t-a       : create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" );
+    Abc_Print( -2, "\t-a       : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" );
     Abc_Print( -2, "\t-t       : run test suite\n" );
     Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n" );
@@ -7415,12 +7417,13 @@ usage:
 int Abc_CommandBmsStart( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern int Abc_ExactIsRunning();
-    extern void Abc_ExactStart( int nBTLimit, int fVerbose );
+    extern void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, const char *pFilename );
 
-    int c, fVerbose = 0, nBTLimit = 10000;
+    int c, fMakeAIG = 0, fVerbose = 0, nBTLimit = 10000;
+    char * pFilename = NULL;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Cavh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7433,6 +7436,9 @@ int Abc_CommandBmsStart( Abc_Frame_t * pAbc, int argc, char ** argv )
             nBTLimit = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
+        case 'a':
+            fMakeAIG ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -7443,19 +7449,26 @@ int Abc_CommandBmsStart( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
 
+    if ( argc > globalUtilOptind )
+    {
+        pFilename = argv[globalUtilOptind++];
+    }
+
     if ( Abc_ExactIsRunning() )
     {
         Abc_Print( -1, "BMS manager is already started." );
         return 1;
     }
 
-    Abc_ExactStart( nBTLimit, fVerbose );
+    Abc_ExactStart( nBTLimit, fMakeAIG, fVerbose, pFilename );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: bms_start [-C <num>] [-vh]\n" );
+    Abc_Print( -2, "usage: bms_start [-C <num>] [-avh] [<file>]\n" );
     Abc_Print( -2, "\t           starts BMS manager for recording optimum networks\n" );
+    Abc_Print( -2, "\t           if <file> is specified, store entries are read from that file\n" );
     Abc_Print( -2, "\t-C <num> : the limit on the number of conflicts [default = %d]\n", nBTLimit );
+    Abc_Print( -2, "\t-a       : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" );
     Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n" );
     Abc_Print( -2, "\t\n" );
@@ -7475,6 +7488,62 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandBmsStop( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern int Abc_ExactIsRunning();
+    extern void Abc_ExactStop( const char *pFilename );
+
+    int c;
+    char * pFilename = NULL;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( argc > globalUtilOptind )
+    {
+        pFilename = argv[globalUtilOptind++];
+    }
+
+    if ( !Abc_ExactIsRunning() )
+    {
+        Abc_Print( -1, "BMS manager is not started." );
+        return 1;
+    }
+
+    Abc_ExactStop( pFilename );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: bms_stop [-C <num>] [-vh] [<file>]\n" );
+    Abc_Print( -2, "\t           stops BMS manager for recording optimum networks\n" );
+    Abc_Print( -2, "\t           if <file> is specified, store entries are written to that file\n" );
+    Abc_Print( -2, "\t-h       : print the command usage\n" );
+    Abc_Print( -2, "\t\n" );
+    Abc_Print( -2, "\t           This command was contributed by Mathias Soeken from EPFL in July 2016.\n" );
+    Abc_Print( -2, "\t           The author can be contacted as mathias.soeken at epfl.ch\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandBmsPs( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern int Abc_ExactIsRunning();
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c
index c9a4def4..d739118a 100644
--- a/src/base/abci/abcExact.c
+++ b/src/base/abci/abcExact.c
@@ -50,6 +50,10 @@ static word s_Truths8[32] = {
     ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF)
 };
 
+#define ABC_EXACT_SOL_NVARS  0
+#define ABC_EXACT_SOL_NFUNC  1
+#define ABC_EXACT_SOL_NGATES 2
+
 typedef struct Ses_Man_t_ Ses_Man_t;
 struct Ses_Man_t_
 {
@@ -120,8 +124,10 @@ struct Ses_TruthEntry_t_
 typedef struct Ses_Store_t_ Ses_Store_t;
 struct Ses_Store_t_
 {
+    int                fMakeAIG;                       /* create AIG instead of general network */
     int                fVerbose;                       /* be verbose */
     int                nBTLimit;                       /* conflict limit */
+    int                nEntriesCount;                  /* number of entries */
     Ses_TruthEntry_t * pEntries[SES_STORE_TABLE_SIZE]; /* hash table for truth table entries */
 
     unsigned long      nCutCount;
@@ -159,11 +165,13 @@ static int Abc_NormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int * ma
     return delta;
 }
 
-static inline Ses_Store_t * Ses_StoreAlloc( int nBTLimit, int fVerbose )
+static inline Ses_Store_t * Ses_StoreAlloc( int nBTLimit, int fMakeAIG, int fVerbose )
 {
     Ses_Store_t * pStore = ABC_CALLOC( Ses_Store_t, 1 );
-    pStore->fVerbose = fVerbose;
-    pStore->nBTLimit = nBTLimit;
+    pStore->fMakeAIG      = fMakeAIG;
+    pStore->fVerbose      = fVerbose;
+    pStore->nBTLimit      = nBTLimit;
+    pStore->nEntriesCount = 0;
     memset( pStore->pEntries, 0, SES_STORE_TABLE_SIZE );
 
     pStore->nCutCount = 0;
@@ -302,6 +310,7 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr
 
         /* item has been added */
         fAdded = 1;
+        pStore->nEntriesCount++;
     }
     else
         /* item was already present */
@@ -358,6 +367,85 @@ char * Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int *
     return pTiEntry->pNetwork;
 }
 
+static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename )
+{
+    int i;
+    Ses_TruthEntry_t * pTEntry;
+    Ses_TimesEntry_t * pTiEntry;
+    FILE * pFile;
+
+    pFile = fopen( pFilename, "wb" );
+    if (pFile == NULL)
+    {
+        printf( "cannot open file \"%s\" for writing\n", pFilename );
+        return;
+    }
+
+    fwrite( &pStore->nEntriesCount, sizeof( int ), 1, pFile );
+
+    for ( i = 0; i < SES_STORE_TABLE_SIZE; ++i )
+        if ( pStore->pEntries[i] )
+        {
+            pTEntry = pStore->pEntries[i];
+
+            while ( pTEntry )
+            {
+                pTiEntry = pTEntry->head;
+                while ( pTiEntry )
+                {
+                    fwrite( pTEntry->pTruth, sizeof( word ), 4, pFile );
+                    fwrite( &pTEntry->nVars, sizeof( int ), 1, pFile );
+                    fwrite( pTiEntry->pArrTimeProfile, sizeof( int ), 8, pFile );
+                    fwrite( pTiEntry->pNetwork, sizeof( char ), 3 + 4 * pTiEntry->pNetwork[ABC_EXACT_SOL_NGATES] + 2 + pTiEntry->pNetwork[ABC_EXACT_SOL_NVARS], pFile );
+                    pTiEntry = pTiEntry->next;
+                }
+                pTEntry = pTEntry->next;
+            }
+        }
+
+
+    fclose( pFile );
+}
+
+static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename )
+{
+    int i, nEntries;
+    word pTruth[4];
+    int nVars;
+    int pArrTimeProfile[8];
+    char pHeader[3];
+    char * pNetwork;
+    FILE * pFile;
+
+    pFile = fopen( pFilename, "rb" );
+    if (pFile == NULL)
+    {
+        printf( "cannot open file \"%s\" for reading\n", pFilename );
+        return;
+    }
+
+    fread( &nEntries, sizeof( int ), 1, pFile );
+
+    for ( i = 0; i < nEntries; ++i )
+    {
+        fread( pTruth, sizeof( word ), 4, pFile );
+        fread( &nVars, sizeof( int ), 1, pFile );
+        fread( pArrTimeProfile, sizeof( int ), 8, pFile );
+        fread( pHeader, sizeof( char ), 3, pFile );
+
+        pNetwork = ABC_CALLOC( char, 3 + 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS] );
+        pNetwork[0] = pHeader[0];
+        pNetwork[1] = pHeader[1];
+        pNetwork[2] = pHeader[2];
+
+        fread( pNetwork + 3, sizeof( char ), 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS], pFile );
+
+        Ses_StoreAddEntry( pStore, pTruth, nVars, pArrTimeProfile, pNetwork );
+    }
+
+    fclose( pFile );
+}
+
 static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fMakeAIG, int fVerbose )
 {
     int h, i;
@@ -809,9 +897,6 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes )
 //   delay:     maximum delay to output (taking arrival times into account, not normalized) or 0 if not specified
 //   pin[i]:    pin to pin delay to input i or 0 if not specified or if there is no connection to input i
 // NOTE: since outputs can only point to gates, delay and pin-to-pin times cannot be 0
-#define ABC_EXACT_SOL_NVARS  0
-#define ABC_EXACT_SOL_NFUNC  1
-#define ABC_EXACT_SOL_NGATES 2
 static char * Ses_ManExtractSolution( Ses_Man_t * pSes )
 {
     int nSol, h, i, j, k, l, aj, ak, d, nOp;
@@ -1362,18 +1447,26 @@ int Abc_ExactInputNum()
     return 8;
 }
 // start exact store manager
-void Abc_ExactStart( int nBTLimit, int fVerbose )
+void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, const char * pFilename )
 {
     if ( !s_pSesStore )
-        s_pSesStore = Ses_StoreAlloc( nBTLimit, fVerbose );
+    {
+        s_pSesStore = Ses_StoreAlloc( nBTLimit, fMakeAIG, fVerbose );
+        if ( pFilename )
+            Ses_StoreRead( s_pSesStore, pFilename );
+    }
     else
         printf( "BMS manager already started\n" );
 }
 // stop exact store manager
-void Abc_ExactStop()
+void Abc_ExactStop( const char * pFilename )
 {
     if ( s_pSesStore )
+    {
+        if ( pFilename )
+            Ses_StoreWrite( s_pSesStore, pFilename );
         Ses_StoreClean( s_pSesStore );
+    }
     else
         printf( "BMS manager has not been started\n" );
 }
@@ -1393,6 +1486,7 @@ void Abc_ExactStats()
         printf( " %d = %lu  ", i, s_pSesStore->pCutCount[i] );
     printf( " total = %lu\n", s_pSesStore->nCutCount );
     printf( "cache hits                : %lu\n", s_pSesStore->nCacheHit );
+    printf( "number of entries         : %d\n", s_pSesStore->nEntriesCount );
 }
 // this procedure takes TT and input arrival times (pArrTimeProfile) and return the smallest output arrival time;
 // it also returns the pin-to-pin delays (pPerm) between each cut leaf and the cut output and the cut area cost (Cost)
@@ -1433,7 +1527,7 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
 
         *Cost = ABC_INFINITY;
 
-        pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, 1 /* fMakeAIG */, s_pSesStore->fVerbose );
+        pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, s_pSesStore->fMakeAIG, s_pSesStore->fVerbose );
         pSes->nBTLimit = s_pSesStore->nBTLimit;
 
         while ( 1 ) /* there is improvement */
@@ -1529,9 +1623,6 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile,
     }
 
     /* output */
-    //if ( Abc_LitIsCompl( *p ) )
-    //    pObj = Abc_NtkCreateNodeInv( pNtk, (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) ) );
-    //else
     pObj = (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) );
 
     Vec_PtrFree( pGates );
@@ -1563,7 +1654,7 @@ void Abc_ExactStoreTest( int fVerbose )
     }
     Abc_NodeFreeNames( vNames );
 
-    Abc_ExactStart( 10000, fVerbose );
+    Abc_ExactStart( 10000, 1, fVerbose, NULL );
 
     assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins ) );
 
@@ -1575,7 +1666,7 @@ void Abc_ExactStoreTest( int fVerbose )
     assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins ) );
     (*pArrTimeProfile)--;
 
-    Abc_ExactStop();
+    Abc_ExactStop( NULL );
 
     Abc_NtkDelete( pNtk );
 }