diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/giaAbsIter.c | 149 | ||||
-rw-r--r-- | src/aig/gia/giaEquiv.c | 2 | ||||
-rw-r--r-- | src/aig/gia/module.make | 1 | ||||
-rw-r--r-- | src/aig/saig/saig.h | 2 | ||||
-rw-r--r-- | src/aig/saig/saigAbsStart.c | 4 | ||||
-rw-r--r-- | src/aig/saig/saigBmc2.c | 48 | ||||
-rw-r--r-- | src/aig/saig/saigTempor.c | 2 | ||||
-rw-r--r-- | src/base/abci/abc.c | 93 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 4 | ||||
-rw-r--r-- | src/proof/ssw/sswRarity.c | 2 |
10 files changed, 278 insertions, 29 deletions
diff --git a/src/aig/gia/giaAbsIter.c b/src/aig/gia/giaAbsIter.c new file mode 100644 index 00000000..4600530b --- /dev/null +++ b/src/aig/gia/giaAbsIter.c @@ -0,0 +1,149 @@ +/**CFile**************************************************************** + + FileName [giaIter.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Iterative improvement of abstraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaIter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "giaAig.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Gia_ObjIsInGla( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vGateClasses, Gia_ObjId(p, pObj)); } +static inline void Gia_ObjAddToGla( Gia_Man_t * p, Gia_Obj_t * pObj ) { Vec_IntWriteEntry(p->vGateClasses, Gia_ObjId(p, pObj), 1); } +static inline void Gia_ObjRemFromGla( Gia_Man_t * p, Gia_Obj_t * pObj ) { Vec_IntWriteEntry(p->vGateClasses, Gia_ObjId(p, pObj), 0); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_IterTryImprove( Gia_Man_t * p, int nTimeOut, int iFrame0 ) +{ + extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ); + Gia_Man_t * pAbs = Gia_ManDupAbsGates( p, p->vGateClasses ); + Aig_Man_t * pAig = Gia_ManToAigSimple( pAbs ); + int nStart = 0; + int nFrames = iFrame0 ? iFrame0 + 1 : 10000000; + int nNodeDelta = 2000; + int nBTLimit = 0; + int nBTLimitAll = 0; + int fVerbose = 0; + int RetValue, iFrame; + RetValue = Saig_BmcPerform( pAig, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, &iFrame, 1 ); + assert( RetValue == 0 || RetValue == -1 ); + Aig_ManStop( pAig ); + Gia_ManStop( pAbs ); + return iFrame; +} +Gia_Man_t * Gia_IterImprove( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose ) +{ + Gia_Obj_t * pObj; + int i, iFrame0, iFrame; + int nTotal = 0, nRemoved = 0; + Vec_Int_t * vGScopy; + clock_t clk, clkTotal = clock(); + assert( Gia_ManPoNum(p) == 1 ); + assert( p->vGateClasses != NULL ); + vGScopy = Vec_IntDup( p->vGateClasses ); + if ( nFrameMax == 0 ) + iFrame0 = Gia_IterTryImprove( p, 0, 0 ); + else + iFrame0 = nFrameMax - 1; + while ( 1 ) + { + int fChanges = 0; + Gia_ManForEachObj1( p, pObj, i ) + { + if ( pObj->fMark0 ) + continue; + if ( !Gia_ObjIsInGla(p, pObj) ) + continue; + if ( pObj == Gia_ObjFanin0( Gia_ManPo(p, 0) ) ) + continue; + if ( Gia_ObjIsAnd(pObj) ) + { + if ( Gia_ObjIsInGla(p, Gia_ObjFanin0(pObj)) && Gia_ObjIsInGla(p, Gia_ObjFanin1(pObj)) ) + continue; + } + if ( Gia_ObjIsRo(p, pObj) ) + { + if ( Gia_ObjIsInGla(p, Gia_ObjRoToRi(p, pObj)) ) + continue; + } + clk = clock(); + printf( "%5d : ", nTotal ); + printf( "Obj =%7d ", i ); + Gia_ObjRemFromGla( p, pObj ); + iFrame = Gia_IterTryImprove( p, nTimeOut, iFrame0 ); + if ( nFrameMax ) + assert( iFrame <= nFrameMax ); + else + assert( iFrame <= iFrame0 ); + printf( "Frame =%6d ", iFrame ); + if ( iFrame < iFrame0 ) + { + pObj->fMark0 = 1; + Gia_ObjAddToGla( p, pObj ); + printf( " " ); + } + else + { + fChanges = 1; + nRemoved++; + printf( "Removing " ); + Vec_IntWriteEntry( vGScopy, Gia_ObjId(p, pObj), 0 ); + } + Abc_PrintTime( 1, "Time", clock() - clk ); + nTotal++; + // update the classes + Vec_IntFreeP( &p->vGateClasses ); + p->vGateClasses = Vec_IntDup(vGScopy); + } + if ( !fChanges ) + break; + } + Gia_ManCleanMark0(p); + Vec_IntFree( vGScopy ); + printf( "Tried = %d. ", nTotal ); + printf( "Removed = %d. (%.2f %%) ", nRemoved, 100.0 * nRemoved / Vec_IntCountPositive(p->vGateClasses) ); + Abc_PrintTime( 1, "Time", clock() - clkTotal ); + return NULL; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index bf1e4c06..62afe26c 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -1723,7 +1723,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f pTemp = Gia_ManToAig( pSrm, 0 ); // Aig_ManPrintStats( pTemp ); Gia_ManStop( pSrm ); - Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVerbose, 0, NULL ); + Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVerbose, 0, NULL, 0 ); pCex = pTemp->pSeqModel; pTemp->pSeqModel = NULL; Aig_ManStop( pTemp ); if ( pCex == NULL ) diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 83399eb8..cac2986e 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -2,6 +2,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaAbs.c \ src/aig/gia/giaAbsGla.c \ src/aig/gia/giaAbsGla2.c \ + src/aig/gia/giaAbsIter.c \ src/aig/gia/giaAbsRef.c \ src/aig/gia/giaAbsRef2.c \ src/aig/gia/giaAbsVta.c \ diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index ec33b3eb..e7cdea90 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -147,7 +147,7 @@ extern int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlop extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ); /*=== saigBmc.c ==========================================================*/ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); -extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames ); +extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ); /*=== saigBmc3.c ==========================================================*/ extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p ); extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ); diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c index 51033dee..90efef26 100644 --- a/src/aig/saig/saigAbsStart.c +++ b/src/aig/saig/saigAbsStart.c @@ -72,7 +72,7 @@ int Saig_ManCexFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs ) ***********************************************************************/ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, int * piRetValue, int * pnFrames ) { - extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames ); + extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ); Vec_Int_t * vFlopsNew; int i, Entry, RetValue; *piRetValue = -1; @@ -119,7 +119,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo } else { - Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames ); + Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames, 0 ); } if ( pAbs->pSeqModel == NULL ) return NULL; diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index a1dee6e4..f70a0015 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -754,7 +754,7 @@ void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p ) SeeAlso [] ***********************************************************************/ -int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames ) +int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ) { Saig_Bmc_t * p; Aig_Man_t * pNew; @@ -817,7 +817,8 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax // check the timeout if ( nTimeOut && clock() > nTimeToStop ) { - printf( "Reached timeout (%d seconds).\n", nTimeOut ); + if ( !fSilent ) + printf( "Reached timeout (%d seconds).\n", nTimeOut ); if ( piFrames ) *piFrames = p->iFrameLast-1; Saig_BmcManStop( p ); @@ -827,15 +828,17 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax if ( RetValue == l_True ) { assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved ); - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", - p->iOutputFail, p->iFrameFail ); + if ( !fSilent ) + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", + p->iOutputFail, p->iFrameFail ); Status = 0; if ( piFrames ) *piFrames = p->iFrameFail; } else // if ( RetValue == l_False || RetValue == l_Undef ) { - printf( "No output was asserted in %d frames. ", Abc_MaxInt(p->iFramePrev-1, 0) ); + if ( !fSilent ) + printf( "No output was asserted in %d frames. ", Abc_MaxInt(p->iFramePrev-1, 0) ); if ( piFrames ) { if ( p->iOutputLast > 0 ) @@ -844,24 +847,27 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax *piFrames = p->iFramePrev; } } - if ( fVerbOverwrite ) + if ( !fSilent ) { - ABC_PRTr( "Time", clock() - clk ); - } - else - { - ABC_PRT( "Time", clock() - clk ); - } - if ( RetValue != l_True ) - { - if ( p->iFrameLast >= p->nFramesMax ) - printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax ); - else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll ) - printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll ); - else if ( nTimeOut && clock() > nTimeToStop ) - printf( "Reached timeout (%d seconds).\n", nTimeOut ); + if ( fVerbOverwrite ) + { + ABC_PRTr( "Time", clock() - clk ); + } else - printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne ); + { + ABC_PRT( "Time", clock() - clk ); + } + if ( RetValue != l_True ) + { + if ( p->iFrameLast >= p->nFramesMax ) + printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax ); + else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll ) + printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll ); + else if ( nTimeOut && clock() > nTimeToStop ) + printf( "Reached timeout (%d seconds).\n", nTimeOut ); + else + printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne ); + } } Saig_BmcManStop( p ); fflush( stdout ); diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c index c8c33680..040df1f9 100644 --- a/src/aig/saig/saigTempor.c +++ b/src/aig/saig/saigTempor.c @@ -222,7 +222,7 @@ Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nCon // run BMC2 if ( fUseBmc ) { - RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished ); + RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished, 0 ); if ( RetValue == 0 ) { Vec_IntFreeP( &vTransSigs ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ddce0cf5..874a1057 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -358,6 +358,7 @@ static int Abc_CommandAbc9AbsRefine ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9GlaDerive ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GlaRefine ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GlaPurify ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9GlaShrink ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9GlaCba ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Gla ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -817,6 +818,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&gla_derive", Abc_CommandAbc9GlaDerive, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gla_refine", Abc_CommandAbc9GlaRefine, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gla_purify", Abc_CommandAbc9GlaPurify, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&gla_shrink", Abc_CommandAbc9GlaShrink, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&gla_cba", Abc_CommandAbc9GlaCba, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&gla_pba", Abc_CommandAbc9GlaPba, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gla", Abc_CommandAbc9Gla, 0 ); @@ -27941,6 +27943,97 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9GlaShrink( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_IterImprove( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose ); + int fUsePdr = 0; + int fUseSat = 1; + int fUseBdd = 0; + int nFrameMax = 0; + int nTimeOut = 0; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FTpsbvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrameMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrameMax < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + nTimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nTimeOut < 0 ) + goto usage; + break; + case 'p': + fUsePdr ^= 1; + break; + case 's': + fUseSat ^= 1; + break; + case 'b': + fUseBdd ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9GlaShrink(): There is no AIG.\n" ); + return 1; + } + if ( pAbc->pGia->vGateClasses == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9GlaShrink(): There is no gate-level abstraction.\n" ); + return 0; + } + Gia_IterImprove( pAbc->pGia, nFrameMax, nTimeOut, fUsePdr, fUseSat, fUseBdd, fVerbose ); + return 0; + +usage: + Abc_Print( -2, "usage: &gla_shrink [-FT num] [-psbvh]\n" ); + Abc_Print( -2, "\t shrinks the abstraction by removing redundant objects\n" ); + Abc_Print( -2, "\t-F num : the maximum timeframe to check to [default = %d]\n", nFrameMax ); + Abc_Print( -2, "\t-T num : the timeout per call, in seconds [default = %d]\n", nTimeOut ); + Abc_Print( -2, "\t-p : toggle using PDR for checking [default = %s]\n", fUsePdr? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle using BMC for checking [default = %s]\n", fUseSat? "yes": "no" ); + Abc_Print( -2, "\t-b : toggle using BDDs for checking [default = %s]\n", fUseBdd? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv ) { Saig_ParBmc_t Pars, * pPars = &Pars; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index bea8e6b9..97385b91 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1905,7 +1905,7 @@ ABC_PRT( "Time", clock() - clk ); } else { - RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames ); + RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames, 0 ); ABC_FREE( pNtk->pModel ); ABC_FREE( pNtk->pSeqModel ); pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; @@ -2414,7 +2414,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, i if ( pSecPar->fTryBmc ) { - RetValue = Saig_BmcPerform( pMan, 0, nBmcFramesMax, 2000, 0, nBmcConfMax, 0, pSecPar->fVerbose, 0, &iFrame ); + RetValue = Saig_BmcPerform( pMan, 0, nBmcFramesMax, 2000, 0, nBmcConfMax, 0, pSecPar->fVerbose, 0, &iFrame, 0 ); if ( RetValue == 0 ) { Abc_Print( 1, "Networks are not equivalent.\n" ); diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index 7d12b724..d13e82ee 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -927,7 +927,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in if ( fTryBmc ) { Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits ); - Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail ); + Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0 ); // if ( pNewAig->pSeqModel != NULL ) // printf( "BMC has found a counter-example in frame %d.\n", iFrameFail ); Aig_ManStop( pNewAig ); |