From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 23 Jul 2013 15:55:39 +0000 (-0400)
Subject: (get-info :all-options) to get option values; also command-line option suggestions
X-Git-Tag: cvc5-1.0.0~7287^2~50
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e12e7b9f980ec3f2b3db6de73e5fbe6f0daa1c00;p=cvc5.git

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

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 {
 
@@ -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 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
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2cddc29cf..927b8fe6f 100644
--- 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();
   }