diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
| -rw-r--r-- | src/aig/gia/giaUtil.c | 19 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 10 | ||||
| -rw-r--r-- | src/misc/util/utilCex.c | 11 | ||||
| -rw-r--r-- | src/misc/util/utilCex.h | 1 | ||||
| -rw-r--r-- | src/sat/bmc/module.make | 3 |
7 files changed, 47 insertions, 2 deletions
@@ -1413,6 +1413,10 @@ SOURCE=.\src\sat\bmc\bmcCexMin1.c SOURCE=.\src\sat\bmc\bmcCexMin2.c # End Source File +# Begin Source File + +SOURCE=.\src\sat\bmc\bmcCexTools.c +# End Source File # End Group # End Group # Begin Group "opt" diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 9d361fe8..5a87bd7a 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -928,6 +928,7 @@ extern void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart extern char * Gia_TimeStamp(); extern char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix ); extern void Gia_ManIncrementTravId( Gia_Man_t * p ); +extern void Gia_ManCleanMark01( Gia_Man_t * p ); extern void Gia_ManSetMark0( Gia_Man_t * p ); extern void Gia_ManCleanMark0( Gia_Man_t * p ); extern void Gia_ManCheckMark0( Gia_Man_t * p ); diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index dafd3641..a7f594e4 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -168,6 +168,25 @@ void Gia_ManIncrementTravId( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ +void Gia_ManCleanMark01( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i; + Gia_ManForEachObj( p, pObj, i ) + pObj->fMark0 = pObj->fMark1 = 0; +} + +/**Function************************************************************* + + Synopsis [Sets phases of the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Gia_ManSetMark0( Gia_Man_t * p ) { Gia_Obj_t * pObj; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index de37c441..7c10aa64 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30136,6 +30136,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern void Gia_VtaTest( Gia_Man_t * p, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose ); // extern void Gia_IsoTest( Gia_Man_t * p, int fVerbose ); extern void Ga2_ManComputeTest( Gia_Man_t * p ); + extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex ); + Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) @@ -30159,6 +30161,11 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" ); return 1; } + if ( pAbc->pCex == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Test(): There is no CEX.\n" ); + return 1; + } // Gia_ManFrontTest( pAbc->pGia ); // Gia_ManReduceConst( pAbc->pGia, 1 ); // Sat_ManTest( pAbc->pGia, Gia_ManCo(pAbc->pGia, 0), 0 ); @@ -30174,7 +30181,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Gia_ManSuppSizeTest( pAbc->pGia ); // Gia_VtaTest( pAbc->pGia, 10, 100000, 0, 0, 1 ); // Gia_IsoTest( pAbc->pGia, fVerbose ); - Ga2_ManComputeTest( pAbc->pGia ); +// Ga2_ManComputeTest( pAbc->pGia ); + Bmc_CexTest( pAbc->pGia, pAbc->pCex ); return 0; usage: Abc_Print( -2, "usage: &test [-svh]\n" ); diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index 01afd489..1bdf1276 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -59,6 +59,17 @@ Abc_Cex_t * Abc_CexAlloc( int nRegs, int nRealPis, int nFrames ) pCex->nBits = nRegs + nRealPis * nFrames; return pCex; } +Abc_Cex_t * Abc_CexAllocFull( int nRegs, int nRealPis, int nFrames ) +{ + Abc_Cex_t * pCex; + int nWords = Abc_BitWordNum( nRegs + nRealPis * nFrames ); + pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); + memset( pCex, 0xFF, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords ); + pCex->nRegs = nRegs; + pCex->nPis = nRealPis; + pCex->nBits = nRegs + nRealPis * nFrames; + return pCex; +} /**Function************************************************************* diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h index 1fd06f96..646a2592 100644 --- a/src/misc/util/utilCex.h +++ b/src/misc/util/utilCex.h @@ -57,6 +57,7 @@ struct Abc_Cex_t_ /*=== utilCex.c ===========================================================*/ extern Abc_Cex_t * Abc_CexAlloc( int nRegs, int nTruePis, int nFrames ); +extern Abc_Cex_t * Abc_CexAllocFull( int nRegs, int nTruePis, int nFrames ); extern Abc_Cex_t * Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int iFrameOut ); 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 ); diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make index 071834d8..41747be7 100644 --- a/src/sat/bmc/module.make +++ b/src/sat/bmc/module.make @@ -4,4 +4,5 @@ SRC += src/sat/bmc/bmc.c \ src/sat/bmc/bmcBmc3.c \ src/sat/bmc/bmcCexCut.c \ src/sat/bmc/bmcCexMin1.c \ - src/sat/bmc/bmcCexMin2.c + src/sat/bmc/bmcCexMin2.c \ + src/sat/bmc/bmcCexTools.c |