luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/base/abci/abcExact.c

2972 lines
105 KiB
C
Raw Blame History

/**CFile****************************************************************
FileName [abcExact.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Find minimum size networks with a SAT solver.]
Author [Mathias Soeken]
Affiliation [EPFL]
Date [Ver. 1.0. Started - July 15, 2016.]
Revision [$Id: abcFanio.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
/* This implementation is based on Exercises 477 and 478 in
* Donald E. Knuth TAOCP Fascicle 6 (Satisfiability) Section 7.2.2.2
*/
#include "base/abc/abc.h"
#include "aig/gia/gia.h"
#include "misc/util/utilTruth.h"
#include "misc/vec/vecInt.h"
#include "misc/vec/vecPtr.h"
#include "proof/cec/cec.h"
#include "sat/bsat/satSolver.h"
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),
ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xF0F0F0F0F0F0F0F0),
ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFF00FF00FF00FF00),
ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFF0000FFFF0000),
ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0xFFFFFFFF00000000),
ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF),
ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000000000), ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0xFFFFFFFFFFFFFFFF)
};
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;
}
static int Abc_TtCofsOppositeWithMask( word * pTruth, word * pMask, int nWords, int iVar )
{
if ( iVar < 6 )
{
int w, Shift = ( 1 << iVar );
for ( w = 0; w < nWords; ++w )
if ( ( ( pTruth[w] << Shift ) & s_Truths6[iVar] & pMask[w] ) != ( ~pTruth[w] & s_Truths6[iVar] & pMask[w] ) )
return 0;
return 1;
}
else
{
int w, Step = ( 1 << ( iVar - 6 ) );
word * p = pTruth, * m = pMask, * pLimit = pTruth + nWords;
for ( ; p < pLimit; p += 2 * Step, m += 2 * Step )
for ( w = 0; w < Step; ++w )
if ( ( p[w] & m[w] ) != ( ~p[w + Step] & m[w + Step] ) )
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 iVar )
{
assert( iVar < 8 );
if ( Abc_TtIsSubsetWithMask( pTruth, &s_Truths8[iVar << 2], pMask, nWords ) ) return 1;
if ( Abc_TtIsSubsetWithMask( pTruth, &s_Truths8Neg[iVar << 2], pMask, nWords ) ) return 2;
if ( Abc_TtIsSubsetWithMask( &s_Truths8[iVar << 2], pTruth, pMask, nWords ) ) return 3;
if ( Abc_TtIsSubsetWithMask( &s_Truths8Neg[iVar << 2], pTruth, pMask, nWords ) ) return 4;
if ( Abc_TtCofsOppositeWithMask( pTruth, pMask, nWords, iVar ) ) return 5;
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 * pStairFunc )
{
int i, d;
word pMask[4];
word pCopy[4];
Abc_TtCopy( pCopy, pTruth, nWords, 0 );
Abc_TtMask( pMask, nWords, nWords * 64 );
for ( i = 0; i < nSize; ++i )
{
d = Abc_TtIsTopDecomposable( pCopy, pMask, nWords, pVars[i] );
if ( !d )
return 0; /* not decomposable */
pStairFunc[i] = d;
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;
case 5:
Abc_TtXor( pCopy, pCopy, &s_Truths8[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 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 */
Vec_Int_t * vPolar; /* variables with positive polarity */
Vec_Int_t * vAssump; /* assumptions */
int nRandRowAssigns; /* number of random row assignments to initialize CEGAR */
int fKeepRowAssigns; /* if 1, keep counter examples in CEGAR for next number of gates */
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 */
Vec_Int_t * vStairDecVars; /* list of stair decomposable variables */
int pStairDecFunc[8]; /* list of stair decomposable functions */
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 nSimOffset; /* offset where gate variables start */
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 */
int nDebugOffset; /* for debug printing */
};
/***********************************************************************
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 */
int fResLimit; /* solution found after resource limit */
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 */
int nVars; /* number of variables */
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 fMakeAIG; /* create AIG instead of general network */
int fVerbose; /* be verbose */
int fVeryVerbose; /* be very verbose */
int nBTLimit; /* conflict limit */
int nEntriesCount; /* number of entries */
int nValidEntriesCount; /* number of entries with network */
Ses_TruthEntry_t * pEntries[SES_STORE_TABLE_SIZE]; /* hash table for truth table entries */
sat_solver * pSat; /* own SAT solver instance to reuse when calling exact algorithm */
FILE * pDebugEntries; /* debug unsynth. (rl) entries */
char * szDBName; /* if given, database is written every time a new entry is added */
/* 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;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static int Abc_NormalizeArrivalTimes( int * pArrTimeProfile, int nVars, int * maxNormalized )
{
int * p = pArrTimeProfile, * pEnd = pArrTimeProfile + nVars;
int delta = *p;
while ( ++p < pEnd )
if ( *p < delta )
delta = *p;
*maxNormalized = 0;
p = pArrTimeProfile;
while ( p < pEnd )
{
*p -= delta;
if ( *p > *maxNormalized )
*maxNormalized = *p;
++p;
}
*maxNormalized += 1;
return delta;
}
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;
memset( pStore->pEntries, 0, SES_STORE_TABLE_SIZE );
pStore->pSat = sat_solver_new();
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 );
}
}
sat_solver_delete( pStore->pSat );
if ( pStore->szDBName )
ABC_FREE( pStore->szDBName );
ABC_FREE( pStore );
}
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 < Abc_TtWordNum( nVars ); ++i )
uHash ^= pTruth[i] * s_Primes[i & 0xf];
return (int)(uHash % SES_STORE_TABLE_SIZE );
}
static inline int Ses_StoreTruthEqual( Ses_TruthEntry_t * pEntry, word * pTruth, int nVars )
{
int i;
if ( pEntry->nVars != nVars )
return 0;
for ( i = 0; i < Abc_TtWordNum( nVars ); ++i )
if ( pEntry->pTruth[i] != pTruth[i] )
return 0;
return 1;
}
static inline void Ses_StoreTruthCopy( Ses_TruthEntry_t * pEntry, word * pTruthSrc, int nVars )
{
int i;
pEntry->nVars = nVars;
for ( i = 0; i < Abc_TtWordNum( nVars ); ++i )
pEntry->pTruth[i] = pTruthSrc[i];
}
static inline int Ses_StoreTimesEqual( int * pTimes1, int * pTimes2, int nVars )
{
int i;
for ( i = 0; i < nVars; ++i )
if ( pTimes1[i] != pTimes2[i] )
return 0;
return 1;
}
static inline void Ses_StoreTimesCopy( int * pTimesDest, int * pTimesSrc, int nVars )
{
int i;
for ( i = 0; i < nVars; ++i )
pTimesDest[i] = pTimesSrc[i];
}
static inline void Ses_StorePrintEntry( Ses_TruthEntry_t * pEntry, Ses_TimesEntry_t * pTiEntry )
{
int i;
printf( "f = " );
Abc_TtPrintHexRev( stdout, pEntry->pTruth, pEntry->nVars );
printf( ", n = %d", pEntry->nVars );
printf( ", arrival =" );
for ( i = 0; i < pEntry->nVars; ++i )
printf( " %d", pTiEntry->pArrTimeProfile[i] );
printf( "\n" );
}
static inline void Ses_StorePrintDebugEntry( Ses_Store_t * pStore, word * pTruth, int nVars, int * pNormalArrTime, int nMaxDepth, 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 );
}
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;
pFile = fopen( pFilename, "wb" );
if (pFile == NULL)
{
printf( "cannot open file \"%s\" for writing\n", pFilename );
return;
}
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] )
{
pTEntry = pStore->pEntries[i];
while ( pTEntry )
{
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( 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;
}
}
fclose( pFile );
}
// 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 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];
/* does truth table already exist? */
while ( pTEntry )
{
if ( Ses_StoreTruthEqual( pTEntry, pTruth, nVars ) )
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( pTEntry, pTruth, nVars );
pTEntry->next = pStore->pEntries[key];
pStore->pEntries[key] = pTEntry;
}
/* does arrival time already exist? */
pTiEntry = pTEntry->head;
while ( pTiEntry )
{
if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) )
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( pTiEntry->pArrTimeProfile, pArrTimeProfile, nVars );
pTiEntry->pNetwork = pSol;
pTiEntry->fResLimit = fResLimit;
pTiEntry->next = pTEntry->head;
pTEntry->head = pTiEntry;
/* item has been added */
fAdded = 1;
pStore->nEntriesCount++;
if ( pSol )
pStore->nValidEntriesCount++;
}
else
{
//assert( 0 );
/* item was already present */
fAdded = 0;
}
/* statistics */
if ( pSol )
{
if ( fResLimit )
{
pStore->nSynthesizedRL++;
pStore->pSynthesizedRL[nVars]++;
}
else
{
pStore->nSynthesizedImp++;
pStore->pSynthesizedImp[nVars]++;
}
}
else
{
if ( fResLimit )
{
pStore->nUnsynthesizedRL++;
pStore->pUnsynthesizedRL[nVars]++;
}
else
{
pStore->nUnsynthesizedImp++;
pStore->pUnsynthesizedImp[nVars]++;
}
}
if ( fAdded && pStore->szDBName )
Ses_StoreWrite( pStore, pStore->szDBName, 1, 0, 0, 0 );
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_StoreGetEntrySimple( Ses_Store_t * pStore, word * pTruth, int nVars, int * pArrTimeProfile, char ** pSol )
{
int key;
Ses_TruthEntry_t * pTEntry;
Ses_TimesEntry_t * pTiEntry;
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 )
{
if ( Ses_StoreTimesEqual( pArrTimeProfile, pTiEntry->pArrTimeProfile, nVars ) )
break;
else
pTiEntry = pTiEntry->next;
}
/* no entry found? */
if ( !pTiEntry )
return 0;
*pSol = pTiEntry->pNetwork;
return 1;
}
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_StoreRead( Ses_Store_t * pStore, const char * pFilename, int fSynthImp, int fSynthRL, int fUnsynthImp, int fUnsynthRL )
{
int i;
unsigned long nEntries;
word pTruth[4];
int nVars, fResLimit;
int pArrTimeProfile[8];
char pHeader[3];
char * pNetwork;
FILE * pFile;
int value;
if ( pStore->szDBName )
{
printf( "cannot read from database when szDBName is set" );
return;
}
pFile = fopen( pFilename, "rb" );
if (pFile == NULL)
{
printf( "cannot open file \"%s\" for reading\n", pFilename );
return;
}
value = fread( &nEntries, sizeof( unsigned long ), 1, pFile );
for ( i = 0; i < (int)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 );
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 );
}
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;
word pMask[4];
Abc_TtMask( pMask, pSes->nSpecWords, pSes->nSpecWords * 64 );
for ( l = 0; l < pSes->nSpecVars; ++l )
if ( Abc_TtIsTopDecomposable( pSes->pSpec, pMask, pSes->nSpecWords, l ) )
pSes->pDecVars |= ( 1 << l );
}
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;
Ses_Man_t * p = ABC_CALLOC( Ses_Man_t, 1 );
p->pSat = NULL;
p->bSpecInv = 0;
for ( h = 0; h < nFunc; ++h )
if ( pTruth[h << 2] & 1 )
{
for ( i = 0; i < 4; ++i )
pTruth[(h << 2) + i] = ~pTruth[(h << 2) + i];
p->bSpecInv |= ( 1 << h );
}
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 = nBTLimit;
p->fVerbose = fVerbose;
p->fVeryVerbose = 0;
p->fExtractVerbose = 0;
p->fSatVerbose = 0;
p->vPolar = Vec_IntAlloc( 100 );
p->vAssump = Vec_IntAlloc( 10 );
p->vStairDecVars = Vec_IntAlloc( nVars );
p->nRandRowAssigns = 2 * nVars;
p->fKeepRowAssigns = 0;
if ( p->nSpecFunc == 1 )
Ses_ManComputeTopDec( p );
srand( 0xCAFE );
return p;
}
static inline void Ses_ManCleanLight( Ses_Man_t * pSes )
{
int h, i;
for ( h = 0; h < pSes->nSpecFunc; ++h )
if ( ( pSes->bSpecInv >> h ) & 1 )
for ( i = 0; i < 4; ++i )
pSes->pSpec[(h << 2) + i] = ~( pSes->pSpec[(h << 2) + i] );
if ( pSes->pArrTimeProfile )
for ( i = 0; i < pSes->nSpecVars; ++i )
pSes->pArrTimeProfile[i] += pSes->nArrTimeDelta;
Vec_IntFree( pSes->vPolar );
Vec_IntFree( pSes->vAssump );
Vec_IntFree( pSes->vStairDecVars );
ABC_FREE( pSes );
}
static inline void Ses_ManClean( Ses_Man_t * pSes )
{
if ( pSes->pSat )
sat_solver_delete( pSes->pSat );
Ses_ManCleanLight( pSes );
}
/**Function*************************************************************
Synopsis [Access variables based on indexes.]
***********************************************************************/
static inline int Ses_ManSimVar( Ses_Man_t * pSes, int i, int t )
{
assert( i < pSes->nGates );
assert( t < pSes->nRows );
return pSes->nSimOffset + pSes->nRows * i + t;
}
static inline int Ses_ManOutputVar( Ses_Man_t * pSes, int h, int i )
{
assert( h < pSes->nSpecFunc );
assert( i < pSes->nGates );
return pSes->nOutputOffset + pSes->nGates * h + i;
}
static inline int Ses_ManGateVar( Ses_Man_t * pSes, int i, int p, int q )
{
assert( i < pSes->nGates );
assert( p < 2 );
assert( q < 2 );
assert( p > 0 || q > 0 );
return pSes->nGateOffset + i * 3 + ( p << 1 ) + q - 1;
}
static inline int Ses_ManSelectVar( Ses_Man_t * pSes, int i, int j, int k )
{
int a;
int offset;
assert( i < pSes->nGates );
assert( k < pSes->nSpecVars + i );
assert( j < k );
offset = pSes->nSelectOffset;
for ( a = pSes->nSpecVars; a < pSes->nSpecVars + i; ++a )
offset += a * ( a - 1 ) / 2;
return offset + ( -j * ( 1 + j - 2 * ( pSes->nSpecVars + i ) ) ) / 2 + ( k - j - 1 );
}
static inline int Ses_ManDepthVar( Ses_Man_t * pSes, int i, int j )
{
assert( i < pSes->nGates );
assert( j <= pSes->nArrTimeMax + i );
return pSes->nDepthOffset + i * pSes->nArrTimeMax + ( ( i * ( i + 1 ) ) / 2 ) + 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 = NULL, * 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.]
***********************************************************************/
static void Ses_ManCreateVars( Ses_Man_t * pSes, int nGates )
{
int i;
if ( pSes->fSatVerbose )
{
printf( "create variables for network with %d functions over %d variables and %d/%d gates\n", pSes->nSpecFunc, pSes->nSpecVars, nGates, pSes->nMaxGates );
}
pSes->nGates = nGates;
pSes->nSimVars = nGates * pSes->nRows;
pSes->nOutputVars = pSes->nSpecFunc * nGates;
pSes->nGateVars = nGates * 3;
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->nArrTimeMax + ( nGates * ( nGates + 1 ) ) / 2 : 0;
/* pSes->nSimOffset = 0; */
/* pSes->nOutputOffset = pSes->nSimVars; */
/* pSes->nGateOffset = pSes->nSimVars + pSes->nOutputVars; */
/* pSes->nSelectOffset = pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars; */
/* pSes->nDepthOffset = pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars + pSes->nSelectVars; */
pSes->nDepthOffset = 0;
pSes->nSelectOffset = pSes->nDepthVars;
pSes->nGateOffset = pSes->nDepthVars + pSes->nSelectVars;
pSes->nOutputOffset = pSes->nDepthVars + pSes->nSelectVars + pSes->nGateVars;
pSes->nSimOffset = pSes->nDepthVars + pSes->nSelectVars + pSes->nGateVars + pSes->nOutputVars;
/* pSes->nDepthOffset = 0; */
/* pSes->nSelectOffset = pSes->nDepthVars; */
/* pSes->nOutputOffset = pSes->nDepthVars + pSes->nSelectVars; */
/* pSes->nGateOffset = pSes->nDepthVars + pSes->nSelectVars + pSes->nOutputVars; */
/* pSes->nSimOffset = pSes->nDepthVars + pSes->nSelectVars + pSes->nOutputVars + pSes->nGateVars; */
/* if we already have a SAT solver, then restart it (this saves a lot of time) */
if ( pSes->pSat )
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 );
}
/**Function*************************************************************
Synopsis [Create clauses.]
***********************************************************************/
static inline void Ses_ManGateCannotHaveChild( Ses_Man_t * pSes, int i, int j )
{
int k;
for ( k = 0; k < j; ++k )
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, k, j ), 1 ) );
for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 ) );
}
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;
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 ( ( ( ( t + 1 ) & ( 1 << j ) ) ? 1 : 0 ) != b )
return;
}
else
pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, j - pSes->nSpecVars, t ), b );
if ( k < pSes->nSpecVars )
{
if ( ( ( ( t + 1 ) & ( 1 << k ) ) ? 1 : 0 ) != c )
return;
}
else
pLits[ctr++] = Abc_Var2Lit( Ses_ManSimVar( pSes, k - pSes->nSpecVars, t ), c );
if ( b > 0 || c > 0 )
pLits[ctr++] = Abc_Var2Lit( Ses_ManGateVar( pSes, i, b, c ), 1 - a );
sat_solver_addclause( pSes->pSat, pLits, pLits + ctr );
}
static int inline Ses_ManCreateTruthTableClause( Ses_Man_t * pSes, int t )
{
int i, j, k, h;
int pLits[3];
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 */
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 ) );
if ( !sat_solver_addclause( pSes->pSat, pLits, pLits + 2 ) )
return 0;
}
}
if ( pSes->nSpecFunc == 1 )
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSimVar( pSes, pSes->nGates - 1, t ), 1 - Abc_TtGetBit( pSes->pSpec, t + 1 ) ) );
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 )
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, i ), 1 ) );
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManOutputVar( pSes, 0, pSes->nGates - 1 ), 0 ) );
vLits = Vec_IntAlloc( 0u );
}
else
{
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 )
{
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_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 )
{
for ( i = 0; i < pSes->nGates; ++i )
{
/* not 2 ones */
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 );
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 );
}
}
/* 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 stair decomposition */
if (Vec_IntSize( pSes->vStairDecVars ) )
{
Vec_IntForEachEntry( pSes->vStairDecVars, j, i )
{
if ( pSes->nGates - 2 - i < j )
{
continue;
}
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManSelectVar( pSes, pSes->nGates - 1 - i, j, pSes->nSpecVars + pSes->nGates - 2 - i ), 0 ) );
//printf( "dec %d for var %d\n", pSes->pStairDecFunc[i], j );
switch ( pSes->pStairDecFunc[i] )
{
case 1: /* AND(x,g) */
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 1 ) );
//Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 1 ) );
//Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) );
break;
case 2: /* AND(!x,g) */
//Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) );
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 1 ) );
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 1 ) );
break;
case 3: /* OR(x,g) */
//Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) );
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 0 ) );
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) );
break;
case 4: /* OR(!x,g) */
////Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) );
////Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 1 ) );
////Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 0 ) );
break;
case 5: /* XOR(x,g) */
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 0, 1 ), 0 ) );
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 0 ), 0 ) );
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManGateVar( pSes, pSes->nGates - 1 - i, 1, 1 ), 1 ) );
break;
default:
printf( "func: %d\n", pSes->pStairDecFunc[i] );
assert( 0 );
}
}
}
/* 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 )
{
jj = 0;
for ( h = 0; h < pSes->nSpecFunc; ++h )
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_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_IntSetEntry( vLits, jj++, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, pSes->nSpecVars + i, j ), 0 ) );
}
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 )
{
for ( k = 2; k < pSes->nSpecVars + i; ++k )
{
for ( j = 1; j < k; ++j )
for ( jj = 0; jj < j; ++jj )
{
pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i + 1, jj, k ), 1 );
sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
}
for ( j = 0; j < k; ++j )
for ( kk = 1; kk < k; ++kk )
for ( jj = 0; jj < kk; ++jj )
{
pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i + 1, jj, kk ), 1 );
sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
}
}
}
/* EXTRA clauses: symmetric variables */
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 ), pSes->nSpecVars, p, q ) &&
( !pSes->pArrTimeProfile || ( pSes->pArrTimeProfile[p] <= pSes->pArrTimeProfile[q] ) ) )
{
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 )
{
if ( j == p ) continue;
vLits = Vec_IntAlloc( 0 );
Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, q ), 1 ) );
for ( ii = 0; ii < i; ++ii )
for ( kk = 1; kk < pSes->nSpecVars + ii; ++kk )
for ( jj = 0; jj < kk; ++jj )
if ( jj == p || kk == p )
Vec_IntPush( vLits, Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, jj, kk ), 0 ) );
sat_solver_addclause( pSes->pSat, Vec_IntArray( vLits ), Vec_IntLimit( vLits ) );
Vec_IntFree( vLits );
}
}
return 1;
}
static int Ses_ManCreateDepthClauses( Ses_Man_t * pSes )
{
int i, j, k, jj, kk, d, h;
int pLits[3];
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 );
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 );
sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
}
}
/* 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];
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 */
Vec_IntPush( pSes->vAssump, Abc_Var2Lit( Ses_ManDepthVar( pSes, i, 0 ), 0 ) );
/* 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;
}
/**Function*************************************************************
Synopsis [Solve.]
***********************************************************************/
static inline double Sat_Wrd2Dbl( word w ) { return (double)(unsigned)(w&0x3FFFFFFF) + (double)(1<<30)*(unsigned)(w>>30); }
static inline int Ses_ManSolve( Ses_Man_t * pSes )
{
int status;
abctime timeStart, timeDelta;
if ( pSes->fSatVerbose )
{
printf( "SAT CL: %7d VA: %5d", sat_solver_nclauses( pSes->pSat ), sat_solver_nvars( pSes->pSat ) );
fflush( stdout );
}
timeStart = Abc_Clock();
status = sat_solver_solve( pSes->pSat, Vec_IntArray( pSes->vAssump ), Vec_IntLimit( pSes->vAssump ), pSes->nBTLimit, 0, 0, 0 );
timeDelta = Abc_Clock() - timeStart;
if ( pSes->fSatVerbose )
printf( " RE: %2d ST: %4.f CO: %7.0f DE: %6.0f PR: %6.0f\n",
status,
Sat_Wrd2Dbl( pSes->pSat->stats.starts ), Sat_Wrd2Dbl( pSes->pSat->stats.conflicts ),
Sat_Wrd2Dbl( pSes->pSat->stats.decisions ), Sat_Wrd2Dbl( pSes->pSat->stats.propagations ) );
//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" );
}
return 2;
}
}
/**Function*************************************************************
Synopsis [Extract solution.]
***********************************************************************/
// 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: integer with number of fanins
// fanin[i]: 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
static char * Ses_ManExtractSolution( Ses_Man_t * pSes )
{
int nSol, h, i, j, k, l, aj, ak, d, nOp;
char * pSol, * p;
int * pPerm = NULL; /* 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;
if ( pSes->fExtractVerbose )
printf( "add gate %d with operation %d", pSes->nSpecVars + i, nOp );
for ( k = 0; k < pSes->nSpecVars + i; ++k )
for ( j = 0; j < k; ++j )
if ( sat_solver_var_value( pSes->pSat, Ses_ManSelectVar( pSes, i, j, k ) ) )
{
if ( pSes->fExtractVerbose )
printf( " and operands %d and %d", j, k );
*p++ = j;
*p++ = k;
k = pSes->nSpecVars + i;
break;
}
if ( pSes->fExtractVerbose )
{
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 + 3];
for ( l = 0; l < pSes->nSpecVars; ++l )
{
/* pin-to-pin delay to input l of child nodes */
aj = j < pSes->nSpecVars ? 0 : pPerm[(j - pSes->nSpecVars) * pSes->nSpecVars + l];
ak = k < pSes->nSpecVars ? 0 : pPerm[(k - pSes->nSpecVars) * pSes->nSpecVars + l];
if ( aj == 0 && ak == 0 )
pPerm[i * pSes->nSpecVars + l] = ( l == j || l == k ) ? 1 : 0;
else
pPerm[i * pSes->nSpecVars + l] = Abc_MaxInt( 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 )
for ( l = 0; l < 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->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->pArrTimeProfile && pSes->fExtractVerbose )
printf( " pin-to-pin arrival time from input %d is %d (pArrTimeProfile = %d)\n", l, d, pSes->pArrTimeProfile[l] );
*p++ = d;
}
}
/* pin-to-pin delays */
if ( pSes->nMaxDepth != -1 )
ABC_FREE( pPerm );
/* 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;
}
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;
char pGateTruth[5];
char * pSopCover;
pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
pNtk->pName = Extra_UtilStrsav( "exact" );
pGates = Vec_PtrAlloc( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NGATES] );
pGateTruth[3] = '0';
pGateTruth[4] = '\0';
vNames = Abc_NodeGetFakeNames( pSol[ABC_EXACT_SOL_NVARS] + pSol[ABC_EXACT_SOL_NFUNC] );
/* primary inputs */
Vec_PtrPush( pNtk->vObjs, NULL );
for ( i = 0; i < pSol[ABC_EXACT_SOL_NVARS]; ++i )
{
pObj = Abc_NtkCreatePi( pNtk );
Abc_ObjAssignName( pObj, (char*)Vec_PtrEntry( vNames, i ), NULL );
Vec_PtrPush( pGates, pObj );
}
/* 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++ ) );
}
/* outputs */
for ( h = 0; h < pSol[ABC_EXACT_SOL_NFUNC]; ++h )
{
pObj = Abc_NtkCreatePo( pNtk );
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 );
Vec_PtrFree( pGates );
if ( !Abc_NtkCheck( pNtk ) )
printf( "Ses_ManExtractSolution(): Network check has failed.\n" );
return pNtk;
}
static Gia_Man_t * Ses_ManExtractGia( char const * pSol )
{
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( 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( 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( pSol[ABC_EXACT_SOL_NVARS] );
for ( i = 0; i < pSol[ABC_EXACT_SOL_NVARS]; ++i )
{
nObj = Gia_ManAppendCi( pGia );
Vec_IntPush( pGates, nObj );
Vec_PtrSetEntry( pGia->vNamesIn, i, Extra_UtilStrsav( (const char*)Vec_PtrEntry( vNames, i ) ) );
}
/* gates */
p = pSol + 3;
for ( i = 0; i < pSol[ABC_EXACT_SOL_NGATES]; ++i )
{
assert( p[1] == 2 );
nChild1 = Vec_IntEntry( pGates, p[2] );
nChild2 = Vec_IntEntry( pGates, p[3] );
fChild1Comp = fChild2Comp = 0;
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 );
p += 4;
}
/* outputs */
pGia->vNamesOut = Vec_PtrStart( pSol[ABC_EXACT_SOL_NFUNC] );
for ( h = 0; h < pSol[ABC_EXACT_SOL_NFUNC]; ++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( (const char*)Vec_PtrEntry( vNames, pSol[ABC_EXACT_SOL_NVARS] + h ) ) );
p += ( 2 + pSol[ABC_EXACT_SOL_NVARS] );
}
Abc_NodeFreeNames( vNames );
Vec_IntFree( pGates );
return pGia;
}
/**Function*************************************************************
Synopsis [Debug.]
***********************************************************************/
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( " 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 )
{
int h;
printf( "find optimum circuit for %d %d-variable functions:\n", pSes->nSpecFunc, pSes->nSpecVars );
for ( h = 0; h < pSes->nSpecFunc; ++h )
{
printf( " func %d: ", h + 1 );
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 )
{
int h, i, j, k, p, q, t;
for ( i = 0; i < pSes->nGates; ++i )
for ( t = 0; t < pSes->nRows; ++t )
printf( "x(%d, %d) : %d\n", i, t, Ses_ManSimVar( pSes, i, t ) );
for ( h = 0; h < pSes->nSpecFunc; ++h )
for ( i = 0; i < pSes->nGates; ++i )
printf( "h(%d, %d) : %d\n", h, i, Ses_ManOutputVar( pSes, h, i ) );
for ( i = 0; i < pSes->nGates; ++i )
for ( p = 0; p <= 1; ++p )
for ( q = 0; q <= 1; ++ q)
{
if ( p == 0 && q == 0 ) { continue; }
printf( "f(%d, %d, %d) : %d\n", i, p, q, Ses_ManGateVar( pSes, i, p, q ) );
}
for ( i = 0; i < pSes->nGates; ++i )
for ( j = 0; j < pSes->nSpecVars + i; ++j )
for ( k = j + 1; k < pSes->nSpecVars + i; ++k )
printf( "s(%d, %d, %d) : %d\n", i, j, k, Ses_ManSelectVar( pSes, i, j, k ) );
if ( pSes->nMaxDepth > 0 )
for ( i = 0; i < pSes->nGates; ++i )
for ( j = 0; j <= i; ++j )
printf( "d(%d, %d) : %d\n", i, j, Ses_ManDepthVar( pSes, i, j ) );
}
/**Function*************************************************************
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_IntClear( pSes->vStairDecVars );
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->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 )
{
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( pSes->vStairDecVars ) );
if ( fAdded > 1 || ( nLevel + 1 < pSes->nSpecVars ) )
{
if ( pSes->fReasonVerbose )
printf( "give up due to impossible decomposition at level %d", nLevel );
return 0;
}
}
else
{
Vec_IntPush( pSes->vStairDecVars, l );
}
fAdded++;
}
if ( !fAdded ) break;
++nLevel;
}
if ( Vec_IntSize( pSes->vStairDecVars ) && !Abc_TtIsStairDecomposable( pSes->pSpec, pSes->nSpecWords, Vec_IntArray( pSes->vStairDecVars ), Vec_IntSize( pSes->vStairDecVars ), pSes->pStairDecFunc ) )
{
if ( pSes->fReasonVerbose )
{
printf( "give up due to impossible stair decomposition at level %d: ", nLevel );
Vec_IntPrint( pSes->vStairDecVars );
}
return 0;
}
}
/* 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();
Vec_IntClear( pSes->vPolar );
Vec_IntClear( pSes->vAssump );
Ses_ManCreateVars( pSes, nGates );
if ( pSes->nMaxDepth != -1 )
{
f = Ses_ManCreateDepthClauses( pSes );
pSes->timeInstance += ( Abc_Clock() - timeStart );
if ( !f ) return 2; /* proven UNSAT while creating clauses */
}
sat_solver_set_polarity( pSes->pSat, Vec_IntArray( pSes->vPolar ), Vec_IntSize( pSes->vPolar ) );
/* 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 */
}
// is there a network for a given number of gates
/* return: (3: impossible, 2: continue, 1: found, 0: gave up) */
static int Ses_ManFindNetworkExactCEGAR( Ses_Man_t * pSes, int nGates, char ** pSol )
{
int fRes, iMint, fSat, i;
word pTruth[4];
/* debug */
Abc_DebugErase( pSes->nDebugOffset + ( nGates > 10 ? 5 : 4 ), pSes->fVeryVerbose );
Abc_DebugPrintIntInt( " (%d/%d)", nGates, pSes->nMaxGates, pSes->fVeryVerbose );
/* do #gates and max depth allow for a network? */
if ( !Ses_CheckGatesConsistency( pSes, nGates ) )
return 3;
for ( i = 0; i < pSes->nRandRowAssigns; ++i )
Abc_TtSetBit( pSes->pTtValues, rand() % pSes->nRows );
fRes = Ses_ManFindNetworkExact( pSes, nGates );
if ( fRes != 1 ) return fRes;
while ( true )
{
*pSol = Ses_ManExtractSolution( pSes );
Abc_TtXor( pTruth, Ses_ManDeriveTruth( pSes, *pSol, 0 ), pSes->pSpec, pSes->nSpecWords, 0 );
iMint = Abc_TtFindFirstBit( pTruth, pSes->nSpecVars );
if ( iMint == -1 )
{
assert( fRes == 1 );
return 1;
}
ABC_FREE( *pSol );
if ( pSes->fKeepRowAssigns )
Abc_TtSetBit( pSes->pTtValues, iMint - 1 );
if ( !Ses_ManCreateTruthTableClause( pSes, iMint - 1 ) ) /* UNSAT, continue */
return 2;
if ( ( fSat = Ses_ManSolve( pSes ) ) == 1 ) continue;
return ( fSat == 2 ) ? 0 : 2;
}
}
// find minimum size by increasing the number of gates
static char * Ses_ManFindMinimumSizeBottomUp( Ses_Man_t * pSes )
{
int nGates = pSes->nStartGates, fRes;
char * pSol = NULL;
/* store whether call was unsuccessful due to resource limit and not due to impossible constraint */
pSes->fHitResLimit = 0;
pSes->nDebugOffset = pSes->nMaxGates >= 10 ? 3 : 2;
/* adjust number of gates if there is a stair decomposition */
if ( Vec_IntSize( pSes->vStairDecVars ) )
nGates = Abc_MaxInt( nGates, Vec_IntSize( pSes->vStairDecVars ) - 1 );
//Ses_ManStoreDepthAndArrivalTimes( pSes );
memset( pSes->pTtValues, 0, 4 * sizeof( word ) );
Abc_DebugPrintIntInt( " (%d/%d)", nGates, pSes->nMaxGates, pSes->fVeryVerbose );
while ( true )
{
++nGates;
fRes = Ses_ManFindNetworkExactCEGAR( pSes, nGates, &pSol );
if ( fRes == 0 )
{
pSes->fHitResLimit = 1;
break;
}
else if ( fRes == 1 || fRes == 3 )
break;
}
Abc_DebugErase( pSes->nDebugOffset + ( nGates >= 10 ? 5 : 4 ), pSes->fVeryVerbose );
return pSol;
}
static char * Ses_ManFindMinimumSizeTopDown( Ses_Man_t * pSes, int nMinGates )
{
int nGates = pSes->nMaxGates, fRes;
char * pSol = NULL, * pSol2 = NULL;
pSes->fHitResLimit = 0;
Abc_DebugPrintIntInt( " (%d/%d)", nGates, pSes->nMaxGates, pSes->fVeryVerbose );
while ( true )
{
fRes = Ses_ManFindNetworkExactCEGAR( pSes, nGates, &pSol2 );
if ( fRes == 0 )
{
pSes->fHitResLimit = 1;
break;
}
else if ( fRes == 2 || fRes == 3 )
break;
pSol = pSol2;
if ( nGates == nMinGates )
break;
--nGates;
}
Abc_DebugErase( pSes->nDebugOffset + ( nGates >= 10 ? 5 : 4 ), pSes->fVeryVerbose );
return pSol;
}
static char * Ses_ManFindMinimumSize( Ses_Man_t * pSes )
{
char * pSol = NULL;
/* do the arrival times allow for a network? */
if ( pSes->nMaxDepth != -1 && pSes->pArrTimeProfile )
{
if ( !Ses_CheckDepthConsistency( pSes ) )
return 0;
Ses_ManComputeMaxGates( pSes );
}
pSol = Ses_ManFindMinimumSizeBottomUp( pSes );
if ( !pSol && pSes->nMaxDepth != -1 && pSes->fHitResLimit && pSes->nGates != pSes->nMaxGates )
return Ses_ManFindMinimumSizeTopDown( pSes, pSes->nGates + 1 );
else
return pSol;
}
/**Function*************************************************************
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 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 * pArrTimeProfile, int nBTLimit, int nStartGates, int fVerbose )
{
Ses_Man_t * pSes;
char * pSol;
Abc_Ntk_t * pNtk = NULL;
abctime timeStart;
/* some checks */
assert( nVars >= 2 && nVars <= 8 );
timeStart = Abc_Clock();
pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 0, nBTLimit, fVerbose );
pSes->nStartGates = nStartGates;
pSes->fReasonVerbose = 0;
pSes->fSatVerbose = 0;
if ( fVerbose )
Ses_ManPrintFuncs( pSes );
if ( ( pSol = Ses_ManFindMinimumSize( pSes ) ) != NULL )
{
pNtk = Ses_ManExtractNtk( pSol );
ABC_FREE( pSol );
}
pSes->timeTotal = Abc_Clock() - timeStart;
if ( fVerbose )
Ses_ManPrintRuntime( pSes );
/* cleanup */
Ses_ManClean( pSes );
return pNtk;
}
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;
Gia_Man_t * pGia = NULL;
abctime timeStart;
/* some checks */
assert( nVars >= 2 && nVars <= 8 );
timeStart = Abc_Clock();
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 );
if ( ( pSol = Ses_ManFindMinimumSize( pSes ) ) != NULL )
{
pGia = Ses_ManExtractGia( pSol );
ABC_FREE( pSol );
}
pSes->timeTotal = Abc_Clock() - timeStart;
if ( fVerbose )
Ses_ManPrintRuntime( pSes );
/* cleanup */
Ses_ManClean( pSes );
return pGia;
}
/**Function*************************************************************
Synopsis [Some test cases.]
***********************************************************************/
Abc_Ntk_t * Abc_NtkFromTruthTable( word * pTruth, int nVars )
{
Abc_Ntk_t * pNtk;
Mem_Flex_t * pMan;
char * pSopCover;
pMan = Mem_FlexStart();
pSopCover = Abc_SopCreateFromTruth( pMan, nVars, (unsigned*)pTruth );
pNtk = Abc_NtkCreateWithNode( pSopCover );
Abc_NtkShortNames( pNtk );
Mem_FlexStop( pMan, 0 );
return pNtk;
}
void Abc_ExactTestSingleOutput( int fVerbose )
{
extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit );
word pTruth[4] = {0xcafe, 0, 0, 0};
Abc_Ntk_t * pNtk, * pNtk2, * pNtk3, * pNtk4;
int pArrTimeProfile[4] = {6, 2, 8, 5};
pNtk = Abc_NtkFromTruthTable( pTruth, 4 );
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, 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, 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, 50000, 0, fVerbose ) );
assert( !Abc_NtkFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, 0, fVerbose ) );
Abc_NtkDelete( pNtk );
}
void Abc_ExactTestSingleOutputAIG( int fVerbose )
{
word pTruth[4] = {0xcafe, 0, 0, 0};
Abc_Ntk_t * pNtk;
Gia_Man_t * pGia, * pGia2, * pGia3, * pGia4, * pMiter;
Cec_ParCec_t ParsCec, * pPars = &ParsCec;
int pArrTimeProfile[4] = {6, 2, 8, 5};
Cec_ManCecSetDefaultParams( pPars );
pNtk = Abc_NtkFromTruthTable( pTruth, 4 );
Abc_NtkToAig( pNtk );
pGia = Abc_NtkAigToGia( pNtk, 1 );
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, 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, 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, 50000, 0, fVerbose ) );
assert( !Gia_ManFindExact( pTruth, 4, 1, 8, pArrTimeProfile, 50000, 0, fVerbose ) );
Gia_ManStop( pGia );
Gia_ManStop( pGia2 );
Gia_ManStop( pGia3 );
Gia_ManStop( pGia4 );
}
void Abc_ExactTest( int fVerbose )
{
Abc_ExactTestSingleOutput( fVerbose );
Abc_ExactTestSingleOutputAIG( fVerbose );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [APIs for integraging with the mapper.]
***********************************************************************/
// may need to have a static pointer to the SAT-based synthesis engine and/or loaded library
// this procedure should return 1, if the engine/library are available, and 0 otherwise
int Abc_ExactIsRunning()
{
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 8;
}
// start exact store manager
void Abc_ExactStart( int nBTLimit, int fMakeAIG, int fVerbose, int fVeryVerbose, const char * pFilename )
{
if ( !s_pSesStore )
{
s_pSesStore = Ses_StoreAlloc( nBTLimit, fMakeAIG, fVerbose );
s_pSesStore->fVeryVerbose = fVeryVerbose;
if ( pFilename )
{
Ses_StoreRead( s_pSesStore, pFilename, 1, 0, 0, 0 );
s_pSesStore->szDBName = ABC_CALLOC( char, strlen( pFilename ) + 1 );
strcpy( s_pSesStore->szDBName, pFilename );
}
if ( s_pSesStore->fVeryVerbose )
{
s_pSesStore->pDebugEntries = fopen( "bms.debug", "w" );
}
}
else
printf( "BMS manager already started\n" );
}
// stop exact store manager
void Abc_ExactStop( const char * pFilename )
{
if ( s_pSesStore )
{
if ( pFilename )
Ses_StoreWrite( s_pSesStore, pFilename, 1, 0, 0, 0 );
if ( s_pSesStore->pDebugEntries )
fclose( s_pSesStore->pDebugEntries );
Ses_StoreClean( s_pSesStore );
}
else
printf( "BMS manager has not been started\n" );
}
// show statistics about store manager
void Abc_ExactStats()
{
int i;
if ( !s_pSesStore )
{
printf( "BMS manager has not been started\n" );
return;
}
printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
printf( " 0 1 2 3 4 5 6 7 8 total\n" );
printf( "-------------------------------------------------------------------------------------------------------------------------------\n" );
printf( "number of considered cuts :" );
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, nMaxArrival, nDelta, l;
Ses_Man_t * pSes = NULL;
char * pSol = NULL, * pSol2 = NULL, * p;
int pNormalArrTime[8];
int Delay = ABC_INFINITY, nMaxDepth, fResLimit;
abctime timeStart = Abc_Clock(), timeStartExact;
/* some checks */
if ( nVars < 0 || nVars > 8 )
{
printf( "invalid truth table size %d\n", nVars );
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];
}
for ( l = 0; l < nVars; ++l )
pNormalArrTime[l] = pArrTimeProfile[l];
nDelta = Abc_NormalizeArrivalTimes( pNormalArrTime, nVars, &nMaxArrival );
*Cost = ABC_INFINITY;
if ( Ses_StoreGetEntry( s_pSesStore, pTruth, nVars, pNormalArrTime, &pSol ) )
{
s_pSesStore->nCacheHits++;
s_pSesStore->pCacheHits[nVars]++;
}
else
{
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, pNormalArrTime[i] );
nMaxDepth += nVars + 1;
if ( AigLevel != -1 )
nMaxDepth = Abc_MinInt( AigLevel - nDelta, nMaxDepth + nVars + 1 );
timeStartExact = Abc_Clock();
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( " %d", pSes->nMaxDepth );
fflush( stdout );
}
if ( ( pSol2 = Ses_ManFindMinimumSize( pSes ) ) != NULL )
{
if ( s_pSesStore->fVeryVerbose )
{
if ( pSes->nMaxDepth >= 10 ) printf( "\b" );
printf( "\b" ANSI_COLOR_GREEN "%d" ANSI_COLOR_RESET, pSes->nMaxDepth );
}
if ( pSol )
ABC_FREE( pSol );
pSol = pSol2;
pSes->nMaxDepth--;
}
else
{
if ( s_pSesStore->fVeryVerbose )
{
if ( pSes->nMaxDepth >= 10 ) printf( "\b" );
printf( "\b%s%d" ANSI_COLOR_RESET, pSes->fHitResLimit ? ANSI_COLOR_RED : ANSI_COLOR_YELLOW, pSes->nMaxDepth );
}
break;
}
}
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 );
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, pNormalArrTime, pSol, fResLimit );
}
if ( pSol )
{
*Cost = pSol[ABC_EXACT_SOL_NGATES];
p = pSol + 3 + 4 * pSol[ABC_EXACT_SOL_NGATES] + 1;
Delay = *p++;
for ( l = 0; l < nVars; ++l )
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 );
//}
s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
return Delay2;
}
else
{
assert( *Cost == ABC_INFINITY );
s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
return ABC_INFINITY;
}
}
// this procedure returns a new node whose output in terms of the given fanins
// has the smallest possible arrival time (in agreement with the above Abc_ExactDelayCost)
Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins, Abc_Ntk_t * pNtk )
{
char * pSol = NULL;
int i, j, 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]);
}
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 );
pGates = Vec_PtrAlloc( nVars + pSol[ABC_EXACT_SOL_NGATES] );
pGateTruth[3] = '0';
pGateTruth[4] = '\0';
/* primary inputs */
for ( i = 0; i < nVars; ++i )
{
assert( pFanins[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;
/* invert truth table if we are last gate and inverted */
if ( i + 1 == pSol[ABC_EXACT_SOL_NGATES] && Abc_LitIsCompl( *( p + 2 ) ) )
for ( j = 0; j < 4; ++j )
pGateTruth[j] = ( pGateTruth[j] == '0' ) ? '1' : '0';
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 );
Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
Abc_ObjAddFanin( pObj, (Abc_Obj_t *)Vec_PtrEntry( pGates, *p++ ) );
}
/* output */
pObj = (Abc_Obj_t *)Vec_PtrEntry( pGates, nVars + Abc_Lit2Var( *p ) );
Vec_PtrFree( pGates );
s_pSesStore->timeTotal += ( Abc_Clock() - timeStart );
return pObj;
}
void Abc_ExactStoreTest( int fVerbose )
{
int i;
word pTruth[4] = {0xcafe, 0, 0, 0};
int pArrTimeProfile[4] = {6, 2, 8, 5};
Abc_Ntk_t * pNtk;
Abc_Obj_t * pFanins[4];
Vec_Ptr_t * vNames;
char pPerm[4];
int Cost;
pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
pNtk->pName = Extra_UtilStrsav( "exact" );
vNames = Abc_NodeGetFakeNames( 4u );
/* primary inputs */
Vec_PtrPush( pNtk->vObjs, NULL );
for ( i = 0; i < 4; ++i )
{
pFanins[i] = Abc_NtkCreatePi( pNtk );
Abc_ObjAssignName( pFanins[i], (char*)Vec_PtrEntry( vNames, i ), NULL );
}
Abc_NodeFreeNames( vNames );
Abc_ExactStart( 10000, 1, fVerbose, 0, NULL );
assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );
assert( Abc_ExactDelayCost( pTruth, 4, pArrTimeProfile, pPerm, &Cost, 12 ) == 1 );
assert( Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );
(*pArrTimeProfile)++;
assert( !Abc_ExactBuildNode( pTruth, 4, pArrTimeProfile, pFanins, pNtk ) );
(*pArrTimeProfile)--;
Abc_ExactStop( NULL );
Abc_NtkDelete( pNtk );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink