(get-info :all-options) to get option values; also command-line option suggestions

3 files changed, 96 insertions, 5 deletions

diff --git a/src/options/mkoptions b/src/options/mkoptions
index 2e152ee07..bfb35ff26 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -73,7 +73,9 @@ options_cpp_template="$1"; shift
 all_modules_defaults=
 all_modules_short_options=
 all_modules_long_options=
+all_modules_smt_options=
 all_modules_option_handlers=
+all_modules_get_options=
 smt_getoption_handlers=
 smt_setoption_handlers=
 include_all_option_headers=
@@ -665,34 +667,57 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
   fi
 
   if [ -n "$smtname" ]; then
+    all_modules_smt_options="${all_modules_smt_options:+$all_modules_smt_options,}
+#line $lineno \"$kf\"
+  \"$smtname\""
     if [ "$internal" != - ]; then
       case "$type" in
-      bool) smt_getoption_handlers="${smt_getoption_handlers}
+      bool)
+        all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
+#line $lineno \"$kf\"
+  }{ std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(d_holder->$internal); opts.push_back(v); }"
+        smt_getoption_handlers="${smt_getoption_handlers}
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
     return SExprKeyword(options::$internal() ? \"true\" : \"false\");
   }";;
-      int|unsigned|int*_t|uint*_t|CVC4::Integer) smt_getoption_handlers="${smt_getoption_handlers}
+      int|unsigned|int*_t|uint*_t|CVC4::Integer)
+        all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
+#line $lineno \"$kf\"
+  }{ std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(d_holder->$internal); opts.push_back(v); }"
+        smt_getoption_handlers="${smt_getoption_handlers}
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
     return SExpr(Integer(options::$internal()));
   }";;
-      float|double) smt_getoption_handlers="${smt_getoption_handlers}
+      float|double)
+        all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
+#line $lineno \"$kf\"
+  }{ std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(Rational::fromDouble(d_holder->$internal)); opts.push_back(v); }"
+        smt_getoption_handlers="${smt_getoption_handlers}
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
     stringstream ss; ss << std::fixed << options::$internal();
     return SExpr(Rational::fromDecimal(ss.str()));
   }";;
-      CVC4::Rational) smt_getoption_handlers="${smt_getoption_handlers}
+      CVC4::Rational)
+        all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
+#line $lineno \"$kf\"
+  }{ std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(d_holder->$internal); opts.push_back(v); }"
+        smt_getoption_handlers="${smt_getoption_handlers}
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
     return SExpr(options::$internal());
   }";;
-      *) smt_getoption_handlers="${smt_getoption_handlers}
+      *)
+        all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
+#line $lineno \"$kf\"
+  }{ std::stringstream ss; ss << d_holder->$internal; std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(ss.str()); opts.push_back(v); }"
+        smt_getoption_handlers="${smt_getoption_handlers}
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
@@ -1473,7 +1498,9 @@ for var in \
     all_modules_defaults \
     all_modules_short_options \
     all_modules_long_options \
+    all_modules_smt_options \
     all_modules_option_handlers \
+    all_modules_get_options \
     include_all_option_headers \
     all_modules_contributions \
     all_custom_handlers \
diff --git a/src/options/options.h b/src/options/options.h
index 2be0e7b51..eaafade93 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -27,6 +27,7 @@
 #include "options/option_exception.h"
 #include "util/language.h"
 #include "util/tls.h"
+#include "util/sexpr.h"
 
 namespace CVC4 {
 
@@ -118,12 +119,33 @@ 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.
+   */
+  static std::vector<std::string> suggestCommandLineOptions(const std::string& optionName) throw();
+
+  /**
+   * Look up SMT 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.
+   */
+  static std::vector<std::string> suggestSmtOptions(const std::string& optionName) throw();
+
+  /**
    * Initialize the options based on the given command-line arguments.
    * The return value is what's left of the command line (that is, the
    * non-option arguments).
    */
   std::vector<std::string> parseOptions(int argc, char* argv[]) throw(OptionException);
 
+  /**
+   * Get the setting for all options.
+   */
+  SExpr getOptions() const throw();
+
 };/* class Options */
 
 }/* CVC4 namespace */
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 81ffe1b27..7888beec3 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -518,6 +518,48 @@ ${all_modules_option_handlers}
   return nonOptions;
 }
 
+std::vector<std::string> Options::suggestCommandLineOptions(const std::string& optionName) throw() {
+  std::vector<std::string> suggestions;
+
+  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);
+    }
+  }
+
+  return suggestions;
+}
+
+static const char* smtOptions[] = {
+  ${all_modules_smt_options},
+#line 547 "${template}"
+  NULL
+};/* smtOptions[] */
+
+std::vector<std::string> Options::suggestSmtOptions(const std::string& optionName) throw() {
+  std::vector<std::string> suggestions;
+
+  const char* opt;
+  for(size_t i = 0; (opt = smtOptions[i]) != NULL; ++i) {
+    if(std::strstr(opt, optionName.c_str()) != NULL) {
+      suggestions.push_back(opt);
+    }
+  }
+
+  return suggestions;
+}
+
+SExpr Options::getOptions() const throw() {
+  std::vector<SExpr> opts;
+
+  ${all_modules_get_options}
+
+#line 569 "${template}"
+
+  return SExpr(opts);
+}
+
 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT