diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-28 18:05:58 -0800 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-28 18:05:58 -0800 |
| commit | 902a78eeb883cb97131e03cc31cf0892787e806e (patch) | |
| tree | 6a3a83a72d13c1afbfe9a6da4415ac34dd6bab4b /src/base/wlc/wlcAbs.c | |
| parent | d95d51c474fdd5d882b34c8bcbcd27173ba8431c (diff) | |
| download | abc-902a78eeb883cb97131e03cc31cf0892787e806e.tar.gz abc-902a78eeb883cb97131e03cc31cf0892787e806e.tar.bz2 abc-902a78eeb883cb97131e03cc31cf0892787e806e.zip | |
added an option -r to %pdra: proof-based refinement only
Diffstat (limited to 'src/base/wlc/wlcAbs.c')
| -rw-r--r-- | src/base/wlc/wlcAbs.c | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 69d1df77..1eb5a964 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -1107,9 +1107,16 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) } // perform refinement - clk2 = Abc_Clock(); - vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); - tCbr += Abc_Clock() - clk2; + if ( pPars->fHybrid || !pPars->fProofRefine ) + { + clk2 = Abc_Clock(); + vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); + tCbr += Abc_Clock() - clk2; + } + else // proof-based only + { + vRefine = Vec_IntDup( vPisNew ); + } if ( pPars->fProofRefine ) { clk2 = Abc_Clock(); |