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.

1 files changed, 50 insertions, 0 deletions

diff --git a/src/util/chain.h b/src/util/chain.h
new file mode 100644
index 000000000..2e9cf7bf6
--- /dev/null
+++ b/src/util/chain.h
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file chain.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__CHAIN_H
+#define __CVC4__CHAIN_H
+
+#include "expr/kind.h"
+#include <iostream>
+
+namespace CVC4 {
+
+/** A class to represent a chained, built-in operator. */
+class Chain {
+  Kind d_kind;
+public:
+  explicit Chain(Kind k) : d_kind(k) { }
+  bool operator==(const Chain& ch) const { return d_kind == ch.d_kind; }
+  bool operator!=(const Chain& ch) const { return d_kind != ch.d_kind; }
+  Kind getOperator() const { return d_kind; }
+};/* class Chain */
+
+inline std::ostream& operator<<(std::ostream& out, const Chain& ch) {
+  return out << ch.getOperator();
+}
+
+struct ChainHashFunction {
+  size_t operator()(const Chain& ch) const {
+    return kind::KindHashFunction()(ch.getOperator());
+  }
+};/* struct ChainHashFunction */
+
+}/* CVC4 namespace */
+
+#endif  /* __CVC4__CHAIN_H */