From f370dbd93ba38f4619a0d63abb8a01e2a8482861 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 23 Jul 2013 16:59:45 -0400
Subject: [PATCH] Some fixes for (get-info :all-options)

---
 src/options/mkoptions            | 34 ++++++++++++++++++++++++++++++--
 src/options/options_template.cpp | 20 +++++++++----------
 2 files changed, 42 insertions(+), 12 deletions(-)

diff --git a/src/options/mkoptions b/src/options/mkoptions
index bfb35ff26..d856c7293 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -675,14 +675,14 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
       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); }"
+  }{ std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(SExpr::Keyword(d_holder->$internal ? \"true\" : \"false\")); 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)
+      int|unsigned|int*_t|uint*_t|unsigned\ long|long|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); }"
@@ -783,6 +783,36 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
     return;
   }"
     fi
+  elif [ -n "$long_option" -o "$long_option_alternate" ] && [ "$internal" != - ]; then
+    case "$type" in
+    bool)
+      getoption_name="$long_option"
+      inv=
+      # case where we have a --disable but no corresponding --enable
+      if [ -z "$getoption_name" ]; then
+        getoption_name="$long_option_alternate"
+        inv='!'
+      fi
+      all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
+#line $lineno \"$kf\"
+  }{ std::vector<SExpr> v; v.push_back(\"$getoption_name\"); v.push_back(SExpr::Keyword((${inv}d_holder->$internal) ? \"true\" : \"false\")); opts.push_back(v); }";;
+    int|unsigned|int*_t|uint*_t|unsigned\ long|long|CVC4::Integer)
+        all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
+#line $lineno \"$kf\"
+  }{ std::vector<SExpr> v; v.push_back(\"$long_option\"); v.push_back(d_holder->$internal); opts.push_back(v); }";;
+    float|double)
+      all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
+#line $lineno \"$kf\"
+  }{ std::vector<SExpr> v; v.push_back(\"$long_option\"); v.push_back(Rational::fromDouble(d_holder->$internal)); opts.push_back(v); }";;
+    CVC4::Rational)
+      all_modules_get_options="${all_modules_get_options:+$all_modules_get_options
+#line $lineno \"$kf\"
+  }{ std::vector<SExpr> v; v.push_back(\"$long_option\"); v.push_back(d_holder->$internal); opts.push_back(v); }";;
+    *)
+      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(\"$long_option\"); v.push_back(ss.str()); opts.push_back(v); }";;
+    esac
   fi
 
   if [ "$type" = bool ]; then
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 04d8adaa0..8af61b79f 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -49,7 +49,7 @@
 
 ${include_all_option_headers}
 
-#line 53 "${template}"
+#line 57 "${template}"
 
 #include "util/output.h"
 #include "options/options_holder.h"
@@ -58,7 +58,7 @@ ${include_all_option_headers}
 
 ${option_handler_includes}
 
-#line 62 "${template}"
+#line 66 "${template}"
 
 using namespace CVC4;
 using namespace CVC4::options;
@@ -195,7 +195,7 @@ void runBoolPredicates(T, std::string option, bool b, SmtEngine* smt) {
 
 ${all_custom_handlers}
 
-#line 199 "${template}"
+#line 203 "${template}"
 
 #ifdef CVC4_DEBUG
 #  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
@@ -225,18 +225,18 @@ options::OptionsHolder::OptionsHolder() : ${all_modules_defaults}
 {
 }
 
-#line 229 "${template}"
+#line 233 "${template}"
 
 static const std::string mostCommonOptionsDescription = "\
 Most commonly-used CVC4 options:${common_documentation}";
 
-#line 234 "${template}"
+#line 238 "${template}"
 
 static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
 \n\
 Additional CVC4 options:${remaining_documentation}";
 
-#line 240 "${template}"
+#line 244 "${template}"
 
 static const std::string optionsFootnote = "\n\
 [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
@@ -307,7 +307,7 @@ static struct option cmdlineOptions[] = {${all_modules_long_options}
   { NULL, no_argument, NULL, '\0' }
 };/* cmdlineOptions */
 
-#line 311 "${template}"
+#line 315 "${template}"
 
 static void preemptGetopt(int& argc, char**& argv, const char* opt) {
   const size_t maxoptlen = 128;
@@ -500,7 +500,7 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro
     switch(c) {
 ${all_modules_option_handlers}
 
-#line 492 "${template}"
+#line 508 "${template}"
 
     case ':':
       // This can be a long or short option, and the way to get at the
@@ -572,7 +572,7 @@ std::vector<std::string> Options::suggestCommandLineOptions(const std::string& o
 
 static const char* smtOptions[] = {
   ${all_modules_smt_options},
-#line 547 "${template}"
+#line 590 "${template}"
   NULL
 };/* smtOptions[] */
 
@@ -594,7 +594,7 @@ SExpr Options::getOptions() const throw() {
 
   ${all_modules_get_options}
 
-#line 569 "${template}"
+#line 612 "${template}"
 
   return SExpr(opts);
 }
-- 
2.30.2