diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-11-27 19:02:50 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-11-27 19:02:50 +0000 |
| commit | 95dcbc6781cd8e62f8436f0cfe944b21dfd60ec0 (patch) | |
| tree | e0259b9f2993e397e662d6c71a74e473133850b1 /src/decision/options_handlers.h | |
| parent | 0697e19c09a8ac5f1d9c30ee053845f06ea39c0e (diff) | |
Simplify --help=decision with only currently supported options
Add notice/warning when using incremental-mode + decision (it was
already disabled)
Some other minor cleanup
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/decision/options_handlers.h')
| -rw-r--r-- | src/decision/options_handlers.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h index fd05a0c9f..826bd8acb 100644 --- a/src/decision/options_handlers.h +++ b/src/decision/options_handlers.h @@ -36,6 +36,9 @@ justification\n\ \n\ justification-stoponly\n\ + Use the justification heuristic only to stop early, not for decisions\n\ +"; +/** Under-development options, commenting out from help for the release */ +/* \n\ relevancy\n\ + Under development may-relevancy\n\ @@ -52,7 +55,7 @@ justification-rel\n\ justification-must\n\ + Start deciding on literals close to root instead of those\n\ + near leaves (don't expect it to work well) [Unimplemented]\n\ -"; +";*/ inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { options::decisionRelevancyLeaves.set(false); |