summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/abs/absOldRef.c10
-rw-r--r--src/proof/abs/absPth.c3
-rw-r--r--src/proof/fra/fraSec.c10
-rw-r--r--src/proof/pdr/pdr.h2
-rw-r--r--src/proof/pdr/pdrCore.c25
-rw-r--r--src/proof/pdr/pdrInt.h1
-rw-r--r--src/proof/pdr/pdrMan.c2
-rw-r--r--src/proof/pdr/pdrUtil.c18
8 files changed, 45 insertions, 26 deletions
diff --git a/src/proof/abs/absOldRef.c b/src/proof/abs/absOldRef.c
index eb9b84fa..0b99ab40 100644
--- a/src/proof/abs/absOldRef.c
+++ b/src/proof/abs/absOldRef.c
@@ -134,7 +134,6 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
pSecPar->fVerbose = fVerbose;
RetValue = Fra_FraigSec( pAbs, pSecPar, NULL );
*/
- Abc_Cex_t * pCex = NULL;
Aig_Man_t * pAbsOrpos = Saig_ManDupOrpos( pAbs );
Pdr_Par_t Pars, * pPars = &Pars;
Pdr_ManSetDefaultParams( pPars );
@@ -142,11 +141,12 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
pPars->fVerbose = fVerbose;
if ( pPars->fVerbose )
printf( "Running property directed reachability...\n" );
- RetValue = Pdr_ManSolve( pAbsOrpos, pPars, &pCex );
- if ( pCex )
- pCex->iPo = Saig_ManFindFailedPoCex( pAbs, pCex );
+ RetValue = Pdr_ManSolve( pAbsOrpos, pPars );
+ if ( pAbsOrpos->pSeqModel )
+ pAbsOrpos->pSeqModel->iPo = Saig_ManFindFailedPoCex( pAbs, pAbsOrpos->pSeqModel );
+ pAbs->pSeqModel = pAbsOrpos->pSeqModel;
+ pAbsOrpos->pSeqModel = NULL;
Aig_ManStop( pAbsOrpos );
- pAbs->pSeqModel = pCex;
if ( RetValue )
*piRetValue = 1;
diff --git a/src/proof/abs/absPth.c b/src/proof/abs/absPth.c
index 3c24d83e..ef38369c 100644
--- a/src/proof/abs/absPth.c
+++ b/src/proof/abs/absPth.c
@@ -107,8 +107,7 @@ void * Abs_ProverThread( void * pArg )
pPars->fSilent = 1;
pPars->RunId = pThData->RunId;
pPars->pFuncStop = Abs_CallBackToStop;
- RetValue = Pdr_ManSolve( pThData->pAig, pPars, NULL );
-// RetValue = Pdr_ManSolve_test( pAig, pPars, NULL );
+ RetValue = Pdr_ManSolve( pThData->pAig, pPars );
// update the result
if ( RetValue == 1 )
{
diff --git a/src/proof/fra/fraSec.c b/src/proof/fra/fraSec.c
index c43fc4dd..04c9d668 100644
--- a/src/proof/fra/fraSec.c
+++ b/src/proof/fra/fraSec.c
@@ -589,19 +589,15 @@ ABC_PRT( "Time", clock() - clk );
// try PDR
if ( pParSec->fUsePdr && RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
{
- Abc_Cex_t * pCex = NULL;
- Aig_Man_t * pNewOrpos = Saig_ManDupOrpos( pNew );
Pdr_Par_t Pars, * pPars = &Pars;
Pdr_ManSetDefaultParams( pPars );
pPars->nTimeOut = pParSec->nPdrTimeout;
pPars->fVerbose = pParSec->fVerbose;
if ( pParSec->fVerbose )
printf( "Running property directed reachability...\n" );
- RetValue = Pdr_ManSolve( pNewOrpos, pPars, &pCex );
- if ( pCex )
- pCex->iPo = Saig_ManFindFailedPoCex( pNew, pCex );
- Aig_ManStop( pNewOrpos );
- pNew->pSeqModel = pCex;
+ RetValue = Pdr_ManSolve( pNew, pPars );
+ if ( pNew->pSeqModel )
+ pNew->pSeqModel->iPo = Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel );
}
finish:
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index 3c40d2d5..a815bb30 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -71,7 +71,7 @@ struct Pdr_Par_t_
/*=== pdrCore.c ==========================================================*/
extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
-extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
+extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars );
ABC_NAMESPACE_HEADER_END
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index f72983da..76d6f788 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -635,7 +635,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( !p->pPars->fSolveAll )
{
- p->pAig->pSeqModel = Pdr_ManDeriveCex( p );
+ p->pAig->pSeqModel = Pdr_ManDeriveCex(p);
return 0; // SAT
}
p->pPars->nFailOuts++;
@@ -647,6 +647,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, Pdr_ManDeriveCex(p) );
if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
return 0; // all SAT
+ Pdr_QueueClean( p );
+ pCube = NULL;
+ break; // keep solving
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 0, clock() - clkStart );
@@ -735,7 +738,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
SeeAlso []
***********************************************************************/
-int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
+int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
{
Pdr_Man_t * p;
int RetValue;
@@ -743,16 +746,19 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
if ( pPars->fVerbose )
{
// Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
- Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ",
- pPars->nRecycle, pPars->nFrameMax, pPars->nRestLimit, pPars->nTimeOut );
- Abc_Print( 1, "MonoCNF = %s. SkipGen = %s.\n",
- pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" );
+ Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueMax = %d. TimeMax = %d. ",
+ pPars->nRecycle,
+ pPars->nFrameMax,
+ pPars->nRestLimit,
+ pPars->nTimeOut );
+ Abc_Print( 1, "MonoCNF = %s. SkipGen = %s. SolveAll = %s.\n",
+ pPars->fMonoCnf ? "yes" : "no",
+ pPars->fSkipGeneral ? "yes" : "no",
+ pPars->fSolveAll ? "yes" : "no" );
}
ABC_FREE( pAig->pSeqModel );
p = Pdr_ManStart( pAig, pPars, NULL );
RetValue = Pdr_ManSolveInt( p );
-// if ( ppCex )
-// *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
if ( RetValue == 0 )
assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
if ( p->vCexes )
@@ -763,9 +769,6 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
}
if ( p->pPars->fDumpInv )
Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
-// if ( *ppCex && pPars->fVerbose )
-// Abc_Print( 1, "Found counter-example in frame %d after exploring %d frames.\n",
-// (*ppCex)->iFrame, p->nFrames );
p->tTotal += clock() - clk;
Pdr_ManStop( p );
pPars->iFrame--;
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index abc8f12b..f6d3d170 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -187,6 +187,7 @@ extern void Pdr_OblDeref( Pdr_Obl_t * p );
extern int Pdr_QueueIsEmpty( Pdr_Man_t * p );
extern Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p );
extern Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p );
+extern void Pdr_QueueClean( Pdr_Man_t * p );
extern void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl );
extern void Pdr_QueuePrint( Pdr_Man_t * p );
extern void Pdr_QueueStop( Pdr_Man_t * p );
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index 78aa2b69..95e7641b 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -188,6 +188,8 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
}
assert( f == nFrames );
+ if ( !Saig_ManVerifyCex(p->pAig, pCex) )
+ printf( "CEX for output %d is not valid.\n", p->iOutCur );
return pCex;
}
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index a47bc9f0..c70554e3 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -510,6 +510,24 @@ Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p )
SeeAlso []
***********************************************************************/
+void Pdr_QueueClean( Pdr_Man_t * p )
+{
+ Pdr_Obl_t * pThis;
+ while ( (pThis = Pdr_QueuePop(p)) )
+ Pdr_OblDeref( pThis );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl )
{
Pdr_Obl_t * pTemp, ** ppPrev;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 02:02:28 +0000