support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary define-fun; several set-info, set-option, get-option, get-info improvementss

2 files changed, 14 insertions, 6 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 8c90f337e..15fea22da 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -352,7 +352,9 @@ GetInfoCommand::GetInfoCommand(std::string flag) :
 
 void GetInfoCommand::invoke(SmtEngine* smtEngine) {
   try {
-    d_result = smtEngine->getInfo(d_flag).getValue();
+    stringstream ss;
+    ss << smtEngine->getInfo(d_flag);
+    d_result = ss.str();
   } catch(BadOptionException& bo) {
     d_result = "unsupported";
   }
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index c4968af26..351893feb 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -195,9 +195,9 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > {
 }
 
 function registerOperatorToKind {
-	operatorKind=$1
-	applyKind=$2
-	metakind_operatorKinds="${metakind_operatorKinds}    case kind::$applyKind: return kind::$operatorKind;
+  operatorKind=$1
+  applyKind=$2
+  metakind_operatorKinds="${metakind_operatorKinds}    case kind::$applyKind: return kind::$operatorKind;
 ";
 }
 
@@ -227,8 +227,14 @@ function register_metakind {
     exit 1
   fi
 
-  if [ $mk = OPERATOR ] || [ $mk = PARAMETERIZED -a "$k" != SORT_TYPE ]; then
-    if [ $lb = 0 ]; then
+  if [ $mk = OPERATOR -o $mk = PARAMETERIZED ]; then
+    if [ $mk = PARAMETERIZED -a "$k" = SORT_TYPE ]; then
+      # exception: zero-ary SORT_TYPE is permitted for sort constructors
+      :
+    elif [ $mk = PARAMETERIZED -a "$k" = APPLY ]; then
+      # exception: zero-ary APPLY is permitted for defined zero-ary functions
+      :
+    elif [ $lb = 0 ]; then
       echo "$kf:$lineno: error in range \`$nc' for \`$k': $mk-kinded kinds must always take at least one child" >&2
       exit 1
     fi