diff options
Diffstat (limited to 'src/misc/util')
| -rw-r--r-- | src/misc/util/utilCex.c | 58 | ||||
| -rw-r--r-- | src/misc/util/utilCex.h | 1 |
2 files changed, 59 insertions, 0 deletions
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index 80d8e141..16dbb076 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -172,6 +172,64 @@ Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int i /**Function************************************************************* + Synopsis [Derives CEX from comb model.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int iFrEnd ) +{ + Abc_Cex_t * pNew; + int nFramesGain; + int i, f, iBit; + + if ( iFrBeg < 0 ) + { printf( "Starting frame is less than 0.\n" ); return NULL; } + if ( iFrEnd < 0 ) + { printf( "Stopping frame is less than 0.\n" ); return NULL; } + if ( iFrBeg > pCex->iFrame ) + { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; } + if ( iFrEnd > pCex->iFrame ) + { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; } + if ( iFrBeg >= iFrEnd ) + { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; } + assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame ); + assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame ); + assert( iFrBeg < iFrEnd ); + + assert( pCex->nPis == pPart->nPis ); + assert( iFrEnd - iFrBeg > pPart->iFrame ); + + nFramesGain = (iFrEnd - iFrBeg) - pPart->iFrame; + pNew = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 - nFramesGain ); + pNew->iPo = pCex->iPo; + pNew->iFrame = pCex->iFrame - nFramesGain; + + for ( iBit = 0; iBit < pCex->nRegs; iBit++ ) + if ( Abc_InfoHasBit(pCex->pData, iBit) ) + Abc_InfoSetBit( pNew->pData, iBit++ ); + for ( f = 0; f < iFrBeg; f++ ) + for ( i = 0; i < pCex->nPis; i++ ) + if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) ) + Abc_InfoSetBit( pNew->pData, iBit++ ); + for ( f = 0; f < pPart->iFrame; f++ ) + for ( i = 0; i < pCex->nPis; i++ ) + if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) ) + Abc_InfoSetBit( pNew->pData, iBit++ ); + for ( f = iFrEnd; f <= pCex->iFrame; f++ ) + for ( i = 0; i < pCex->nPis; i++ ) + if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) ) + Abc_InfoSetBit( pNew->pData, iBit++ ); + assert( iBit == pNew->nBits ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Prints out the counter-example.] Description [] diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h index b45cd27b..1fd06f96 100644 --- a/src/misc/util/utilCex.h +++ b/src/misc/util/utilCex.h @@ -61,6 +61,7 @@ extern Abc_Cex_t * Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int extern Abc_Cex_t * Abc_CexCreate( int nRegs, int nTruePis, int * pArray, int iFrame, int iPo, int fSkipRegs ); extern Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew ); extern Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int iPo ); +extern Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int iFrEnd ); extern void Abc_CexPrintStats( Abc_Cex_t * p ); extern void Abc_CexPrint( Abc_Cex_t * p ); extern void Abc_CexFreeP( Abc_Cex_t ** p ); |