A couple of fixes to the get-option command for compliance with SMT-LIB.

Thanks to David Cok for reporting this issue.

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 3a88a6cbabe9bba317bfe03be2f4df5201405bd5..593f84ced8052d9bae1cd14bfdb3d8213b39915a 100644 (file)
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1228,11 +1228,9 @@ std::string GetOptionCommand::getFlag() const throw() {
 
 void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
-    vector<SExpr> v;
-    v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
-    v.push_back(smtEngine->getOption(d_flag));
+    SExpr res = smtEngine->getOption(d_flag);
     stringstream ss;
-    ss << SExpr(v);
+    ss << res;
     d_result = ss.str();
     d_commandStatus = CommandSuccess::instance();
   } catch(UnrecognizedOptionException&) {

diff --git a/src/options/mkoptions b/src/options/mkoptions
index fa6c4c260915cb5830d2269c6cb7cd0e28dada18..2e152ee078a542c3cc8bb46466898bf5185e318e 100755 (executable)
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -666,13 +666,40 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 
   if [ -n "$smtname" ]; then
     if [ "$internal" != - ]; then
-      smt_getoption_handlers="${smt_getoption_handlers}
+      case "$type" in
+      bool) 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}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    return SExpr(Integer(options::$internal()));
+  }";;
+      float|double) 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}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    return SExpr(options::$internal());
+  }";;
+      *) smt_getoption_handlers="${smt_getoption_handlers}
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
     stringstream ss; ss << options::$internal();
     return SExpr(ss.str());
-  }"
+  }";;
+      esac
     fi
 
     if [ "$type" = bool ]; then