Skip to content

A
abc
Commit 30b3a7ab by Mathias Soeken
Options

BMS: Store I/O, better implications to stop search.

parent 6e7fb2ea
Showing with 225 additions and 46 deletions
src/base/abci/abcExact.c
...@@ -38,6 +38,17 @@ ABC_NAMESPACE_IMPL_START ...@@ -38,6 +38,17 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
static word s_Truths8[32] = {
ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xAAAAAAAAAAAAAAAA),
ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xCCCCCCCCCCCCCCCC),
ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0),
ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00),
ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000),
ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000),
ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF),
ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF)
};
#define ABC_EXACT_SOL_NVARS 0 #define ABC_EXACT_SOL_NVARS 0
#define ABC_EXACT_SOL_NFUNC 1 #define ABC_EXACT_SOL_NFUNC 1
#define ABC_EXACT_SOL_NGATES 2 #define ABC_EXACT_SOL_NGATES 2
...@@ -51,6 +62,7 @@ struct Ses_Man_t_ ...@@ -51,6 +62,7 @@ struct Ses_Man_t_
int bSpecInv; /* remembers whether spec was inverted for normalization */ int bSpecInv; /* remembers whether spec was inverted for normalization */
int nSpecVars; /* number of variables in specification */ int nSpecVars; /* number of variables in specification */
int nSpecFunc; /* number of functions to synthesize */ int nSpecFunc; /* number of functions to synthesize */
int nSpecWords; /* number of words for function */
int nRows; /* number of rows in the specification (without 0) */ int nRows; /* number of rows in the specification (without 0) */
int nMaxDepth; /* maximum depth (-1 if depth is not constrained) */ int nMaxDepth; /* maximum depth (-1 if depth is not constrained) */
int * pArrTimeProfile; /* arrival times of inputs (NULL if arrival times are ignored) */ int * pArrTimeProfile; /* arrival times of inputs (NULL if arrival times are ignored) */
...@@ -105,6 +117,7 @@ typedef struct Ses_TimesEntry_t_ Ses_TimesEntry_t; ...@@ -105,6 +117,7 @@ typedef struct Ses_TimesEntry_t_ Ses_TimesEntry_t;
struct Ses_TimesEntry_t_ struct Ses_TimesEntry_t_
{ {
int pArrTimeProfile[8]; /* normalized arrival time profile */ int pArrTimeProfile[8]; /* normalized arrival time profile */
int fResLimit; /* solution found after resource limit */
Ses_TimesEntry_t * next; /* linked list pointer */ Ses_TimesEntry_t * next; /* linked list pointer */
char * pNetwork; /* pointer to char array representation of optimum network */ char * pNetwork; /* pointer to char array representation of optimum network */
}; };
...@@ -130,6 +143,7 @@ struct Ses_Store_t_ ...@@ -130,6 +143,7 @@ struct Ses_Store_t_
int nValidEntriesCount; /* number of entries with network */ int nValidEntriesCount; /* number of entries with network */
Ses_TruthEntry_t * pEntries[SES_STORE_TABLE_SIZE]; /* hash table for truth table entries */ 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 */ sat_solver * pSat; /* own SAT solver instance to reuse when calling exact algorithm */
FILE * pDebugEntries; /* debug unsynth. (rl) entries */
/* statistics */ /* statistics */
unsigned long nCutCount; /* number of cuts investigated */ unsigned long nCutCount; /* number of cuts investigated */
...@@ -281,9 +295,36 @@ static inline void Ses_StoreTimesCopy( int * pTimesDest, int * pTimesSrc, int nV ...@@ -281,9 +295,36 @@ static inline void Ses_StoreTimesCopy( int * pTimesDest, int * pTimesSrc, int nV
pTimesDest[i] = pTimesSrc[i]; pTimesDest[i] = pTimesSrc[i];
} }
static inline void Ses_StorePrintEntry( Ses_TruthEntry_t * pEntry, Ses_TimesEntry_t * pTiEntry )
{
int i;
printf( "f = " );
Abc_TtPrintHexRev( stdout, pEntry->pTruth, pEntry->nVars );
printf( ", n = %d", pEntry->nVars );
printf( ", arrival =" );
for ( i = 0; i < pEntry->nVars; ++i )
printf( " %d", pTiEntry->pArrTimeProfile[i] );
printf( "\n" );
}
static inline void Ses_StorePrintDebugEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pNormalArrTime, int nMaxDepth )
{
int l;
fprintf( pStore->pDebugEntries, "abc -c \"exact -v -C %d", pStore->nBTLimit );
if ( s_pSesStore->fMakeAIG ) fprintf( pStore->pDebugEntries, " -a" );
fprintf( pStore->pDebugEntries, " -D %d -A", nMaxDepth );
for ( l = 0; l < nVars; ++l )
fprintf( pStore->pDebugEntries, "%c%d", ( l == 0 ? ' ' : ',' ), pNormalArrTime[l] );
fprintf( pStore->pDebugEntries, " " );
Abc_TtPrintHexRev( pStore->pDebugEntries, pTruth, nVars );
fprintf( pStore->pDebugEntries, "\"\n" );
}
// pArrTimeProfile is normalized // pArrTimeProfile is normalized
// returns 1 if and only if a new TimesEntry has been created // 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 Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char * pSol, int fResLimit )
{ {
int key, fAdded; int key, fAdded;
Ses_TruthEntry_t * pTEntry; Ses_TruthEntry_t * pTEntry;
...@@ -326,6 +367,7 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr ...@@ -326,6 +367,7 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr
pTiEntry = ABC_CALLOC( Ses_TimesEntry_t, 1 ); pTiEntry = ABC_CALLOC( Ses_TimesEntry_t, 1 );
Ses_StoreTimesCopy( pTiEntry->pArrTimeProfile, pArrTimeProfile, nVars ); Ses_StoreTimesCopy( pTiEntry->pArrTimeProfile, pArrTimeProfile, nVars );
pTiEntry->pNetwork = pSol; pTiEntry->pNetwork = pSol;
pTiEntry->fResLimit = fResLimit;
pTiEntry->next = pTEntry->head; pTiEntry->next = pTEntry->head;
pTEntry->head = pTiEntry; pTEntry->head = pTiEntry;
...@@ -342,6 +384,34 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr ...@@ -342,6 +384,34 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr
fAdded = 0; fAdded = 0;
} }
/* statistics */
if ( pSol )
{
if ( fResLimit )
{
s_pSesStore->nSynthesizedRL++;
s_pSesStore->pSynthesizedRL[nVars]++;
}
else
{
s_pSesStore->nSynthesizedImp++;
s_pSesStore->pSynthesizedImp[nVars]++;
}
}
else
{
if ( fResLimit )
{
s_pSesStore->nUnsynthesizedRL++;
s_pSesStore->pUnsynthesizedRL[nVars]++;
}
else
{
s_pSesStore->nUnsynthesizedImp++;
s_pSesStore->pUnsynthesizedImp[nVars]++;
}
}
return fAdded; return fAdded;
} }
...@@ -387,9 +457,11 @@ int Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr ...@@ -387,9 +457,11 @@ int Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr
return 1; return 1;
} }
static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename ) static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename, int fSynthImp, int fSynthRL, int fUnsynthImp, int fUnsynthRL )
{ {
int i; int i;
char zero = '\0';
unsigned long nEntries = 0;
Ses_TruthEntry_t * pTEntry; Ses_TruthEntry_t * pTEntry;
Ses_TimesEntry_t * pTiEntry; Ses_TimesEntry_t * pTiEntry;
FILE * pFile; FILE * pFile;
...@@ -401,7 +473,11 @@ static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename ) ...@@ -401,7 +473,11 @@ static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename )
return; return;
} }
fwrite( &pStore->nValidEntriesCount, sizeof( int ), 1, pFile ); 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 ) for ( i = 0; i < SES_STORE_TABLE_SIZE; ++i )
if ( pStore->pEntries[i] ) if ( pStore->pEntries[i] )
...@@ -413,13 +489,30 @@ static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename ) ...@@ -413,13 +489,30 @@ static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename )
pTiEntry = pTEntry->head; pTiEntry = pTEntry->head;
while ( pTiEntry ) while ( pTiEntry )
{ {
if ( pTiEntry->pNetwork ) if ( pStore->fVeryVerbose && !pTiEntry->pNetwork && pTiEntry->fResLimit )
{ Ses_StorePrintEntry( pTEntry, 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->pTruth, sizeof( word ), 4, pFile );
fwrite( &pTEntry->nVars, sizeof( int ), 1, pFile ); fwrite( &pTEntry->nVars, sizeof( int ), 1, pFile );
fwrite( pTiEntry->pArrTimeProfile, sizeof( int ), 8, 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 ); 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; pTiEntry = pTiEntry->next;
} }
pTEntry = pTEntry->next; pTEntry = pTEntry->next;
...@@ -430,11 +523,12 @@ static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename ) ...@@ -430,11 +523,12 @@ static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename )
fclose( pFile ); fclose( pFile );
} }
static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename ) static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename, int fSynthImp, int fSynthRL, int fUnsynthImp, int fUnsynthRL )
{ {
int i, nEntries; int i;
unsigned long nEntries;
word pTruth[4]; word pTruth[4];
int nVars; int nVars, fResLimit;
int pArrTimeProfile[8]; int pArrTimeProfile[8];
char pHeader[3]; char pHeader[3];
char * pNetwork; char * pNetwork;
...@@ -448,26 +542,39 @@ static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename ) ...@@ -448,26 +542,39 @@ static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename )
return; return;
} }
value = fread( &nEntries, sizeof( int ), 1, pFile ); value = fread( &nEntries, sizeof( unsigned long ), 1, pFile );
for ( i = 0; i < nEntries; ++i ) for ( i = 0; i < nEntries; ++i )
{ {
value = fread( pTruth, sizeof( word ), 4, pFile ); value = fread( pTruth, sizeof( word ), 4, pFile );
value = fread( &nVars, sizeof( int ), 1, pFile ); value = fread( &nVars, sizeof( int ), 1, pFile );
value = fread( pArrTimeProfile, sizeof( int ), 8, pFile ); value = fread( pArrTimeProfile, sizeof( int ), 8, pFile );
value = fread( &fResLimit, sizeof( int ), 1, pFile );
value = fread( pHeader, sizeof( char ), 3, pFile ); value = fread( pHeader, sizeof( char ), 3, pFile );
if ( pHeader[0] == '\0' )
pNetwork = NULL;
else
{
pNetwork = ABC_CALLOC( char, 3 + 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS] ); pNetwork = ABC_CALLOC( char, 3 + 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS] );
pNetwork[0] = pHeader[0]; pNetwork[0] = pHeader[0];
pNetwork[1] = pHeader[1]; pNetwork[1] = pHeader[1];
pNetwork[2] = pHeader[2]; pNetwork[2] = pHeader[2];
value = fread( pNetwork + 3, sizeof( char ), 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS], pFile ); value = fread( pNetwork + 3, sizeof( char ), 4 * pHeader[ABC_EXACT_SOL_NGATES] + 2 + pHeader[ABC_EXACT_SOL_NVARS], pFile );
}
if ( !fSynthImp && pNetwork && !fResLimit ) continue;
if ( !fSynthRL && pNetwork && fResLimit ) continue;
if ( !fUnsynthImp && !pNetwork && !fResLimit ) continue;
if ( !fUnsynthRL && !pNetwork && fResLimit ) continue;
Ses_StoreAddEntry( pStore, pTruth, nVars, pArrTimeProfile, pNetwork ); Ses_StoreAddEntry( pStore, pTruth, nVars, pArrTimeProfile, pNetwork, fResLimit );
} }
fclose( pFile ); fclose( pFile );
printf( "read %lu entries from file\n", nEntries );
} }
static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fMakeAIG, int nBTLimit, int fVerbose ) static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fMakeAIG, int nBTLimit, int fVerbose )
...@@ -487,6 +594,7 @@ static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int ...@@ -487,6 +594,7 @@ static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int
p->pSpec = pTruth; p->pSpec = pTruth;
p->nSpecVars = nVars; p->nSpecVars = nVars;
p->nSpecFunc = nFunc; p->nSpecFunc = nFunc;
p->nSpecWords = Abc_TtWordNum( nVars );
p->nRows = ( 1 << nVars ) - 1; p->nRows = ( 1 << nVars ) - 1;
p->nMaxDepth = nMaxDepth; p->nMaxDepth = nMaxDepth;
p->pArrTimeProfile = nMaxDepth >= 0 ? pArrTimeProfile : NULL; p->pArrTimeProfile = nMaxDepth >= 0 ? pArrTimeProfile : NULL;
...@@ -684,6 +792,27 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) ...@@ -684,6 +792,27 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
} }
} }
/* if there is only one output, we know it must point to the last gate */
if ( pSes->nSpecFunc == 1 )
{
for ( i = 0; i < pSes->nGates - 1; ++i )
{
pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, i ), 1 );
if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) )
{
Vec_IntFree( vLits );
return 0;
}
}
pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, pSes->nGates - 1 ), 0 );
if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) )
{
Vec_IntFree( vLits );
return 0;
}
}
else
{
/* some output is selected */ /* some output is selected */
for ( h = 0; h < pSes->nSpecFunc; ++h ) for ( h = 0; h < pSes->nSpecFunc; ++h )
{ {
...@@ -692,6 +821,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) ...@@ -692,6 +821,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
Vec_IntSetEntry( vLits, i, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) ); Vec_IntSetEntry( vLits, i, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) );
sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntArray( vLits ) + pSes->nGates ); sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntArray( vLits ) + pSes->nGates );
} }
}
/* each gate has two operands */ /* each gate has two operands */
for ( i = 0; i < pSes->nGates; ++i ) for ( i = 0; i < pSes->nGates; ++i )
...@@ -1268,9 +1398,65 @@ static inline void Ses_ManPrintVars( Ses_Man_t * pSes ) ...@@ -1268,9 +1398,65 @@ static inline void Ses_ManPrintVars( Ses_Man_t * pSes )
***********************************************************************/ ***********************************************************************/
static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) static int Ses_ManFindMinimumSize( Ses_Man_t * pSes )
{ {
int nGates = 0, f; int nGates = 0, f, i, l, mask = ~0;
int fAndDecStructure = 0; /* network must be f = AND(x_i, g) or f = AND(!x_i, g) structure */
int fMaxGatesLevel2 = 1;
abctime timeStart; abctime timeStart;
/* do the arrival times allow for a network? */
if ( pSes->nMaxDepth != -1 )
{
for ( l = 0; l < pSes->nSpecVars; ++l )
{
if ( pSes->pArrTimeProfile[l] >= pSes->nMaxDepth )
{
if ( pSes->fVeryVerbose )
printf( "give up due to impossible arrival time (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
return 0;
}
else if ( pSes->nSpecFunc == 1 && pSes->fMakeAIG && pSes->pArrTimeProfile[l] + 1 == pSes->nMaxDepth )
{
if ( ( fAndDecStructure == 1 && pSes->nSpecVars > 2 ) || fAndDecStructure == 2 )
{
if ( pSes->fVeryVerbose )
printf( "give up due to impossible decomposition (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
return 0;
}
fAndDecStructure++;
if ( pSes->nSpecVars < 6u )
mask = ( 1 << pSes->nSpecVars ) - 1u;
/* A subset B <=> A and B = A */
for ( i = 0; i < pSes->nSpecWords; ++i )
if ( ( ( s_Truths8[(l << 2) + i] & pSes->pSpec[i] & mask ) != ( pSes->pSpec[i] & mask ) ) &&
( ( ~( s_Truths8[(l << 2) + i] ) & pSes->pSpec[i] & mask ) != ( pSes->pSpec[i] & mask ) ) )
{
if ( pSes->fVeryVerbose )
printf( "give up due to impossible decomposition (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
return 0;
}
}
}
/* check if depth's match with structure at second level from top */
if ( fAndDecStructure )
fMaxGatesLevel2 = ( pSes->nSpecVars == 3 ) ? 2 : 1;
else
fMaxGatesLevel2 = ( pSes->nSpecVars == 4 ) ? 4 : 3;
i = 0;
for ( l = 0; l < pSes->nSpecVars; ++l )
if ( pSes->pArrTimeProfile[l] + 2 == pSes->nMaxDepth )
if ( ++i > fMaxGatesLevel2 )
{
if ( pSes->fVeryVerbose )
printf( "give up due to impossible decomposition at second level (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] );
return 0;
}
}
/* store whether call was unsuccessful due to resource limit and not due to impossible constraint */ /* store whether call was unsuccessful due to resource limit and not due to impossible constraint */
pSes->fHitResLimit = 0; pSes->fHitResLimit = 0;
...@@ -1279,10 +1465,17 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) ...@@ -1279,10 +1465,17 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes )
++nGates; ++nGates;
/* give up if number of gates is impossible for given depth */ /* give up if number of gates is impossible for given depth */
if ( pSes->nMaxDepth != -1 && nGates >= ( 1 << pSes->nMaxDepth ) ) if ( pSes->nMaxDepth != -1 && nGates >= (1 << pSes->nMaxDepth ) )
{ {
if ( pSes->fVeryVerbose ) if ( pSes->fVeryVerbose )
printf( "give up due to impossible depth (depth = %d, gates = %d)\n", pSes->nMaxDepth, nGates ); printf( "give up due to impossible depth (depth = %d, gates = %d)", pSes->nMaxDepth, nGates );
return 0;
}
if ( fAndDecStructure && nGates >= ( 1 << ( pSes->nMaxDepth - 1 ) ) + 1 )
{
if ( pSes->fVeryVerbose )
printf( "give up due to impossible depth in AND-dec structure (depth = %d, gates = %d)", pSes->nMaxDepth, nGates );
return 0; return 0;
} }
...@@ -1290,7 +1483,7 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) ...@@ -1290,7 +1483,7 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes )
if ( nGates >= ( 1 << pSes->nSpecVars ) ) if ( nGates >= ( 1 << pSes->nSpecVars ) )
{ {
if ( pSes->fVeryVerbose ) if ( pSes->fVeryVerbose )
printf( "give up due to impossible number of gates\n" ); printf( "give up due to impossible number of gates" );
return 0; return 0;
} }
...@@ -1373,6 +1566,8 @@ Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth ...@@ -1373,6 +1566,8 @@ Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth
timeStart = Abc_Clock(); timeStart = Abc_Clock();
pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 1, nBTLimit, fVerbose ); pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 1, nBTLimit, fVerbose );
pSes->fVeryVerbose = 1;
pSes->fSatVerbose = 1;
if ( fVerbose ) if ( fVerbose )
Ses_ManPrintFuncs( pSes ); Ses_ManPrintFuncs( pSes );
...@@ -1529,7 +1724,11 @@ void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, int fVeryVerbose, ...@@ -1529,7 +1724,11 @@ void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, int fVeryVerbose,
s_pSesStore = Ses_StoreAlloc( nBTLimit, fMakeAIG, fVerbose ); s_pSesStore = Ses_StoreAlloc( nBTLimit, fMakeAIG, fVerbose );
s_pSesStore->fVeryVerbose = fVeryVerbose; s_pSesStore->fVeryVerbose = fVeryVerbose;
if ( pFilename ) if ( pFilename )
Ses_StoreRead( s_pSesStore, pFilename ); Ses_StoreRead( s_pSesStore, pFilename, 1, 0, 0, 0 );
if ( s_pSesStore->fVeryVerbose )
{
s_pSesStore->pDebugEntries = fopen( "bms.debug", "w" );
}
} }
else else
printf( "BMS manager already started\n" ); printf( "BMS manager already started\n" );
...@@ -1540,7 +1739,9 @@ void Abc_ExactStop( const char * pFilename ) ...@@ -1540,7 +1739,9 @@ void Abc_ExactStop( const char * pFilename )
if ( s_pSesStore ) if ( s_pSesStore )
{ {
if ( pFilename ) if ( pFilename )
Ses_StoreWrite( s_pSesStore, pFilename ); Ses_StoreWrite( s_pSesStore, pFilename, 1, 0, 0, 0 );
if ( s_pSesStore->pDebugEntries )
fclose( s_pSesStore->pDebugEntries );
Ses_StoreClean( s_pSesStore ); Ses_StoreClean( s_pSesStore );
} }
else else
...@@ -1617,7 +1818,7 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * ...@@ -1617,7 +1818,7 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
Ses_Man_t * pSes = NULL; Ses_Man_t * pSes = NULL;
char * pSol = NULL, * p; char * pSol = NULL, * p;
int pNormalArrTime[8]; int pNormalArrTime[8];
int Delay = ABC_INFINITY, nMaxDepth; int Delay = ABC_INFINITY, nMaxDepth, fResLimit;
abctime timeStart = Abc_Clock(), timeStartExact; abctime timeStart = Abc_Clock(), timeStartExact;
/* some checks */ /* some checks */
...@@ -1725,36 +1926,13 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * ...@@ -1725,36 +1926,13 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
} }
} }
/* log unsuccessful case for debugging */
if ( s_pSesStore->pDebugEntries && pSes->fHitResLimit )
Ses_StorePrintDebugEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, pSes->nMaxDepth );
pSes->timeTotal = Abc_Clock() - timeStartExact; pSes->timeTotal = Abc_Clock() - timeStartExact;
/* statistics */ /* statistics */
if ( pSol )
{
if ( pSes->fHitResLimit )
{
s_pSesStore->nSynthesizedRL++;
s_pSesStore->pSynthesizedRL[nVars]++;
}
else
{
s_pSesStore->nSynthesizedImp++;
s_pSesStore->pSynthesizedImp[nVars]++;
}
}
else
{
if ( pSes->fHitResLimit )
{
s_pSesStore->nUnsynthesizedRL++;
s_pSesStore->pUnsynthesizedRL[nVars]++;
}
else
{
s_pSesStore->nUnsynthesizedImp++;
s_pSesStore->pUnsynthesizedImp[nVars]++;
}
}
s_pSesStore->nSatCalls += pSes->nSatCalls; s_pSesStore->nSatCalls += pSes->nSatCalls;
s_pSesStore->nUnsatCalls += pSes->nUnsatCalls; s_pSesStore->nUnsatCalls += pSes->nUnsatCalls;
s_pSesStore->nUndefCalls += pSes->nUndefCalls; s_pSesStore->nUndefCalls += pSes->nUndefCalls;
...@@ -1766,11 +1944,12 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * ...@@ -1766,11 +1944,12 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
s_pSesStore->timeInstance += pSes->timeInstance; s_pSesStore->timeInstance += pSes->timeInstance;
s_pSesStore->timeExact += pSes->timeTotal; s_pSesStore->timeExact += pSes->timeTotal;
/* cleanup */ /* cleanup (we need to clean before adding since pTruth may have been modified by pSes) */
fResLimit = pSes->fHitResLimit;
Ses_ManCleanLight( pSes ); Ses_ManCleanLight( pSes );
/* store solution */ /* store solution */
Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, pSol ); Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, pSol, fResLimit );
} }
if ( pSol ) if ( pSol )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment