summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/proof/pdr/pdr.h1
-rw-r--r--src/proof/pdr/pdrCore.c18
-rw-r--r--src/proof/ssw/ssw.h2
-rw-r--r--src/proof/ssw/sswRarity.c166
-rw-r--r--src/sat/bmc/bmc.h1
-rw-r--r--src/sat/bmc/bmcBmc3.c21
6 files changed, 122 insertions, 87 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index 6e157aad..cfb13356 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -62,6 +62,7 @@ struct Pdr_Par_t_
int iFrame; // explored up to this frame
int RunId; // PDR id in this run
int(*pFuncStop)(int); // callback to terminate
+ int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
clock_t timeLastSolved; // the time when the last output was solved
};
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index eb21edfc..3df1d7de 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -591,6 +591,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 );
+ if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
+ {
+ if ( p->pPars->fVerbose )
+ Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ if ( !p->pPars->fSilent )
+ Abc_Print( 1, "Quitting due to callback on fail.\n" );
+ p->pPars->iFrame = k;
+ return -1;
+ }
if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
return 0; // all SAT
p->pPars->timeLastSolved = clock();
@@ -659,6 +668,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 );
+ if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
+ {
+ if ( p->pPars->fVerbose )
+ Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+ if ( !p->pPars->fSilent )
+ Abc_Print( 1, "Quitting due to callback on fail.\n" );
+ p->pPars->iFrame = k;
+ return -1;
+ }
if ( !p->pPars->fNotVerbose )
Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
nOutDigits, p->iOutCur, k, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h
index d81bae20..a05409ee 100644
--- a/src/proof/ssw/ssw.h
+++ b/src/proof/ssw/ssw.h
@@ -105,7 +105,9 @@ struct Ssw_RarPars_t_
int fMiter;
int fUseCex;
int fLatchOnly;
+ int nSolved;
Abc_Cex_t * pCex;
+ int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
};
typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index cad7b9ed..013ee130 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -34,10 +34,7 @@ typedef struct Ssw_RarMan_t_ Ssw_RarMan_t;
struct Ssw_RarMan_t_
{
// parameters
- int nWords; // the number of words to simulate
- int nFrames; // the number of frames to simulate
- int nBinSize; // the number of flops in one group
- int fVerbose; // the verbosiness flag
+ Ssw_RarPars_t* pPars;
int nGroups; // the number of flop groups
int nWordsReg; // the number of words in the registers
// internal data
@@ -64,27 +61,27 @@ struct Ssw_RarMan_t_
static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{
- assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
- assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
- return p->pRarity[iBin * (1 << p->nBinSize) + iPat];
+ assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize );
+ assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) );
+ return p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat];
}
static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value )
{
- assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
- assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
- p->pRarity[iBin * (1 << p->nBinSize) + iPat] = Value;
+ assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize );
+ assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) );
+ p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat] = Value;
}
static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{
- assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
- assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
- p->pRarity[iBin * (1 << p->nBinSize) + iPat]++;
+ assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize );
+ assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) );
+ p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat]++;
}
static inline int Ssw_RarBitWordNum( int nBits ) { return (nBits>>6) + ((nBits&63) > 0); }
-static inline word * Ssw_RarObjSim( Ssw_RarMan_t * p, int Id ) { assert( Id < Aig_ManObjNumMax(p->pAig) ); return p->pObjData + p->nWords * Id; }
-static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 64 * p->nWords ); return p->pPatData + p->nWordsReg * Id; }
+static inline word * Ssw_RarObjSim( Ssw_RarMan_t * p, int Id ) { assert( Id < Aig_ManObjNumMax(p->pAig) ); return p->pObjData + p->pPars->nWords * Id; }
+static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 64 * p->pPars->nWords ); return p->pPatData + p->nWordsReg * Id; }
////////////////////////////////////////////////////////////////////////
@@ -158,7 +155,7 @@ void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p )
Saig_ManForEachPi( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
- for ( w = 0; w < p->nWords; w++ )
+ for ( w = 0; w < p->pPars->nWords; w++ )
pSim[w] = Aig_ManRandom64(0);
// pSim[0] <<= 1;
// pSim[0] = (pSim[0] << 2) | 2;
@@ -186,11 +183,11 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin
int i, r, f, iBit, iPatThis;
// compute the pattern sequence
iPatThis = iPatFinal;
- vTrace = Vec_IntStartFull( iFrame / p->nFrames + 1 );
- Vec_IntWriteEntry( vTrace, iFrame / p->nFrames, iPatThis );
- for ( r = iFrame / p->nFrames - 1; r >= 0; r-- )
+ vTrace = Vec_IntStartFull( iFrame / p->pPars->nFrames + 1 );
+ Vec_IntWriteEntry( vTrace, iFrame / p->pPars->nFrames, iPatThis );
+ for ( r = iFrame / p->pPars->nFrames - 1; r >= 0; r-- )
{
- iPatThis = Vec_IntEntry( p->vPatBests, r * p->nWords + iPatThis / 64 );
+ iPatThis = Vec_IntEntry( p->vPatBests, r * p->pPars->nWords + iPatThis / 64 );
Vec_IntWriteEntry( vTrace, r, iPatThis );
}
// create counter-example
@@ -202,7 +199,7 @@ Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFin
for ( f = 0; f <= iFrame; f++ )
{
Ssw_RarManAssingRandomPis( p );
- iPatThis = Vec_IntEntry( vTrace, f / p->nFrames );
+ iPatThis = Vec_IntEntry( vTrace, f / p->pPars->nFrames );
Saig_ManForEachPi( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
@@ -365,7 +362,7 @@ void Ssw_RarTranspose( Ssw_RarMan_t * p )
Aig_Obj_t * pObj;
word M[64];
int w, r, i;
- for ( w = 0; w < p->nWords; w++ )
+ for ( w = 0; w < p->pPars->nWords; w++ )
for ( r = 0; r < p->nWordsReg; r++ )
{
// save input
@@ -389,10 +386,10 @@ void Ssw_RarTranspose( Ssw_RarMan_t * p )
Saig_ManForEachLi( p->pAig, pObj, i )
{
word * pBitData = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
- Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->nWords ); Abc_Print( 1, "\n" );
+ Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->pPars->nWords ); Abc_Print( 1, "\n" );
}
Abc_Print( 1, "\n" );
- for ( i = 0; i < p->nWords*64; i++ )
+ for ( i = 0; i < p->pPars->nWords*64; i++ )
{
word * pBitData = Ssw_RarPatSim( p, i );
Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); Abc_Print( 1, "\n" );
@@ -423,18 +420,18 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
// constant
pObj = Aig_ManConst1( p->pAig );
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
- for ( w = 0; w < p->nWords; w++ )
+ for ( w = 0; w < p->pPars->nWords; w++ )
pSim[w] = ~(word)0;
// primary inputs
Ssw_RarManAssingRandomPis( p );
// flop outputs
if ( vInit )
{
- assert( Vec_IntSize(vInit) == Saig_ManRegNum(p->pAig) * p->nWords );
+ assert( Vec_IntSize(vInit) == Saig_ManRegNum(p->pAig) * p->pPars->nWords );
Saig_ManForEachLo( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
- for ( w = 0; w < p->nWords; w++ )
+ for ( w = 0; w < p->pPars->nWords; w++ )
pSim[w] = Vec_IntEntry(vInit, w * Saig_ManRegNum(p->pAig) + i) ? ~(word)0 : (word)0;
}
}
@@ -444,7 +441,7 @@ void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
{
pSimLi = Ssw_RarObjSim( p, Aig_ObjId(pObjLi) );
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
- for ( w = 0; w < p->nWords; w++ )
+ for ( w = 0; w < p->pPars->nWords; w++ )
pSim[w] = pSimLi[w];
}
}
@@ -466,7 +463,7 @@ int Ssw_RarManPoIsConst0( void * pMan, Aig_Obj_t * pObj )
Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
int w;
- for ( w = 0; w < p->nWords; w++ )
+ for ( w = 0; w < p->pPars->nWords; w++ )
if ( pSim[w] )
return 0;
return 1;
@@ -489,7 +486,7 @@ int Ssw_RarManObjIsConst( void * pMan, Aig_Obj_t * pObj )
word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
word Flip = pObj->fPhase ? ~(word)0 : 0;
int w;
- for ( w = 0; w < p->nWords; w++ )
+ for ( w = 0; w < p->pPars->nWords; w++ )
if ( pSim[w] ^ Flip )
return 0;
return 1;
@@ -513,7 +510,7 @@ int Ssw_RarManObjsAreEqual( void * pMan, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
word * pSim1 = Ssw_RarObjSim( p, pObj1->Id );
word Flip = (pObj0->fPhase != pObj1->fPhase) ? ~(word)0 : 0;
int w;
- for ( w = 0; w < p->nWords; w++ )
+ for ( w = 0; w < p->pPars->nWords; w++ )
if ( pSim0[w] ^ pSim1[w] ^ Flip )
return 0;
return 1;
@@ -553,7 +550,7 @@ unsigned Ssw_RarManObjHashWord( void * pMan, Aig_Obj_t * pObj )
int i;
uHash = 0;
pSims = (unsigned *)Ssw_RarObjSim( p, pObj->Id );
- for ( i = 0; i < 2 * p->nWords; i++ )
+ for ( i = 0; i < 2 * p->pPars->nWords; i++ )
uHash ^= pSims[i] * s_SPrimes[i & 0x7F];
return uHash;
}
@@ -574,7 +571,7 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
word Flip = pObj->fPhase ? ~(word)0 : 0;
int w, i;
- for ( w = 0; w < p->nWords; w++ )
+ for ( w = 0; w < p->pPars->nWords; w++ )
if ( pSim[w] ^ Flip )
{
for ( i = 0; i < 64; i++ )
@@ -597,10 +594,10 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int * pnSolvedNow, int iFrame, int fNotVerbose, clock_t Time )
+int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int iFrame, clock_t Time )
{
Aig_Obj_t * pObj;
- int i, RetValue = 0;
+ int i;
p->iFailPo = -1;
p->iFailPat = -1;
Saig_ManForEachPo( p->pAig, pObj, i )
@@ -611,29 +608,33 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int * pnSolvedNow, int iFr
continue;
if ( Ssw_RarManPoIsConst0(p, pObj) )
continue;
- RetValue = 1;
p->iFailPo = i;
p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
- if ( pnSolvedNow == NULL )
+ if ( !p->pPars->fSolveAll )
break;
// remember the one solved
- (*pnSolvedNow)++;
+ p->pPars->nSolved++;
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
assert( Vec_PtrEntry(p->vCexes, i) == NULL );
Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 );
+ if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(i, NULL) )
+ return 2; // quitting due to callback
// print final report
- if ( !fNotVerbose )
+ if ( !p->pPars->fNotVerbose )
{
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs). ",
nOutDigits, p->iFailPo, iFrame,
- nOutDigits, *pnSolvedNow,
+ nOutDigits, p->pPars->nSolved,
nOutDigits, Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", Time );
}
}
- return RetValue;
+ if ( p->iFailPo >= 0 ) // found CEX
+ return 1;
+ else
+ return 0;
}
/**Function*************************************************************
@@ -684,7 +685,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
pSim1 = Ssw_RarObjSim( p, Aig_ObjFaninId1(pObj) );
Flip0 = Aig_ObjFaninC0(pObj) ? ~(word)0 : 0;
Flip1 = Aig_ObjFaninC1(pObj) ? ~(word)0 : 0;
- for ( w = 0; w < p->nWords; w++ )
+ for ( w = 0; w < p->pPars->nWords; w++ )
pSim[w] = (Flip0 ^ pSim0[w]) & (Flip1 ^ pSim1[w]);
@@ -711,7 +712,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
Flip = Aig_ObjFaninC0(pObj) ? ~(word)0 : 0;
- for ( w = 0; w < p->nWords; w++ )
+ for ( w = 0; w < p->pPars->nWords; w++ )
pSim[w] = Flip ^ pSim0[w];
}
// refine classes
@@ -747,23 +748,20 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
SeeAlso []
***********************************************************************/
-static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose )
+static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
{
Ssw_RarMan_t * p;
// if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 )
// return NULL;
p = ABC_CALLOC( Ssw_RarMan_t, 1 );
p->pAig = pAig;
- p->nWords = nWords;
- p->nFrames = nFrames;
- p->nBinSize = nBinSize;
- p->fVerbose = fVerbose;
- p->nGroups = Aig_ManRegNum(pAig) / nBinSize;
- p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups );
- p->pPatCosts = ABC_CALLOC( double, p->nWords * 64 );
+ p->pPars = pPars;
+ p->nGroups = Aig_ManRegNum(pAig) / pPars->nBinSize;
+ p->pRarity = ABC_CALLOC( int, (1 << pPars->nBinSize) * p->nGroups );
+ p->pPatCosts = ABC_CALLOC( double, p->pPars->nWords * 64 );
p->nWordsReg = Ssw_RarBitWordNum( Aig_ManRegNum(pAig) );
- p->pObjData = ABC_ALLOC( word, Aig_ManObjNumMax(pAig) * p->nWords );
- p->pPatData = ABC_ALLOC( word, 64 * p->nWords * p->nWordsReg );
+ p->pObjData = ABC_ALLOC( word, Aig_ManObjNumMax(pAig) * p->pPars->nWords );
+ p->pPatData = ABC_ALLOC( word, 64 * p->pPars->nWords * p->nWordsReg );
p->vUpdConst = Vec_PtrAlloc( 100 );
p->vUpdClass = Vec_PtrAlloc( 100 );
p->vPatBests = Vec_IntAlloc( 100 );
@@ -824,7 +822,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
Ssw_RarTranspose( p );
// update counters
- for ( k = 0; k < p->nWords * 64; k++ )
+ for ( k = 0; k < p->pPars->nWords * 64; k++ )
{
pData = (unsigned char *)Ssw_RarPatSim( p, k );
for ( i = 0; i < p->nGroups; i++ )
@@ -832,7 +830,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
}
// for each pattern
- for ( k = 0; k < p->nWords * 64; k++ )
+ for ( k = 0; k < p->pPars->nWords * 64; k++ )
{
pData = (unsigned char *)Ssw_RarPatSim( p, k );
// find the cost of its values
@@ -849,12 +847,12 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
// choose as many as there are words
Vec_IntClear( vInits );
- for ( i = 0; i < p->nWords; i++ )
+ for ( i = 0; i < p->pPars->nWords; i++ )
{
// select the best
int iPatBest = -1;
double iCostBest = -ABC_INFINITY;
- for ( k = 0; k < p->nWords * 64; k++ )
+ for ( k = 0; k < p->pPars->nWords * 64; k++ )
if ( iCostBest < p->pPatCosts[k] )
{
iCostBest = p->pPatCosts[k];
@@ -870,7 +868,7 @@ static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
//Abc_Print( 1, "Best pattern %5d\n", iPatBest );
Vec_IntPush( p->vPatBests, iPatBest );
}
- assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords );
+ assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->pPars->nWords );
}
@@ -985,7 +983,6 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
int nSavedSeed = pPars->nRandSeed;
int RetValue = -1;
int iFrameFail = -1;
- int nSolved = 0;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 );
ABC_FREE( pAig->pSeqModel );
@@ -1002,10 +999,11 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
Ssw_RarManPrepareRandom( nSavedSeed );
// create manager
- p = Ssw_RarManStart( pAig, pPars->nWords, pPars->nFrames, pPars->nBinSize, pPars->fVerbose );
+ p = Ssw_RarManStart( pAig, pPars );
p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * pPars->nWords );
// perform simulation rounds
+ pPars->nSolved = 0;
timeLastSolved = clock();
for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ )
{
@@ -1022,23 +1020,33 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
for ( f = 0; f < pPars->nFrames; f++ )
{
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
- if ( fMiter && Ssw_RarManCheckNonConstOutputs(p, pPars->fSolveAll ? &nSolved : NULL, r * p->nFrames + f, pPars->fNotVerbose, clock() - clkTotal) )
+ if ( fMiter )
{
- RetValue = 0;
- if ( !pPars->fSolveAll )
+ int Status = Ssw_RarManCheckNonConstOutputs(p, r * p->pPars->nFrames + f, clock() - clkTotal);
+ if ( Status == 2 )
{
- if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
- // Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
- Ssw_RarManPrepareRandom( nSavedSeed );
- if ( pPars->fVerbose )
- Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
- pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, pPars->fVerbose );
- // print final report
- Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
- Abc_PrintTime( 1, "Time", clock() - clkTotal );
+ Abc_Print( 1, "Quitting due to callback on fail.\n" );
goto finish;
}
- timeLastSolved = clock();
+ if ( Status == 1 ) // found CEX
+ {
+ RetValue = 0;
+ if ( !pPars->fSolveAll )
+ {
+ if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
+ // Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
+ Ssw_RarManPrepareRandom( nSavedSeed );
+ if ( pPars->fVerbose )
+ Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
+ pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, pPars->fVerbose );
+ // print final report
+ Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
+ Abc_PrintTime( 1, "Time", clock() - clkTotal );
+ goto finish;
+ }
+ timeLastSolved = clock();
+ }
+ // else - did not find a counter example
}
// check timeout
if ( pPars->TimeOut && clock() > nTimeToStop )
@@ -1081,7 +1089,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
Abc_Print( 1, "Starts =%6d ", nNumRestart );
Abc_Print( 1, "Rounds =%6d ", nNumRestart * pPars->nRestart + ((r==-1)?0:r) );
Abc_Print( 1, "Frames =%6d ", (nNumRestart * pPars->nRestart + r) * pPars->nFrames );
- Abc_Print( 1, "CEX =%6d (%6.2f %%) ", nSolved, 100.0*nSolved/Saig_ManPoNum(p->pAig) );
+ Abc_Print( 1, "CEX =%6d (%6.2f %%) ", pPars->nSolved, 100.0*pPars->nSolved/Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
else
@@ -1096,10 +1104,10 @@ finish:
Vec_IntShrink( p->vInits, Aig_ManRegNum(pAig) );
pAig->pData = p->vInits; p->vInits = NULL;
}
- if ( nSolved )
+ if ( pPars->nSolved )
{
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
- Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, nSolved, Saig_ManPoNum(p->pAig) );
+ Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved, Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
else if ( r == pPars->nRounds && f == pPars->nFrames )
@@ -1175,7 +1183,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
Ssw_RarManPrepareRandom( nSavedSeed );
// create manager
- p = Ssw_RarManStart( pAig, pPars->nWords, pPars->nFrames, pPars->nBinSize, pPars->fVerbose );
+ p = Ssw_RarManStart( pAig, pPars );
// compute starting state if needed
assert( p->vInits == NULL );
if ( pPars->pCex )
@@ -1216,7 +1224,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
for ( f = 0; f < pPars->nFrames; f++ )
{
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
- if ( pPars->fMiter && Ssw_RarManCheckNonConstOutputs(p, NULL, -1, -1, 0) )
+ if ( pPars->fMiter && Ssw_RarManCheckNonConstOutputs(p, -1, 0) )
{
if ( !pPars->fVerbose )
Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
@@ -1225,7 +1233,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Ssw_RarManPrepareRandom( nSavedSeed );
Abc_CexFree( pAig->pSeqModel );
- pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, 1 );
+ pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, 1 );
// print final report
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 93bfd78a..19084ada 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -60,6 +60,7 @@ struct Saig_ParBmc_t_
int iFrame; // explored up to this frame
int nFailOuts; // the number of failed outputs
clock_t timeLastSolved; // the time when the last output was solved
+ int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
};
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 0c828dbd..b737749d 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1477,13 +1477,13 @@ clkOther += clock() - clk2;
continue;
if ( Lit == 1 )
{
+ RetValue = 0;
if ( !pPars->fSolveAll )
{
Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
printf( "Output %d is trivially SAT in frame %d.\n", i, f );
ABC_FREE( pAig->pSeqModel );
pAig->pSeqModel = pCex;
- RetValue = 0;
goto finish;
}
pPars->nFailOuts++;
@@ -1492,11 +1492,12 @@ clkOther += clock() - clk2;
nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
- if ( pPars->fStoreCex )
- Vec_PtrWriteEntry( p->vCexes, i, Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ) );
- else
- Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 );
- RetValue = 0;
+ Vec_PtrWriteEntry( p->vCexes, i, pPars->fStoreCex ? Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ) : (void *)(ABC_PTRINT_T)1 );
+ if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) )
+ {
+ Abc_Print( 1, "Quitting due to callback on fail.\n" );
+ goto finish;
+ }
// reset the timeout
pPars->timeLastSolved = clock();
nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
@@ -1533,6 +1534,7 @@ nTimeUnsat += clock() - clk2;
else if ( status == l_True )
{
nTimeSat += clock() - clk2;
+ RetValue = 0;
fFirst = 0;
if ( !pPars->fSolveAll )
{
@@ -1558,7 +1560,6 @@ nTimeSat += clock() - clk2;
}
ABC_FREE( pAig->pSeqModel );
pAig->pSeqModel = Saig_ManGenerateCex( p, f, i );
- RetValue = 0;
goto finish;
}
pPars->nFailOuts++;
@@ -1568,7 +1569,11 @@ nTimeSat += clock() - clk2;
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pPars->fStoreCex? Saig_ManGenerateCex( p, f, i ) : (void *)(ABC_PTRINT_T)1 );
- RetValue = 0;
+ if ( pPars->pFuncOnFail && pPars->pFuncOnFail(i, pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, i) : NULL) )
+ {
+ Abc_Print( 1, "Quitting due to callback on fail.\n" );
+ goto finish;
+ }
// reset the timeout
pPars->timeLastSolved = clock();
nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-30 03:03:13 +0000