Support for TPTP's TFF0 (with arithmetic)

This commit reverses an "SZS ontology compliance hack" that was
done for CASC-24 this year, and adds a TPTP pretty-printer which
is capable of outputting results in the TPTP way (rather than the
SMT way).

This commit includes minor changes to the Expr package to add
obvious missing functionality, and to fix the way expressions
with builtin operators are made.  These changes are truly a
_fix_, the implementation had not been properly aligned with
the design vision for some corner cases.

7 files changed, 125 insertions, 58 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 524bc2095..3a2feb624 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -304,8 +304,8 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherC
 
 Expr ExprManager::mkExpr(Expr opExpr) {
   const unsigned n = 0;
-  Kind kind = kind::operatorKindToKind(opExpr.getKind());
-  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
                 "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
@@ -323,8 +323,8 @@ Expr ExprManager::mkExpr(Expr opExpr) {
 
 Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
   const unsigned n = 1;
-  Kind kind = kind::operatorKindToKind(opExpr.getKind());
-  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
                 "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
@@ -342,8 +342,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
 
 Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
   const unsigned n = 2;
-  Kind kind = kind::operatorKindToKind(opExpr.getKind());
-  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
                 "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
@@ -363,8 +363,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
 
 Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) {
   const unsigned n = 3;
-  Kind kind = kind::operatorKindToKind(opExpr.getKind());
-  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
                 "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
@@ -386,8 +386,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) {
 Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
                          Expr child4) {
   const unsigned n = 4;
-  Kind kind = kind::operatorKindToKind(opExpr.getKind());
-  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
                 "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
@@ -410,8 +410,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
 Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
                          Expr child4, Expr child5) {
   const unsigned n = 5;
-  Kind kind = kind::operatorKindToKind(opExpr.getKind());
-  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
                 "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
@@ -434,8 +434,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
 
 Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
   const unsigned n = children.size();
-  Kind kind = kind::operatorKindToKind(opExpr.getKind());
-  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+  Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+  CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
                 "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 22d7baac3..8486e8ec3 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -126,18 +126,6 @@ ${metakind_kinds}
   return metaKinds[k + 1];
 }/* metaKindOf(k) */
 
-/**
- * Map a kind of the operator to the kind of the enclosing expression. For
- * example, since the kind of functions is just VARIABLE, it should map
- * VARIABLE to APPLY_UF.
- */
-static inline Kind operatorKindToKind(Kind k) {
-  switch (k) {
-${metakind_operatorKinds}
-  default:
-    return kind::UNDEFINED_KIND;  /* LAST_KIND */
-  };
-}
 }/* CVC4::kind namespace */
 
 namespace expr {
@@ -324,9 +312,29 @@ ${metakind_ubchildren}
 }
 
 }/* CVC4::kind::metakind namespace */
+
+/**
+ * Map a kind of the operator to the kind of the enclosing expression. For
+ * example, since the kind of functions is just VARIABLE, it should map
+ * VARIABLE to APPLY_UF.
+ */
+static inline Kind operatorToKind(::CVC4::expr::NodeValue* nv) {
+  if(nv->getKind() == kind::BUILTIN) {
+    return nv->getConst<Kind>();
+  } else if(nv->getKind() == kind::LAMBDA) {
+    return kind::APPLY_UF;
+  }
+
+  switch(Kind k CVC4_UNUSED = nv->getKind()) {
+${metakind_operatorKinds}
+  default:
+    return kind::UNDEFINED_KIND;  /* LAST_KIND */
+  };
+}
+
 }/* CVC4::kind namespace */
 
-#line 330 "${template}"
+#line 338 "${template}"
 
 namespace theory {
 
diff --git a/src/expr/node.h b/src/expr/node.h
index d9e88d8af..99e1e7ee7 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1337,7 +1337,11 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
   NodeBuilder<> nb(getKind());
   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
     // push the operator
-    nb << getOperator();
+    if(getOperator() == node) {
+      nb << replacement;
+    } else {
+      nb << getOperator().substitute(node, replacement, cache);
+    }
   }
   for(const_iterator i = begin(),
         iend = end();
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 1f098b4e8..64080c275 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -660,6 +660,9 @@ public:
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
     Assert(!n.isNull(), "Cannot use NULL Node as a child of a Node");
+    if(n.getKind() == kind::BUILTIN) {
+      return *this << NodeManager::operatorToKind(n);
+    }
     allocateNvIfNecessaryForAppend();
     expr::NodeValue* nv = n.d_nv;
     nv->inc();
@@ -980,7 +983,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
 #if 0
   // if the kind is PARAMETERIZED, check that the operator is correctly-kinded
   Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED ||
-         kind::operatorKindToKind(getOperator().getKind()) == getKind(),
+         NodeManager::operatorToKind(getOperator()) == getKind(),
          "Attempted to construct a parameterized kind `%s' with "
          "incorrectly-kinded operator `%s'",
          kind::kindToString(getKind()).c_str(),
@@ -1165,7 +1168,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
 #if 0
   // if the kind is PARAMETERIZED, check that the operator is correctly-kinded
   Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED ||
-         kind::operatorKindToKind(getOperator().getKind()) == getKind(),
+         NodeManager::operatorToKind(getOperator()) == getKind(),
          "Attempted to construct a parameterized kind `%s' with "
          "incorrectly-kinded operator `%s'",
          kind::kindToString(getKind()).c_str(),
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 0c62d31c5..913b8befb 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -353,6 +353,9 @@ public:
     d_listeners.erase(elt);
   }
 
