From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 17 May 2013 13:27:55 +0000 (-0400)
Subject: A couple of fixes to the get-option command for compliance with SMT-LIB.
X-Git-Tag: cvc5-1.0.0~7287^2~33^2~23
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dee8aad2f6e54738ad26266618ae71d98e31aa54;p=cvc5.git

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 3a88a6cba..593f84ced 100644
--- 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 fa6c4c260..2e152ee07 100755
--- 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