diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-29 14:20:40 -0700 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-29 14:20:40 -0700 |
| commit | 4d479048319e714c636c3dbeb37ee90911ef4130 (patch) | |
| tree | 506ca790aa29a47f86da9b2eaad723fec0551fe9 /src/proof/pdr | |
| parent | bf4be3fc25d3edae0f87630e8c7162cb8bfec6e0 (diff) | |
| download | abc-4d479048319e714c636c3dbeb37ee90911ef4130.tar.gz abc-4d479048319e714c636c3dbeb37ee90911ef4130.tar.bz2 abc-4d479048319e714c636c3dbeb37ee90911ef4130.zip | |
%pdra: fixed bugs
Diffstat (limited to 'src/proof/pdr')
| -rw-r--r-- | src/proof/pdr/pdrIncr.c | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 1f578242..8cc964e5 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -272,7 +272,9 @@ int IPdr_ManRebuildClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses ) Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j ) { ++nCubes; + RetValue = Pdr_ManCheckCube( p, 0, pCube, NULL, 0, 0, 1 ); + Vec_IntWriteEntry( p->vActVars, 0, 0 ); assert( RetValue != -1 ); @@ -288,7 +290,9 @@ int IPdr_ManRebuildClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses ) } Abc_Print( 1, "RebuildClauses: %d out of %d cubes reused in R1.\n", Vec_PtrSize(Vec_VecEntry(p->vClauses, 1)), nCubes ); IPdr_ManSetSolver( p, 1, 0 ); + Vec_VecFree( vClauses ); + /* for ( i = 1; i < Vec_VecSize( vClauses ) - 1; ++i ) { vArrayK = IPdr_ManPushClausesK( p, i ); @@ -308,8 +312,8 @@ int IPdr_ManRebuildClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses ) Vec_VecForEachLevel( p->vClauses, vArrayK, i ) Abc_Print( 1, " %d", Vec_PtrSize( vArrayK ) ); Abc_Print( 1, "\n" ); + */ - Vec_VecFree( vClauses ); return 0; } |