Fix for bug 115, mapping was going in the wrong direction.

3 files changed, 18 insertions, 15 deletions

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 57bfc51e5..5b0ac150b 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -148,13 +148,11 @@ ${metakind_canbeatomic}
  * VARIABLE to APPLY_UF.
  */
 static inline Kind operatorKindToKind(Kind k) {
-  static const Kind kind2kind[] = {
-    kind::UNDEFINED_KIND, /* NULL_EXPR */
+  switch (k) {
 ${metakind_operatorKinds}
-    kind::UNDEFINED_KIND  /* LAST_KIND */
+  default:
+    return kind::UNDEFINED_KIND;  /* LAST_KIND */
   };
-
-  return kind2kind[k];
 }
 }/* CVC4::kind namespace */
 
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index e8f3724f1..4915a17ec 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -87,7 +87,7 @@ function variable {
   lineno=${BASH_LINENO[0]}
 
   check_theory_seen
-  register_metakind VARIABLE "$1" UNDEFINED_KIND 0
+  register_metakind VARIABLE "$1" 0
 }
 
 function operator {
@@ -96,7 +96,7 @@ function operator {
   lineno=${BASH_LINENO[0]}
 
   check_theory_seen
-  register_metakind OPERATOR "$1" UNDEFINED_KIND "$2"
+  register_metakind OPERATOR "$1" "$2"
 }
 
 function nonatomic_operator {
@@ -105,7 +105,7 @@ function nonatomic_operator {
   lineno=${BASH_LINENO[0]}
 
   check_theory_seen
-  register_metakind NONATOMIC_OPERATOR "$1" UNDEFINED_KIND "$2"
+  register_metakind NONATOMIC_OPERATOR "$1" "$2"
 }
 
 function parameterized {
@@ -114,7 +114,8 @@ function parameterized {
   lineno=${BASH_LINENO[0]}
 
   check_theory_seen
-  register_metakind PARAMETERIZED "$1" "$2" "$3"
+  register_metakind PARAMETERIZED "$1" "$3"
+  registerOperatorToKind "$1" "$2"
 }
 
 function constant {
@@ -142,7 +143,7 @@ function constant {
     metakind_includes="${metakind_includes}
 #include \"$4\""
   fi
-  register_metakind CONSTANT "$1" UNDEFINED_KIND 0
+  register_metakind CONSTANT "$1" 0
   metakind_constantMaps="${metakind_constantMaps}
 }/* CVC4::kind::metakind namespace */
 }/* CVC4::kind namespace */
@@ -204,14 +205,18 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > {
 "
 }
 
+function registerOperatorToKind {
+	operatorKind=$1
+	applyKind=$2
+	metakind_operatorKinds="${metakind_operatorKinds}    case kind::$applyKind: return kind::$operatorKind;
+"; 
+}
+
 function register_metakind {
   mk=$1
   k=$2
-  k1=$3
-  nc=$4
+  nc=$3
 
-  metakind_operatorKinds="${metakind_operatorKinds}    kind::$k1, /* $k */
-"; 
 
   if [ $mk = NONATOMIC_OPERATOR ]; then
     metakind_canbeatomic="${metakind_canbeatomic}    false, /* $k */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index ab8199d1e..4bda235f5 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -871,7 +871,7 @@ template <bool ref_count>
 inline Node* NodeManager::mkNodePtr(TNode opNode,
                                 const std::vector<NodeTemplate<ref_count> >&
                                 children) {
-  return NodeBuilder<>(this, kind::operatorKindToKind(opNode.getKind())).constructNodePtr();
+  return NodeBuilder<>(this, kind::operatorKindToKind(opNode.getKind())).append(children).constructNodePtr();
 }