From 452303b77ab9181087624e6562fba7b6160afda6 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Sat, 10 Sep 2016 14:23:43 +0200 Subject: Updates to BMS. --- src/base/abci/abcExact.c | 162 ++++++++++++++++++++++++++--------------------- 1 file changed, 90 insertions(+), 72 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 7e2aa5b9..139240a5 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -317,6 +317,7 @@ struct Ses_Store_t_ Ses_TruthEntry_t * pEntries[SES_STORE_TABLE_SIZE]; /* hash table for truth table entries */ sat_solver * pSat; /* own SAT solver instance to reuse when calling exact algorithm */ FILE * pDebugEntries; /* debug unsynth. (rl) entries */ + char * szDBName; /* if given, database is written every time a new entry is added */ /* statistics */ unsigned long nCutCount; /* number of cuts investigated */ @@ -418,6 +419,9 @@ static inline void Ses_StoreClean( Ses_Store_t * pStore ) } sat_solver_delete( pStore->pSat ); + + if ( pStore->szDBName ) + ABC_FREE( pStore->szDBName ); ABC_FREE( pStore ); } @@ -553,6 +557,69 @@ static void Abc_ExactNormalizeArrivalTimesForNetwork( int nVars, int * pArrTimeP Vec_IntFree( vLevels ); } +static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename, int fSynthImp, int fSynthRL, int fUnsynthImp, int fUnsynthRL ) +{ + int i; + char zero = '\0'; + unsigned long nEntries = 0; + 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; + } + + if ( fSynthImp ) nEntries += pStore->nSynthesizedImp; + if ( fSynthRL ) nEntries += pStore->nSynthesizedRL; + if ( fUnsynthImp ) nEntries += pStore->nUnsynthesizedImp; + if ( fUnsynthRL ) nEntries += pStore->nUnsynthesizedRL; + fwrite( &nEntries, sizeof( unsigned long ), 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 ) + { + if ( !fSynthImp && pTiEntry->pNetwork && !pTiEntry->fResLimit ) { pTiEntry = pTiEntry->next; continue; } + if ( !fSynthRL && pTiEntry->pNetwork && pTiEntry->fResLimit ) { pTiEntry = pTiEntry->next; continue; } + if ( !fUnsynthImp && !pTiEntry->pNetwork && !pTiEntry->fResLimit ) { pTiEntry = pTiEntry->next; continue; } + if ( !fUnsynthRL && !pTiEntry->pNetwork && pTiEntry->fResLimit ) { pTiEntry = pTiEntry->next; continue; } + + fwrite( pTEntry->pTruth, sizeof( word ), 4, pFile ); + fwrite( &pTEntry->nVars, sizeof( int ), 1, pFile ); + fwrite( pTiEntry->pArrTimeProfile, sizeof( int ), 8, pFile ); + fwrite( &pTiEntry->fResLimit, sizeof( int ), 1, pFile ); + + if ( pTiEntry->pNetwork ) + { + fwrite( pTiEntry->pNetwork, sizeof( char ), 3 + 4 * pTiEntry->pNetwork[ABC_EXACT_SOL_NGATES] + 2 + pTiEntry->pNetwork[ABC_EXACT_SOL_NVARS], pFile ); + } + else + { + fwrite( &zero, sizeof( char ), 1, pFile ); + fwrite( &zero, sizeof( char ), 1, pFile ); + fwrite( &zero, sizeof( char ), 1, pFile ); + } + + pTiEntry = pTiEntry->next; + } + pTEntry = pTEntry->next; + } + } + + + fclose( pFile ); +} + // pArrTimeProfile is normalized // returns 1 if and only if a new TimesEntry has been created int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char * pSol, int fResLimit ) @@ -613,7 +680,7 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr } else { - assert( 0 ); + //assert( 0 ); /* item was already present */ fAdded = 0; } @@ -623,29 +690,32 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr { if ( fResLimit ) { - s_pSesStore->nSynthesizedRL++; - s_pSesStore->pSynthesizedRL[nVars]++; + pStore->nSynthesizedRL++; + pStore->pSynthesizedRL[nVars]++; } else { - s_pSesStore->nSynthesizedImp++; - s_pSesStore->pSynthesizedImp[nVars]++; + pStore->nSynthesizedImp++; + pStore->pSynthesizedImp[nVars]++; } } else { if ( fResLimit ) { - s_pSesStore->nUnsynthesizedRL++; - s_pSesStore->pUnsynthesizedRL[nVars]++; + pStore->nUnsynthesizedRL++; + pStore->pUnsynthesizedRL[nVars]++; } else { - s_pSesStore->nUnsynthesizedImp++; - s_pSesStore->pUnsynthesizedImp[nVars]++; + pStore->nUnsynthesizedImp++; + pStore->pUnsynthesizedImp[nVars]++; } } + if ( fAdded && pStore->szDBName ) + Ses_StoreWrite( pStore, pStore->szDBName, 1, 0, 0, 0 ); + return fAdded; } @@ -742,69 +812,6 @@ int Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr return 1; } -static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename, int fSynthImp, int fSynthRL, int fUnsynthImp, int fUnsynthRL ) -{ - int i; - char zero = '\0'; - unsigned long nEntries = 0; - 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; - } - - if ( fSynthImp ) nEntries += pStore->nSynthesizedImp; - if ( fSynthRL ) nEntries += pStore->nSynthesizedRL; - if ( fUnsynthImp ) nEntries += pStore->nUnsynthesizedImp; - if ( fUnsynthRL ) nEntries += pStore->nUnsynthesizedRL; - fwrite( &nEntries, sizeof( unsigned long ), 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 ) - { - if ( !fSynthImp && pTiEntry->pNetwork && !pTiEntry->fResLimit ) { pTiEntry = pTiEntry->next; continue; } - if ( !fSynthRL && pTiEntry->pNetwork && pTiEntry->fResLimit ) { pTiEntry = pTiEntry->next; continue; } - if ( !fUnsynthImp && !pTiEntry->pNetwork && !pTiEntry->fResLimit ) { pTiEntry = pTiEntry->next; continue; } - if ( !fUnsynthRL && !pTiEntry->pNetwork && pTiEntry->fResLimit ) { pTiEntry = pTiEntry->next; continue; } - - fwrite( pTEntry->pTruth, sizeof( word ), 4, pFile ); - fwrite( &pTEntry->nVars, sizeof( int ), 1, pFile ); - fwrite( pTiEntry->pArrTimeProfile, sizeof( int ), 8, pFile ); - fwrite( &pTiEntry->fResLimit, sizeof( int ), 1, pFile ); - - if ( pTiEntry->pNetwork ) - { - fwrite( pTiEntry->pNetwork, sizeof( char ), 3 + 4 * pTiEntry->pNetwork[ABC_EXACT_SOL_NGATES] + 2 + pTiEntry->pNetwork[ABC_EXACT_SOL_NVARS], pFile ); - } - else - { - fwrite( &zero, sizeof( char ), 1, pFile ); - fwrite( &zero, sizeof( char ), 1, pFile ); - fwrite( &zero, sizeof( char ), 1, pFile ); - } - - pTiEntry = pTiEntry->next; - } - pTEntry = pTEntry->next; - } - } - - - fclose( pFile ); -} - static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename, int fSynthImp, int fSynthRL, int fUnsynthImp, int fUnsynthRL ) { int i; @@ -817,6 +824,12 @@ static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename, int fSy FILE * pFile; int value; + if ( pStore->szDBName ) + { + printf( "cannot read from database when szDBName is set" ); + return; + } + pFile = fopen( pFilename, "rb" ); if (pFile == NULL) { @@ -2535,7 +2548,12 @@ void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, int fVeryVerbose, s_pSesStore = Ses_StoreAlloc( nBTLimit, fMakeAIG, fVerbose ); s_pSesStore->fVeryVerbose = fVeryVerbose; if ( pFilename ) + { Ses_StoreRead( s_pSesStore, pFilename, 1, 0, 0, 0 ); + + s_pSesStore->szDBName = ABC_CALLOC( char, strlen( pFilename ) + 1 ); + strcpy( s_pSesStore->szDBName, pFilename ); + } if ( s_pSesStore->fVeryVerbose ) { s_pSesStore->pDebugEntries = fopen( "bms.debug", "w" ); -- cgit v1.2.3