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/wlc.h | |
| 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/wlc.h')
| -rw-r--r-- | src/base/wlc/wlc.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 229a6bfb..7086cc9f 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -175,6 +175,7 @@ struct Wlc_Par_t_ int fPushClauses; // Push clauses in the reloaded trace int fMFFC; // Refine the entire MFFC of a PPI int fPdra; // Use pdr -nct + int fLoadTrace; // Load previous traces if any int fProofRefine; // Use proof-based refinement int fHybrid; // Use a hybrid of CBR and PBR int fCheckCombUnsat; // Check if ABS becomes comb. unsat |