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, 24 insertions, 11 deletions

diff --git a/src/util/result.h b/src/util/result.h
index cb1bd50fa..54ec3a38c 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -71,47 +71,58 @@ private:
   enum Validity d_validity;
   enum Type d_which;
   enum UnknownExplanation d_unknownExplanation;
+  std::string d_inputName;
 
 public:
-  Result() :
+  Result(std::string inputName = "") :
     d_sat(SAT_UNKNOWN),
     d_validity(VALIDITY_UNKNOWN),
     d_which(TYPE_NONE),
-    d_unknownExplanation(UNKNOWN_REASON) {
+    d_unknownExplanation(UNKNOWN_REASON),
+    d_inputName(inputName) {
   }
-  Result(enum Sat s) :
+  Result(enum Sat s, std::string inputName = "") :
     d_sat(s),
     d_validity(VALIDITY_UNKNOWN),
     d_which(TYPE_SAT),
-    d_unknownExplanation(UNKNOWN_REASON) {
+    d_unknownExplanation(UNKNOWN_REASON),
+    d_inputName(inputName) {
     CheckArgument(s != SAT_UNKNOWN,
                   "Must provide a reason for satisfiability being unknown");
   }
-  Result(enum Validity v) :
+  Result(enum Validity v, std::string inputName = "") :
     d_sat(SAT_UNKNOWN),
     d_validity(v),
     d_which(TYPE_VALIDITY),
-    d_unknownExplanation(UNKNOWN_REASON) {
+    d_unknownExplanation(UNKNOWN_REASON),
+    d_inputName(inputName) {
     CheckArgument(v != VALIDITY_UNKNOWN,
                   "Must provide a reason for validity being unknown");
   }
-  Result(enum Sat s, enum UnknownExplanation unknownExplanation) :
+  Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = "") :
     d_sat(s),
     d_validity(VALIDITY_UNKNOWN),
     d_which(TYPE_SAT),
-    d_unknownExplanation(unknownExplanation) {
+    d_unknownExplanation(unknownExplanation),
+    d_inputName(inputName) {
     CheckArgument(s == SAT_UNKNOWN,
                   "improper use of unknown-result constructor");
   }
-  Result(enum Validity v, enum UnknownExplanation unknownExplanation) :
+  Result(enum Validity v, enum UnknownExplanation unknownExplanation, std::string inputName = "") :
     d_sat(SAT_UNKNOWN),
     d_validity(v),
     d_which(TYPE_VALIDITY),
-    d_unknownExplanation(unknownExplanation) {
+    d_unknownExplanation(unknownExplanation),
+    d_inputName(inputName) {
     CheckArgument(v == VALIDITY_UNKNOWN,
                   "improper use of unknown-result constructor");
   }
-  Result(const std::string& s);
+  Result(const std::string& s, std::string inputName = "");
+
+  Result(const Result& r, std::string inputName) {
+    *this = r;
+    d_inputName = inputName;
+  }
 
   enum Sat isSat() const {
     return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
@@ -142,6 +153,8 @@ public:
 
   std::string toString() const;
 
+  std::string getInputName() const { return d_inputName; }
+
 };/* class Result */
 
 inline bool Result::operator!=(const Result& r) const throw() {