diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-18 17:31:23 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-18 17:31:23 -0700 |
commit | 68e1a07fdbcf07e99934586e3727b6d7ffd6870f (patch) | |
tree | ed9a45d0fb396895b0d57c1cb3c5a3e9fd9e2aae /src | |
parent | 29a995685df6ae6b57b66a5ef9ee7a29b9dedde6 (diff) | |
download | abc-68e1a07fdbcf07e99934586e3727b6d7ffd6870f.tar.gz abc-68e1a07fdbcf07e99934586e3727b6d7ffd6870f.tar.bz2 abc-68e1a07fdbcf07e99934586e3727b6d7ffd6870f.zip |
Improvements to 'bmc3'.
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abc.c | 2 | ||||
-rw-r--r-- | src/sat/bmc/bmcBmc3.c | 169 |
2 files changed, 12 insertions, 159 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7222ad1d..1d9836b7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -21437,7 +21437,6 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) } pAbc->Status = Abc_NtkDarBmc3( pNtk, pPars, fOrDecomp ); pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame; - Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); if ( pLogFileName ) Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc3" ); vSeqModelVec = pNtk->vSeqModelVec; pNtk->vSeqModelVec = NULL; @@ -21463,6 +21462,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) vStatuses = Abc_FrameDeriveStatusArray( vSeqModelVec ); Abc_FrameReplacePoStatuses( pAbc, &vStatuses ); Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec ); + Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); return 0; usage: diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 6e3f95a5..87edbb5f 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -46,17 +46,11 @@ struct Gia_ManBmc_t_ Vec_Ptr_t * vId2Var; // SAT vars for each object clock_t * pTime4Outs; // timeout per output // hash table -/* - int * pTable; - int nTable; -*/ - Vec_Int_t * vData; - Hsh_IntMan_t * vHash; - Vec_Int_t * vId2Lit; - int nHashHit; - int nHashMiss; - int nHashOver; - + Vec_Int_t * vData; // storage for cuts + Hsh_IntMan_t * vHash; // hash table + Vec_Int_t * vId2Lit; // mapping cuts into literals + int nHashHit; // hash table hits + int nHashMiss; // hash table misses int nBufNum; // the number of simple nodes int nDupNum; // the number of simple nodes int nUniProps; // propagating learned clause values @@ -742,8 +736,6 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne ) // terminary simulation p->nWordNum = Abc_BitWordNum( 2 * Aig_ManObjNumMax(pAig) ); // hash table -// p->nTable = Abc_PrimeCudd( 10000000 ); -// p->pTable = ABC_CALLOC( int, 6 * p->nTable ); // 2.4 MB p->vData = Vec_IntAlloc( 5 * 10000 ); p->vHash = Hsh_IntManStart( p->vData, 5, 10000 ); p->vId2Lit = Vec_IntAlloc( 10000 ); @@ -776,8 +768,8 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) printf( "LStart(P) = %d LDelta(Q) = %d LRatio(R) = %d ReduceDB = %d Vars = %d Used = %d (%.2f %%)\n", p->pSat->nLearntStart, p->pSat->nLearntDelta, p->pSat->nLearntRatio, p->pSat->nDBreduces, p->pSat->size, nUsedVars, 100.0*nUsedVars/p->pSat->size ); - printf( "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. Hash overs = %d. UniProps = %d.\n", - p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nHashOver, p->nUniProps ); + printf( "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. UniProps = %d.\n", + p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nUniProps ); } // Aig_ManCleanMarkA( p->pAig ); if ( p->vCexes ) @@ -795,11 +787,9 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) Vec_PtrFreeFree( p->vTerInfo ); sat_solver_delete( p->pSat ); ABC_FREE( p->pTime4Outs ); -// ABC_FREE( p->pTable ); Vec_IntFree( p->vData ); Hsh_IntManStop( p->vHash ); Vec_IntFree( p->vId2Lit ); - ABC_FREE( p->pSopSizes ); ABC_FREE( p->pSops[1] ); ABC_FREE( p->pSops ); @@ -945,75 +935,6 @@ static inline int Saig_ManBmcReduceTruth( int uTruth, int Lits[] ) return uTruth; } -/* -void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover ) -{ - int Lits[4], Cube, iCube, i, b; - Vec_IntClear( vCover ); - for ( i = 0; i < nCubes; i++ ) - { - Cube = pSop[i]; - for ( b = 0; b < 4; b++ ) - { - if ( Cube % 3 == 0 ) - Lits[b] = 1; - else if ( Cube % 3 == 1 ) - Lits[b] = 2; - else - Lits[b] = 0; - Cube = Cube / 3; - } - iCube = 0; - for ( b = 0; b < 4; b++ ) - iCube = (iCube << 2) | Lits[b]; - Vec_IntPush( vCover, iCube ); - } -} - - Vec_IntForEachEntry( vCover, Cube, k ) - { - *pClas++ = pLits; - *pLits++ = 2 * OutVar; - pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits ); - } - - -int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int * pLiterals ) -{ - int nLits = nVars, b; - for ( b = 0; b < nVars; b++ ) - { - if ( (Cube & 3) == 1 ) // value 0 --> write positive literal - *pLiterals++ = 2 * pVars[b]; - else if ( (Cube & 3) == 2 ) // value 1 --> write negative literal - *pLiterals++ = 2 * pVars[b] + 1; - else - nLits--; - Cube >>= 2; - } - return nLits; -} - - iTruth = pData[0] & 0xffff; - for ( k = 0; k < pSopSizes[iTruth]; k++ ) - { - int Lit = pSops[iTruth][k]; - for ( b = 3; b >= 0; b-- ) - { - if ( Lit % 3 == 0 ) - Vals[b] = '0'; - else if ( Lit % 3 == 1 ) - Vals[b] = '1'; - else - Vals[b] = '-'; - Lit = Lit / 3; - } - for ( b = 0; b < iFan; b++ ) - fprintf( pFile, "%c", Vals[b] ); - fprintf( pFile, " 1\n" ); - } -*/ - /**Function************************************************************* Synopsis [Derives CNF for one node.] @@ -1060,46 +981,6 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits } } - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -#if 0 -static inline unsigned Saig_ManBmcHashKey( int * pArray ) -{ - static int s_Primes[5] = { 12582917, 25165843, 50331653, 100663319, 201326611 }; - unsigned i, Key = 0; - for ( i = 0; i < 5; i++ ) - Key += pArray[i] * s_Primes[i]; - return Key; -} -static inline int * Saig_ManBmcLookup( Gia_ManBmc_t * p, int * pArray ) -{ - int * pTable = p->pTable + 6 * (Saig_ManBmcHashKey(pArray) % p->nTable); - if ( memcmp( pTable, pArray, 20 ) ) - { - if ( pTable[0] == 0 ) - p->nHashMiss++; - else - p->nHashOver++; - memcpy( pTable, pArray, 20 ); - pTable[5] = 0; - } - else - p->nHashHit++; - assert( pTable + 5 < pTable + 6 * p->nTable ); - return pTable + 5; -} -#endif - /**Function************************************************************* Synopsis [Derives CNF for one node.] @@ -1160,35 +1041,8 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame ) else { int iEntry, iRes; - - int fCompl = 0; - if ( uTruth & 1 ) - { - fCompl = 1; - uTruth = 0xffff & ~uTruth; - } - assert( !(uTruth == 0xAAAA || (0xffff & ~uTruth) == 0xAAAA || - uTruth == 0xCCCC || (0xffff & ~uTruth) == 0xCCCC || - uTruth == 0xF0F0 || (0xffff & ~uTruth) == 0xF0F0 || - uTruth == 0xFF00 || (0xffff & ~uTruth) == 0xFF00) ); - - Lits[4] = uTruth; -#if 0 - pLookup = Saig_ManBmcLookup( p, Lits ); - if ( *pLookup == 0 ) - { - *pLookup = toLit( p->nSatVars++ ); - Saig_ManBmcAddClauses( p, uTruth, Lits, *pLookup ); -/* - if ( (Lits[0] > 1 && (Lits[0] == Lits[1] || Lits[0] == Lits[2] || Lits[0] == Lits[3])) || - (Lits[1] > 1 && (Lits[1] == Lits[2] || Lits[1] == Lits[2])) || - (Lits[2] > 1 && (Lits[2] == Lits[3])) ) - p->nDupNum++; -*/ - } - iLit = *pLookup; -#endif - + int fCompl = (uTruth & 1); + Lits[4] = (uTruth & 1) ? 0xffff & ~uTruth : uTruth; iEntry = Vec_IntSize(p->vData) / 5; assert( iEntry * 5 == Vec_IntSize(p->vData) ); for ( i = 0; i < 5; i++ ) @@ -1197,18 +1051,17 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame ) if ( iRes == iEntry ) { iLit = toLit( p->nSatVars++ ); - Saig_ManBmcAddClauses( p, uTruth, Lits, iLit ); + Saig_ManBmcAddClauses( p, Lits[4], Lits, iLit ); assert( iEntry == Vec_IntSize(p->vId2Lit) ); Vec_IntPush( p->vId2Lit, iLit ); p->nHashMiss++; } else { - Vec_IntShrink( p->vData, Vec_IntSize(p->vData) - 5 ); iLit = Vec_IntEntry( p->vId2Lit, iRes ); + Vec_IntShrink( p->vData, Vec_IntSize(p->vData) - 5 ); p->nHashHit++; } - iLit = Abc_LitNotCond( iLit, fCompl ); } return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit ); |