diff options
| -rw-r--r-- | src/base/abci/abc.c | 16 | ||||
| -rw-r--r-- | src/base/abci/abcExact.c | 777 |
2 files changed, 610 insertions, 183 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 703fd63d..6138013e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7362,15 +7362,21 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fMakeAIG ) { pGiaRes = Gia_ManFindExact( pTruth, nVars, nFunc, nMaxDepth, NULL, fVerbose ); - assert( pGiaRes != NULL ); - Abc_FrameUpdateGia( pAbc, pGiaRes ); + if ( pGiaRes ) + Abc_FrameUpdateGia( pAbc, pGiaRes ); + else + Abc_Print( 0, "Could not find AIG within given resource constraints.\n" ); } else { pNtkRes = Abc_NtkFindExact( pTruth, nVars, nFunc, nMaxDepth, NULL, fVerbose ); - assert( pNtkRes != NULL ); - Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); - Abc_FrameClearVerifStatus( pAbc ); + if ( pNtkRes ) + { + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + Abc_FrameClearVerifStatus( pAbc ); + } + else + Abc_Print( 0, "Could not find network within given resource constraints.\n" ); } return 0; diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 384399cb..99b44bce 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -25,6 +25,7 @@ #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" @@ -52,48 +53,86 @@ static word s_Truths8[32] = { 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 * pArrivalTimes; /* arrival times of inputs (NULL if arrival times are ignored) */ - int nArrivalDelta; /* delta to the original arrival times (arrival times are normalized to have 0 as minimum element) */ - int nArrivalMax; /* 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 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 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 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 */ }; +/*********************************************************************** + + Synopsis [Store truth tables based on normalized arrival times.] + +***********************************************************************/ + +// The hash table is a list of pointers to Ses_TruthEntry_t elements, which +// are arranged in a linked list, each of which pointing to a linked list +// of Ses_TimesEntry_t elements which contain the char* representation of the +// optimum netlist according to then normalized arrival times: + +typedef struct Ses_TimesEntry_t_ Ses_TimesEntry_t; +struct Ses_TimesEntry_t_ +{ + int pArrTimeProfile[8]; /* normalized arrival time profile */ + Ses_TimesEntry_t * next; /* linked list pointer */ + char * pNetwork; /* pointer to char array representation of optimum network */ +}; + +typedef struct Ses_TruthEntry_t_ Ses_TruthEntry_t; +struct Ses_TruthEntry_t_ +{ + word pTruth[4]; /* truth table for comparison */ + Ses_TruthEntry_t * next; /* linked list pointer */ + Ses_TimesEntry_t * head; /* pointer to head of sub list with arrival times */ +}; + +#define SES_STORE_TABLE_SIZE 1024 +typedef struct Ses_Store_t_ Ses_Store_t; +struct Ses_Store_t_ +{ + int nNumVars; /* store has been allocated for this number of variables */ + int nWords; /* number of truth table words */ + Ses_TruthEntry_t * pEntries[SES_STORE_TABLE_SIZE]; /* hash table for truth table entries */ +}; + +static Ses_Store_t * s_pSesStore = NULL; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -int NormalizeArrivalTimes( int * pArrivalTimes, int nVars, int * maxNormalized ) +static int Abc_NormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int * maxNormalized ) { - int * p = pArrivalTimes, * pEnd = pArrivalTimes + nVars; + int * p = pArrTimeProfile, * pEnd = pArrTimeProfile + nVars; int delta = *p; while ( ++p < pEnd ) @@ -101,7 +140,7 @@ int NormalizeArrivalTimes( int * pArrivalTimes, int nVars, int * maxNormalized ) delta = *p; *maxNormalized = 0; - p = pArrivalTimes; + p = pArrTimeProfile; while ( p < pEnd ) { *p -= delta; @@ -115,7 +154,202 @@ int NormalizeArrivalTimes( int * pArrivalTimes, int nVars, int * maxNormalized ) return delta; } -static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fMakeAIG, int fVerbose ) +static inline Ses_Store_t * Ses_StoreAlloc( int nVars ) +{ + Ses_Store_t * pStore = ABC_CALLOC( Ses_Store_t, 1 ); + pStore->nNumVars = nVars; + pStore->nWords = Kit_TruthWordNum( nVars ); + + return pStore; +} + +static inline void Ses_StoreClean( Ses_Store_t * pStore ) +{ + int i; + Ses_TruthEntry_t * pTEntry, * pTEntry2; + Ses_TimesEntry_t * pTiEntry, * pTiEntry2; + + for ( i = 0; i < SES_STORE_TABLE_SIZE; ++i ) + if ( pStore->pEntries[i] ) + { + pTEntry = pStore->pEntries[i]; + + while ( pTEntry ) + { + pTiEntry = pTEntry->head; + while ( pTiEntry ) + { + ABC_FREE( pTiEntry->pNetwork ); + pTiEntry2 = pTiEntry; + pTiEntry = pTiEntry->next; + ABC_FREE( pTiEntry2 ); + } + pTEntry2 = pTEntry; + pTEntry = pTEntry->next; + ABC_FREE( pTEntry2 ); + } + } + + ABC_FREE( pStore ); +} + +static inline int Ses_StoreTableHash( Ses_Store_t * pStore, word * pTruth ) +{ + static int s_Primes[4] = { 1291, 1699, 1999, 2357 }; + int i; + unsigned uHash = 0; + for ( i = 0; i < pStore->nWords; ++i ) + uHash ^= pTruth[i] * s_Primes[i & 0xf]; + return (int)(uHash % SES_STORE_TABLE_SIZE ); +} + +static inline int Ses_StoreTruthEqual( Ses_Store_t * pStore, word * pTruth1, word * pTruth2 ) +{ + int i; + for ( i = 0; i < pStore->nWords; ++i ) + if ( pTruth1[i] != pTruth2[i] ) + return 0; + return 1; +} + +static inline void Ses_StoreTruthCopy( Ses_Store_t * pStore, word * pTruthDest, word * pTruthSrc ) +{ + int i; + for ( i = 0; i < pStore->nWords; ++i ) + pTruthDest[i] = pTruthSrc[i]; +} + +static inline int Ses_StoreTimesEqual( Ses_Store_t * pStore, int * pTimes1, int * pTimes2 ) +{ + int i; + for ( i = 0; i < pStore->nNumVars; ++i ) + if ( pTimes1[i] != pTimes2[i] ) + return 0; + return 1; +} + +static inline void Ses_StoreTimesCopy( Ses_Store_t * pStore, int * pTimesDest, int * pTimesSrc ) +{ + int i; + for ( i = 0; i < pStore->nNumVars; ++i ) + pTimesDest[i] = pTimesSrc[i]; +} + +// pArrTimeProfile is not 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 i, nDelta, maxNormalized, key, fAdded; + Ses_TruthEntry_t * pTEntry; + Ses_TimesEntry_t * pTiEntry; + + if ( pStore->nNumVars != nVars ) + return 0; + + nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &maxNormalized ); + + key = Ses_StoreTableHash( pStore, pTruth ); + pTEntry = pStore->pEntries[key]; + + /* does truth table already exist? */ + while ( pTEntry ) + { + if ( Ses_StoreTruthEqual( pStore, pTruth, pTEntry->pTruth ) ) + break; + else + pTEntry = pTEntry->next; + } + + /* entry does not yet exist, so create new one and enqueue */ + if ( !pTEntry ) + { + pTEntry = ABC_CALLOC( Ses_TruthEntry_t, 1 ); + Ses_StoreTruthCopy( pStore, pTEntry->pTruth, pTruth ); + pTEntry->next = pStore->pEntries[key]; + pStore->pEntries[key] = pTEntry; + } + + /* does arrival time already exist? */ + pTiEntry = pTEntry->head; + while ( pTiEntry ) + { + if ( Ses_StoreTimesEqual( pStore, pArrTimeProfile, pTiEntry->pArrTimeProfile ) ) + break; + else + pTiEntry = pTiEntry->next; + } + + /* entry does not yet exist, so create new one and enqueue */ + if ( !pTiEntry ) + { + pTiEntry = ABC_CALLOC( Ses_TimesEntry_t, 1 ); + Ses_StoreTimesCopy( pStore, pTiEntry->pArrTimeProfile, pArrTimeProfile ); + pTiEntry->pNetwork = pSol; + pTiEntry->next = pTEntry->head; + pTEntry->head = pTiEntry; + + /* item has been added */ + fAdded = 1; + } + else + /* item was already present */ + fAdded = 0; + + for ( i = 0; i < nVars; ++i ) + pArrTimeProfile[i] += nDelta; + return fAdded; +} + +// pArrTimeProfile is not normalized +// returns 0 if no solution was found +char * Ses_StoreGetEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile ) +{ + int i, nDelta, maxNormalized, key; + Ses_TruthEntry_t * pTEntry; + Ses_TimesEntry_t * pTiEntry; + + if ( pStore->nNumVars != nVars ) + return 0; + + key = Ses_StoreTableHash( pStore, pTruth ); + pTEntry = pStore->pEntries[key]; + + /* find truth table entry */ + while ( pTEntry ) + { + if ( Ses_StoreTruthEqual( pStore, pTruth, pTEntry->pTruth ) ) + break; + else + pTEntry = pTEntry->next; + } + + /* no entry found? */ + if ( !pTEntry ) + return 0; + + nDelta = Abc_NormalizeArrivalTimes( pArrTimeProfile, nVars, &maxNormalized ); + + /* find times entry */ + pTiEntry = pTEntry->head; + while ( pTiEntry ) + { + if ( Ses_StoreTimesEqual( pStore, pArrTimeProfile, pTiEntry->pArrTimeProfile ) ) + break; + else + pTiEntry = pTiEntry->next; + } + + for ( i = 0; i < nVars; ++i ) + pArrTimeProfile[i] += nDelta; + + /* no entry found? */ + if ( !pTiEntry ) + return 0; + + return pTiEntry->pNetwork; +} + +static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fMakeAIG, int fVerbose ) { int h, i; @@ -134,11 +368,11 @@ static inline Ses_Man_t * Ses_ManAlloc( word * pTruth, int nVars, int nFunc, int p->nSpecFunc = nFunc; p->nRows = ( 1 << nVars ) - 1; p->nMaxDepth = nMaxDepth; - p->pArrivalTimes = nMaxDepth >= 0 ? pArrivalTimes : NULL; - if ( p->pArrivalTimes ) - p->nArrivalDelta = NormalizeArrivalTimes( p->pArrivalTimes, nVars, &p->nArrivalMax ); + p->pArrTimeProfile = nMaxDepth >= 0 ? pArrTimeProfile : NULL; + if ( p->pArrTimeProfile ) + p->nArrTimeDelta = Abc_NormalizeArrivalTimes( p->pArrTimeProfile, nVars, &p->nArrTimeMax ); else - p->nArrivalDelta = p->nArrivalMax = 0; + p->nArrTimeDelta = p->nArrTimeMax = 0; p->fMakeAIG = fMakeAIG; p->nBTLimit = nMaxDepth >= 0 ? 50000 : 0; p->fVerbose = fVerbose; @@ -155,9 +389,9 @@ static inline void Ses_ManClean( Ses_Man_t * pSes ) for ( i = 0; i < 4; ++i ) pSes->pSpec[(h << 2) + i] = ~( pSes->pSpec[(h << 2) + i] ); - if ( pSes->pArrivalTimes ) + if ( pSes->pArrTimeProfile ) for ( i = 0; i < pSes->nSpecVars; ++i ) - pSes->pArrivalTimes[i] += pSes->nArrivalDelta; + pSes->pArrTimeProfile[i] += pSes->nArrTimeDelta; if ( pSes->pSat ) sat_solver_delete( pSes->pSat ); @@ -215,9 +449,9 @@ static inline int Ses_ManSelectVar( Ses_Man_t * pSes, int i, int j, int k ) static inline int Ses_ManDepthVar( Ses_Man_t * pSes, int i, int j ) { assert( i < pSes->nGates ); - assert( j <= pSes->nArrivalMax + i ); + assert( j <= pSes->nArrTimeMax + i ); - return pSes->nDepthOffset + i * pSes->nArrivalMax + ( ( i * ( i + 1 ) ) / 2 ) + j; + return pSes->nDepthOffset + i * pSes->nArrTimeMax + ( ( i * ( i + 1 ) ) / 2 ) + j; } /**Function************************************************************* @@ -241,7 +475,7 @@ static void Ses_ManCreateVars( Ses_Man_t * pSes, int nGates ) pSes->nSelectVars = 0; for ( i = pSes->nSpecVars; i < pSes->nSpecVars + nGates; ++i ) pSes->nSelectVars += ( i * ( i - 1 ) ) / 2; - pSes->nDepthVars = pSes->nMaxDepth > 0 ? nGates * pSes->nArrivalMax + ( nGates * ( nGates + 1 ) ) / 2 : 0; + pSes->nDepthVars = pSes->nMaxDepth > 0 ? nGates * pSes->nArrTimeMax + ( nGates * ( nGates + 1 ) ) / 2 : 0; pSes->nOutputOffset = pSes->nSimVars; pSes->nGateOffset = pSes->nSimVars + pSes->nOutputVars; @@ -440,7 +674,7 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes ) 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->nArrivalMax + j; ++jj ) + 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 ); @@ -452,7 +686,7 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes ) 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->nArrivalMax + k; ++kk ) + 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 ); @@ -461,14 +695,14 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes ) } /* propagate depths from arrival times at PIs */ - if ( pSes->pArrivalTimes ) + if ( pSes->pArrTimeProfile ) { for ( k = 1; k < pSes->nSpecVars + i; ++k ) for ( j = 0; j < ( ( k < pSes->nSpecVars ) ? k : pSes->nSpecVars ); ++j ) { - d = pSes->pArrivalTimes[j]; - if ( k < pSes->nSpecVars && pSes->pArrivalTimes[k] > d ) - d = pSes->pArrivalTimes[k]; + 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 + 1 ), 0 ); @@ -483,7 +717,7 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes ) } /* reverse order encoding of depth variables */ - for ( j = 1; j <= pSes->nArrivalMax + i; ++j ) + 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 ); @@ -491,7 +725,7 @@ static void Ses_ManCreateClauses( Ses_Man_t * pSes ) } /* constrain maximum depth */ - if ( pSes->nMaxDepth < pSes->nArrivalMax + i ) + if ( pSes->nMaxDepth < pSes->nArrTimeMax + i ) for ( h = 0; h < pSes->nSpecFunc; ++h ) { pLits[0] = Abc_Var2Lit( Ses_ManOutputVar( pSes, h, i ), 1 ); @@ -548,9 +782,126 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes ) Synopsis [Extract solution.] ***********************************************************************/ -static Abc_Ntk_t * Ses_ManExtractNtk( Ses_Man_t * pSes ) +// char is an array of short integers that stores the synthesized network +// using the following format +// | nvars | nfunc | ngates | gate[1] | ... | gate[ngates] | func[1] | .. | func[nfunc] | +// nvars: integer with number of variables +// nfunc: integer with number of functions +// ngates: integer with number of gates +// gate[i]: | op | nfanin | fanin[1] | ... | fanin[nfanin] | +// op: integer of gate's truth table (divided by 2, because gate is normal) +// nfanin[i]: integer with number of fanins +// fanin: integer to primary input or other gate +// func[i]: | fanin | delay | pin[1] | ... | pin[nvars] | +// fanin: integer as literal to some gate (not primary input), can be complemented +// delay: maximum delay to output (taking arrival times into account, not normalized) or 0 if not specified +// pin[i]: pin to pin delay to input i or 0 if not specified or if there is no connection to input i +// NOTE: since outputs can only point to gates, delay and pin-to-pin times cannot be 0 +#define ABC_EXACT_SOL_NVARS 0 +#define ABC_EXACT_SOL_NFUNC 1 +#define ABC_EXACT_SOL_NGATES 2 +static char * Ses_ManExtractSolution( Ses_Man_t * pSes ) { - int h, i, j, k; + int nSol, h, i, j, k, l, aj, ak, d, nOp; + char * pSol, * p; + int * pPerm; /* will be a 2d array [i][l] where is is gate id and l is PI id */ + + /* compute length of solution, for now all gates have 2 inputs */ + nSol = 3 + pSes->nGates * 4 + pSes->nSpecFunc * ( 2 + pSes->nSpecVars ); + + p = pSol = ABC_CALLOC( char, nSol ); + + /* header */ + *p++ = pSes->nSpecVars; + *p++ = pSes->nSpecFunc; + *p++ = pSes->nGates; + + /* gates */ + for ( i = 0; i < pSes->nGates; ++i ) + { + nOp = sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 0, 1 ) ); + nOp |= sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 0 ) ) << 1; + nOp |= sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 1 ) ) << 2; + + *p++ = nOp; + *p++ = 2; + + for ( k = 0; k < pSes->nSpecVars + i; ++k ) + for ( j = 0; j < k; ++j ) + if ( sat_solver_var_value( pSes->pSat, Ses_ManSelectVar( pSes, i, j, k ) ) ) + { + *p++ = j; + *p++ = k; + break; + } + + /* if ( pSes->fVeryVerbose ) */ + /* { */ + /* if ( pSes->nMaxDepth > 0 ) */ + /* { */ + /* printf( " and depth vector " ); */ + /* for ( j = 0; j <= pSes->nArrTimeMax + i; ++j ) */ + /* printf( "%d", sat_solver_var_value( pSes->pSat, Ses_ManDepthVar( pSes, i, j ) ) ); */ + /* } */ + /* printf( "\n" ); */ + /* } */ + } + + /* pin-to-pin delay */ + if ( pSes->nMaxDepth != -1 ) + { + pPerm = ABC_CALLOC( int, pSes->nGates * pSes->nSpecVars ); + for ( i = 0; i < pSes->nGates; ++i ) + { + /* since all gates are binary for now */ + j = pSol[3 + i * 4 + 2]; + k = pSol[3 + i * 4 + 2]; + + for ( l = 0; l < pSes->nSpecVars; ++l ) + { + /* pin-to-pin delay to input l of child nodes */ + aj = j < pSes->nGates ? 0 : pPerm[j * pSes->nSpecVars + l]; + ak = k < pSes->nGates ? 0 : pPerm[k * pSes->nSpecVars + l]; + + if ( aj == 0 && ak == 0 ) + pPerm[i * pSes->nSpecVars + l] = 0; + else + pPerm[i * pSes->nSpecVars + l] = ( ( aj > ak ) ? aj : ak ) + 1; + } + } + } + + /* outputs */ + for ( h = 0; h < pSes->nSpecFunc; ++h ) + for ( i = 0; i < pSes->nGates; ++i ) + if ( sat_solver_var_value( pSes->pSat, Ses_ManOutputVar( pSes, h, i ) ) ) + { + *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; + *p++ = d + pSes->nArrTimeDelta; + for ( l = 0; l < pSes->nSpecVars; ++l ) + *p++ = ( pSes->nMaxDepth != -1 ) ? pPerm[i * pSes->nSpecVars + l] : 0; + if ( pSes->fVeryVerbose ) + printf( "output %d points to %d and has normalized delay %d\n", h, i, d ); + } + + /* pin-to-pin delays */ + if ( pSes->nMaxDepth != -1 ) + ABC_FREE( pPerm ); + + /* have we used all the fields? */ + assert( ( p - pSol ) == nSol ); + + return pSol; +} + +static Abc_Ntk_t * Ses_ManExtractNtk( char const * pSol ) +{ + int h, i; + char const * p; Abc_Ntk_t * pNtk; Abc_Obj_t * pObj; Vec_Ptr_t * pGates, * vNames; @@ -559,14 +910,14 @@ static Abc_Ntk_t * Ses_ManExtractNtk( Ses_Man_t * pSes ) pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 ); pNtk->pName = Extra_UtilStrsav( "exact" ); - pGates = Vec_PtrAlloc( pSes->nSpecVars + pSes->nGates ); + pGates = Vec_PtrAlloc( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NGATES] ); pGateTruth[3] = '0'; pGateTruth[4] = '\0'; - vNames = Abc_NodeGetFakeNames( pSes->nSpecVars + pSes->nSpecFunc ); + vNames = Abc_NodeGetFakeNames( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NFUNC] ); /* primary inputs */ Vec_PtrPush( pNtk->vObjs, NULL ); - for ( i = 0; i < pSes->nSpecVars; ++i ) + for ( i = 0; i < pSol[ABC_EXACT_SOL_NVARS]; ++i ) { pObj = Abc_NtkCreatePi( pNtk ); Abc_ObjAssignName( pObj, (char*)Vec_PtrEntry( vNames, i ), NULL ); @@ -574,16 +925,16 @@ static Abc_Ntk_t * Ses_ManExtractNtk( Ses_Man_t * pSes ) } /* gates */ - for ( i = 0; i < pSes->nGates; ++i ) + p = pSol + 3; + for ( i = 0; i < pSol[ABC_EXACT_SOL_NGATES]; ++i ) { - pGateTruth[2] = '0' + sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 0, 1 ) ); - pGateTruth[1] = '0' + sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 0 ) ); - pGateTruth[0] = '0' + sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 1 ) ); + pGateTruth[2] = '0' + ( *p & 1 ); + pGateTruth[1] = '0' + ( ( *p >> 1 ) & 1 ); + pGateTruth[0] = '0' + ( ( *p >> 2 ) & 1 ); + ++p; - if ( pSes->fVeryVerbose ) - { - printf( "gate %d has truth table %s", pSes->nSpecVars + i, pGateTruth ); - } + assert( *p == 2 ); /* binary gate */ + ++p; pSopCover = Abc_SopFromTruthBin( pGateTruth ); pObj = Abc_NtkCreateNode( pNtk ); @@ -591,54 +942,20 @@ static Abc_Ntk_t * Ses_ManExtractNtk( Ses_Man_t * pSes ) Vec_PtrPush( pGates, pObj ); ABC_FREE( pSopCover ); - for ( k = 0; k < pSes->nSpecVars + i; ++k ) - for ( j = 0; j < k; ++j ) - if ( sat_solver_var_value( pSes->pSat, Ses_ManSelectVar( pSes, i, j, k ) ) ) - { - if ( pSes->fVeryVerbose ) - printf( " with children %d and %d", j, k ); - Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, j ) ); - Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, k ) ); - break; - } - - if ( pSes->fVeryVerbose ) - { - if ( pSes->nMaxDepth > 0 ) - { - printf( " and depth vector " ); - for ( j = 0; j <= pSes->nArrivalMax + i; ++j ) - printf( "%d", sat_solver_var_value( pSes->pSat, Ses_ManDepthVar( pSes, i, j ) ) ); - } - printf( "\n" ); - } + Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) ); + Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) ); } /* outputs */ - for ( h = 0; h < pSes->nSpecFunc; ++h ) + for ( h = 0; h < pSol[ABC_EXACT_SOL_NFUNC]; ++h ) { pObj = Abc_NtkCreatePo( pNtk ); - Abc_ObjAssignName( pObj, (char*)Vec_PtrEntry( vNames, pSes->nSpecVars + h ), NULL ); - for ( i = 0; i < pSes->nGates; ++i ) - { - if ( sat_solver_var_value( pSes->pSat, Ses_ManOutputVar( pSes, h, i ) ) ) - { - if ( pSes->fVeryVerbose ) - printf( "output %d points to gate %d", h, pSes->nSpecVars + i ); - /* if output has been inverted, we need to add an inverter */ - if ( ( pSes->bSpecInv >> h ) & 1 ) - { - Abc_ObjAddFanin( pObj, Abc_NtkCreateNodeInv( pNtk, (Abc_Obj_t *)Vec_PtrEntry( pGates, pSes->nSpecVars + i ) ) ); - if ( pSes->fVeryVerbose ) - printf( " and needs to be inverted" ); - } - else - Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, pSes->nSpecVars + i ) ); - - if ( pSes->fVeryVerbose ) - printf( "\n" ); - } - } + Abc_ObjAssignName( pObj, (char*)Vec_PtrEntry( vNames, pSol[ABC_EXACT_SOL_NVARS] + h ), NULL ); + if ( Abc_LitIsCompl( *p ) ) + Abc_ObjAddFanin( pObj, Abc_NtkCreateNodeInv( pNtk, (Abc_Obj_t *)Vec_PtrEntry( pGates, pSol[ABC_EXACT_SOL_NVARS] + Abc_Lit2Var( *p ) ) ) ); + else + Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, pSol[ABC_EXACT_SOL_NVARS] + Abc_Lit2Var( *p ) ) ); + p += ( 2 + pSol[ABC_EXACT_SOL_NVARS] ); } Abc_NodeFreeNames( vNames ); @@ -647,28 +964,28 @@ static Abc_Ntk_t * Ses_ManExtractNtk( Ses_Man_t * pSes ) if ( !Abc_NtkCheck( pNtk ) ) printf( "Ses_ManExtractSolution(): Network check has failed.\n" ); - return pNtk; } -static Gia_Man_t * Ses_ManExtractGia( Ses_Man_t * pSes ) +static Gia_Man_t * Ses_ManExtractGia( char const * pSol ) { - int h, i, j, k; + int h, i; + char const * p; Gia_Man_t * pGia; Vec_Int_t * pGates; Vec_Ptr_t * vNames; int nObj, nChild1, nChild2, fChild1Comp, fChild2Comp; - pGia = Gia_ManStart( pSes->nSpecVars + pSes->nGates + pSes->nSpecFunc + 1 ); + pGia = Gia_ManStart( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NGATES] + pSol[ABC_EXACT_SOL_NFUNC] + 1 ); pGia->nConstrs = 0; pGia->pName = Extra_UtilStrsav( "exact" ); - pGates = Vec_IntAlloc( pSes->nSpecVars + pSes->nGates ); - vNames = Abc_NodeGetFakeNames( pSes->nSpecVars + pSes->nSpecFunc ); + pGates = Vec_IntAlloc( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NGATES] ); + vNames = Abc_NodeGetFakeNames( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NFUNC] ); /* primary inputs */ - pGia->vNamesIn = Vec_PtrStart( pSes->nSpecVars ); - for ( i = 0; i < pSes->nSpecVars; ++i ) + pGia->vNamesIn = Vec_PtrStart( pSol[ABC_EXACT_SOL_NVARS] ); + for ( i = 0; i < pSol[ABC_EXACT_SOL_NVARS]; ++i ) { nObj = Gia_ManAppendCi( pGia ); Vec_IntPush( pGates, nObj ); @@ -676,55 +993,46 @@ static Gia_Man_t * Ses_ManExtractGia( Ses_Man_t * pSes ) } /* gates */ - for ( i = 0; i < pSes->nGates; ++i ) + p = pSol + 3; + for ( i = 0; i < pSol[ABC_EXACT_SOL_NGATES]; ++i ) { - for ( k = 0; k < pSes->nSpecVars + i; ++k ) - for ( j = 0; j < k; ++j ) - if ( sat_solver_var_value( pSes->pSat, Ses_ManSelectVar( pSes, i, j, k ) ) ) - { - nChild1 = Vec_IntEntry( pGates, j ); - nChild2 = Vec_IntEntry( pGates, k ); - fChild1Comp = fChild2Comp = 0; + assert( p[1] == 2 ); + nChild1 = Vec_IntEntry( pGates, p[2] ); + nChild2 = Vec_IntEntry( pGates, p[3] ); + fChild1Comp = fChild2Comp = 0; - if ( sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 0, 1 ) ) ) - { - nChild1 = Abc_LitNot( nChild1 ); - fChild1Comp = 1; - } - if ( sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 0 ) ) ) - { - nChild2 = Abc_LitNot( nChild2 ); - fChild2Comp = 1; - } - nObj = Gia_ManAppendAnd( pGia, nChild1, nChild2 ); - if ( fChild1Comp && fChild2Comp ) - { - assert( sat_solver_var_value( pSes->pSat, Ses_ManGateVar( pSes, i, 1, 1 ) ) ); - nObj = Abc_LitNot( nObj ); - } + if ( *p & 1 ) + { + nChild1 = Abc_LitNot( nChild1 ); + fChild1Comp = 1; + } + if ( ( *p >> 1 ) & 1 ) + { + nChild2 = Abc_LitNot( nChild2 ); + fChild2Comp = 1; + } + nObj = Gia_ManAppendAnd( pGia, nChild1, nChild2 ); + if ( fChild1Comp && fChild2Comp ) + { + assert( ( *p >> 2 ) & 1 ); + nObj = Abc_LitNot( nObj ); + } - Vec_IntPush( pGates, nObj ); + Vec_IntPush( pGates, nObj ); - break; - } + p += 4; } /* outputs */ - pGia->vNamesOut = Vec_PtrStart( pSes->nSpecFunc ); - for ( h = 0; h < pSes->nSpecFunc; ++h ) + pGia->vNamesOut = Vec_PtrStart( pSol[ABC_EXACT_SOL_NFUNC] ); + for ( h = 0; h < pSol[ABC_EXACT_SOL_NFUNC]; ++h ) { - for ( i = 0; i < pSes->nGates; ++i ) - { - if ( sat_solver_var_value( pSes->pSat, Ses_ManOutputVar( pSes, h, i ) ) ) - { - nObj = Vec_IntEntry( pGates, pSes->nSpecVars + i ); - /* if output has been inverted, we need to add an inverter */ - if ( ( pSes->bSpecInv >> h ) & 1 ) - nObj = Abc_LitNot( nObj ); - Gia_ManAppendCo( pGia, nObj ); - Vec_PtrSetEntry( pGia->vNamesOut, h, Extra_UtilStrsav( Vec_PtrEntry( vNames, pSes->nSpecVars + h ) ) ); - } - } + nObj = Vec_IntEntry( pGates, pSol[ABC_EXACT_SOL_NVARS] + Abc_Lit2Var( *p ) ); + if ( Abc_LitIsCompl( *p ) ) + nObj = Abc_LitNot( nObj ); + Gia_ManAppendCo( pGia, nObj ); + Vec_PtrSetEntry( pGia->vNamesOut, h, Extra_UtilStrsav( Vec_PtrEntry( vNames, pSol[ABC_EXACT_SOL_NVARS] + h ) ) ); + p += ( 2 + pSol[ABC_EXACT_SOL_NVARS] ); } Abc_NodeFreeNames( vNames ); @@ -827,17 +1135,18 @@ static int Ses_ManFindMinimumSize( Ses_Man_t * pSes ) Synopsis [Find minimum size networks with a SAT solver.] Description [If nMaxDepth is -1, then depth constraints are ignored. - If nMaxDepth is not -1, one can set pArrivalTimes which should have the length of nVars. - One can ignore pArrivalTimes by setting it to NULL.] + If nMaxDepth is not -1, one can set pArrTimeProfile which should have the length of nVars. + One can ignore pArrTimeProfile by setting it to NULL.] SideEffects [] SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fVerbose ) +Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fVerbose ) { Ses_Man_t * pSes; + char * pSol; Abc_Ntk_t * pNtk = NULL; abctime timeStart; @@ -846,12 +1155,16 @@ Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth timeStart = Abc_Clock(); - pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrivalTimes, 0, fVerbose ); + pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 0, fVerbose ); if ( fVerbose ) Ses_ManPrintFuncs( pSes ); if ( Ses_ManFindMinimumSize( pSes ) ) - pNtk = Ses_ManExtractNtk( pSes ); + { + pSol = Ses_ManExtractSolution( pSes ); + pNtk = Ses_ManExtractNtk( pSol ); + ABC_FREE( pSol ); + } pSes->timeTotal = Abc_Clock() - timeStart; @@ -864,9 +1177,10 @@ 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 * pArrivalTimes, int fVerbose ) +Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrTimeProfile, int fVerbose ) { Ses_Man_t * pSes; + char * pSol; Gia_Man_t * pGia = NULL; abctime timeStart; @@ -875,12 +1189,16 @@ Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth timeStart = Abc_Clock(); - pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrivalTimes, 1, fVerbose ); + pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 1, fVerbose ); if ( fVerbose ) Ses_ManPrintFuncs( pSes ); if ( Ses_ManFindMinimumSize( pSes ) ) - pGia = Ses_ManExtractGia( pSes ); + { + pSol = Ses_ManExtractSolution( pSes ); + pGia = Ses_ManExtractGia( pSol ); + ABC_FREE( pSol ); + } pSes->timeTotal = Abc_Clock() - timeStart; @@ -920,7 +1238,7 @@ void Abc_ExactTestSingleOutput( int fVerbose ) word pTruth[4] = {0xcafe, 0, 0, 0}; Abc_Ntk_t * pNtk, * pNtk2, * pNtk3, * pNtk4; - int pArrivalTimes[4] = {6, 2, 8, 5}; + int pArrTimeProfile[4] = {6, 2, 8, 5}; pNtk = Abc_NtkFromTruthTable( pTruth, 4 ); @@ -938,7 +1256,7 @@ void Abc_ExactTestSingleOutput( int fVerbose ) assert( Abc_NtkLevel( pNtk3 ) <= 3 ); Abc_NtkDelete( pNtk3 ); - pNtk4 = Abc_NtkFindExact( pTruth, 4, 1, 9, pArrivalTimes, fVerbose ); + pNtk4 = Abc_NtkFindExact( pTruth, 4, 1, 9, pArrTimeProfile, fVerbose ); Abc_NtkShortNames( pNtk4 ); Abc_NtkCecSat( pNtk, pNtk4, 10000, 0 ); assert( pNtk4 ); @@ -947,7 +1265,7 @@ void Abc_ExactTestSingleOutput( int fVerbose ) assert( !Abc_NtkFindExact( pTruth, 4, 1, 2, NULL, fVerbose ) ); - assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrivalTimes, fVerbose ) ); + assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrTimeProfile, fVerbose ) ); Abc_NtkDelete( pNtk ); } @@ -958,7 +1276,7 @@ void Abc_ExactTestSingleOutputAIG( int fVerbose ) Abc_Ntk_t * pNtk; Gia_Man_t * pGia, * pGia2, * pGia3, * pGia4, * pMiter; Cec_ParCec_t ParsCec, * pPars = &ParsCec; - int pArrivalTimes[4] = {6, 2, 8, 5}; + int pArrTimeProfile[4] = {6, 2, 8, 5}; Cec_ManCecSetDefaultParams( pPars ); @@ -978,7 +1296,7 @@ void Abc_ExactTestSingleOutputAIG( int fVerbose ) Cec_ManVerify( pMiter, pPars ); Gia_ManStop( pMiter ); - pGia4 = Gia_ManFindExact( pTruth, 4, 1, 9, pArrivalTimes, fVerbose ); + pGia4 = Gia_ManFindExact( pTruth, 4, 1, 9, pArrTimeProfile, fVerbose ); pMiter = Gia_ManMiter( pGia, pGia4, 0, 1, 0, 0, 1 ); assert( pMiter ); Cec_ManVerify( pMiter, pPars ); @@ -986,7 +1304,7 @@ void Abc_ExactTestSingleOutputAIG( int fVerbose ) assert( !Gia_ManFindExact( pTruth, 4, 1, 2, NULL, fVerbose ) ); - assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrivalTimes, fVerbose ) ); + assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrTimeProfile, fVerbose ) ); Gia_ManStop( pGia ); Gia_ManStop( pGia2 ); @@ -1012,27 +1330,130 @@ void Abc_ExactTest( int fVerbose ) // this procedure should return 1, if the engine/library are available, and 0 otherwise int Abc_ExactIsRunning() { - return 0; + return s_pSesStore != NULL; } // this procedure returns the number of inputs of the library // for example, somebody may try to map into 10-cuts while the library only contains 8-functions int Abc_ExactInputNum() { - return 0; + assert( s_pSesStore ); + return s_pSesStore->nNumVars; } // 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 l; + Ses_Man_t * pSes; + char * pSol = NULL, * p; + int Delay = ABC_INFINITY, nMaxDepth = nVars - 1; + abctime timeStart; + + /* some checks */ + assert( nVars >= 2 && nVars <= 8 ); + + timeStart = Abc_Clock(); + *Cost = ABC_INFINITY; - return ABC_INFINITY; + + pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, 1 /* fMakeAIG */, 0 ); + + while ( 1 ) /* there is improvement */ + { + if ( Ses_ManFindMinimumSize( pSes ) ) + { + if ( pSol ) + ABC_FREE( pSol ); + pSol = Ses_ManExtractSolution( pSes ); + pSes->nMaxDepth--; + } + else + break; + } + + if ( pSol ) + { + *Cost = pSol[ABC_EXACT_SOL_NGATES]; + p = pSol + 3 + 4 * ABC_EXACT_SOL_NGATES + 1; + Delay = *p++; + for ( l = 0; l < nVars; ++l ) + pPerm[l] = *p++; + + /* store solution */ + if ( !Ses_StoreAddEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile, pSol ) ) + ABC_FREE( pSol ); /* store entry already exists, so free solution */ + } + + pSes->timeTotal = Abc_Clock() - timeStart; + + /* cleanup */ + Ses_ManClean( pSes ); + + return Delay; } -// this procedure returns a new node whose output in terms of the given fanins +// 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 ) { - return NULL; + char * pSol; + int i; + char const * p; + Abc_Obj_t * pObj; + Vec_Ptr_t * pGates; + char pGateTruth[5]; + char * pSopCover; + + Abc_Ntk_t * pNtk = NULL; /* need that to create node */ + + pSol = Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pArrTimeProfile ); + if ( !pSol ) + return NULL; + + assert( pSol[ABC_EXACT_SOL_NVARS] == nVars ); + assert( pSol[ABC_EXACT_SOL_NFUNC] == 1 ); + + pGates = Vec_PtrAlloc( nVars + pSol[ABC_EXACT_SOL_NGATES] ); + pGateTruth[3] = '0'; + pGateTruth[4] = '\0'; + + /* primary inputs */ + for ( i = 0; i < nVars; ++i ) + { + Vec_PtrPush( pGates, pFanins[i] ); + } + + /* gates */ + p = pSol + 3; + for ( i = 0; i < pSol[ABC_EXACT_SOL_NGATES]; ++i ) + { + pGateTruth[2] = '0' + ( *p & 1 ); + pGateTruth[1] = '0' + ( ( *p >> 1 ) & 1 ); + pGateTruth[0] = '0' + ( ( *p >> 2 ) & 1 ); + ++p; + + assert( *p == 2 ); /* binary gate */ + ++p; + + pSopCover = Abc_SopFromTruthBin( pGateTruth ); + pObj = Abc_NtkCreateNode( pNtk ); + pObj->pData = Abc_SopRegister( (Mem_Flex_t*)pNtk->pManFunc, pSopCover ); + Vec_PtrPush( pGates, pObj ); + ABC_FREE( pSopCover ); + + Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) ); + Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) ); + } + + /* output */ + if ( Abc_LitIsCompl( *p ) ) + pObj = Abc_NtkCreateNodeInv( pNtk, (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) ) ); + else + pObj = (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) ); + + Vec_PtrFree( pGates ); + + return pObj; } //////////////////////////////////////////////////////////////////////// |