diff options
| author | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-08-28 13:44:59 +0200 |
|---|---|---|
| committer | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-08-28 13:44:59 +0200 |
| commit | 2d71abd581e5c1572bdc83a15f0b5dbdd1cc0e28 (patch) | |
| tree | 8fe75e268b75d4a91040a910cf6b63c06e29d243 | |
| parent | 610fcb27121bd00ecca74faacb2f53b4f088f201 (diff) | |
| download | abc-2d71abd581e5c1572bdc83a15f0b5dbdd1cc0e28.tar.gz abc-2d71abd581e5c1572bdc83a15f0b5dbdd1cc0e28.tar.bz2 abc-2d71abd581e5c1572bdc83a15f0b5dbdd1cc0e28.zip | |
Symmetric variables in BMS.
| -rw-r--r-- | src/base/abci/abcExact.c | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 3f65af9e..f328d9b3 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -1204,12 +1204,13 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes ) } /* EXTRA clauses: symmetric variables */ - if ( pSes->nMaxDepth == -1 && pSes->nSpecFunc == 1 ) /* only check if there is one output function */ + if ( /*pSes->nMaxDepth == -1 &&*/ pSes->nSpecFunc == 1 ) /* only check if there is one output function */ for ( q = 1; q < pSes->nSpecVars; ++q ) for ( p = 0; p < q; ++p ) - if ( Extra_TruthVarsSymm( (unsigned*)( pSes->pSpec ), pSes->nSpecVars, p, q ) ) + if ( Extra_TruthVarsSymm( (unsigned*)( pSes->pSpec ), pSes->nSpecVars, p, q ) && + ( !pSes->pArrTimeProfile || ( pSes->pArrTimeProfile[p] == pSes->pArrTimeProfile[q] ) ) ) { - if ( pSes->fVeryVerbose ) + if ( pSes->fSatVerbose ) printf( "variables %d and %d are symmetric\n", p, q ); for ( i = 0; i < pSes->nGates; ++i ) for ( j = 0; j < q; ++j ) @@ -2033,6 +2034,8 @@ Abc_Ntk_t * Abc_NtkFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 0, nBTLimit, fVerbose ); pSes->nStartGates = nStartGates; + pSes->fReasonVerbose = 1; + pSes->fSatVerbose = 1; if ( fVerbose ) Ses_ManPrintFuncs( pSes ); @@ -2069,7 +2072,7 @@ Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth pSes = Ses_ManAlloc( pTruth, nVars, nFunc, nMaxDepth, pArrTimeProfile, 1, nBTLimit, fVerbose ); pSes->nStartGates = nStartGates; pSes->fVeryVerbose = 1; - pSes->fExtractVerbose = 1; + pSes->fExtractVerbose = 0; pSes->fSatVerbose = 0; pSes->fReasonVerbose = 1; if ( fVerbose ) |