diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-03 19:51:53 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-03 19:51:53 -0800 |
| commit | 45bf0369a84f9fdc55dd8cdc6227bdfd7c146dee (patch) | |
| tree | ec47c75bdec7ce1b52bdfea6b10bb726fbd5947d /src/proof/pdr/pdr.h | |
| parent | a2cebd3e205751bf6e01d509c9568926069b6ab5 (diff) | |
| download | abc-45bf0369a84f9fdc55dd8cdc6227bdfd7c146dee.tar.gz abc-45bf0369a84f9fdc55dd8cdc6227bdfd7c146dee.tar.bz2 abc-45bf0369a84f9fdc55dd8cdc6227bdfd7c146dee.zip | |
Adding structural flop priority heuristics in 'pdr'.
Diffstat (limited to 'src/proof/pdr/pdr.h')
| -rw-r--r-- | src/proof/pdr/pdr.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 9f9ef238..18b059c6 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -53,6 +53,7 @@ struct Pdr_Par_t_ int fTwoRounds; // use two rounds for generalization int fMonoCnf; // monolythic CNF int fNewXSim; // updated X-valued simulation + int fFlopPrio; // use structural flop priorities int fDumpInv; // dump inductive invariant int fUseSupp; // use support in the invariant int fShortest; // forces bug traces to be shortest |