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, 108 insertions, 22 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 51eb5cb1a..23318b95d 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -77,6 +77,7 @@ libutil_la_SOURCES = \
 	ite_removal.h \
 	ite_removal.cpp \
 	node_visitor.h \
+	chain.h \
 	index.h \
 	uninterpreted_constant.h \
 	uninterpreted_constant.cpp \
@@ -139,7 +140,8 @@ EXTRA_DIST = \
 	rational.i \
 	hash.i \
 	predicate.i \
-	uninterpreted_constant.i
+	uninterpreted_constant.i \
+	chain.i
 
 DISTCLEANFILES = \
 	integer.h.tmp \
diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h
index e5c4ead6c..be39f69c1 100644
--- a/src/util/boolean_simplification.h
+++ b/src/util/boolean_simplification.h
@@ -22,6 +22,7 @@
 #include <vector>
 #include <algorithm>
 
+#include "expr/expr_manager_scope.h"
 #include "expr/node.h"
 #include "util/cvc4_assert.h"
 
@@ -202,6 +203,7 @@ public:
    * @param e the Expr to negate (cannot be the null Expr)
    */
   static Expr negate(Expr e) throw(AssertionException) {
+    ExprManagerScope ems(e);
     return negate(Node::fromExpr(e)).toExpr();
   }
 
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 */
diff --git a/src/util/chain.i b/src/util/chain.i
new file mode 100644
index 000000000..1c97a527f
--- /dev/null
+++ b/src/util/chain.i
@@ -0,0 +1,12 @@
+%{
+#include "util/chain.h"
+%}
+
+%rename(equals) CVC4::Chain::operator==(const Chain&) const;
+%ignore CVC4::Chain::operator!=(const Chain&) const;
+
+%ignore CVC4::operator<<(std::ostream&, const Chain&);
+
+%rename(apply) CVC4::ChainHashFunction::operator()(const CVC4::Chain&) const;
+
+%include "util/chain.h"
diff --git a/src/util/result.cpp b/src/util/result.cpp
index e0e34f07d..909a7d8c6 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -27,11 +27,12 @@ using namespace std;
 
 namespace CVC4 {
 
-Result::Result(const std::string& instr) :
+Result::Result(const std::string& instr, 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) {
   string s = instr;
   transform(s.begin(), s.end(), s.begin(), ::tolower);
   if(s == "sat" || s == "satisfiable") {
@@ -115,13 +116,13 @@ Result Result::asSatisfiabilityResult() const throw() {
     switch(d_validity) {
 
     case INVALID:
-      return Result(SAT);
+      return Result(SAT, d_inputName);
 
     case VALID:
-      return Result(UNSAT);
+      return Result(UNSAT, d_inputName);
 
     case VALIDITY_UNKNOWN:
-      return Result(SAT_UNKNOWN, d_unknownExplanation);
+      return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
 
     default:
       Unhandled(d_validity);
@@ -129,7 +130,7 @@ Result Result::asSatisfiabilityResult() const throw() {
   }
 
   // TYPE_NONE
-  return Result(SAT_UNKNOWN, NO_STATUS);
+  return Result(SAT_UNKNOWN, NO_STATUS, d_inputName);
 }
 
 Result Result::asValidityResult() const throw() {
@@ -141,13 +142,13 @@ Result Result::asValidityResult() const throw() {
     switch(d_sat) {
 
     case SAT:
-      return Result(INVALID);
+      return Result(INVALID, d_inputName);
 
     case UNSAT:
-      return Result(VALID);
+      return Result(VALID, d_inputName);
 
     case SAT_UNKNOWN:
-      return Result(VALIDITY_UNKNOWN, d_unknownExplanation);
+      return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
 
     default:
       Unhandled(d_sat);
@@ -155,7 +156,7 @@ Result Result::asValidityResult() const throw() {
   }
 
   // TYPE_NONE
-  return Result(VALIDITY_UNKNOWN, NO_STATUS);
+  return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName);
 }
 
 string Result::toString() const {
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() {
diff --git a/src/util/util_model.h b/src/util/util_model.h
index 365e7124d..e5bd1f955 100644
--- a/src/util/util_model.h
+++ b/src/util/util_model.h
@@ -33,6 +33,10 @@ std::ostream& operator<<(std::ostream&, const Model&);
 
 class Model {
   friend std::ostream& operator<<(std::ostream&, const Model&);
+  friend class SmtEngine;
+
+  /** the input name (file name, etc.) this model is associated to */
+  std::string d_inputName;
 
 protected:
   /** The SmtEngine we're associated with */
@@ -52,6 +56,8 @@ public:
   SmtEngine* getSmtEngine() { return &d_smt; }
   /** get the smt engine (as a pointer-to-const) that this model is hooked up to */
   const SmtEngine* getSmtEngine() const { return &d_smt; }
+  /** get the input name (file name, etc.) this model is associated to */
+  std::string getInputName() const { return d_inputName; }
 
 public:
   /** get value for expression */