diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-27 15:18:35 -0700 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-27 15:18:35 -0700 |
| commit | 758270d66350b36f4b3a8ceeefcea3a3efe230f1 (patch) | |
| tree | e316abf13a0570e4b0afb3cbc5f7bc89074bfbae /src/proof/pdr | |
| parent | e6098d20beeb5b05ad6b113ff35c62ba2a386e47 (diff) | |
| download | abc-758270d66350b36f4b3a8ceeefcea3a3efe230f1.tar.gz abc-758270d66350b36f4b3a8ceeefcea3a3efe230f1.tar.bz2 abc-758270d66350b36f4b3a8ceeefcea3a3efe230f1.zip | |
%pdra: refactor
Diffstat (limited to 'src/proof/pdr')
| -rw-r--r-- | src/proof/pdr/pdrIncr.c | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index abf8ab93..1f578242 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -309,20 +309,6 @@ int IPdr_ManRebuildClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses ) Abc_Print( 1, " %d", Vec_PtrSize( vArrayK ) ); Abc_Print( 1, "\n" ); - /* - for ( i = 1; i < Vec_VecSize(p->vClauses); ++i ) - IPdr_ManSetSolver( p, i, 0 ); - - p->iUseFrame = Vec_VecSize(p->vClauses) - 1; - RetValue = Pdr_ManPushClauses( p ); - - if ( RetValue == 1 ) - { - Abc_Print( 1, "Found an invariant!\n"); - return 1; - } - */ - Vec_VecFree( vClauses ); return 0; } |