summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c14
-rw-r--r--src/base/abci/abcExact.c135
2 files changed, 86 insertions, 63 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 31f3a275..471e6eef 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7417,13 +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 fMakeAIG, int fVerbose, const char *pFilename );
+ extern void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, int fVeryVerbose, const char *pFilename );
- int c, fMakeAIG = 0, fVerbose = 0, nBTLimit = 10000;
+ int c, fMakeAIG = 0, fVerbose = 0, fVeryVerbose = 0, nBTLimit = 100;
char * pFilename = NULL;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Cavh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Cavwh" ) ) != EOF )
{
switch ( c )
{
@@ -7442,6 +7442,9 @@ int Abc_CommandBmsStart( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
fVerbose ^= 1;
break;
+ case 'w':
+ fVeryVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -7460,16 +7463,17 @@ int Abc_CommandBmsStart( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- Abc_ExactStart( nBTLimit, fMakeAIG, fVerbose, pFilename );
+ Abc_ExactStart( nBTLimit, fMakeAIG, fVerbose, fVeryVerbose, pFilename );
return 0;
usage:
- Abc_Print( -2, "usage: bms_start [-C <num>] [-avh] [<file>]\n" );
+ Abc_Print( -2, "usage: bms_start [-C <num>] [-avwh] [<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-w : toggle very verbose printout [default = %s]\n", fVeryVerbose ? "yes" : "no" );
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" );
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c
index 19b0188a..7d968b70 100644
--- a/src/base/abci/abcExact.c
+++ b/src/base/abci/abcExact.c
@@ -72,6 +72,8 @@ struct Ses_Man_t_
int fMakeAIG; /* create AIG instead of general network */
int fVerbose; /* be verbose */
int fVeryVerbose; /* be very verbose */
+ int fExtractVerbose; /* be verbose about solution extraction */
+ int fSatVerbose; /* be verbose about SAT solving */
int nGates; /* number of gates */
@@ -126,8 +128,10 @@ struct Ses_Store_t_
{
int fMakeAIG; /* create AIG instead of general network */
int fVerbose; /* be verbose */
+ int fVeryVerbose; /* be very verbose */
int nBTLimit; /* conflict limit */
int nEntriesCount; /* number of entries */
+ int nValidEntriesCount; /* number of entries with network */
Ses_TruthEntry_t * pEntries[SES_STORE_TABLE_SIZE]; /* hash table for truth table entries */
unsigned long nCutCount;
@@ -266,7 +270,7 @@ static inline void Ses_StoreTimesCopy( int * pTimesDest, int * pTimesSrc, int nV
pTimesDest[i] = pTimesSrc[i];
}
-// pArrTimeProfile is not normalized
+// 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 )
{
@@ -317,6 +321,8 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr
/* item has been added */
fAdded = 1;
pStore->nEntriesCount++;
+ if ( pSol )
+ pStore->nValidEntriesCount++;
}
else
/* item was already present */
@@ -325,9 +331,9 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr
return fAdded;
}
-// pArrTimeProfile is not normalized
-// returns 0 if no solution was found
-char * Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile )
+// pArrTimeProfile is normalized
+// returns 1 if entry was in store, pSol may still be 0 if it couldn't be computed
+int Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char ** pSol )
{
int key;
Ses_TruthEntry_t * pTEntry;
@@ -363,7 +369,8 @@ char * Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int *
if ( !pTiEntry )
return 0;
- return pTiEntry->pNetwork;
+ *pSol = pTiEntry->pNetwork;
+ return 1;
}
static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename )
@@ -380,7 +387,7 @@ static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename )
return;
}
- fwrite( &pStore->nEntriesCount, sizeof( int ), 1, pFile );
+ fwrite( &pStore->nValidEntriesCount, sizeof( int ), 1, pFile );
for ( i = 0; i < SES_STORE_TABLE_SIZE; ++i )
if ( pStore->pEntries[i] )
@@ -392,10 +399,13 @@ static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename )
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 );
+ if ( pTiEntry->pNetwork )
+ {
+ 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;
@@ -560,7 +570,7 @@ static void Ses_ManCreateVars( Ses_Man_t * pSes, int nGates )
{
int i;
- if ( pSes->fVerbose )
+ if ( pSes->fSatVerbose )
{
printf( "create variables for network with %d functions over %d variables and %d gates\n", pSes->nSpecFunc, pSes->nSpecVars, nGates );
}
@@ -846,7 +856,7 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes )
int status;
abctime timeStart, timeDelta;
- if ( pSes->fVeryVerbose )
+ if ( pSes->fSatVerbose )
{
printf( "solve SAT instance with %d clauses and %d variables\n", sat_solver_nclauses( pSes->pSat ), sat_solver_nvars( pSes->pSat ) );
}
@@ -869,7 +879,7 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes )
}
else
{
- if ( pSes->fVerbose )
+ if ( pSes->fSatVerbose )
{
printf( "resource limit reached\n" );
}
@@ -923,21 +933,21 @@ static char * Ses_ManExtractSolution( Ses_Man_t * pSes )
*p++ = nOp;
*p++ = 2;
- if ( pSes->fVeryVerbose )
+ if ( pSes->fExtractVerbose )
printf( "add gate %d with operation %d", pSes->nSpecVars + i, nOp );
for ( k = 0; k < pSes->nSpecVars + i; ++k )
for ( j = 0; j < k; ++j )
if ( sat_solver_var_value( pSes->pSat, Ses_ManSelectVar( pSes, i, j, k ) ) )
{
- if ( pSes->fVeryVerbose )
+ if ( pSes->fExtractVerbose )
printf( " and operands %d and %d", j, k );
*p++ = j;
*p++ = k;
break;
}
- if ( pSes->fVeryVerbose )
+ if ( pSes->fExtractVerbose )
{
if ( pSes->nMaxDepth > 0 )
{
@@ -986,12 +996,12 @@ static char * Ses_ManExtractSolution( Ses_Man_t * pSes )
for ( l = 0; l < pSes->nSpecVars; ++l )
d = Abc_MaxInt( d, pSes->pArrTimeProfile[l] + pPerm[i * pSes->nSpecVars + l] );
*p++ = d;
- if ( pSes->fVeryVerbose )
+ if ( pSes->fExtractVerbose )
printf( "output %d points to %d and has normalized delay %d (nArrTimeDelta = %d)\n", h, i, d, pSes->nArrTimeDelta );
for ( l = 0; l < pSes->nSpecVars; ++l )
{
d = ( pSes->nMaxDepth != -1 ) ? pPerm[i * pSes->nSpecVars + l] : 0;
- if ( pSes->fVeryVerbose )
+ if ( pSes->fExtractVerbose )
printf( " pin-to-pin arrival time from input %d is %d (pArrTimeProfile = %d)\n", l, d, pSes->pArrTimeProfile[l] );
*p++ = d;
}
@@ -1449,11 +1459,12 @@ int Abc_ExactInputNum()
return 8;
}
// start exact store manager
-void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, const char * pFilename )
+void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, int fVeryVerbose, const char * pFilename )
{
if ( !s_pSesStore )
{
s_pSesStore = Ses_StoreAlloc( nBTLimit, fMakeAIG, fVerbose );
+ s_pSesStore->fVeryVerbose = fVeryVerbose;
if ( pFilename )
Ses_StoreRead( s_pSesStore, pFilename );
}
@@ -1489,13 +1500,14 @@ void Abc_ExactStats()
printf( " total = %lu\n", s_pSesStore->nCutCount );
printf( "cache hits : %lu\n", s_pSesStore->nCacheHit );
printf( "number of entries : %d\n", s_pSesStore->nEntriesCount );
+ printf( "number of valid entries : %d\n", s_pSesStore->nValidEntriesCount );
}
// 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)
// the area cost should not exceed 2048, if the cut is implementable; otherwise, it should be ABC_INFINITY
int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * pPerm, int * Cost, int AigLevel )
{
- int i, nDelta, nMaxArrival, l, fExists = 0;
+ int i, nDelta, nMaxArrival, l;
Ses_Man_t * pSes = NULL;
char * pSol = NULL, * p;
int Delay = ABC_INFINITY, nMaxDepth;
@@ -1523,60 +1535,74 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &nMaxArrival );
- if ( s_pSesStore->fVerbose )
+ if ( s_pSesStore->fVeryVerbose )
{
printf( "compute delay for nontrivial truth table " );
Abc_TtPrintHexRev( stdout, pTruth, nVars );
printf( " with arrival times" );
for ( l = 0; l < nVars; ++l )
printf( " %d", pArrTimeProfile[l] );
- printf( "\n" );
+ printf( " at level %d\n", AigLevel );
}
/* statistics */
s_pSesStore->nCutCount++;
s_pSesStore->pCutCount[nVars]++;
- pSol = Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile );
- if ( pSol )
+ *Cost = ABC_INFINITY;
+
+ if ( Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, &pSol ) )
{
- if ( s_pSesStore->fVerbose )
+ if ( s_pSesStore->fVeryVerbose )
printf( " truth table already in store\n" );
s_pSesStore->nCacheHit++;
- fExists = 1;
}
else
{
nMaxDepth = pArrTimeProfile[0];
for ( i = 1; i < nVars; ++i )
nMaxDepth = Abc_MaxInt( nMaxDepth, pArrTimeProfile[i] );
- nMaxDepth = Abc_MinInt( AigLevel, nMaxDepth + nVars + 1 );
+ nMaxDepth += nVars + 1;
+ //nMaxDepth = Abc_MinInt( AigLevel, nMaxDepth + nVars + 1 );
timeStart = Abc_Clock();
- *Cost = ABC_INFINITY;
-
- pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, s_pSesStore->fMakeAIG, s_pSesStore->fVerbose );
+ pSes = Ses_ManAlloc( pTruth, nVars, 1 /* nSpecFunc */, nMaxDepth, pArrTimeProfile, s_pSesStore->fMakeAIG, s_pSesStore->fVerbose );
pSes->nBTLimit = s_pSesStore->nBTLimit;
- pSes->fVeryVerbose = 0;
+ pSes->fVeryVerbose = s_pSesStore->fVeryVerbose;
- while ( 1 ) /* there is improvement */
+ while ( pSes->nMaxDepth ) /* there is improvement */
{
+ if ( s_pSesStore->fVeryVerbose )
+ {
+ printf( " try to compute network starting with depth %d ", pSes->nMaxDepth );
+ fflush( stdout );
+ }
+
if ( Ses_ManFindMinimumSize( pSes ) )
{
+ if ( s_pSesStore->fVeryVerbose )
+ printf( " FOUND\n" );
if ( pSol )
ABC_FREE( pSol );
pSol = Ses_ManExtractSolution( pSes );
pSes->nMaxDepth--;
}
else
+ {
+ if ( s_pSesStore->fVeryVerbose )
+ printf( " NOT FOUND\n" );
break;
+ }
}
pSes->timeTotal = Abc_Clock() - timeStart;
/* cleanup */
Ses_ManClean( pSes );
+
+ /* store solution */
+ Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol );
}
if ( pSol )
@@ -1586,31 +1612,24 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
Delay = *p++;
for ( l = 0; l < nVars; ++l )
pPerm[l] = *p++;
-
- /* store solution */
- if ( !fExists )
- Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol );
}
- //for ( l = 0; l < nVars; ++l )
- // printf( "pArrTimeProfile[%d] = %d\n", l, pArrTimeProfile[l] );
-
- if ( pSol )
- {
- int Delay2 = 0;
- for ( l = 0; l < nVars; ++l )
- {
- //printf( "%d ", pPerm[l] );
- Delay2 = Abc_MaxInt( Delay2, pArrTimeProfile[l] + pPerm[l] );
- }
- //printf( " output arrival = %d recomputed = %d\n", Delay, Delay2 );
- if ( Delay != Delay2 )
- {
- printf( "^--- BUG!\n" );
- assert( 0 );
- }
- //Delay = Delay2;
- }
+ /* if ( pSol ) */
+ /* { */
+ /* int Delay2 = 0; */
+ /* for ( l = 0; l < nVars; ++l ) */
+ /* { */
+ /* //printf( "%d ", pPerm[l] ); */
+ /* Delay2 = Abc_MaxInt( Delay2, pArrTimeProfile[l] + pPerm[l] ); */
+ /* } */
+ /* //printf( " output arrival = %d recomputed = %d\n", Delay, Delay2 ); */
+ /* if ( Delay != Delay2 ) */
+ /* { */
+ /* printf( "^--- BUG!\n" ); */
+ /* assert( 0 ); */
+ /* } */
+ /* //Delay = Delay2; */
+ /* } */
Abc_UnnormalizeArrivalTimes( pArrTimeProfile, nVars, nDelta );
@@ -1620,7 +1639,7 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
// has the smallest possible arrival time (in agreement with the above Abc_ExactDelayCost)
Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins, Abc_Ntk_t * pNtk )
{
- char * pSol;
+ char * pSol = NULL;
int i, j, nDelta, nMaxArrival;
char const * p;
Abc_Obj_t * pObj;
@@ -1634,7 +1653,7 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile,
return (pTruth[0] & 1) ? Abc_NtkCreateNodeInv(pNtk, pFanins[0]) : Abc_NtkCreateNodeBuf(pNtk, pFanins[0]);
nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &nMaxArrival );
- pSol = Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile );
+ Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, &pSol );
Abc_UnnormalizeArrivalTimes( pArrTimeProfile, nVars, nDelta );
if ( !pSol )
return NULL;
@@ -1711,7 +1730,7 @@ void Abc_ExactStoreTest( int fVerbose )
}
Abc_NodeFreeNames( vNames );
- Abc_ExactStart( 10000, 1, fVerbose, NULL );
+ Abc_ExactStart( 10000, 1, fVerbose, 0, NULL );
assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 02:11:42 +0000