summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/wlc/wlc.h2
-rw-r--r--src/base/wlc/wlcAbs.c10
-rw-r--r--src/base/wlc/wlcCom.c12
-rw-r--r--src/proof/pdr/pdrIncr.c37
4 files changed, 51 insertions, 10 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index cf8bdab4..9cb34bf3 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -184,6 +184,8 @@ struct WlcPdr_Par_t_
int nBitsFlop; // flop bit-width
int nIterMax; // the max number of iterations
int fXorOutput; // XOR outputs of word-level miter
+ int fCheckClauses; // Check clauses in the reloaded trace
+ int fPushClauses; // Push clauses in the reloaded trace
int fVerbose; // verbose output
int fPdrVerbose; // verbose output
};
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index 8fde7f56..fbaa1b8a 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -32,7 +32,7 @@ ABC_NAMESPACE_IMPL_START
extern Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast );
extern int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses );
-extern int IPdr_ManSolveInt( Pdr_Man_t * p );
+extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -59,6 +59,8 @@ void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars )
pPars->nBitsFlop = ABC_INFINITY; // flop bit-width
pPars->nIterMax = 1000; // the max number of iterations
pPars->fXorOutput = 1; // XOR outputs of word-level miter
+ pPars->fCheckClauses = 1; // Check clauses in the reloaded trace
+ pPars->fPushClauses = 0; // Push clauses in the reloaded trace
pPars->fVerbose = 0; // verbose output
pPars->fPdrVerbose = 0; // show verbose PDR output
}
@@ -76,7 +78,7 @@ void WlcPdr_ManSetDefaultParams( WlcPdr_Par_t * pPars )
SeeAlso []
***********************************************************************/
-static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
+static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
{
Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
Wlc_Obj_t * pObj; int i, Count[4] = {0};
@@ -197,7 +199,7 @@ static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t *
SeeAlso []
***********************************************************************/
-static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose )
+static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose )
{
Wlc_Ntk_t * pNtkNew = NULL;
Vec_Int_t * vPisOld = Vec_IntAlloc( 100 );
@@ -401,7 +403,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, WlcPdr_Par_t * pPars )
IPdr_ManRestore( pPdr, vClauses );
}
- RetValue = IPdr_ManSolveInt( pPdr );
+ RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
pPdr->tTotal += Abc_Clock() - pdrClk;
pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index d30b376e..7801abc6 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
WlcPdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF )
{
switch ( c )
{
@@ -524,6 +524,12 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'x':
pPars->fXorOutput ^= 1;
break;
+ case 'c':
+ pPars->fCheckClauses ^= 1;
+ break;
+ case 'p':
+ pPars->fPushClauses ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -544,7 +550,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
Wlc_NtkPdrAbs( pNtk, pPars );
return 0;
usage:
- Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-xvwh]\n" );
+ Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpxvwh]\n" );
Abc_Print( -2, "\t abstraction for word-level networks\n" );
Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
@@ -552,6 +558,8 @@ usage:
Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop );
Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax );
Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" );
+ Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" );
+ Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c
index 09a06a27..85403a7d 100644
--- a/src/proof/pdr/pdrIncr.c
+++ b/src/proof/pdr/pdrIncr.c
@@ -68,7 +68,9 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs )
/**Function*************************************************************
- Synopsis []
+ Synopsis [ Check if each cube c_k in frame k satisfies the query
+ R_{k-1} && T && !c_k && c_k' (must be UNSAT).
+ Return True if all cubes pass the check. ]
Description []
@@ -214,7 +216,7 @@ int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses )
SeeAlso []
***********************************************************************/
-int IPdr_ManSolveInt( Pdr_Man_t * p )
+int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
{
int fPrintClauses = 0;
Pdr_Set_t * pCube = NULL;
@@ -242,7 +244,34 @@ int IPdr_ManSolveInt( Pdr_Man_t * p )
Pdr_ManCreateSolver( p, (iFrame = 0) );
else {
iFrame = Vec_VecSize(p->vClauses) - 1;
- IPdr_ManCheckClauses( p );
+
+ if ( fCheckClauses )
+ {
+ if ( p->pPars->fVerbose )
+ Abc_Print( 1, "IPDR: Checking the reloaded length-%d trace...", iFrame + 1 ) ;
+ IPdr_ManCheckClauses( p );
+ if ( p->pPars->fVerbose )
+ Abc_Print( 1, " Passed!\n" ) ;
+ }
+
+ if ( fPushClauses )
+ {
+ p->iUseFrame = Abc_MaxInt(iFrame, 1);
+
+ if ( p->pPars->fVerbose )
+ {
+ Abc_Print( 1, "IPDR: Pushing the reloaded clauses. Before:\n" );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
+ }
+
+ RetValue = Pdr_ManPushClauses( p );
+
+ if ( p->pPars->fVerbose )
+ {
+ Abc_Print( 1, "IPDR: Finished pushing. After:\n" );
+ Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
+ }
+ }
}
while ( 1 )
{
@@ -602,7 +631,7 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
p = Pdr_ManStart( pAig, pPars, NULL );
while ( 1 ) {
- RetValue = IPdr_ManSolveInt( p );
+ RetValue = IPdr_ManSolveInt( p, 1, 0 );
if ( RetValue == -1 && pPars->iFrame == pPars->nFrameMax) {
vClausesSaved = IPdr_ManSaveClauses( p, 1 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-30 13:10:29 +0000