diff options
author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-19 15:57:13 -0800 |
---|---|---|
committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-19 15:57:13 -0800 |
commit | 2d1792040a8c09a12d70413ceb99bd11bb145c2b (patch) | |
tree | 7a1f8a998ed3067f6483d23b86b0e51544e6ab19 /src/proof | |
parent | 2732cbc1ee3b82fa7f609ef4c7156132058612dc (diff) | |
download | abc-2d1792040a8c09a12d70413ceb99bd11bb145c2b.tar.gz abc-2d1792040a8c09a12d70413ceb99bd11bb145c2b.tar.bz2 abc-2d1792040a8c09a12d70413ceb99bd11bb145c2b.zip |
working on pdr with wla
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/pdr/pdrIncr.c | 47 |
1 files changed, 42 insertions, 5 deletions
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index b1f126f4..4f66eeb4 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -77,12 +77,52 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs ) SeeAlso [] ***********************************************************************/ +int IPdr_ManCheckClauses( Pdr_Man_t * p ) +{ + Pdr_Set_t * pCubeK; + Vec_Ptr_t * vArrayK; + int j, k, RetValue, kMax = Vec_PtrSize(p->vSolvers)-1; + int iStartFrame = 1; + + Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax ) + { + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) + { + RetValue = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0, 1 ); + + if ( !RetValue ) { + printf( "Cube[%d][%d] not inductive!\n", k, j ); + } + + assert( RetValue == 1 ); + } + } + + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast ) { int i, k; Vec_Vec_t * vClausesSaved; Pdr_Set_t * pCla; + if ( Vec_VecSize( p->vClauses ) == 1 ) + return NULL; + if ( Vec_VecSize( p->vClauses ) == 2 && fDropLast ) + return NULL; + if ( fDropLast ) vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses)-1 ); else @@ -147,9 +187,6 @@ int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses ) assert(vClauses); - printf( "IPdr restore:\n" ); - IPdr_ManPrintClauses( vClauses, 0, Aig_ManRegNum( p->pAig ) ); - Vec_VecFree(p->vClauses); p->vClauses = vClauses; @@ -197,8 +234,8 @@ int IPdr_ManSolveInt( Pdr_Man_t * p ) if ( Vec_VecSize(p->vClauses) == 0 ) Pdr_ManCreateSolver( p, (iFrame = 0) ); else { - iFrame = Vec_VecSize(p->vClauses); - Pdr_ManCreateSolver( p, iFrame ); + iFrame = Vec_VecSize(p->vClauses) - 1; + IPdr_ManCheckClauses( p ); } while ( 1 ) { |