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.

3 files changed, 17 insertions, 2 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index fca79aff0..6a6fb2e31 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -300,7 +300,12 @@ operator SEXPR 0: "a symbolic expression"
 
 operator LAMBDA 2 "lambda"
 
-parameterized CHAIN BUILTIN 2: "chain operator"
+parameterized CHAIN CHAIN_OP 2: "chained operator"
+constant CHAIN_OP \
+    ::CVC4::Chain \
+    ::CVC4::ChainHashFunction \
+    "util/chain.h" \
+    "the chained operator"
 
 constant TYPE_CONSTANT \
     ::CVC4::TypeConstant \
@@ -344,6 +349,7 @@ typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
+typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule
 
 constant SUBTYPE_TYPE \
     ::CVC4::Predicate \
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 4d62ce511..392e146ba 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -16,6 +16,7 @@
  **/
 
 #include "theory/builtin/theory_builtin_rewriter.h"
+#include "util/chain.h"
 
 using namespace std;
 
@@ -53,7 +54,7 @@ Node TheoryBuiltinRewriter::blastChain(TNode in) {
 
   Assert(in.getKind() == kind::CHAIN);
 
-  Kind chainedOp = in.getOperator().getConst<Kind>();
+  Kind chainedOp = in.getOperator().getConst<Chain>().getOperator();
 
   if(in.getNumChildren() == 2) {
     // if this is the case exactly 1 pair will be generated so the
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 2a4e07528..a04f9f88a 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -220,6 +220,14 @@ public:
   }
 };/* class ChainTypeRule */
 
+class ChainedOperatorTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    Assert(n.getKind() == kind::CHAIN_OP);
+    return nodeManager->getType(nodeManager->operatorOf(n.getConst<Chain>().getOperator()), check);
+  }
+};/* class ChainedOperatorTypeRule */
+
 class SortProperties {
 public:
   inline static bool isWellFounded(TypeNode type) {