summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/aig/aig.h2
-rw-r--r--src/aig/aig/aigMan.c4
-rw-r--r--src/aig/saig/saigBmc3.c9
-rw-r--r--src/aig/saig/saigCexMin.c63
-rw-r--r--src/base/abc/abc.h2
-rw-r--r--src/base/abc/abcNtk.c4
-rw-r--r--src/base/abci/abc.c37
-rw-r--r--src/base/abci/abcDar.c6
-rw-r--r--src/base/main/mainInt.h1
9 files changed, 112 insertions, 16 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index a0216f37..e614d58f 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -154,7 +154,7 @@ struct Aig_Man_t_
Vec_Int_t * vFlopNums;
Vec_Int_t * vFlopReprs;
Abc_Cex_t * pSeqModel;
- Vec_Ptr_t * pSeqModelVec; // vector of counter-examples (for sequential miters)
+ Vec_Ptr_t * vSeqModelVec; // vector of counter-examples (for sequential miters)
Aig_Man_t * pManExdc;
Vec_Ptr_t * vOnehots;
Aig_Man_t * pManHaig;
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index bce56424..b0544c90 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -211,8 +211,8 @@ void Aig_ManStop( Aig_Man_t * p )
Vec_IntFreeP( &p->vProbs );
Vec_IntFreeP( &p->vCiNumsOrig );
Vec_PtrFreeP( &p->vMapped );
- if ( p->pSeqModelVec )
- Vec_PtrFreeFree( p->pSeqModelVec );
+ if ( p->vSeqModelVec )
+ Vec_PtrFreeFree( p->vSeqModelVec );
ABC_FREE( p->pTerSimData );
ABC_FREE( p->pFastSim );
ABC_FREE( p->pData );
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index b984844e..4dc0c714 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -612,8 +612,8 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
Aig_ManCleanMarkA( p->pAig );
if ( p->vCexes )
{
- assert( p->pAig->pSeqModelVec == NULL );
- p->pAig->pSeqModelVec = p->vCexes;
+ assert( p->pAig->vSeqModelVec == NULL );
+ p->pAig->vSeqModelVec = p->vCexes;
p->vCexes = NULL;
}
// Vec_PtrFreeFree( p->vCexes );
@@ -1133,7 +1133,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
return 0;
}
// consider the next timeframe
- pPars->iFrame = f;
+ if ( RetValue == -1 && pPars->nStart == 0 )
+ pPars->iFrame = f;
// resize the array
Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 );
// map nodes of this section
@@ -1206,6 +1207,7 @@ clkOther += clock() - clk2;
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pCex );
+ RetValue = 0;
continue;
}
// solve this output
@@ -1254,6 +1256,7 @@ clkOther += clock() - clk2;
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
Vec_PtrWriteEntry( p->vCexes, i, pCex );
+ RetValue = 0;
}
else
{
diff --git a/src/aig/saig/saigCexMin.c b/src/aig/saig/saigCexMin.c
index dd88fb70..824f9eb3 100644
--- a/src/aig/saig/saigCexMin.c
+++ b/src/aig/saig/saigCexMin.c
@@ -252,7 +252,7 @@ void Saig_ManCexMinDerivePhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_
SeeAlso []
***********************************************************************/
-Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
+Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
{
Vec_Vec_t * vFramePPs;
Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
@@ -302,6 +302,67 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC
return vFramePPs;
}
+/**Function*************************************************************
+
+ Synopsis [Collects phase and priority of all timeframes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
+{
+ Vec_Vec_t * vFramePPs;
+ Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
+ Aig_Obj_t * pObj;
+ int i, f, nPrioOffset;
+
+ // initialize phase and priority
+ Aig_ManForEachObj( pAig, pObj, i )
+ pObj->iData = -1;
+
+ // set the constant node to higher priority than the flops
+ vFramePPs = Vec_VecStart( pCex->iFrame+1 );
+ nPrioOffset = pCex->nRegs;
+ Aig_ManConst1(pAig)->iData = Aig_Var2Lit( nPrioOffset + (pCex->iFrame + 1) * pCex->nPis, 1 );
+ vRoots = Vec_IntAlloc( 1000 );
+//printf( "Const1 = %d Offset = %d\n", Aig_ManConst1(pAig)->iData, nPrioOffset );
+ for ( f = 0; f <= pCex->iFrame; f++ )
+ {
+ int nPiCount = 0;
+ // fill in PP for the CIs
+ vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
+ vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
+ assert( Vec_IntSize(vFramePPsOne) == 0 );
+ Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
+ {
+ assert( Aig_ObjIsPi(pObj) );
+ if ( Saig_ObjIsPi(pAig, pObj) )
+ Vec_IntPush( vFramePPsOne, Aig_Var2Lit( nPrioOffset + (f+1) * pCex->nPis - 1 - nPiCount++, Aig_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) );
+ else if ( f == 0 )
+ Vec_IntPush( vFramePPsOne, Aig_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) );
+ else
+ {
+ Aig_Obj_t * pObj0 = Saig_ObjLoToLi(pAig, pObj);
+ int Value = Saig_ObjLoToLi(pAig, pObj)->iData;
+ Vec_IntPush( vFramePPsOne, Saig_ObjLoToLi(pAig, pObj)->iData );
+ }
+//printf( "%d ", Vec_IntEntryLast(vFramePPsOne) );
+ }
+//printf( "\n" );
+ // compute the PP info
+ Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
+ }
+ Vec_IntFree( vRoots );
+ // check the output
+ pObj = Aig_ManPo( pAig, pCex->iPo );
+ assert( Aig_LitIsCompl(pObj->iData) );
+ return vFramePPs;
+}
+
/**Function*************************************************************
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index e707c57e..0d59d7e0 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -203,7 +203,7 @@ struct Abc_Ntk_t_
Vec_Ptr_t * vSupps; // CO support information
int * pModel; // counter-example (for miters)
Abc_Cex_t * pSeqModel; // counter-example (for sequential miters)
- Vec_Ptr_t * pSeqModelVec; // vector of counter-examples (for sequential miters)
+ Vec_Ptr_t * vSeqModelVec; // vector of counter-examples (for sequential miters)
Abc_Ntk_t * pExdc; // the EXDC network (if given)
void * pExcare; // the EXDC network (if given)
void * pData; // misc
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index ac488114..4295835d 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -995,8 +995,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
if ( pNtk->vLevelsR ) Vec_IntFree( pNtk->vLevelsR );
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
- if ( pNtk->pSeqModelVec )
- Vec_PtrFreeFree( pNtk->pSeqModelVec );
+ if ( pNtk->vSeqModelVec )
+ Vec_PtrFreeFree( pNtk->vSeqModelVec );
TotalMemory = 0;
TotalMemory += pNtk->pMmObj? Mem_FixedReadMemUsage(pNtk->pMmObj) : 0;
TotalMemory += pNtk->pMmStep? Mem_StepReadMemUsage(pNtk->pMmStep) : 0;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5e9041b1..3a28d169 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -410,9 +410,38 @@ extern int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc,
***********************************************************************/
void Abc_FrameReplaceCex( Abc_Frame_t * pAbc, Abc_Cex_t ** ppCex )
{
+ // update CEX
ABC_FREE( pAbc->pCex );
pAbc->pCex = *ppCex;
*ppCex = NULL;
+ // remove CEX vector
+ if ( pAbc->vCexVec )
+ {
+ Vec_PtrFreeFree( pAbc->vCexVec );
+ pAbc->vCexVec = NULL;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec )
+{
+ // update CEX vector
+ if ( pAbc->vCexVec )
+ Vec_PtrFreeFree( pAbc->vCexVec );
+ pAbc->vCexVec = *pvCexVec;
+ *pvCexVec = NULL;
+ // remove CEX
+ ABC_FREE( pAbc->pCex );
}
/**Function*************************************************************
@@ -19015,14 +19044,14 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc3" );
if ( pPars->fSolveAll && pPars->fDropSatOuts )
{
- if ( pNtk->pSeqModelVec == NULL )
+ if ( pNtk->vSeqModelVec == NULL )
printf( "The array of counter-examples is not available.\n" );
- else if ( Vec_PtrSize(pNtk->pSeqModelVec) != Abc_NtkPoNum(pNtk) )
+ else if ( Vec_PtrSize(pNtk->vSeqModelVec) != Abc_NtkPoNum(pNtk) )
printf( "The array size does not match the number of outputs.\n" );
else
{
extern void Abc_NtkDropSatOutputs( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCexes, int fVerbose );
- Abc_NtkDropSatOutputs( pNtk, pNtk->pSeqModelVec, pPars->fVerbose );
+ Abc_NtkDropSatOutputs( pNtk, pNtk->vSeqModelVec, pPars->fVerbose );
pNtkRes = Abc_NtkDarLatchSweep( pNtk, 1, 1, 1, 0 );
if ( pNtkRes == NULL )
{
@@ -19032,6 +19061,8 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
}
}
+ if ( pNtk->vSeqModelVec )
+ Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
return 0;
usage:
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 064529cc..ebeafa86 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1824,9 +1824,9 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
printf( "(timeout %d sec). ", pPars->nTimeOut );
else
printf( "(conf limit %d). ", pPars->nConfLimit );
- if ( pNtk->pSeqModelVec )
- Vec_PtrFreeFree( pNtk->pSeqModelVec );
- pNtk->pSeqModelVec = pMan->pSeqModelVec; pMan->pSeqModelVec = NULL;
+ if ( pNtk->vSeqModelVec )
+ Vec_PtrFreeFree( pNtk->vSeqModelVec );
+ pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL;
}
}
else // if ( RetValue == 0 )
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index d3a1fc9f..c008fc8b 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -98,6 +98,7 @@ struct Abc_Frame_t_
Gia_Man_t * pGia;
Gia_Man_t * pGia2;
Abc_Cex_t * pCex;
+ Vec_Ptr_t * vCexVec;
void * pSave1;
void * pSave2;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 08:07:30 +0000