diff options
author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-04-16 22:03:47 -0700 |
---|---|---|
committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-04-16 22:03:47 -0700 |
commit | 38e5c8c9e6eaa5fa97e85ced24970e0628afcdf9 (patch) | |
tree | 731b8b8c8403aa1fbd046813113e6ab54c8f45ea /src/base/wlc/wlcNtk.c | |
parent | fea18c2d42273f1cf100472328ba1c267ba096b3 (diff) | |
download | abc-38e5c8c9e6eaa5fa97e85ced24970e0628afcdf9.tar.gz abc-38e5c8c9e6eaa5fa97e85ced24970e0628afcdf9.tar.bz2 abc-38e5c8c9e6eaa5fa97e85ced24970e0628afcdf9.zip |
%pdra: added an option for disabling incremental solving
Diffstat (limited to 'src/base/wlc/wlcNtk.c')
-rw-r--r-- | src/base/wlc/wlcNtk.c | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 6efa0f6b..d36cff30 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -119,6 +119,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ) pPars->fPushClauses = 0; // Push clauses in the reloaded trace pPars->fMFFC = 1; // Refine the entire MFFC of a PPI pPars->fPdra = 0; // Use pdr -nct + pPars->fLoadTrace = 1; // Load previous PDR traces pPars->fProofRefine = 0; // Use proof-based refinement pPars->fHybrid = 1; // Use a hybrid of CBR and PBR pPars->fCheckCombUnsat = 0; // Check if ABS becomes comb. unsat |