diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-27 15:10:33 -0700 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-27 15:10:33 -0700 |
| commit | e6098d20beeb5b05ad6b113ff35c62ba2a386e47 (patch) | |
| tree | 8876934135028f73b01a554aa28ec51dd3e83724 /src/base/wlc | |
| parent | 2ccd0f9b85cb42d3e6e894a71cd8e962b2d3bd12 (diff) | |
| download | abc-e6098d20beeb5b05ad6b113ff35c62ba2a386e47.tar.gz abc-e6098d20beeb5b05ad6b113ff35c62ba2a386e47.tar.bz2 abc-e6098d20beeb5b05ad6b113ff35c62ba2a386e47.zip | |
%pdra: added a procedure to rebuild traces
Diffstat (limited to 'src/base/wlc')
| -rw-r--r-- | src/base/wlc/wlcAbs.c | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index f069c95f..5293de9e 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -32,7 +32,8 @@ 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, Vec_Int_t * vMap ); +extern int IPdr_ManRestoreClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap ); +extern int IPdr_ManRebuildClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses ); extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses ); extern int IPdr_ManCheckCombUnsat( Pdr_Man_t * p ); extern int IPdr_ManReduceClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses ); @@ -1319,7 +1320,8 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) pPdr = Pdr_ManStart( pAig, pPdrPars, NULL ); if ( pWla->vClauses ) { assert( Vec_VecSize( pWla->vClauses) >= 2 ); - IPdr_ManRestore( pPdr, pWla->vClauses, NULL ); + IPdr_ManRestoreClauses( pPdr, pWla->vClauses, NULL ); + //IPdr_ManRebuildClauses( pPdr, pWla->vClauses ); } RetValue = IPdr_ManSolveInt( pPdr, pWla->pPars->fCheckClauses, pWla->pPars->fPushClauses ); |