summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abc.h2
-rw-r--r--src/base/abci/abc.c62
-rw-r--r--src/base/abci/abcExact.c703
3 files changed, 586 insertions, 181 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 35b20dbe..e752fb71 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -646,7 +646,7 @@ extern ABC_DLL Vec_Ptr_t * Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, in
extern ABC_DLL int Abc_ExactInputNum();
extern ABC_DLL int Abc_ExactIsRunning();
extern ABC_DLL Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins, Abc_Ntk_t * pNtk );
-extern ABC_DLL Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fVerbose );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int nBTLimit, int fVerbose );
/*=== abcFanio.c ==========================================================*/
extern ABC_DLL void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
extern ABC_DLL void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2eb3f0b5..9e45a7da 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7291,15 +7291,17 @@ usage:
***********************************************************************/
int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fVerbose );
+ extern Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int nBTLimit, int fVerbose );
- int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0;
+ int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0, nBTLimit = 100;
+ char * p1, * p2;
word pTruth[64];
+ int pArrTimeProfile[8], fHasArrTimeProfile = 0;
Abc_Ntk_t * pNtkRes;
Gia_Man_t * pGiaRes;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Datvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "DACatvh" ) ) != EOF )
{
switch ( c )
{
@@ -7314,6 +7316,40 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nMaxDepth < 0 )
goto usage;
break;
+ case 'A':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ fHasArrTimeProfile = 1;
+ p1 = p2 = argv[globalUtilOptind++];
+ while ( true ) {
+ if ( *p2 == ',' )
+ {
+ *p2 = '\0';
+ pArrTimeProfile[nVars++] = atoi( p1 );
+ *p2++ = ',';
+ p1 = p2;
+ }
+ else if ( *p2 == '\0' )
+ {
+ pArrTimeProfile[nVars++] = atoi( p1 );
+ break;
+ }
+ else
+ ++p2;
+ }
+ break;
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nBTLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ break;
case 'a':
fMakeAIG ^= 1;
break;
@@ -7370,7 +7406,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fMakeAIG )
{
- pGiaRes = Gia_ManFindExact( pTruth, nVars, nFunc, nMaxDepth, NULL, fVerbose );
+ pGiaRes = Gia_ManFindExact( pTruth, nVars, nFunc, nMaxDepth, fHasArrTimeProfile ? pArrTimeProfile : NULL, nBTLimit, fVerbose );
if ( pGiaRes )
Abc_FrameUpdateGia( pAbc, pGiaRes );
else
@@ -7378,7 +7414,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else
{
- pNtkRes = Abc_NtkFindExact( pTruth, nVars, nFunc, nMaxDepth, NULL, fVerbose );
+ pNtkRes = Abc_NtkFindExact( pTruth, nVars, nFunc, nMaxDepth, fHasArrTimeProfile ? pArrTimeProfile : NULL, nBTLimit, fVerbose );
if ( pNtkRes )
{
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -7392,14 +7428,16 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv )
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 : 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" );
+ Abc_Print( -2, "\t-D <num> : constrain maximum depth (if too low, algorithm may not terminate)\n" );
+ Abc_Print( -2, "\t-A <list> : input arrival times (comma separated list)\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-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" );
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" );
+ 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;
}
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c
index 506eeabb..2d386157 100644
--- a/src/base/abci/abcExact.c
+++ b/src/base/abci/abcExact.c
@@ -25,7 +25,6 @@
#include "base/abc/abc.h"
#include "aig/gia/gia.h"
-#include "bool/kit/kit.h"
#include "misc/util/utilTruth.h"
#include "misc/vec/vecInt.h"
#include "misc/vec/vecPtr.h"
@@ -63,6 +62,7 @@ struct Ses_Man_t_
int bSpecInv; /* remembers whether spec was inverted for normalization */
int nSpecVars; /* number of variables in specification */
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 nMaxDepth; /* maximum depth (-1 if depth is not constrained) */
int * pArrTimeProfile; /* arrival times of inputs (NULL if arrival times are ignored) */
@@ -88,10 +88,18 @@ struct Ses_Man_t_
int nSelectOffset; /* offset where select variables start */
int nDepthOffset; /* offset where depth variables start */
+ int fHitResLimit; /* SAT solver gave up due to resource limit */
+
abctime timeSat; /* SAT runtime */
abctime timeSatSat; /* SAT runtime (sat instance) */
abctime timeSatUnsat; /* SAT runtime (unsat instance) */
+ abctime timeSatUndef; /* SAT runtime (undef instance) */
+ abctime timeInstance; /* creating instance runtime */
abctime timeTotal; /* all runtime */
+
+ int nSatCalls; /* number of SAT calls */
+ int nUnsatCalls; /* number of UNSAT calls */
+ int nUndefCalls; /* number of UNDEF calls */
};
/***********************************************************************
@@ -109,6 +117,7 @@ typedef struct Ses_TimesEntry_t_ Ses_TimesEntry_t;
struct Ses_TimesEntry_t_
{
int pArrTimeProfile[8]; /* normalized arrival time profile */
+ int fResLimit; /* solution found after resource limit */
Ses_TimesEntry_t * next; /* linked list pointer */
char * pNetwork; /* pointer to char array representation of optimum network */
};
@@ -133,10 +142,36 @@ struct Ses_Store_t_
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 */
+ sat_solver * pSat; /* own SAT solver instance to reuse when calling exact algorithm */
+ FILE * pDebugEntries; /* debug unsynth. (rl) entries */
- unsigned long nCutCount;
- unsigned long pCutCount[9];
- unsigned long nCacheHit;
+ /* statistics */
+ unsigned long nCutCount; /* number of cuts investigated */
+ unsigned long pCutCount[9]; /* -> per cut size */
+ unsigned long nUnsynthesizedImp; /* number of cuts which couldn't be optimized at all, opt. stopped because of imp. constraints */
+ unsigned long pUnsynthesizedImp[9]; /* -> per cut size */
+ unsigned long nUnsynthesizedRL; /* number of cuts which couldn't be optimized at all, opt. stopped because of resource limits */
+ unsigned long pUnsynthesizedRL[9]; /* -> per cut size */
+ unsigned long nSynthesizedTrivial; /* number of cuts which could be synthesized trivially (n < 2) */
+ unsigned long pSynthesizedTrivial[9]; /* -> per cut size */
+ unsigned long nSynthesizedImp; /* number of cuts which could be synthesized, opt. stopped because of imp. constraints */
+ unsigned long pSynthesizedImp[9]; /* -> per cut size */
+ unsigned long nSynthesizedRL; /* number of cuts which could be synthesized, opt. stopped because of resource limits */
+ unsigned long pSynthesizedRL[9]; /* -> per cut size */
+ unsigned long nCacheHits; /* number of cache hits */
+ unsigned long pCacheHits[9]; /* -> per cut size */
+
+ unsigned long nSatCalls; /* number of total SAT calls */
+ unsigned long nUnsatCalls; /* number of total UNSAT calls */
+ unsigned long nUndefCalls; /* number of total UNDEF calls */
+
+ abctime timeExact; /* Exact synthesis runtime */
+ abctime timeSat; /* SAT runtime */
+ abctime timeSatSat; /* SAT runtime (sat instance) */
+ abctime timeSatUnsat; /* SAT runtime (unsat instance) */
+ abctime timeSatUndef; /* SAT runtime (undef instance) */
+ abctime timeInstance; /* creating instance runtime */
+ abctime timeTotal; /* all runtime */
};
static Ses_Store_t * s_pSesStore = NULL;
@@ -169,26 +204,15 @@ static int Abc_NormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int * ma
return delta;
}
-static inline void Abc_UnnormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int nDelta )
-{
- int l;
-
- for ( l = 0; l < nVars; ++l )
- pArrTimeProfile[l] += nDelta;
-}
-
static inline Ses_Store_t * Ses_StoreAlloc( int nBTLimit, int fMakeAIG, int fVerbose )
{
Ses_Store_t * pStore = ABC_CALLOC( Ses_Store_t, 1 );
- pStore->fMakeAIG = fMakeAIG;
- pStore->fVerbose = fVerbose;
- pStore->nBTLimit = nBTLimit;
- pStore->nEntriesCount = 0;
+ pStore->fMakeAIG = fMakeAIG;
+ pStore->fVerbose = fVerbose;
+ pStore->nBTLimit = nBTLimit;
memset( pStore->pEntries, 0, SES_STORE_TABLE_SIZE );
- pStore->nCutCount = 0;
- memset( pStore->pCutCount, 0, 9 );
- pStore->nCacheHit = 0;
+ pStore->pSat = sat_solver_new();
return pStore;
}
@@ -220,6 +244,7 @@ static inline void Ses_StoreClean( Ses_Store_t * pStore )
}
}
+ sat_solver_delete( pStore->pSat );
ABC_FREE( pStore );
}
@@ -228,7 +253,7 @@ static inline int Ses_StoreTableHash( word * pTruth, int nVars )
static int s_Primes[4] = { 1291, 1699, 1999, 2357 };
int i;
unsigned uHash = 0;
- for ( i = 0; i < Kit_TruthWordNum( nVars ); ++i )
+ for ( i = 0; i < Abc_TtWordNum( nVars ); ++i )
uHash ^= pTruth[i] * s_Primes[i & 0xf];
return (int)(uHash % SES_STORE_TABLE_SIZE );
}
@@ -240,7 +265,7 @@ static inline int Ses_StoreTruthEqual( Ses_TruthEntry_t * pEntry, word * pTruth,
if ( pEntry->nVars != nVars )
return 0;
- for ( i = 0; i < Kit_TruthWordNum( nVars ); ++i )
+ for ( i = 0; i < Abc_TtWordNum( nVars ); ++i )
if ( pEntry->pTruth[i] != pTruth[i] )
return 0;
return 1;
@@ -250,7 +275,7 @@ static inline void Ses_StoreTruthCopy( Ses_TruthEntry_t * pEntry, word * pTruthS
{
int i;
pEntry->nVars = nVars;
- for ( i = 0; i < Kit_TruthWordNum( nVars ); ++i )
+ for ( i = 0; i < Abc_TtWordNum( nVars ); ++i )
pEntry->pTruth[i] = pTruthSrc[i];
}
@@ -270,9 +295,36 @@ static inline void Ses_StoreTimesCopy( int * pTimesDest, int * pTimesSrc, int nV
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
// 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;
Ses_TruthEntry_t * pTEntry;
@@ -315,6 +367,7 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr
pTiEntry = ABC_CALLOC( Ses_TimesEntry_t, 1 );
Ses_StoreTimesCopy( pTiEntry->pArrTimeProfile, pArrTimeProfile, nVars );
pTiEntry->pNetwork = pSol;
+ pTiEntry->fResLimit = fResLimit;
pTiEntry->next = pTEntry->head;
pTEntry->head = pTiEntry;
@@ -325,8 +378,39 @@ int Ses_StoreAddEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pAr
pStore->nValidEntriesCount++;
}
else
+ {
+ assert( 0 );
/* item was already present */
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;
}
@@ -373,9 +457,11 @@ 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 )
+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;
@@ -387,7 +473,11 @@ static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename )
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 )
if ( pStore->pEntries[i] )
@@ -399,13 +489,30 @@ static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename )
pTiEntry = pTEntry->head;
while ( pTiEntry )
{
+ 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->nVars, sizeof( int ), 1, pFile );
+ fwrite( pTiEntry->pArrTimeProfile, sizeof( int ), 8, pFile );
+ fwrite( &pTiEntry->fResLimit, sizeof( int ), 1, 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 );
}
+ 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;
@@ -416,11 +523,12 @@ static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename )
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];
- int nVars;
+ int nVars, fResLimit;
int pArrTimeProfile[8];
char pHeader[3];
char * pNetwork;
@@ -434,29 +542,42 @@ static void Ses_StoreRead( Ses_Store_t * pStore, const char * pFilename )
return;
}
- value = fread( &nEntries, sizeof( int ), 1, pFile );
+ value = fread( &nEntries, sizeof( unsigned long ), 1, pFile );
for ( i = 0; i < nEntries; ++i )
{
value = fread( pTruth, sizeof( word ), 4, pFile );
value = fread( &nVars, sizeof( int ), 1, pFile );
value = fread( pArrTimeProfile, sizeof( int ), 8, pFile );
+ value = fread( &fResLimit, sizeof( int ), 1, pFile );
value = 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];
+ 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[0] = pHeader[0];
+ pNetwork[1] = pHeader[1];
+ 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 );
+
+ 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 fVerbose )
+static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fMakeAIG, int nBTLimit, int fVerbose )
{
int h, i;
@@ -470,25 +591,28 @@ static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int
pTruth[(h << 2) + i] = ~pTruth[(h << 2) + i];
p->bSpecInv |= ( 1 << h );
}
- p->pSpec = pTruth;
- p->nSpecVars = nVars;
- p->nSpecFunc = nFunc;
- p->nRows = ( 1 << nVars ) - 1;
- p->nMaxDepth = nMaxDepth;
+ p->pSpec = pTruth;
+ p->nSpecVars = nVars;
+ p->nSpecFunc = nFunc;
+ p->nSpecWords = Abc_TtWordNum( nVars );
+ p->nRows = ( 1 << nVars ) - 1;
+ p->nMaxDepth = nMaxDepth;
p->pArrTimeProfile = nMaxDepth >= 0 ? pArrTimeProfile : NULL;
if ( p->pArrTimeProfile )
p->nArrTimeDelta = Abc_NormalizeArrivalTimes( p->pArrTimeProfile, nVars, &p->nArrTimeMax );
else
p->nArrTimeDelta = p->nArrTimeMax = 0;
- p->fMakeAIG = fMakeAIG;
- p->nBTLimit = nMaxDepth >= 0 ? 50000 : 0;
- p->fVerbose = fVerbose;
- p->fVeryVerbose = 0;
+ p->fMakeAIG = fMakeAIG;
+ p->nBTLimit = nBTLimit;
+ p->fVerbose = fVerbose;
+ p->fVeryVerbose = 0;
+ p->fExtractVerbose = 0;
+ p->fSatVerbose = 0;
return p;
}
-static inline void Ses_ManClean( Ses_Man_t * pSes )
+static inline void Ses_ManCleanLight( Ses_Man_t * pSes )
{
int h, i;
for ( h = 0; h < pSes->nSpecFunc; ++h )
@@ -500,10 +624,14 @@ static inline void Ses_ManClean( Ses_Man_t * pSes )
for ( i = 0; i < pSes->nSpecVars; ++i )
pSes->pArrTimeProfile[i] += pSes->nArrTimeDelta;
+ ABC_FREE( pSes );
+}
+
+static inline void Ses_ManClean( Ses_Man_t * pSes )
+{
if ( pSes->pSat )
sat_solver_delete( pSes->pSat );
-
- ABC_FREE( pSes );
+ Ses_ManCleanLight( pSes );
}
/**Function*************************************************************
@@ -589,9 +717,11 @@ static void Ses_ManCreateVars( Ses_Man_t * pSes, int nGates )
pSes->nSelectOffset = pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars;
pSes->nDepthOffset = pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars + pSes->nSelectVars;
+ /* if we already have a SAT solver, then restart it (this saves a lot of time) */
if ( pSes->pSat )
- sat_solver_delete( pSes->pSat );
- pSes->pSat = sat_solver_new();
+ sat_solver_restart( pSes->pSat );
+ else
+ pSes->pSat = sat_solver_new();
sat_solver_setnvars( pSes->pSat, pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars + pSes->nSelectVars + pSes->nDepthVars );
}
@@ -602,14 +732,14 @@ static void Ses_ManCreateVars( Ses_Man_t * pSes, int nGates )
***********************************************************************/
static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int j, int k, int a, int b, int c )
{
- int pLits[5], ctr = 0, value;
+ int pLits[5], ctr = 0;
pLits[ctr++] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), a );
if ( j < pSes->nSpecVars )
{
- if ( Abc_TtGetBit( s_Truths8 + ( j << 2 ), t + 1 ) != b ) /* 1 in clause, we can omit the clause */
+ if ( ( ( ( t + 1 ) & ( 1 << j ) ) ? 1 : 0 ) != b )
return;
}
else
@@ -617,7 +747,7 @@ static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int
if ( k < pSes->nSpecVars )
{
- if ( Abc_TtGetBit( s_Truths8 + ( k << 2 ), t + 1 ) != c ) /* 1 in clause, we can omit the clause */
+ if ( ( ( ( t + 1 ) & ( 1 << k ) ) ? 1 : 0 ) != c )
return;
}
else
@@ -626,8 +756,7 @@ static inline void Ses_ManCreateMainClause( Ses_Man_t * pSes, int t, int i, int
if ( b > 0 || c > 0 )
pLits[ctr++] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, b, c ), 1 - a );
- value = sat_solver_addclause( pSes->pSat, pLits, pLits + ctr );
- assert( value );
+ sat_solver_addclause( pSes->pSat, pLits, pLits + ctr );
}
static int Ses_ManCreateClauses( Ses_Man_t * pSes )
@@ -636,7 +765,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
int h, i, j, k, t, ii, jj, kk, p, q, d;
int pLits[3];
- Vec_Int_t * vLits;
+ Vec_Int_t * vLits = Vec_IntAlloc( 0u );
for ( t = 0; t < pSes->nRows; ++t )
for ( i = 0; i < pSes->nGates; ++i )
@@ -659,29 +788,50 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
{
pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 );
pLits[1] = Abc_Var2Lit( Ses_ManSimVar( pSes, i, t ), 1 - Abc_TtGetBit( &pSes->pSpec[h << 2], t + 1 ) );
- assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) );
+ sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
}
}
- /* some output is selected */
- for ( h = 0; h < pSes->nSpecFunc; ++h )
+ /* if there is only one output, we know it must point to the last gate */
+ if ( pSes->nSpecFunc == 1 )
{
- vLits = Vec_IntAlloc( pSes->nGates );
- for ( i = 0; i < pSes->nGates; ++i )
- Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) );
- assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) );
- Vec_IntFree( vLits );
+ 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 */
+ for ( h = 0; h < pSes->nSpecFunc; ++h )
+ {
+ Vec_IntGrowResize( vLits, pSes->nGates );
+ for ( i = 0; i < pSes->nGates; ++i )
+ 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 );
+ }
}
/* each gate has two operands */
for ( i = 0; i < pSes->nGates; ++i )
{
- vLits = Vec_IntAlloc( ( ( pSes->nSpecVars + i ) * ( pSes->nSpecVars + i - 1 ) ) / 2 );
+ Vec_IntGrowResize( vLits, ( ( pSes->nSpecVars + i ) * ( pSes->nSpecVars + i - 1 ) ) / 2 );
+ jj = 0;
for ( j = 0; j < pSes->nSpecVars + i; ++j )
for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
- Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 0 ) );
- assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) );
- Vec_IntFree( vLits );
+ Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 0 ) );
+ sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntArray( vLits ) + jj );
}
/* only AIG */
@@ -693,36 +843,37 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 );
pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 );
pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 0 );
- assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) );
+ sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 1 );
pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 0 );
pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 );
- assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) );
+ sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 0 );
pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 1 );
pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 1 );
- assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) );
+ sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
}
}
/* EXTRA clauses: use gate i at least once */
+ Vec_IntGrowResize( vLits, pSes->nSpecFunc + pSes->nGates * ( pSes->nSpecVars + pSes->nGates - 2 ) );
for ( i = 0; i < pSes->nGates; ++i )
{
- vLits = Vec_IntAlloc( 0 );
+ jj = 0;
for ( h = 0; h < pSes->nSpecFunc; ++h )
- Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) );
+ Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 0 ) );
for ( ii = i + 1; ii < pSes->nGates; ++ii )
{
for ( j = 0; j < pSes->nSpecVars + i; ++j )
- Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, pSes->nSpecVars + i ), 0 ) );
+ Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, pSes->nSpecVars + i ), 0 ) );
for ( j = pSes->nSpecVars + i + 1; j < pSes->nSpecVars + ii; ++j )
- Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, pSes->nSpecVars + i, j ), 0 ) );
+ Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, pSes->nSpecVars + i, j ), 0 ) );
}
- assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) );
- Vec_IntFree( vLits );
+ sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntArray( vLits ) + jj );
}
+ Vec_IntFree( vLits );
/* EXTRA clauses: co-lexicographic order */
for ( i = 0; i < pSes->nGates - 1; ++i )
@@ -766,13 +917,13 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
for ( jj = 0; jj < kk; ++jj )
if ( jj == p || kk == p )
Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, jj, kk ), 0 ) );
- assert( sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) ) );
+ sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) );
Vec_IntFree( vLits );
}
}
/* DEPTH clauses */
- if ( pSes->nMaxDepth > 0 )
+ if ( pSes->nMaxDepth >= 0 )
{
for ( i = 0; i < pSes->nGates; ++i )
{
@@ -785,7 +936,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
{
pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, j, jj ), 1 );
pLits[2] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, jj + 1 ), 0 );
- assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) );
+ sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
}
}
@@ -797,7 +948,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
{
pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, k, kk ), 1 );
pLits[2] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, kk + 1 ), 0 );
- assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ) );
+ sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
}
}
@@ -812,15 +963,15 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
d = pSes->pArrTimeProfile[k];
pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
- pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, d + 1 ), 0 );
- assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) );
+ pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, d ), 0 );
+ sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
}
}
else
{
/* arrival times are 0 */
pLits[0] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, 0 ), 0 );
- assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) );
+ sat_solver_addclause( pSes->pSat, pLits, pLits + 1 );
}
/* reverse order encoding of depth variables */
@@ -828,7 +979,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
{
pLits[0] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, j ), 1 );
pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, j - 1 ), 0 );
- assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) );
+ sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
}
/* constrain maximum depth */
@@ -869,16 +1020,20 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes )
if ( status == l_True )
{
+ pSes->nSatCalls++;
pSes->timeSatSat += timeDelta;
return 1;
}
else if ( status == l_False )
{
+ pSes->nUnsatCalls++;
pSes->timeSatUnsat += timeDelta;
return 0;
}
else
{
+ pSes->nUndefCalls++;
+ pSes->timeSatUndef += timeDelta;
if ( pSes->fSatVerbose )
{
printf( "resource limit reached\n" );
@@ -991,17 +1146,20 @@ static char * Ses_ManExtractSolution( Ses_Man_t * pSes )
*p++ = Abc_Var2Lit( i, ( pSes->bSpecInv >> h ) & 1 );
d = 0;
if ( pSes->nMaxDepth != -1 )
- /* while ( d < pSes->nArrTimeMax + i && sat_solver_var_value( pSes->pSat, Ses_ManDepthVar( pSes, i, d ) ) ) */
- /* ++d; */
for ( l = 0; l < pSes->nSpecVars; ++l )
- d = Abc_MaxInt( d, pSes->pArrTimeProfile[l] + pPerm[i * pSes->nSpecVars + l] );
+ {
+ if ( pSes->pArrTimeProfile )
+ d = Abc_MaxInt( d, pSes->pArrTimeProfile[l] + pPerm[i * pSes->nSpecVars + l] );
+ else
+ d = Abc_MaxInt( d, pPerm[i * pSes->nSpecVars + l] );
+ }
*p++ = d;
- if ( pSes->fExtractVerbose )
+ if ( pSes->pArrTimeProfile && 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->fExtractVerbose )
+ if ( pSes->pArrTimeProfile && pSes->fExtractVerbose )
printf( " pin-to-pin arrival time from input %d is %d (pArrTimeProfile = %d)\n", l, d, pSes->pArrTimeProfile[l] );
*p++ = d;
}
@@ -1168,10 +1326,12 @@ static Gia_Man_t * Ses_ManExtractGia( char const * pSol )
static void Ses_ManPrintRuntime( Ses_Man_t * pSes )
{
printf( "Runtime breakdown:\n" );
- ABC_PRTP( "Sat ", pSes->timeSat, pSes->timeTotal );
- ABC_PRTP( " Sat ", pSes->timeSatSat, pSes->timeTotal );
- ABC_PRTP( " Unsat", pSes->timeSatUnsat, pSes->timeTotal );
- ABC_PRTP( "ALL ", pSes->timeTotal, pSes->timeTotal );
+ ABC_PRTP( "Sat ", pSes->timeSat, pSes->timeTotal );
+ ABC_PRTP( " Sat ", pSes->timeSatSat, pSes->timeTotal );
+ ABC_PRTP( " Unsat ", pSes->timeSatUnsat, pSes->timeTotal );
+ ABC_PRTP( " Undef ", pSes->timeSatUndef, pSes->timeTotal );
+ ABC_PRTP( "Instance", pSes->timeInstance, pSes->timeTotal );
+ ABC_PRTP( "ALL ", pSes->timeTotal, pSes->timeTotal );
}
static inline void Ses_ManPrintFuncs( Ses_Man_t * pSes )
@@ -1185,6 +1345,18 @@ static inline void Ses_ManPrintFuncs( Ses_Man_t * pSes )
Abc_TtPrintHexRev( stdout, &pSes->pSpec[h >> 2], pSes->nSpecVars );
printf( "\n" );
}
+
+ if ( pSes->nMaxDepth != -1 )
+ {
+ printf( " max depth = %d\n", pSes->nMaxDepth );
+ if ( pSes->pArrTimeProfile )
+ {
+ printf( " arrival times =" );
+ for ( h = 0; h < pSes->nSpecVars; ++h )
+ printf( " %d", pSes->pArrTimeProfile[h] );
+ printf( "\n" );
+ }
+ }
}
static inline void Ses_ManPrintVars( Ses_Man_t * pSes )
@@ -1226,24 +1398,108 @@ static inline void Ses_ManPrintVars( Ses_Man_t * pSes )
***********************************************************************/
static int Ses_ManFindMinimumSize( Ses_Man_t * pSes )
{
- int nGates = 0;
+ 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;
+
+ /* 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 */
+ pSes->fHitResLimit = 0;
while ( true )
{
++nGates;
/* 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 )
+ 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;
+ }
+
+ /* give up if number of gates gets practically too large */
+ if ( nGates >= ( 1 << pSes->nSpecVars ) )
+ {
+ if ( pSes->fVeryVerbose )
+ printf( "give up due to impossible number of gates" );
return 0;
+ }
+ timeStart = Abc_Clock();
Ses_ManCreateVars( pSes, nGates );
- if ( !Ses_ManCreateClauses( pSes ) )
- return 0; /* proven UNSAT while creating clauses */
+ f = Ses_ManCreateClauses( pSes );
+ pSes->timeInstance += ( Abc_Clock() - timeStart );
+ if ( !f )
+ continue; /* proven UNSAT while creating clauses */
switch ( Ses_ManSolve( pSes ) )
{
case 1: return 1; /* SAT */
- case 2: return 0; /* resource limit */
+ case 2:
+ pSes->fHitResLimit = 1;
+ return 0; /* resource limit */
}
}
@@ -1263,7 +1519,7 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fVerbose )
+Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int nBTLimit, int fVerbose )
{
Ses_Man_t * pSes;
char * pSol;
@@ -1275,7 +1531,7 @@ Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth
timeStart = Abc_Clock();
- pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 0, fVerbose );
+ pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 0, nBTLimit, fVerbose );
if ( fVerbose )
Ses_ManPrintFuncs( pSes );
@@ -1297,7 +1553,7 @@ Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth
return pNtk;
}
-Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fVerbose )
+Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int nBTLimit, int fVerbose )
{
Ses_Man_t * pSes;
char * pSol;
@@ -1309,7 +1565,9 @@ Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth
timeStart = Abc_Clock();
- pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 1, fVerbose );
+ pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 1, nBTLimit, fVerbose );
+ pSes->fVeryVerbose = 1;
+ pSes->fSatVerbose = 1;
if ( fVerbose )
Ses_ManPrintFuncs( pSes );
@@ -1362,30 +1620,30 @@ void Abc_ExactTestSingleOutput( int fVerbose )
pNtk = Abc_NtkFromTruthTable( pTruth, 4 );
- pNtk2 = Abc_NtkFindExact( pTruth, 4, 1, -1, NULL, fVerbose );
+ pNtk2 = Abc_NtkFindExact( pTruth, 4, 1, -1, NULL, 0, fVerbose );
Abc_NtkShortNames( pNtk2 );
Abc_NtkCecSat( pNtk, pNtk2, 10000, 0 );
assert( pNtk2 );
assert( Abc_NtkNodeNum( pNtk2 ) == 6 );
Abc_NtkDelete( pNtk2 );
- pNtk3 = Abc_NtkFindExact( pTruth, 4, 1, 3, NULL, fVerbose );
+ pNtk3 = Abc_NtkFindExact( pTruth, 4, 1, 3, NULL, 0, fVerbose );
Abc_NtkShortNames( pNtk3 );
Abc_NtkCecSat( pNtk, pNtk3, 10000, 0 );
assert( pNtk3 );
assert( Abc_NtkLevel( pNtk3 ) <= 3 );
Abc_NtkDelete( pNtk3 );
- pNtk4 = Abc_NtkFindExact( pTruth, 4, 1, 9, pArrTimeProfile, fVerbose );
+ pNtk4 = Abc_NtkFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, fVerbose );
Abc_NtkShortNames( pNtk4 );
Abc_NtkCecSat( pNtk, pNtk4, 10000, 0 );
assert( pNtk4 );
assert( Abc_NtkLevel( pNtk4 ) <= 9 );
Abc_NtkDelete( pNtk4 );
- assert( !Abc_NtkFindExact( pTruth, 4, 1, 2, NULL, fVerbose ) );
+ assert( !Abc_NtkFindExact( pTruth, 4, 1, 2, NULL, 50000, fVerbose ) );
- assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrTimeProfile, fVerbose ) );
+ assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, fVerbose ) );
Abc_NtkDelete( pNtk );
}
@@ -1404,27 +1662,27 @@ void Abc_ExactTestSingleOutputAIG( int fVerbose )
Abc_NtkToAig( pNtk );
pGia = Abc_NtkAigToGia( pNtk, 1 );
- pGia2 = Gia_ManFindExact( pTruth, 4, 1, -1, NULL, fVerbose );
+ pGia2 = Gia_ManFindExact( pTruth, 4, 1, -1, NULL, 0, fVerbose );
pMiter = Gia_ManMiter( pGia, pGia2, 0, 1, 0, 0, 1 );
assert( pMiter );
Cec_ManVerify( pMiter, pPars );
Gia_ManStop( pMiter );
- pGia3 = Gia_ManFindExact( pTruth, 4, 1, 3, NULL, fVerbose );
+ pGia3 = Gia_ManFindExact( pTruth, 4, 1, 3, NULL, 0, fVerbose );
pMiter = Gia_ManMiter( pGia, pGia3, 0, 1, 0, 0, 1 );
assert( pMiter );
Cec_ManVerify( pMiter, pPars );
Gia_ManStop( pMiter );
- pGia4 = Gia_ManFindExact( pTruth, 4, 1, 9, pArrTimeProfile, fVerbose );
+ pGia4 = Gia_ManFindExact( pTruth, 4, 1, 9, pArrTimeProfile, 50000, fVerbose );
pMiter = Gia_ManMiter( pGia, pGia4, 0, 1, 0, 0, 1 );
assert( pMiter );
Cec_ManVerify( pMiter, pPars );
Gia_ManStop( pMiter );
- assert( !Gia_ManFindExact( pTruth, 4, 1, 2, NULL, fVerbose ) );
+ assert( !Gia_ManFindExact( pTruth, 4, 1, 2, NULL, 50000, fVerbose ) );
- assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrTimeProfile, fVerbose ) );
+ assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, fVerbose ) );
Gia_ManStop( pGia );
Gia_ManStop( pGia2 );
@@ -1466,7 +1724,11 @@ 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 );
+ Ses_StoreRead( s_pSesStore, pFilename, 1, 0, 0, 0 );
+ if ( s_pSesStore->fVeryVerbose )
+ {
+ s_pSesStore->pDebugEntries = fopen( "bms.debug", "w" );
+ }
}
else
printf( "BMS manager already started\n" );
@@ -1477,7 +1739,9 @@ void Abc_ExactStop( const char * pFilename )
if ( s_pSesStore )
{
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 );
}
else
@@ -1494,24 +1758,68 @@ void Abc_ExactStats()
return;
}
+ printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
+ printf( " 0 1 2 3 4 5 6 7 8 total\n" );
+ printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
printf( "number of considered cuts :" );
- for ( i = 2; i < 9; ++i )
- printf( " %d = %lu ", i, s_pSesStore->pCutCount[i] );
- printf( " total = %lu\n", s_pSesStore->nCutCount );
- printf( "cache hits : %lu\n", s_pSesStore->nCacheHit );
+ for ( i = 0; i < 9; ++i )
+ printf( "%10lu", s_pSesStore->pCutCount[i] );
+ printf( "%10lu\n", s_pSesStore->nCutCount );
+ printf( " - trivial :" );
+ for ( i = 0; i < 9; ++i )
+ printf( "%10lu", s_pSesStore->pSynthesizedTrivial[i] );
+ printf( "%10lu\n", s_pSesStore->nSynthesizedTrivial );
+ printf( " - synth (imp) :" );
+ for ( i = 0; i < 9; ++i )
+ printf( "%10lu", s_pSesStore->pSynthesizedImp[i] );
+ printf( "%10lu\n", s_pSesStore->nSynthesizedImp );
+ printf( " - synth (res) :" );
+ for ( i = 0; i < 9; ++i )
+ printf( "%10lu", s_pSesStore->pSynthesizedRL[i] );
+ printf( "%10lu\n", s_pSesStore->nSynthesizedRL );
+ printf( " - not synth (imp) :" );
+ for ( i = 0; i < 9; ++i )
+ printf( "%10lu", s_pSesStore->pUnsynthesizedImp[i] );
+ printf( "%10lu\n", s_pSesStore->nUnsynthesizedImp );
+ printf( " - not synth (res) :" );
+ for ( i = 0; i < 9; ++i )
+ printf( "%10lu", s_pSesStore->pUnsynthesizedRL[i] );
+ printf( "%10lu\n", s_pSesStore->nUnsynthesizedRL );
+ printf( " - cache hits :" );
+ for ( i = 0; i < 9; ++i )
+ printf( "%10lu", s_pSesStore->pCacheHits[i] );
+ printf( "%10lu\n", s_pSesStore->nCacheHits );
+ printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
printf( "number of entries : %d\n", s_pSesStore->nEntriesCount );
printf( "number of valid entries : %d\n", s_pSesStore->nValidEntriesCount );
+ printf( "number of invalid entries : %d\n", s_pSesStore->nEntriesCount - s_pSesStore->nValidEntriesCount );
+ printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
+ printf( "number of SAT calls : %lu\n", s_pSesStore->nSatCalls );
+ printf( "number of UNSAT calls : %lu\n", s_pSesStore->nUnsatCalls );
+ printf( "number of UNDEF calls : %lu\n", s_pSesStore->nUndefCalls );
+
+ printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
+ printf( "Runtime breakdown:\n" );
+ ABC_PRTP( "Exact ", s_pSesStore->timeExact, s_pSesStore->timeTotal );
+ ABC_PRTP( " Sat ", s_pSesStore->timeSat, s_pSesStore->timeTotal );
+ ABC_PRTP( " Sat ", s_pSesStore->timeSatSat, s_pSesStore->timeTotal );
+ ABC_PRTP( " Unsat ", s_pSesStore->timeSatUnsat, s_pSesStore->timeTotal );
+ ABC_PRTP( " Undef ", s_pSesStore->timeSatUndef, s_pSesStore->timeTotal );
+ ABC_PRTP( " Instance", s_pSesStore->timeInstance, s_pSesStore->timeTotal );
+ ABC_PRTP( "Other ", s_pSesStore->timeTotal - s_pSesStore->timeExact, s_pSesStore->timeTotal );
+ ABC_PRTP( "ALL ", s_pSesStore->timeTotal, s_pSesStore->timeTotal );
}
// 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;
+ int i, nMaxArrival, l;
Ses_Man_t * pSes = NULL;
char * pSol = NULL, * p;
- int Delay = ABC_INFINITY, nMaxDepth;
- abctime timeStart;
+ int pNormalArrTime[8];
+ int Delay = ABC_INFINITY, nMaxDepth, fResLimit;
+ abctime timeStart = Abc_Clock(), timeStartExact;
/* some checks */
if ( nVars < 0 || nVars > 8 )
@@ -1520,20 +1828,43 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
assert( 0 );
}
+ /* statistics */
+ s_pSesStore->nCutCount++;
+ s_pSesStore->pCutCount[nVars]++;
+
if ( nVars == 0 )
{
+ s_pSesStore->nSynthesizedTrivial++;
+ s_pSesStore->pSynthesizedTrivial[0]++;
+
*Cost = 0;
+ s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
return 0;
}
if ( nVars == 1 )
{
+ s_pSesStore->nSynthesizedTrivial++;
+ s_pSesStore->pSynthesizedTrivial[1]++;
+
*Cost = 0;
pPerm[0] = (char)0;
+ s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
return pArrTimeProfile[0];
}
- nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &nMaxArrival );
+ if ( s_pSesStore->fVeryVerbose )
+ {
+ printf( "arrival times input:" );
+ for ( l = 0; l < nVars; ++l )
+ printf( " %d", pArrTimeProfile[l] );
+ printf( "\n" );
+ }
+
+ for ( l = 0; l < nVars; ++l )
+ pNormalArrTime[l] = pArrTimeProfile[l];
+
+ Abc_NormalizeArrivalTimes( pNormalArrTime, nVars, &nMaxArrival );
if ( s_pSesStore->fVeryVerbose )
{
@@ -1541,35 +1872,34 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
Abc_TtPrintHexRev( stdout, pTruth, nVars );
printf( " with arrival times" );
for ( l = 0; l < nVars; ++l )
- printf( " %d", pArrTimeProfile[l] );
+ printf( " %d", pNormalArrTime[l] );
printf( " at level %d\n", AigLevel );
}
- /* statistics */
- s_pSesStore->nCutCount++;
- s_pSesStore->pCutCount[nVars]++;
-
*Cost = ABC_INFINITY;
- if ( Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, &pSol ) )
+ if ( Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, &pSol ) )
{
if ( s_pSesStore->fVeryVerbose )
printf( " truth table already in store\n" );
- s_pSesStore->nCacheHit++;
+
+ s_pSesStore->nCacheHits++;
+ s_pSesStore->pCacheHits[nVars]++;
}
else
{
- nMaxDepth = pArrTimeProfile[0];
+ nMaxDepth = pNormalArrTime[0];
for ( i = 1; i < nVars; ++i )
- nMaxDepth = Abc_MaxInt( nMaxDepth, pArrTimeProfile[i] );
+ nMaxDepth = Abc_MaxInt( nMaxDepth, pNormalArrTime[i] );
nMaxDepth += nVars + 1;
- //nMaxDepth = Abc_MinInt( AigLevel, nMaxDepth + nVars + 1 );
+ if ( AigLevel != -1 )
+ nMaxDepth = Abc_MinInt( AigLevel, nMaxDepth + nVars + 1 );
- timeStart = Abc_Clock();
+ timeStartExact = Abc_Clock();
- pSes = Ses_ManAlloc( pTruth, nVars, 1 /* nSpecFunc */, nMaxDepth, pArrTimeProfile, s_pSesStore->fMakeAIG, s_pSesStore->fVerbose );
- pSes->nBTLimit = s_pSesStore->nBTLimit;
+ pSes = Ses_ManAlloc( pTruth, nVars, 1 /* nSpecFunc */, nMaxDepth, pNormalArrTime, s_pSesStore->fMakeAIG, s_pSesStore->nBTLimit, s_pSesStore->fVerbose );
pSes->fVeryVerbose = s_pSesStore->fVeryVerbose;
+ pSes->pSat = s_pSesStore->pSat;
while ( pSes->nMaxDepth ) /* there is improvement */
{
@@ -1591,18 +1921,35 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
else
{
if ( s_pSesStore->fVeryVerbose )
- printf( " NOT FOUND\n" );
+ printf( " NOT FOUND (%d)\n", pSes->fHitResLimit );
break;
}
}
- pSes->timeTotal = Abc_Clock() - timeStart;
+ /* 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;
- /* cleanup */
- Ses_ManClean( pSes );
+ /* statistics */
+ s_pSesStore->nSatCalls += pSes->nSatCalls;
+ s_pSesStore->nUnsatCalls += pSes->nUnsatCalls;
+ s_pSesStore->nUndefCalls += pSes->nUndefCalls;
+
+ s_pSesStore->timeSat += pSes->timeSat;
+ s_pSesStore->timeSatSat += pSes->timeSatSat;
+ s_pSesStore->timeSatUnsat += pSes->timeSatUnsat;
+ s_pSesStore->timeSatUndef += pSes->timeSatUndef;
+ s_pSesStore->timeInstance += pSes->timeInstance;
+ s_pSesStore->timeExact += pSes->timeTotal;
+
+ /* cleanup (we need to clean before adding since pTruth may have been modified by pSes) */
+ fResLimit = pSes->fHitResLimit;
+ Ses_ManCleanLight( pSes );
/* store solution */
- Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol );
+ Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, pSol, fResLimit );
}
if ( pSol )
@@ -1614,49 +1961,66 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
pPerm[l] = *p++;
}
- /* 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 );
-
- return nDelta + Delay;
+ 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 );
+ //}
+
+ s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
+ return Delay2;
+ }
+ else
+ {
+ assert( *Cost == ABC_INFINITY );
+
+ s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
+ return ABC_INFINITY;
+ }
}
// this procedure returns a new node whose output in terms of the given fanins
// 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 = NULL;
- int i, j, nDelta, nMaxArrival;
+ int i, j, nMaxArrival;
+ int pNormalArrTime[8];
char const * p;
Abc_Obj_t * pObj;
Vec_Ptr_t * pGates;
char pGateTruth[5];
char * pSopCover;
+ abctime timeStart = Abc_Clock();
if ( nVars == 0 )
+ {
+ s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
return (pTruth[0] & 1) ? Abc_NtkCreateNodeConst1(pNtk) : Abc_NtkCreateNodeConst0(pNtk);
+ }
if ( nVars == 1 )
+ {
+ s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
return (pTruth[0] & 1) ? Abc_NtkCreateNodeInv(pNtk, pFanins[0]) : Abc_NtkCreateNodeBuf(pNtk, pFanins[0]);
+ }
- nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &nMaxArrival );
- Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, &pSol );
- Abc_UnnormalizeArrivalTimes( pArrTimeProfile, nVars, nDelta );
+ for ( i = 0; i < nVars; ++i )
+ pNormalArrTime[i] = pArrTimeProfile[i];
+ Abc_NormalizeArrivalTimes( pNormalArrTime, nVars, &nMaxArrival );
+ Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, &pSol );
if ( !pSol )
+ {
+ s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
return NULL;
+ }
assert( pSol[ABC_EXACT_SOL_NVARS] == nVars );
assert( pSol[ABC_EXACT_SOL_NFUNC] == 1 );
@@ -1668,6 +2032,7 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile,
/* primary inputs */
for ( i = 0; i < nVars; ++i )
{
+ assert( pFanins[i] );
Vec_PtrPush( pGates, pFanins[i] );
}
@@ -1690,6 +2055,7 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile,
pSopCover = Abc_SopFromTruthBin( pGateTruth );
pObj = Abc_NtkCreateNode( pNtk );
+ assert( pObj );
pObj->pData = Abc_SopRegister( (Mem_Flex_t*)pNtk->pManFunc, pSopCover );
Vec_PtrPush( pGates, pObj );
ABC_FREE( pSopCover );
@@ -1703,6 +2069,7 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile,
Vec_PtrFree( pGates );
+ s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
return pObj;
}