diff options
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abc.c | 76 | ||||
| -rw-r--r-- | src/base/abci/abcExact.c | 1672 |
2 files changed, 1438 insertions, 310 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 151d05c9..8322f27c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7293,15 +7293,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 nStartGates, 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, nStartGates = 1, 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, "DASCatvh" ) ) != EOF ) { switch ( c ) { @@ -7316,6 +7318,51 @@ 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 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + nStartGates = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nStartGates < 1 ) + goto usage; + 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; @@ -7372,7 +7419,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, nStartGates - 1, fVerbose ); if ( pGiaRes ) Abc_FrameUpdateGia( pAbc, pGiaRes ); else @@ -7380,7 +7427,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, nStartGates - 1, fVerbose ); if ( pNtkRes ) { Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); @@ -7392,16 +7439,19 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: exact [-D <num>] [-atvh] <truth1> <truth2> ...\n" ); + Abc_Print( -2, "usage: exact [-DSC <num>] [-A <list>] [-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-S <num> : number of start gates in search [default = %s]\n", nStartGates ); + 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..6a7becb8 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" @@ -39,6 +38,12 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*********************************************************************** + + Synopsis [Some truth table helper functions.] + +***********************************************************************/ + 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), @@ -50,48 +55,188 @@ static word s_Truths8[32] = { ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF) }; +static word s_Truths8Neg[32] = { + ABC_CONST(0x5555555555555555), ABC_CONST(0x5555555555555555), ABC_CONST(0x5555555555555555), ABC_CONST(0x5555555555555555), + ABC_CONST(0x3333333333333333), ABC_CONST(0x3333333333333333), ABC_CONST(0x3333333333333333), ABC_CONST(0x3333333333333333), + ABC_CONST(0x0F0F0F0F0F0F0F0F), ABC_CONST(0x0F0F0F0F0F0F0F0F), ABC_CONST(0x0F0F0F0F0F0F0F0F), ABC_CONST(0x0F0F0F0F0F0F0F0F), + ABC_CONST(0x00FF00FF00FF00FF), ABC_CONST(0x00FF00FF00FF00FF), ABC_CONST(0x00FF00FF00FF00FF), ABC_CONST(0x00FF00FF00FF00FF), + ABC_CONST(0x0000FFFF0000FFFF), ABC_CONST(0x0000FFFF0000FFFF), ABC_CONST(0x0000FFFF0000FFFF), ABC_CONST(0x0000FFFF0000FFFF), + ABC_CONST(0x00000000FFFFFFFF), ABC_CONST(0x00000000FFFFFFFF), ABC_CONST(0x00000000FFFFFFFF), ABC_CONST(0x00000000FFFFFFFF), + ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), + ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000) +}; + +static int Abc_TtIsSubsetWithMask( word * pSmall, word * pLarge, word * pMask, int nWords ) +{ + int w; + for ( w = 0; w < nWords; ++w ) + if ( ( pSmall[w] & pLarge[w] & pMask[w] ) != ( pSmall[w] & pMask[w] ) ) + return 0; + return 1; +} + +// checks whether we can decompose as OP(x^p, g) where OP in {AND, OR} and p in {0, 1} +// returns p if OP = AND, and 2 + p if OP = OR +static int Abc_TtIsTopDecomposable( word * pTruth, word * pMask, int nWords, int nVar ) +{ + assert( nVar < 8 ); + + if ( Abc_TtIsSubsetWithMask( pTruth, &s_Truths8[nVar << 2], pMask, nWords ) ) return 1; + if ( Abc_TtIsSubsetWithMask( pTruth, &s_Truths8Neg[nVar << 2], pMask, nWords ) ) return 2; + if ( Abc_TtIsSubsetWithMask( &s_Truths8[nVar << 2], pTruth, pMask, nWords ) ) return 3; + if ( Abc_TtIsSubsetWithMask( &s_Truths8Neg[nVar << 2], pTruth, pMask, nWords ) ) return 4; + + return 0; +} + +// checks whether we can decompose as OP(x1, OP(x2, OP(x3, ...))) where pVars = {x1, x2, x3, ...} +// OP can be different and vars can be complemented +static int Abc_TtIsStairDecomposable( word * pTruth, int nWords, int * pVars, int nSize ) +{ + int i, d; + word pMask[4]; + + Abc_TtMask( pMask, nWords, nWords * 64 ); + + for ( i = 0; i < nSize; ++i ) + { + d = Abc_TtIsTopDecomposable( pTruth, pMask, nWords, pVars[i] ); + if ( !d ) return 0; /* not decomposable */ + + switch ( d ) + { + case 1: /* AND(x, g) */ + case 4: /* OR(!x, g) */ + Abc_TtAnd( pMask, pMask, &s_Truths8[pVars[i] << 2], nWords, 0 ); + break; + case 2: /* AND(!x, g) */ + case 3: /* OR(x, g) */ + Abc_TtAnd( pMask, pMask, &s_Truths8Neg[pVars[i] << 2], nWords, 0 ); + break; + } + } + + return 1; /* decomposable */ +} + +/*********************************************************************** + + Synopsis [Some printing utilities.] + +***********************************************************************/ + +static inline void Abc_DebugPrint( const char* str, int fCond ) +{ + if ( fCond ) + { + printf( "%s", str ); + fflush( stdout ); + } +} + +static inline void Abc_DebugPrintInt( const char* fmt, int n, int fCond ) +{ + if ( fCond ) + { + printf( fmt, n ); + fflush( stdout ); + } +} + +static inline void Abc_DebugPrintIntInt( const char* fmt, int n1, int n2, int fCond ) +{ + if ( fCond ) + { + printf( fmt, n1, n2 ); + fflush( stdout ); + } +} + +static inline void Abc_DebugErase( int n, int fCond ) +{ + int i; + if ( fCond ) + { + for ( i = 0; i < n; ++i ) + printf( "\b" ); + fflush( stdout ); + } +} + +/*********************************************************************** + + Synopsis [BMS.] + +***********************************************************************/ + #define ABC_EXACT_SOL_NVARS 0 #define ABC_EXACT_SOL_NFUNC 1 #define ABC_EXACT_SOL_NGATES 2 +#define ANSI_COLOR_RED "\x1b[31m" +#define ANSI_COLOR_GREEN "\x1b[32m" +#define ANSI_COLOR_YELLOW "\x1b[33m" +#define ANSI_COLOR_BLUE "\x1b[34m" +#define ANSI_COLOR_MAGENTA "\x1b[35m" +#define ANSI_COLOR_CYAN "\x1b[36m" +#define ANSI_COLOR_RESET "\x1b[0m" + typedef struct Ses_Man_t_ Ses_Man_t; struct Ses_Man_t_ { - sat_solver * pSat; /* SAT solver */ - - word * pSpec; /* specification */ - int bSpecInv; /* remembers whether spec was inverted for normalization */ - int nSpecVars; /* number of variables in specification */ - int nSpecFunc; /* number of functions to synthesize */ - 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) */ - int nArrTimeDelta; /* delta to the original arrival times (arrival times are normalized to have 0 as minimum element) */ - int nArrTimeMax; /* maximum normalized arrival time */ - int nBTLimit; /* conflict limit */ - 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 */ - - int nSimVars; /* number of simulation vars x(i, t) */ - int nOutputVars; /* number of output variables g(h, i) */ - int nGateVars; /* number of gate variables f(i, p, q) */ - int nSelectVars; /* number of select variables s(i, j, k) */ - int nDepthVars; /* number of depth variables d(i, j) */ - - int nOutputOffset; /* offset where output variables start */ - int nGateOffset; /* offset where gate variables start */ - int nSelectOffset; /* offset where select variables start */ - int nDepthOffset; /* offset where depth variables start */ - - abctime timeSat; /* SAT runtime */ - abctime timeSatSat; /* SAT runtime (sat instance) */ - abctime timeSatUnsat; /* SAT runtime (unsat instance) */ - abctime timeTotal; /* all runtime */ + sat_solver * pSat; /* SAT solver */ + + word * pSpec; /* specification */ + 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 nMaxDepthTmp; /* temporary copy to modify nMaxDepth temporarily */ + int * pArrTimeProfile; /* arrival times of inputs (NULL if arrival times are ignored) */ + int pArrTimeProfileTmp[8]; /* temporary copy to modify pArrTimeProfile temporarily */ + int nArrTimeDelta; /* delta to the original arrival times (arrival times are normalized to have 0 as minimum element) */ + int nArrTimeMax; /* maximum normalized arrival time */ + int nBTLimit; /* conflict limit */ + 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 fReasonVerbose; /* be verbose about give-up reasons */ + word pTtValues[4]; /* truth table values to assign */ + + int nGates; /* number of gates */ + int nStartGates; /* number of gates to start search (-1), i.e., to start from 1 gate, one needs to specify 0 */ + int nMaxGates; /* maximum number of gates given max. delay and arrival times */ + int fDecStructure; /* set to 1 or higher if nSpecFunc = 1 and f = x_i OP g(X \ {x_i}), otherwise 0 (determined when solving) */ + int pDecVars; /* mask of variables that can be decomposed at top-level */ + word pTtObjs[100]; /* temporary truth tables */ + + int nSimVars; /* number of simulation vars x(i, t) */ + int nOutputVars; /* number of output variables g(h, i) */ + int nGateVars; /* number of gate variables f(i, p, q) */ + int nSelectVars; /* number of select variables s(i, j, k) */ + int nDepthVars; /* number of depth variables d(i, j) */ + + int nOutputOffset; /* offset where output variables start */ + int nGateOffset; /* offset where gate variables start */ + 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 +254,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 +279,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 +341,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 +381,7 @@ static inline void Ses_StoreClean( Ses_Store_t * pStore ) } } + sat_solver_delete( pStore->pSat ); ABC_FREE( pStore ); } @@ -228,7 +390,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 +402,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 +412,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,14 +432,102 @@ 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, char * pSol, int nStartGates ) +{ + int l; + + fprintf( pStore->pDebugEntries, "abc -c \"exact -v -C %d", pStore->nBTLimit ); + if ( s_pSesStore->fMakeAIG ) fprintf( pStore->pDebugEntries, " -a" ); + fprintf( pStore->pDebugEntries, " -S %d -D %d -A", nStartGates + 1, 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, "\" # " ); + + if ( !pSol ) + fprintf( pStore->pDebugEntries, "no " ); + fprintf( pStore->pDebugEntries, "solution found before\n" ); +} + +static void Abc_ExactNormalizeArrivalTimesForNetwork( int nVars, int * pArrTimeProfile, char * pSol ) +{ + int nGates, i, j, k, nMax; + Vec_Int_t * vLevels; + + nGates = pSol[ABC_EXACT_SOL_NGATES]; + + /* printf( "NORMALIZE\n" ); */ + /* printf( " #vars = %d\n", nVars ); */ + /* printf( " #gates = %d\n", nGates ); */ + + vLevels = Vec_IntAllocArrayCopy( pArrTimeProfile, nVars ); + + /* compute level of each gate based on arrival time profile (to compute depth) */ + for ( i = 0; i < nGates; ++i ) + { + j = pSol[3 + i * 4 + 2]; + k = pSol[3 + i * 4 + 3]; + + Vec_IntPush( vLevels, Abc_MaxInt( Vec_IntEntry( vLevels, j ), Vec_IntEntry( vLevels, k ) ) + 1 ); + + /* printf( " gate %d = (%d,%d)\n", nVars + i, j, k ); */ + } + + /* Vec_IntPrint( vLevels ); */ + + /* reset all levels except for the last one */ + for ( i = 0; i < nVars + nGates - 1; ++i ) + Vec_IntSetEntry( vLevels, i, Vec_IntEntry( vLevels, nVars + nGates - 1 ) ); + + /* Vec_IntPrint( vLevels ); */ + + /* compute levels from top to bottom */ + for ( i = nGates - 1; i >= 0; --i ) + { + j = pSol[3 + i * 4 + 2]; + k = pSol[3 + i * 4 + 3]; + + Vec_IntSetEntry( vLevels, j, Abc_MinInt( Vec_IntEntry( vLevels, j ), Vec_IntEntry( vLevels, nVars + i ) - 1 ) ); + Vec_IntSetEntry( vLevels, k, Abc_MinInt( Vec_IntEntry( vLevels, k ), Vec_IntEntry( vLevels, nVars + i ) - 1 ) ); + } + + /* Vec_IntPrint( vLevels ); */ + + /* normalize arrival times */ + Abc_NormalizeArrivalTimes( Vec_IntArray( vLevels ), nVars, &nMax ); + memcpy( pArrTimeProfile, Vec_IntArray( vLevels ), sizeof(int) * nVars ); + + /* printf( " nMax = %d\n", nMax ); */ + /* Vec_IntPrint( vLevels ); */ + + Vec_IntFree( vLevels ); +} + // 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; Ses_TimesEntry_t * pTiEntry; + if ( pSol ) + Abc_ExactNormalizeArrivalTimesForNetwork( nVars, pArrTimeProfile, pSol ); + key = Ses_StoreTableHash( pTruth, nVars ); pTEntry = pStore->pEntries[key]; @@ -315,6 +565,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,15 +576,46 @@ 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; } // 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 Ses_StoreGetEntrySimple( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char ** pSol ) { int key; Ses_TruthEntry_t * pTEntry; @@ -373,9 +655,62 @@ 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 Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char ** pSol ) +{ + int key; + Ses_TruthEntry_t * pTEntry; + Ses_TimesEntry_t * pTiEntry; + int pTimes[8]; + + key = Ses_StoreTableHash( pTruth, nVars ); + pTEntry = pStore->pEntries[key]; + + /* find truth table entry */ + while ( pTEntry ) + { + if ( Ses_StoreTruthEqual( pTEntry, pTruth, nVars ) ) + break; + else + pTEntry = pTEntry->next; + } + + /* no entry found? */ + if ( !pTEntry ) + return 0; + + /* find times entry */ + pTiEntry = pTEntry->head; + while ( pTiEntry ) + { + /* found after normalization wrt. to network */ + if ( pTiEntry->pNetwork ) + { + memcpy( pTimes, pArrTimeProfile, sizeof(int) * nVars ); + Abc_ExactNormalizeArrivalTimesForNetwork( nVars, pTimes, pTiEntry->pNetwork ); + + if ( Ses_StoreTimesEqual( pTimes, pTiEntry->pArrTimeProfile, nVars ) ) + break; + } + /* found for non synthesized network */ + else if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) ) + break; + else + pTiEntry = pTiEntry->next; + } + + /* no entry found? */ + if ( !pTiEntry ) + return 0; + + *pSol = pTiEntry->pNetwork; + 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; @@ -387,7 +722,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 +738,27 @@ static void Ses_StoreWrite( Ses_Store_t * pStore, const char * pFilename ) 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( 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 +769,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 +788,69 @@ 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 ); + } - Ses_StoreAddEntry( pStore, pTruth, nVars, pArrTimeProfile, pNetwork ); + 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, fResLimit ); } fclose( pFile ); + + printf( "read %lu entries from file\n", nEntries ); +} + +// computes top decomposition of variables wrt. to AND and OR +static inline void Ses_ManComputeTopDec( Ses_Man_t * pSes ) +{ + int l, i, mask = ~0; + word * pVar; + int fAnd, fAndC, fOr, fOrC; + + if ( pSes->nSpecVars < 6u ) + mask = Abc_Tt6Mask( 1u << pSes->nSpecVars ); + + for ( l = 0; l < pSes->nSpecVars; ++l ) + { + pVar = &s_Truths8[l << 2]; + fAnd = fAndC = fOr = fOrC = 1; + + for ( i = 0; i < pSes->nSpecWords; ++i ) + { + fAnd &= ( pVar[i] & pSes->pSpec[i] & mask ) == ( pSes->pSpec[i] & mask ); + fAndC &= ( ~pVar[i] & pSes->pSpec[i] & mask ) == ( pSes->pSpec[i] & mask ); + fOr &= ( pVar[i] & pSes->pSpec[i] & mask ) == ( pVar[i] & mask ); + fOrC &= ( ~pVar[i] & pSes->pSpec[i] & mask ) == ( ~pVar[i] & mask ); + } + + pSes->pDecVars |= ( fAnd | fAndC | fOr | fOrC ) << l; + } } -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 +864,31 @@ 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; + + if ( p->nSpecFunc == 1 ) + Ses_ManComputeTopDec( p ); 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 +900,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************************************************************* @@ -563,6 +967,52 @@ static inline int Ses_ManDepthVar( Ses_Man_t * pSes, int i, int j ) /**Function************************************************************* + Synopsis [Compute truth table from a solution.] + +***********************************************************************/ +static word * Ses_ManDeriveTruth( Ses_Man_t * pSes, char * pSol, int fInvert ) +{ + int i, f, j, k, w, nGates = pSol[ABC_EXACT_SOL_NGATES]; + char * p; + word * pTruth, * pTruth0, * pTruth1; + assert( pSol[ABC_EXACT_SOL_NFUNC] == 1 ); + + p = pSol + 3; + + memset( pSes->pTtObjs, 0, sizeof( word ) * 4 * nGates ); + + for ( i = 0; i < nGates; ++i ) + { + f = *p++; + assert( *p++ == 2 ); + j = *p++; + k = *p++; + + pTruth0 = j < pSes->nSpecVars ? &s_Truths8[j << 2] : &pSes->pTtObjs[( j - pSes->nSpecVars ) << 2]; + pTruth1 = k < pSes->nSpecVars ? &s_Truths8[k << 2] : &pSes->pTtObjs[( k - pSes->nSpecVars ) << 2]; + + pTruth = &pSes->pTtObjs[i << 2]; + + if ( f & 1 ) + for ( w = 0; w < pSes->nSpecWords; ++w ) + pTruth[w] |= ~pTruth0[w] & pTruth1[w]; + if ( ( f >> 1 ) & 1 ) + for ( w = 0; w < pSes->nSpecWords; ++w ) + pTruth[w] |= pTruth0[w] & ~pTruth1[w]; + if ( ( f >> 2 ) & 1 ) + for ( w = 0; w < pSes->nSpecWords; ++w ) + pTruth[w] |= pTruth0[w] & pTruth1[w]; + } + + assert( Abc_Lit2Var( *p ) == nGates - 1 ); + if ( fInvert && Abc_LitIsCompl( *p ) ) + Abc_TtNot( pTruth, pSes->nSpecWords ); + + return pTruth; +} + +/**Function************************************************************* + Synopsis [Setup variables to find network with nGates gates.] ***********************************************************************/ @@ -589,9 +1039,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 +1054,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 +1069,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,64 +1078,128 @@ 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 ) +static int inline Ses_ManCreateTruthTableClause( Ses_Man_t * pSes, int t ) { - extern int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 ); - - int h, i, j, k, t, ii, jj, kk, p, q, d; + int i, j, k, h; int pLits[3]; - Vec_Int_t * vLits; - for ( t = 0; t < pSes->nRows; ++t ) - for ( i = 0; i < pSes->nGates; ++i ) - { - /* main clauses */ - for ( j = 0; j < pSes->nSpecVars + i; ++j ) - for ( k = j + 1; k < pSes->nSpecVars + i; ++k ) - { - Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 0, 1 ); - Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 0 ); - Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 1 ); - Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 0 ); - Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 1 ); - Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 0 ); - Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 1 ); - } + for ( i = 0; i < pSes->nGates; ++i ) + { + /* main clauses */ + for ( j = 0; j < pSes->nSpecVars + i; ++j ) + for ( k = j + 1; k < pSes->nSpecVars + i; ++k ) + { + Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 0, 1 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 0 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 0, 1, 1 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 0 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 0, 1 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 0 ); + Ses_ManCreateMainClause( pSes, t, i, j, k, 1, 1, 1 ); + } - /* output clauses */ + /* output clauses */ + if ( pSes->nSpecFunc != 1 ) for ( h = 0; h < pSes->nSpecFunc; ++h ) { 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 ) ); + if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) ) + return 0; } + } + + if ( pSes->nSpecFunc == 1 ) + { + pLits[0] = Abc_Var2Lit( Ses_ManSimVar( pSes, pSes->nGates - 1, t ), 1 - Abc_TtGetBit( pSes->pSpec, t + 1 ) ); + if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) + return 0; + } + + return 1; +} + +static int Ses_ManCreateClauses( Ses_Man_t * pSes ) +{ + extern int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 ); + + int h, i, j, k, t, ii, jj, kk, p, q; + int pLits[3]; + Vec_Int_t * vLits = NULL; + + for ( t = 0; t < pSes->nRows; ++t ) + { + if ( Abc_TtGetBit( pSes->pTtValues, t ) ) + if ( !Ses_ManCreateTruthTableClause( pSes, t ) ) + return 0; + } + + /* 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 ) ) + return 0; } + pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, pSes->nGates - 1 ), 0 ); + if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) + return 0; - /* some output is selected */ - for ( h = 0; h < pSes->nSpecFunc; ++h ) + vLits = Vec_IntAlloc( 0u ); + } + else { - 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 ); + vLits = Vec_IntAlloc( 0u ); + + /* 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 ); } + /* gate decomposition (makes it worse) */ + /* if ( fDecVariable >= 0 && pSes->nGates >= 2 ) */ + /* { */ + /* pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, pSes->nGates - 1, fDecVariable, pSes->nSpecVars + pSes->nGates - 2 ), 0 ); */ + /* if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) */ + /* { */ + /* Vec_IntFree( vLits ); */ + /* return 0; */ + /* } */ + + /* for ( k = 1; k < pSes->nSpecVars + pSes->nGates - 1; ++k ) */ + /* for ( j = 0; j < k; ++j ) */ + /* if ( j != fDecVariable || k != pSes->nSpecVars + pSes->nGates - 2 ) */ + /* { */ + /* pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, pSes->nGates - 1, j, k ), 1 ); */ + /* if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ) */ + /* { */ + /* Vec_IntFree( vLits ); */ + /* return 0; */ + /* } */ + /* } */ + /* } */ + /* only AIG */ if ( pSes->fMakeAIG ) { @@ -693,36 +1209,91 @@ 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 ); } } + /* only binary clauses */ + if ( 1 ) /* TODO: add some meaningful parameter */ + { + for ( i = 0; i < pSes->nGates; ++i ) + { + pLits[0] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 0, 1 ), 0 ); + pLits[1] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 0 ), 0 ); + pLits[2] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, 1, 1 ), 0 ); + 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 ); + 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 ); + sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ); + } + + for ( i = 0; i < pSes->nGates; ++i ) + for ( k = 1; k < pSes->nSpecVars + i; ++k ) + for ( j = 0; j < k; ++j ) + { + pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 ); + + for ( kk = 1; kk < pSes->nSpecVars + i; ++kk ) + for ( jj = 0; jj < kk; ++jj ) + { + if ( k == kk && j == jj ) continue; + pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, jj, kk ), 1 ); + + if ( pLits[0] < pLits[1] ) + sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ); + } + } + + /* Vec_IntGrowResize( vLits, pSes->nGates * ( pSes->nSpecVars + pSes->nGates - 2 ) ); */ + + /* for ( j = 0; j < pSes->nSpecVars; ++j ) */ + /* { */ + /* jj = 0; */ + /* for ( i = 0; i < pSes->nGates; ++i ) */ + /* { */ + /* for ( k = 0; k < j; ++k ) */ + /* Vec_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, k, j ), 0 ) ); */ + /* for ( k = j + 1; k < pSes->nSpecVars + i; ++k ) */ + /* 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 ); */ + /* } */ + } + /* 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 ) @@ -747,12 +1318,13 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) } /* EXTRA clauses: symmetric variables */ - if ( pSes->nMaxDepth == -1 && pSes->nSpecFunc == 1 ) /* only check if there is one output function */ + if ( /*pSes->nMaxDepth == -1 &&*/ pSes->nSpecFunc == 1 ) /* only check if there is one output function */ for ( q = 1; q < pSes->nSpecVars; ++q ) for ( p = 0; p < q; ++p ) - if ( Extra_TruthVarsSymm( (unsigned*)( &pSes->pSpec[h << 2] ), pSes->nSpecVars, p, q ) ) + if ( Extra_TruthVarsSymm( (unsigned*)( pSes->pSpec ), pSes->nSpecVars, p, q ) && + ( !pSes->pArrTimeProfile || ( pSes->pArrTimeProfile[p] <= pSes->pArrTimeProfile[q] ) ) ) { - if ( pSes->fVeryVerbose ) + if ( pSes->fSatVerbose ) printf( "variables %d and %d are symmetric\n", p, q ); for ( i = 0; i < pSes->nGates; ++i ) for ( j = 0; j < q; ++j ) @@ -766,81 +1338,85 @@ 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 ) - { - for ( i = 0; i < pSes->nGates; ++i ) - { - /* propagate depths from children */ - for ( k = 1; k < i; ++k ) - for ( j = 0; j < k; ++j ) - { - pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, pSes->nSpecVars + j, pSes->nSpecVars + k ), 1 ); - for ( jj = 0; jj <= pSes->nArrTimeMax + j; ++jj ) - { - 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 ) ); - } - } - - for ( k = 0; k < i; ++k ) - for ( j = 0; j < pSes->nSpecVars + k; ++j ) - { - pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, pSes->nSpecVars + k ), 1 ); - for ( kk = 0; kk <= pSes->nArrTimeMax + k; ++kk ) - { - 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 ) ); - } - } + return 1; +} - /* propagate depths from arrival times at PIs */ - if ( pSes->pArrTimeProfile ) - { - for ( k = 1; k < pSes->nSpecVars + i; ++k ) - for ( j = 0; j < ( ( k < pSes->nSpecVars ) ? k : pSes->nSpecVars ); ++j ) - { - d = pSes->pArrTimeProfile[j]; - if ( k < pSes->nSpecVars && pSes->pArrTimeProfile[k] > d ) - d = pSes->pArrTimeProfile[k]; +static int Ses_ManCreateDepthClauses( Ses_Man_t * pSes ) +{ + int i, j, k, jj, kk, d, h; + int pLits[3]; - 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 ) ); - } - } - else + for ( i = 0; i < pSes->nGates; ++i ) + { + /* propagate depths from children */ + for ( k = 1; k < i; ++k ) + for ( j = 0; j < k; ++j ) { - /* arrival times are 0 */ - pLits[0] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, 0 ), 0 ); - assert( sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ) ); + pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, pSes->nSpecVars + j, pSes->nSpecVars + k ), 1 ); + for ( jj = 0; jj <= pSes->nArrTimeMax + j; ++jj ) + { + pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, j, jj ), 1 ); + pLits[2] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, jj + 1 ), 0 ); + sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ); + } } - /* reverse order encoding of depth variables */ - for ( j = 1; j <= pSes->nArrTimeMax + i; ++j ) + for ( k = 0; k < i; ++k ) + for ( j = 0; j < pSes->nSpecVars + k; ++j ) { - 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 ) ); + pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, pSes->nSpecVars + k ), 1 ); + for ( kk = 0; kk <= pSes->nArrTimeMax + k; ++kk ) + { + pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, k, kk ), 1 ); + pLits[2] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, kk + 1 ), 0 ); + sat_solver_addclause( pSes->pSat, pLits, pLits + 3 ); + } } - /* constrain maximum depth */ - if ( pSes->nMaxDepth < pSes->nArrTimeMax + i ) - for ( h = 0; h < pSes->nSpecFunc; ++h ) + /* propagate depths from arrival times at PIs */ + if ( pSes->pArrTimeProfile ) + { + for ( k = 1; k < pSes->nSpecVars + i; ++k ) + for ( j = 0; j < ( ( k < pSes->nSpecVars ) ? k : pSes->nSpecVars ); ++j ) { - pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 ); - pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, pSes->nMaxDepth ), 1 ); - if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) ) - return 0; + d = pSes->pArrTimeProfile[j]; + if ( k < pSes->nSpecVars && pSes->pArrTimeProfile[k] > d ) + d = pSes->pArrTimeProfile[k]; + + pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 ); + 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 ); + sat_solver_addclause( pSes->pSat, pLits, pLits + 1 ); + } + + /* reverse order encoding of depth variables */ + for ( j = 1; j <= pSes->nArrTimeMax + i; ++j ) + { + pLits[0] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, j ), 1 ); + pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, j - 1 ), 0 ); + sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ); + } + + /* constrain maximum depth */ + if ( pSes->nMaxDepth < pSes->nArrTimeMax + i ) + for ( h = 0; h < pSes->nSpecFunc; ++h ) + { + pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 ); + pLits[1] = Abc_Var2Lit( Ses_ManDepthVar( pSes, i, pSes->nMaxDepth ), 1 ); + if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) ) + return 0; + } } return 1; @@ -865,20 +1441,27 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes ) status = sat_solver_solve( pSes->pSat, NULL, NULL, pSes->nBTLimit, 0, 0, 0 ); timeDelta = Abc_Clock() - timeStart; + if ( pSes->fSatVerbose ) + Sat_SolverPrintStats( stdout, pSes->pSat ); + pSes->timeSat += timeDelta; 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" ); @@ -944,6 +1527,7 @@ static char * Ses_ManExtractSolution( Ses_Man_t * pSes ) printf( " and operands %d and %d", j, k ); *p++ = j; *p++ = k; + k = pSes->nSpecVars + i; break; } @@ -991,17 +1575,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 ) - printf( "output %d points to %d and has normalized delay %d (nArrTimeDelta = %d)\n", h, i, d, pSes->nArrTimeDelta ); + if ( pSes->pArrTimeProfile && pSes->fExtractVerbose ) + printf( "output %d points to gate %d and has normalized delay %d (nArrTimeDelta = %d)\n", h, pSes->nSpecVars + 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; } @@ -1014,6 +1601,10 @@ static char * Ses_ManExtractSolution( Ses_Man_t * pSes ) /* have we used all the fields? */ assert( ( p - pSol ) == nSol ); + /* printf( "found network: " ); */ + /* Abc_TtPrintHexRev( stdout, Ses_ManDeriveTruth( pSes, pSol, 1 ), pSes->nSpecVars ); */ + /* printf( "\n" ); */ + return pSol; } @@ -1168,10 +1759,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 +1778,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 ) @@ -1224,30 +1829,385 @@ static inline void Ses_ManPrintVars( Ses_Man_t * pSes ) Synopsis [Synthesis algorithm.] ***********************************************************************/ +static void Ses_ManComputeMaxGates( Ses_Man_t * pSes ) +{ + int s = 1, lvl = pSes->nMaxDepth, avail = pSes->nSpecVars, l; + + pSes->nMaxGates = 0; + + /* s is the number of gates we have in the current level */ + while ( s && /* while there are nodes to branch from */ + lvl && /* while we are at some level */ + avail * 2 > s /* while there are still enough available nodes (heuristic) */ ) + { + /* erase from s if we have arriving nodes */ + for ( l = 0; l < pSes->nSpecVars; ++l ) + if ( pSes->pArrTimeProfile[l] == lvl ) + { + --s; + --avail; + } + + --lvl; + pSes->nMaxGates += s; + s *= 2; + } +} + +// returns 0, if current max depth and arrival times are not consistent +static int Ses_CheckDepthConsistency( Ses_Man_t * pSes ) +{ + int l, i, fAdded, nLevel; + int fMaxGatesLevel2 = 1; + Vec_Int_t * pStairDecVars; + + pSes->fDecStructure = 0; + + for ( l = 0; l < pSes->nSpecVars; ++l ) + { + if ( pSes->pArrTimeProfile[l] >= pSes->nMaxDepth ) + { + if ( pSes->fReasonVerbose ) + 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 ( ( pSes->fDecStructure == 1 && pSes->nSpecVars > 2 ) || pSes->fDecStructure == 2 ) + { + if ( pSes->fReasonVerbose ) + printf( "give up due to impossible decomposition (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] ); + return 0; + } + + pSes->fDecStructure++; + + /* A subset B <=> A and B = A */ + if ( !( ( pSes->pDecVars >> l ) & 1 ) ) + { + if ( pSes->fReasonVerbose ) + printf( "give up due to impossible decomposition (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] ); + return 0; + } + } + } + + /* more complicated decomposition */ + if ( pSes->fDecStructure ) + { + pStairDecVars = Vec_IntAlloc( 0 ); + + nLevel = 1; + while ( 1 ) + { + fAdded = 0; + + for ( l = 0; l < pSes->nSpecVars; ++l ) + if ( pSes->pArrTimeProfile[l] + nLevel == pSes->nMaxDepth ) + { + if ( fAdded ) + { + assert( nLevel == Vec_IntSize( pStairDecVars ) ); + if ( fAdded > 1 || ( nLevel + 1 < pSes->nSpecVars ) ) + { + Vec_IntFree( pStairDecVars ); + if ( pSes->fReasonVerbose ) + printf( "give up due to impossible decomposition at level %d", nLevel ); + return 0; + } + } + + Vec_IntPush( pStairDecVars, l ); + fAdded++; + } + + if ( !fAdded ) break; + ++nLevel; + } + + if ( Vec_IntSize( pStairDecVars ) && !Abc_TtIsStairDecomposable( pSes->pSpec, pSes->nSpecWords, Vec_IntArray( pStairDecVars ), Vec_IntSize( pStairDecVars ) ) ) + { + if ( pSes->fReasonVerbose ) + { + printf( "give up due to impossible stair decomposition at level %d: ", nLevel ); + Vec_IntPrint( pStairDecVars ); + } + Vec_IntFree( pStairDecVars ); + return 0; + } + + Vec_IntFree( pStairDecVars ); + } + + /* check if depth's match with structure at second level from top */ + if ( pSes->fDecStructure ) + 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->fReasonVerbose ) + 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; + } + + /* check if depth's match with structure at third level from top */ + if ( pSes->nSpecVars > 4 && pSes->fDecStructure && i == 1 ) /* we have f = AND(x_i, AND(x_j, g)) (x_i and x_j may be complemented) */ + { + i = 0; + for ( l = 0; l < pSes->nSpecVars; ++l ) + if ( pSes->pArrTimeProfile[l] + 3 == pSes->nMaxDepth ) + if ( ++i > 1 ) + { + if ( pSes->fReasonVerbose ) + printf( "give up due to impossible decomposition at third level (depth = %d, input = %d, arrival time = %d)", pSes->nMaxDepth, l, pSes->pArrTimeProfile[l] ); + return 0; + } + } + + return 1; +} + +// returns 0, if current max depth and #gates are not consistent +static int Ses_CheckGatesConsistency( Ses_Man_t * pSes, int nGates ) +{ + /* give up if number of gates is impossible for given depth */ + if ( pSes->nMaxDepth != -1 && nGates >= ( 1 << pSes->nMaxDepth ) ) + { + if ( pSes->fReasonVerbose ) + printf( "give up due to impossible depth (depth = %d, gates = %d)", pSes->nMaxDepth, nGates ); + return 0; + } + + /* give up if number of gates is impossible for given depth and arrival times */ + if ( pSes->nMaxDepth != -1 && pSes->pArrTimeProfile && nGates > pSes->nMaxGates ) + { + if ( pSes->fReasonVerbose ) + printf( "give up due to impossible depth and arrival times (depth = %d, gates = %d)", pSes->nMaxDepth, nGates ); + return 0; + } + + if ( pSes->fDecStructure && nGates >= ( 1 << ( pSes->nMaxDepth - 1 ) ) + 1 ) + { + if ( pSes->fReasonVerbose ) + 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->fReasonVerbose ) + printf( "give up due to impossible number of gates" ); + return 0; + } + + return 1; +} + +static void Abc_ExactCopyDepthAndArrivalTimes( int nVars, int nDepthFrom, int * nDepthTo, int * pTimesFrom, int * pTimesTo ) +{ + int l; + + *nDepthTo = nDepthFrom; + for ( l = 0; l < nVars; ++l ) + pTimesTo[l] = pTimesFrom[l]; +} + +static void Ses_ManStoreDepthAndArrivalTimes( Ses_Man_t * pSes ) +{ + if ( pSes->nMaxDepth == -1 ) return; + Abc_ExactCopyDepthAndArrivalTimes( pSes->nSpecVars, pSes->nMaxDepth, &pSes->nMaxDepthTmp, pSes->pArrTimeProfile, pSes->pArrTimeProfileTmp ); +} + +static void Ses_ManRestoreDepthAndArrivalTimes( Ses_Man_t * pSes ) +{ + if ( pSes->nMaxDepth == -1 ) return; + Abc_ExactCopyDepthAndArrivalTimes( pSes->nSpecVars, pSes->nMaxDepthTmp, &pSes->nMaxDepth, pSes->pArrTimeProfileTmp, pSes->pArrTimeProfile ); +} + +static void Abc_ExactAdjustDepthAndArrivalTimes( int nVars, int nGates, int nDepthFrom, int * nDepthTo, int * pTimesFrom, int * pTimesTo, int nTimesMax ) +{ + int l; + + *nDepthTo = Abc_MinInt( nDepthFrom, nGates ); + for ( l = 0; l < nVars; ++l ) + pTimesTo[l] = Abc_MinInt( pTimesFrom[l], Abc_MaxInt( 0, nGates - 1 - nTimesMax + pTimesFrom[l] ) ); +} + +static void Ses_AdjustDepthAndArrivalTimes( Ses_Man_t * pSes, int nGates ) +{ + Abc_ExactAdjustDepthAndArrivalTimes( pSes->nSpecVars, nGates, pSes->nMaxDepthTmp, &pSes->nMaxDepth, pSes->pArrTimeProfileTmp, pSes->pArrTimeProfile, pSes->nArrTimeMax - 1 ); +} + +/* return: (2: continue, 1: found, 0: gave up) */ +static int Ses_ManFindNetworkExact( Ses_Man_t * pSes, int nGates ) +{ + int f, fSat; + abctime timeStart; + + /* solve */ + timeStart = Abc_Clock(); + Ses_ManCreateVars( pSes, nGates ); + f = Ses_ManCreateDepthClauses( pSes ); + pSes->timeInstance += ( Abc_Clock() - timeStart ); + if ( !f ) return 2; /* proven UNSAT while creating clauses */ + + /* first solve */ + fSat = Ses_ManSolve( pSes ); + if ( fSat == 0 ) + return 2; /* UNSAT, continue with next # of gates */ + else if ( fSat == 2 ) + { + pSes->fHitResLimit = 1; + return 0; + } + + timeStart = Abc_Clock(); + f = Ses_ManCreateClauses( pSes ); + pSes->timeInstance += ( Abc_Clock() - timeStart ); + if ( !f ) return 2; /* proven UNSAT while creating clauses */ + + fSat = Ses_ManSolve( pSes ); + if ( fSat == 1 ) + return 1; + else if ( fSat == 2 ) + { + pSes->fHitResLimit = 1; + return 0; + } + + return 2; /* UNSAT continue */ +} + static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) { - int nGates = 0; + int nGates = pSes->nStartGates, fRes, fSat, nOffset = 0, fFirst = 1, iMint; + char * pSol; + word pTruth[4]; + + /* store whether call was unsuccessful due to resource limit and not due to impossible constraint */ + pSes->fHitResLimit = 0; + + /* do the arrival times allow for a network? */ + if ( pSes->nMaxDepth != -1 && pSes->pArrTimeProfile ) + { + if ( !Ses_CheckDepthConsistency( pSes ) ) + return 0; + Ses_ManComputeMaxGates( pSes ); + nOffset = pSes->nMaxGates >= 10 ? 3 : 2; + } + + //Ses_ManStoreDepthAndArrivalTimes( pSes ); + + //memset( pSes->pTtValues, (word)~0, 4 * sizeof( word ) ); + memset( pSes->pTtValues, 0, 4 * sizeof( word ) ); while ( true ) { ++nGates; - /* give up if number of gates is impossible for given depth */ - if ( pSes->nMaxDepth != -1 && nGates >= ( 1 << pSes->nMaxDepth ) ) - return 0; + Abc_DebugErase( nOffset + ( nGates > 10 ? 5 : 4 ), pSes->fVeryVerbose && !fFirst ); + Abc_DebugPrintIntInt( " (%d/%d)", nGates, pSes->nMaxGates, pSes->fVeryVerbose ); + fFirst = 0; - Ses_ManCreateVars( pSes, nGates ); - if ( !Ses_ManCreateClauses( pSes ) ) - return 0; /* proven UNSAT while creating clauses */ + //Ses_AdjustDepthAndArrivalTimes( pSes, nGates ); - switch ( Ses_ManSolve( pSes ) ) + /* do #gates and max depth allow for a network? */ + if ( !Ses_CheckGatesConsistency( pSes, nGates ) ) { - case 1: return 1; /* SAT */ - case 2: return 0; /* resource limit */ + fRes = 0; + break; + } + + fRes = Ses_ManFindNetworkExact( pSes, nGates ); + if ( fRes == 2 ) continue; /* unsat */ + if ( fRes == 0 ) break; /* undef */ + + while ( true ) + { + pSol = Ses_ManExtractSolution( pSes ); + Abc_TtXor( pTruth, Ses_ManDeriveTruth( pSes, pSol, 0 ), pSes->pSpec, pSes->nSpecWords, 0 ); + ABC_FREE( pSol ); + iMint = Abc_TtFindFirstBit( pTruth, pSes->nSpecVars ); + + if ( iMint == -1 ) + { + assert( fRes == 1 ); + break; + } + + assert( iMint ); + Abc_TtSetBit( pSes->pTtValues, iMint - 1 ); + if ( !Ses_ManCreateTruthTableClause( pSes, iMint - 1 ) ) /* UNSAT, continue */ + { + fRes = 2; + break; + } + + if ( ( fSat = Ses_ManSolve( pSes ) ) == 1 ) continue; + + if ( fSat == 0 ) + fRes = 2; + else if ( fSat == 2 ) + { + pSes->fHitResLimit = 1; + fRes = 0; + } + + break; } + + if ( fRes != 2 ) + break; + + /* /\* solve *\/ */ + /* timeStart = Abc_Clock(); */ + /* Ses_ManCreateVars( pSes, nGates ); */ + /* f = Ses_ManCreateDepthClauses( pSes ); */ + /* pSes->timeInstance += ( Abc_Clock() - timeStart ); */ + /* if ( !f ) continue; /\* proven UNSAT while creating clauses *\/ */ + + /* /\* first solve *\/ */ + /* fSat = Ses_ManSolve( pSes ); */ + /* if ( fSat == 0 ) */ + /* continue; /\* UNSAT, continue with next # of gates *\/ */ + /* else if ( fSat == 2 ) */ + /* { */ + /* pSes->fHitResLimit = 1; */ + /* fRes = 0; */ + /* break; */ + /* } */ + + /* timeStart = Abc_Clock(); */ + /* f = Ses_ManCreateClauses( pSes ); */ + /* pSes->timeInstance += ( Abc_Clock() - timeStart ); */ + /* if ( !f ) continue; /\* proven UNSAT while creating clauses *\/ */ + + /* fSat = Ses_ManSolve( pSes ); */ + /* if ( fSat == 1 ) */ + /* { */ + /* fRes = 1; */ + /* break; */ + /* } */ + /* else if ( fSat == 2 ) */ + /* { */ + /* pSes->fHitResLimit = 1; */ + /* fRes = 0; */ + /* break; */ + /* } */ + + /* UNSAT => continue */ } - return 0; + //Ses_ManRestoreDepthAndArrivalTimes( pSes ); + + Abc_DebugErase( nOffset + ( nGates >= 10 ? 5 : 4 ), pSes->fVeryVerbose ); + return fRes; } /**Function************************************************************* @@ -1263,7 +2223,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 nStartGates, int fVerbose ) { Ses_Man_t * pSes; char * pSol; @@ -1275,7 +2235,10 @@ 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 ); + pSes->nStartGates = nStartGates; + pSes->fReasonVerbose = 1; + pSes->fSatVerbose = 1; if ( fVerbose ) Ses_ManPrintFuncs( pSes ); @@ -1297,7 +2260,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 nStartGates, int fVerbose ) { Ses_Man_t * pSes; char * pSol; @@ -1309,7 +2272,12 @@ 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->nStartGates = nStartGates; + pSes->fVeryVerbose = 1; + pSes->fExtractVerbose = 0; + pSes->fSatVerbose = 0; + pSes->fReasonVerbose = 1; if ( fVerbose ) Ses_ManPrintFuncs( pSes ); @@ -1362,30 +2330,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, 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, 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, 0, 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, 0, fVerbose ) ); - assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrTimeProfile, fVerbose ) ); + assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, 0, fVerbose ) ); Abc_NtkDelete( pNtk ); } @@ -1404,27 +2372,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, 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, 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, 0, 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, 0, fVerbose ) ); - assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrTimeProfile, fVerbose ) ); + assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, 0, fVerbose ) ); Gia_ManStop( pGia ); Gia_ManStop( pGia2 ); @@ -1466,7 +2434,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 +2449,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 +2468,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, nDelta, 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,69 +2538,86 @@ 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( "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( " at level %d\n", AigLevel ); - } + for ( l = 0; l < nVars; ++l ) + pNormalArrTime[l] = pArrTimeProfile[l]; - /* statistics */ - s_pSesStore->nCutCount++; - s_pSesStore->pCutCount[nVars]++; + nDelta = Abc_NormalizeArrivalTimes( pNormalArrTime, nVars, &nMaxArrival ); *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]; + if ( s_pSesStore->fVeryVerbose ) + { + printf( ANSI_COLOR_CYAN ); + Abc_TtPrintHexRev( stdout, pTruth, nVars ); + printf( ANSI_COLOR_RESET ); + printf( " [%d", pNormalArrTime[0] ); + for ( l = 1; l < nVars; ++l ) + printf( " %d", pNormalArrTime[l] ); + printf( "]@%d:", AigLevel ); + fflush( stdout ); + } + + 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 - nDelta, 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; + pSes->nStartGates = nVars - 2; while ( pSes->nMaxDepth ) /* there is improvement */ { if ( s_pSesStore->fVeryVerbose ) { - printf( " try to compute network starting with depth %d ", pSes->nMaxDepth ); + printf( " %d", pSes->nMaxDepth ); fflush( stdout ); } if ( Ses_ManFindMinimumSize( pSes ) ) { if ( s_pSesStore->fVeryVerbose ) - printf( " FOUND\n" ); + { + if ( pSes->nMaxDepth >= 10 ) printf( "\b" ); + printf( "\b" ANSI_COLOR_GREEN "%d" ANSI_COLOR_RESET, pSes->nMaxDepth ); + } if ( pSol ) ABC_FREE( pSol ); pSol = Ses_ManExtractSolution( pSes ); @@ -1591,18 +2626,41 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char * else { if ( s_pSesStore->fVeryVerbose ) - printf( " NOT FOUND\n" ); + { + if ( pSes->nMaxDepth >= 10 ) printf( "\b" ); + printf( "\b%s%d" ANSI_COLOR_RESET, pSes->fHitResLimit ? ANSI_COLOR_RED : ANSI_COLOR_YELLOW, pSes->nMaxDepth ); + } break; } } - pSes->timeTotal = Abc_Clock() - timeStart; + if ( s_pSesStore->fVeryVerbose ) + printf( " \n" ); + + /* log unsuccessful case for debugging */ + if ( s_pSesStore->pDebugEntries && pSes->fHitResLimit ) + Ses_StorePrintDebugEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, pSes->nMaxDepth, pSol, nVars - 2 ); - /* cleanup */ - Ses_ManClean( pSes ); + pSes->timeTotal = Abc_Clock() - timeStartExact; + + /* 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 +2672,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 ); + 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 ); - return nDelta + Delay; + 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 ); + assert( 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 +2743,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 +2766,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 +2780,7 @@ Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Vec_PtrFree( pGates ); + s_pSesStore->timeTotal += ( Abc_Clock() - timeStart ); return pObj; } |