summaryrefslogtreecommitdiff
path: root/src/options
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2014-04-19 16:44:20 -0400
committerKshitij Bansal <kshitij@cs.nyu.edu>2014-04-19 19:45:18 -0400
commite6b834f2976c736b6e9df1cc017bc2d72c00b27c (patch)
treedd5d0c6b880cb2a33ff004c3be26711f0f24c165 /src/options
parentc0314861bfae3fac04bcd60ac42a3592bb73441f (diff)
Eh, what?
Diffstat (limited to 'src/options')
-rw-r--r--src/options/base_options_handlers.h23
-rw-r--r--src/options/options.h13
-rw-r--r--src/options/options_template.cpp36
3 files changed, 43 insertions, 29 deletions
diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h
index 2298f5880..3779f75c1 100644
--- a/src/options/base_options_handlers.h
+++ b/src/options/base_options_handlers.h
@@ -3,9 +3,9 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Kshitij Bansal
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
@@ -25,6 +25,7 @@
#include <sstream>
#include "expr/command.h"
+#include "util/didyoumean.h"
#include "util/language.h"
namespace CVC4 {
@@ -99,11 +100,24 @@ inline InputLanguage stringToInputLanguage(std::string option, std::string optar
Unreachable();
}
+inline std::string suggestTags(char const* const* validTags, std::string inputTag)
+{
+ DidYouMean didYouMean;
+
+ const char* opt;
+ for(size_t i = 0; (opt = validTags[i]) != NULL; ++i) {
+ didYouMean.addWord(validTags[i]);
+ }
+
+ return didYouMean.getMatchAsString(inputTag);
+}
+
inline void addTraceTag(std::string option, std::string optarg, SmtEngine* smt) {
if(Configuration::isTracingBuild()) {
if(!Configuration::isTraceTag(optarg.c_str()))
throw OptionException(std::string("trace tag ") + optarg +
- std::string(" not available"));
+ std::string(" not available.") +
+ suggestTags(Configuration::getTraceTags(), optarg) );
} else {
throw OptionException("trace tags not available in non-tracing builds");
}
@@ -115,7 +129,8 @@ inline void addDebugTag(std::string option, std::string optarg, SmtEngine* smt)
if(!Configuration::isDebugTag(optarg.c_str()) &&
!Configuration::isTraceTag(optarg.c_str())) {
throw OptionException(std::string("debug tag ") + optarg +
- std::string(" not available"));
+ std::string(" not available.") +
+ suggestTags(Configuration::getDebugTags(), optarg) );
}
} else if(! Configuration::isDebugBuild()) {
throw OptionException("debug tags not available in non-debug builds");
diff --git a/src/options/options.h b/src/options/options.h
index eaafade93..b41c9a66e 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -3,9 +3,9 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Kshitij Bansal
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
@@ -119,12 +119,11 @@ public:
static void printLanguageHelp(std::ostream& out);
/**
- * Look up long command-line option names that bear some similarity to
- * the given name. Don't include the initial "--". This might be
- * useful in case of typos. Can return an empty vector if there are
- * no suggestions.
+ * Look up long command-line option names that bear some similarity
+ * to the given name. Returns an empty string if there are no
+ * suggestions.
*/
- static std::vector<std::string> suggestCommandLineOptions(const std::string& optionName) throw();
+ static std::string suggestCommandLineOptions(const std::string& optionName) throw();
/**
* Look up SMT option names that bear some similarity to
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 02bfc6ca0..fc8b31d49 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -3,7 +3,7 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Kshitij Bansal
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
@@ -47,13 +47,14 @@ extern int optreset;
#include "expr/expr.h"
#include "util/configuration.h"
+#include "util/didyoumean.h"
#include "util/exception.h"
#include "util/language.h"
#include "util/tls.h"
${include_all_option_headers}
-#line 57 "${template}"
+#line 58 "${template}"
#include "util/output.h"
#include "options/options_holder.h"
@@ -62,7 +63,7 @@ ${include_all_option_headers}
${option_handler_includes}
-#line 66 "${template}"
+#line 67 "${template}"
using namespace CVC4;
using namespace CVC4::options;
@@ -199,7 +200,7 @@ void runBoolPredicates(T, std::string option, bool b, SmtEngine* smt) {
${all_custom_handlers}
-#line 203 "${template}"
+#line 204 "${template}"
#ifdef CVC4_DEBUG
# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
@@ -229,18 +230,18 @@ options::OptionsHolder::OptionsHolder() : ${all_modules_defaults}
{
}
-#line 233 "${template}"
+#line 234 "${template}"
static const std::string mostCommonOptionsDescription = "\
Most commonly-used CVC4 options:${common_documentation}";
-#line 238 "${template}"
+#line 239 "${template}"
static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
\n\
Additional CVC4 options:${remaining_documentation}";
-#line 244 "${template}"
+#line 245 "${template}"
static const std::string optionsFootnote = "\n\
[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
@@ -312,7 +313,7 @@ static struct option cmdlineOptions[] = {${all_modules_long_options}
{ NULL, no_argument, NULL, '\0' }
};/* cmdlineOptions */
-#line 316 "${template}"
+#line 317 "${template}"
static void preemptGetopt(int& argc, char**& argv, const char* opt) {
const size_t maxoptlen = 128;
@@ -505,7 +506,7 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro
switch(c) {
${all_modules_option_handlers}
-#line 509 "${template}"
+#line 510 "${template}"
case ':':
// This can be a long or short option, and the way to get at the
@@ -549,7 +550,8 @@ ${all_modules_option_handlers}
break;
}
- throw OptionException(std::string("can't understand option `") + option + "'");
+ throw OptionException(std::string("can't understand option `") + option + "'"
+ + suggestCommandLineOptions(option));
}
}
@@ -558,22 +560,20 @@ ${all_modules_option_handlers}
return nonOptions;
}
-std::vector<std::string> Options::suggestCommandLineOptions(const std::string& optionName) throw() {
- std::vector<std::string> suggestions;
+std::string Options::suggestCommandLineOptions(const std::string& optionName) throw() {
+ DidYouMean didYouMean;
const char* opt;
for(size_t i = 0; (opt = cmdlineOptions[i].name) != NULL; ++i) {
- if(std::strstr(opt, optionName.c_str()) != NULL) {
- suggestions.push_back(opt);
- }
+ didYouMean.addWord(std::string("--") + cmdlineOptions[i].name);
}
- return suggestions;
+ return didYouMean.getMatchAsString(optionName);
}
static const char* smtOptions[] = {
${all_modules_smt_options},
-#line 577 "${template}"
+#line 589 "${template}"
NULL
};/* smtOptions[] */
@@ -595,7 +595,7 @@ SExpr Options::getOptions() const throw() {
${all_modules_get_options}
-#line 599 "${template}"
+#line 611 "${template}"
return SExpr(opts);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback