summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abc.c51
-rw-r--r--src/base/abci/abcDar.c47
-rw-r--r--src/misc/util/utilCex.c7
-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
11 files changed, 91 insertions, 85 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e7fe63e9..4b7f21bd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2292,13 +2292,21 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
Abc_Print( 1,"Status = %d Frames = %d ", pAbc->Status, pAbc->nFrames );
- if ( pAbc->pCex == NULL )
+ if ( pAbc->pCex == NULL && pAbc->vCexVec == NULL )
Abc_Print( 1,"Cex is not defined.\n" );
else
- Abc_Print( 1,"Cex: PIs = %d Regs = %d PO = %d Frame = %d Bits = %d\n",
- pAbc->pCex->nPis, pAbc->pCex->nRegs,
- pAbc->pCex->iPo, pAbc->pCex->iFrame,
- pAbc->pCex->nBits );
+ {
+ if ( pAbc->pCex )
+ Abc_CexPrintStats( pAbc->pCex );
+ if ( pAbc->vCexVec )
+ {
+ Abc_Cex_t * pTemp;
+ printf( "\n" );
+ Vec_PtrForEachEntry( Abc_Cex_t *, pAbc->vCexVec, pTemp, c )
+ if ( pTemp )
+ Abc_CexPrintStats( pTemp );
+ }
+ }
return 0;
usage:
@@ -20920,7 +20928,10 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
if ( pNtk->vSeqModelVec )
+ {
Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
+ pAbc->nFrames = -1;
+ }
return 0;
usage:
@@ -22314,10 +22325,9 @@ usage:
***********************************************************************/
int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
+ extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars );
Pdr_Par_t Pars, * pPars = &Pars;
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
- Abc_Cex_t * pCex = NULL;
int c;
Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
@@ -22437,28 +22447,15 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n");
return 0;
}
-/*
- if ( pPars->iOutput != -1 && (pPars->iOutput < 0 || pPars->iOutput >= Abc_NtkPoNum(pNtk)) )
- {
- Abc_Print( -2, "Output index (%d) is incorrect (can be 0 through %d).\n",
- pPars->iOutput, Abc_NtkPoNum(pNtk)-1 );
- return 0;
- }
-*/
-/*
- if ( Abc_NtkPoNum(pNtk) != 1 && pPars->fVerbose )
- {
- if ( pPars->iOutput == -1 )
- Abc_Print( -2, "The %d property outputs are ORed together.\n", Abc_NtkPoNum(pNtk) );
- else
- Abc_Print( -2, "Working on the primary output with zero-based number %d (out of %d).\n",
- pPars->iOutput, Abc_NtkPoNum(pNtk) );
- }
-*/
// run the procedure
- pAbc->Status = Abc_NtkDarPdr( pNtk, pPars, &pCex );
+ pAbc->Status = Abc_NtkDarPdr( pNtk, pPars );
pAbc->nFrames = pPars->iFrame;
- Abc_FrameReplaceCex( pAbc, &pCex );
+ Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
+ if ( pNtk->vSeqModelVec )
+ {
+ Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
+ pAbc->nFrames = -1;
+ }
return 0;
usage:
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 496855c2..742f90bb 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2705,57 +2705,46 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
SeeAlso []
***********************************************************************/
-int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
+int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
{
int RetValue = -1;
clock_t clk = clock();
Aig_Man_t * pMan;
- *ppCex = NULL;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
{
Abc_Print( 1, "Converting network into AIG has failed.\n" );
return -1;
}
-/*
- // perform ORing the primary outputs
- if ( pPars->iOutput == -1 )
- {
- Aig_Man_t * pTemp = Saig_ManDupOrpos( pMan );
- RetValue = Pdr_ManSolve( pTemp, pPars, ppCex );
- if ( RetValue == 0 )
- (*ppCex)->iPo = Saig_ManFindFailedPoCex( pMan, *ppCex );
- Aig_ManStop( pTemp );
- }
- else
- RetValue = Pdr_ManSolve( pMan, pPars, ppCex );
-*/
- RetValue = Pdr_ManSolve( pMan, pPars, ppCex );
-
- // output the result
+ RetValue = Pdr_ManSolve( pMan, pPars );
if ( !pPars->fSilent )
{
if ( RetValue == 1 )
Abc_Print( 1, "Property proved. " );
else if ( RetValue == 0 )
- Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
+ {
+ if ( pMan->pSeqModel == NULL )
+ Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example is not available.\n" );
+ else
+ {
+ Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
+ if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) )
+ Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
+ }
+ }
else if ( RetValue == -1 )
Abc_Print( 1, "Property UNDECIDED. " );
else
assert( 0 );
ABC_PRT( "Time", clock() - clk );
}
-
-// ABC_FREE( pNtk->pSeqModel );
-// pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
- if ( ppCex )
- *ppCex = pMan->pSeqModel;
- else
- ABC_FREE( pMan->pSeqModel );
+ ABC_FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pMan->pSeqModel;
pMan->pSeqModel = NULL;
-
- if ( *ppCex && !Saig_ManVerifyCex( pMan, *ppCex ) )
- Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
+ if ( pNtk->vSeqModelVec )
+ Vec_PtrFreeFree( pNtk->vSeqModelVec );
+ pNtk->vSeqModelVec = pMan->vSeqModelVec;
+ pMan->vSeqModelVec = NULL;
Aig_ManStop( pMan );
return RetValue;
}
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index 2f205d2e..75b99492 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -261,8 +261,9 @@ void Abc_CexPrintStats( Abc_Cex_t * p )
}
for ( k = 0; k < p->nBits; k++ )
Counter += Abc_InfoHasBit(p->pData, k);
- printf( "CEX: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits =%8d nOnes =%8d (%5.2f %%)\n",
- p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, Counter, 100.0 * Counter / (p->nBits - p->nRegs) );
+ printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%8d (%5.2f %%)\n",
+ p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits,
+ Counter, 100.0 * Counter / (p->nBits - p->nRegs) );
}
void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs )
{
@@ -278,7 +279,7 @@ void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs )
if ( (k - p->nRegs) % p->nPis < nInputs )
Counter2 += Abc_InfoHasBit(p->pData, k);
}
- printf( "CEX: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits =%8d nOnes =%8d (%5.2f %%) nOnesIn =%8d (%5.2f %%)\n",
+ printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%8d (%5.2f %%) 1sIn =%8d (%5.2f %%)\n",
p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits,
Counter, 100.0 * Counter / (p->nBits - p->nRegs),
Counter2, 100.0 * Counter2 / (p->nBits - p->nRegs - (p->iFrame + 1) * (p->nPis - nInputs)) );
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 2025-10-31 17:35:41 +0000