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.

2 files changed, 17 insertions, 8 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4ee00161f..b72f52092 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1108,13 +1108,15 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
   }
 
   // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
-  if(key == "name" ||
-     key == "source" ||
+  if(key == "source" ||
      key == "category" ||
      key == "difficulty" ||
      key == "notes") {
     // ignore these
     return;
+  } else if(key == "name") {
+    d_filename = value.getValue();
+    return;
   } else if(key == "smt-lib-version") {
     if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
         (value.isRational() && value.getRationalValue() == Rational(2)) ||
@@ -1133,7 +1135,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
       throw OptionException("argument to (set-info :status ..) must be "
                             "`sat' or `unsat' or `unknown'");
     }
-    d_status = Result(s);
+    d_status = Result(s, d_filename);
     return;
   }
   throw UnrecognizedOptionException();
@@ -2568,7 +2570,7 @@ Result SmtEngine::check() {
   if(d_timeBudgetCumulative != 0) {
     millis = getTimeRemaining();
     if(millis == 0) {
-      return Result(Result::VALIDITY_UNKNOWN, Result::TIMEOUT);
+      return Result(Result::VALIDITY_UNKNOWN, Result::TIMEOUT, d_filename);
     }
   }
   if(d_timeBudgetPerCall != 0 && (millis == 0 || d_timeBudgetPerCall < millis)) {
@@ -2579,7 +2581,7 @@ Result SmtEngine::check() {
   if(d_resourceBudgetCumulative != 0) {
     resource = getResourceRemaining();
     if(resource == 0) {
-      return Result(Result::VALIDITY_UNKNOWN, Result::RESOURCEOUT);
+      return Result(Result::VALIDITY_UNKNOWN, Result::RESOURCEOUT, d_filename);
     }
   }
   if(d_resourceBudgetPerCall != 0 && (resource == 0 || d_resourceBudgetPerCall < resource)) {
@@ -2600,13 +2602,13 @@ Result SmtEngine::check() {
   Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
                  << ", conflicts " << d_cumulativeResourceUsed << endl;
 
-  return result;
+  return Result(result, d_filename);
 }
 
 Result SmtEngine::quickCheck() {
   Assert(d_fullyInited);
   Trace("smt") << "SMT quickCheck()" << endl;
-  return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK);
+  return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename);
 }
 
 
@@ -3427,7 +3429,9 @@ Model* SmtEngine::getModel() throw(ModalException) {
       "Cannot get model when produce-models options is off.";
     throw ModalException(msg);
   }
-  return d_theoryEngine->getModel();
+  TheoryModel* m = d_theoryEngine->getModel();
+  m->d_inputName = d_filename;
+  return m;
 }
 
 void SmtEngine::checkModel(bool hardFailure) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a45fe3383..552f5cd67 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -234,6 +234,11 @@ class CVC4_PUBLIC SmtEngine {
   Result d_status;
 
   /**
+   * The name of the input (if any).
+   */
+  std::string d_filename;
+
+  /**
    * A private utility class to SmtEngine.
    */
   smt::SmtEnginePrivate* d_private;