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

diff --git a/src/options/mkoptions b/src/options/mkoptions
index 2e152ee078a542c3cc8bb46466898bf5185e318e..bfb35ff26a16f1986e461951cc7a6f431f3f847f 100755 (executable)
--- 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 2be0e7b51ff2b8aa3ef8ec414f1ede7c431df261..eaafade936bc247f10fa29df6caf6b261321c2c9 100644 (file)
--- 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 {
 
@@ -117,6 +118,22 @@ public:
   /** Print help for the --lang command line option */
   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
@@ -124,6 +141,11 @@ public:
    */
   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 81ffe1b274a66c59bc65cb54a18ed8a8e9906586..7888beec39c7434e081bed5f8660e82fb5a7ff78 100644 (file)
--- 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
 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2cddc29cf9a5f9f5b09ee5069ddbe9dcf1b11275..927b8fe6f52e008587ed005a984350f3d7ee3ef0 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1196,6 +1196,9 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
       throw ModalException("Can't get-info :reason-unknown when the "
                            "last result wasn't unknown!");
     }
+  } else if(key == "all-options") {
+    // get the options, like all-statistics
+    return Options::current().getOptions();
   } else {
     throw UnrecognizedOptionException();
   }