diff options
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/README.md | 4 | ||||
| -rw-r--r-- | src/options/decision_options.toml | 15 | ||||
| -rw-r--r-- | src/options/options_handler.cpp | 8 | ||||
| -rw-r--r-- | src/options/options_handler.h | 5 |
4 files changed, 8 insertions, 24 deletions
diff --git a/src/options/README.md b/src/options/README.md index df5686abc..b0b026166 100644 --- a/src/options/README.md +++ b/src/options/README.md @@ -194,14 +194,14 @@ Full Example [[option.mode.JUSTIFICATION]] name = "justification" help = "An ATGP-inspired justification heuristic." - [[option.mode.RELEVANCY]] + [[option.mode.STOPONLY]] name = "justification-stoponly" help = "Use the justification heuristic only to stop early, not for decisions." This defines a new option that is accessible via `d_options.{module.id}.decisionMode` and stores an automatically generated mode `DecisionMode`, an enum class with the values `INTERNAL`, `JUSTIFICATION` and -`RELEVANCY`. From the outside, it can be set by `--decision=internal`, but also +`STOPONLY`. From the outside, it can be set by `--decision=internal`, but also with `--decision-mode=justification`, and similarly from an SMT-LIB input with `(set-option :decision internal)` and `(set-option :decision-mode justification)`. The command-line help for this option looks as follows: diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml index 8cc2bf2fe..abb27ac9f 100644 --- a/src/options/decision_options.toml +++ b/src/options/decision_options.toml @@ -8,7 +8,6 @@ name = "Decision Heuristics" long = "decision=MODE" type = "DecisionMode" default = "INTERNAL" - predicates = ["setDecisionModeStopOnly"] help = "choose decision mode, see --decision=help" help_mode = "Decision modes." [[option.mode.INTERNAL]] @@ -17,17 +16,15 @@ name = "Decision Heuristics" [[option.mode.JUSTIFICATION]] name = "justification" help = "An ATGP-inspired justification heuristic." +[[option.mode.STOPONLY]] + name = "stoponly" + help = "Use the justification heuristic only to stop early, not for decisions." [[option.mode.JUSTIFICATION_OLD]] name = "justification-old" help = "Older implementation of an ATGP-inspired justification heuristic." -[[option.mode.RELEVANCY]] - name = "justification-stoponly" - help = "Use the justification heuristic only to stop early, not for decisions." - -[[option]] - name = "decisionStopOnly" - category = "undocumented" - type = "bool" +[[option.mode.STOPONLY_OLD]] + name = "stoponly-old" + help = "Use the old implementation of justification heuristic only to stop early, not for decisions." [[option]] name = "decisionThreshold" diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 6958dcb12..e423dc149 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -234,14 +234,6 @@ InstFormatMode OptionsHandler::stringToInstFormatMode(const std::string& option, } } -// decision/options_handlers.h -void OptionsHandler::setDecisionModeStopOnly(const std::string& option, - const std::string& flag, - DecisionMode m) -{ - d_options->decision.decisionStopOnly = (m == DecisionMode::RELEVANCY); -} - void OptionsHandler::setProduceAssertions(const std::string& option, const std::string& flag, bool value) diff --git a/src/options/options_handler.h b/src/options/options_handler.h index bf07729ae..eed361c0d 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -100,11 +100,6 @@ public: const std::string& flag, const std::string& optarg); - // decision/options_handlers.h - void setDecisionModeStopOnly(const std::string& option, - const std::string& flag, - DecisionMode m); - /** * Throws a ModalException if this option is being set after final * initialization. |