+  /** Get a Kind from an operator expression */
+  static inline Kind operatorToKind(TNode n);
+
   // general expression-builders
 
   /** Create a node with one child. */
@@ -1280,6 +1283,10 @@ inline TypeNode NodeManager::mkSortConstructor(const std::string& name,
   return type;
 }
 
+inline Kind NodeManager::operatorToKind(TNode n) {
+  return kind::operatorToKind(n.d_nv);
+}
+
 inline Node NodeManager::mkNode(Kind kind, TNode child1) {
   NodeBuilder<1> nb(this, kind);
   nb << child1;
@@ -1367,80 +1374,114 @@ inline Node* NodeManager::mkNodePtr(Kind kind,
 
 // for operators
 inline Node NodeManager::mkNode(TNode opNode) {
-  NodeBuilder<1> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode;
+  NodeBuilder<1> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode) {
-  NodeBuilder<1> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode;
+  NodeBuilder<1> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
   return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
-  NodeBuilder<2> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1;
+  NodeBuilder<2> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
-  NodeBuilder<2> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1;
+  NodeBuilder<2> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1;
   return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
-  NodeBuilder<3> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2;
+  NodeBuilder<3> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
-  NodeBuilder<3> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2;
+  NodeBuilder<3> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2;
   return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
                                 TNode child3) {
-  NodeBuilder<4> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2 << child3;
+  NodeBuilder<4> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2 << child3;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
                                 TNode child3) {
-  NodeBuilder<4> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2 << child3;
+  NodeBuilder<4> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2 << child3;
   return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
                                 TNode child3, TNode child4) {
-  NodeBuilder<5> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2 << child3 << child4;
+  NodeBuilder<5> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2 << child3 << child4;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
                                 TNode child3, TNode child4) {
-  NodeBuilder<5> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2 << child3 << child4;
+  NodeBuilder<5> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2 << child3 << child4;
   return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
                                 TNode child3, TNode child4, TNode child5) {
-  NodeBuilder<6> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2 << child3 << child4 << child5;
+  NodeBuilder<6> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2 << child3 << child4 << child5;
   return nb.constructNode();
 }
 
 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
                                     TNode child3, TNode child4, TNode child5) {
-  NodeBuilder<6> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode << child1 << child2 << child3 << child4 << child5;
+  NodeBuilder<6> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
+  nb << child1 << child2 << child3 << child4 << child5;
   return nb.constructNodePtr();
 }
 
@@ -1449,8 +1490,10 @@ template <bool ref_count>
 inline Node NodeManager::mkNode(TNode opNode,
                                 const std::vector<NodeTemplate<ref_count> >&
                                 children) {
-  NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode;
+  NodeBuilder<> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
   nb.append(children);
   return nb.constructNode();
 }
@@ -1459,8 +1502,10 @@ template <bool ref_count>
 inline Node* NodeManager::mkNodePtr(TNode opNode,
                                     const std::vector<NodeTemplate<ref_count> >&
                                     children) {
-  NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
-  nb << opNode;
+  NodeBuilder<> nb(this, operatorToKind(opNode));
+  if(opNode.getKind() != kind::BUILTIN) {
+    nb << opNode;
+  }
   nb.append(children);
   return nb.constructNodePtr();
 }
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 71c25bd50..f3cf992ba 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -317,6 +317,10 @@ bool Type::isSubrange() const {
   return d_typeNode->isSubrange();
 }
 
+size_t FunctionType::getArity() const {
+  return d_typeNode->getNumChildren() - 1;
+}
+
 vector<Type> FunctionType::getArgTypes() const {
   NodeManagerScope nms(d_nodeManager);
   vector<Type> args;
diff --git a/src/expr/type.h b/src/expr/type.h
index 5e4e86264..3c772d461 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -415,6 +415,9 @@ public:
   /** Construct from the base type */
   FunctionType(const Type& type = Type()) throw(IllegalArgumentException);
 
+  /** Get the arity of the function type */
+  size_t getArity() const;
+
   /** Get the argument types */
   std::vector<Type> getArgTypes() const;