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.

4 files changed, 38 insertions, 29 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 556e51216..9ee896107 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -24,11 +24,12 @@
 namespace CVC4 {
 namespace main {
 
-CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options):
+CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) :
   d_exprMgr(exprMgr),
   d_smtEngine(SmtEngine(&exprMgr)),
   d_options(options),
-  d_stats("driver") {
+  d_stats("driver"),
+  d_result() {
 }
 
 bool CommandExecutor::doCommand(Command* cmd)
@@ -58,7 +59,7 @@ bool CommandExecutor::doCommand(Command* cmd)
   }
 }
 
-bool CommandExecutor::doCommandSingleton(Command *cmd)
+bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
   bool status = true;
   if(d_options[options::verbosity] >= -1) {
@@ -66,25 +67,27 @@ bool CommandExecutor::doCommandSingleton(Command *cmd)
   } else {
     status = smtEngineInvoke(&d_smtEngine, cmd, NULL);
   }
-  //dump the model if option is set
-  if(status && d_options[options::produceModels] && d_options[options::dumpModels]) {
-    CheckSatCommand *cs = dynamic_cast<CheckSatCommand*>(cmd);
-    if(cs != NULL) {
-      if(cs->getResult().asSatisfiabilityResult().isSat() == Result::SAT ||
-         (cs->getResult().isUnknown() && cs->getResult().whyUnknown() == Result::INCOMPLETE) ){
-        Command * gm = new GetModelCommand;
-        status = doCommandSingleton(gm);
-      }
-    }
+  Result res;
+  CheckSatCommand* cs = dynamic_cast<CheckSatCommand*>(cmd);
+  if(cs != NULL) {
+    d_result = res = cs->getResult();
+  }
+  QueryCommand* q = dynamic_cast<QueryCommand*>(cmd);
+  if(q != NULL) {
+    d_result = res = q->getResult();
+  }
+  // dump the model if option is set
+  if( status &&
+      d_options[options::produceModels] &&
+      d_options[options::dumpModels] &&
+      ( res.asSatisfiabilityResult() == Result::SAT ||
+        (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
+    Command* gm = new GetModelCommand();
+    status = doCommandSingleton(gm);
   }
   return status;
 }
 
-std::string CommandExecutor::getSmtEngineStatus()
-{
-  return d_smtEngine.getInfo("status").getValue();
-}
-
 bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
 {
   if(out == NULL) {
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index f1b8d8f2f..cbc71b075 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -34,6 +34,7 @@ protected:
   SmtEngine d_smtEngine;
   Options& d_options;
   StatisticsRegistry d_stats;
+  Result d_result;
 
 public:
   CommandExecutor(ExprManager &exprMgr, Options &options);
@@ -47,7 +48,7 @@ public:
    */
   bool doCommand(CVC4::Command* cmd);
 
-  virtual std::string getSmtEngineStatus();
+  Result getResult() const { return d_result; }
 
   StatisticsRegistry& getStatisticsRegistry() {
     return d_stats;
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 63f689d48..2dfd5e6bd 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -184,7 +184,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
   // command
 
   if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
-    dynamic_cast<QueryCommand*>(cmd) != NULL) {
+     dynamic_cast<QueryCommand*>(cmd) != NULL) {
     mode = 1;
   } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL ||
             dynamic_cast<GetAssignmentCommand*>(cmd) != NULL ||
@@ -298,6 +298,16 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
     d_lastWinner = portfolioReturn.first;
 
+    CheckSatCommand* cs = dynamic_cast<CheckSatCommand*>(cmd);
+    if(cs != NULL) {
+      d_result = cs->getResult();
+    }
+    QueryCommand* q = dynamic_cast<QueryCommand*>(cmd);
+    if(q != NULL) {
+      d_result = q->getResult();
+    }
+    dynamic_cast<QueryCommand*>(cmd) != NULL) {
+
     if(d_ostringstreams.size() != 0) {
       assert(d_numThreads == d_options[options::threads]);
       assert(portfolioReturn.first >= 0);
@@ -340,11 +350,6 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
 }/* CommandExecutorPortfolio::doCommandSingleton() */
 
-std::string CommandExecutorPortfolio::getSmtEngineStatus()
-{
-  return d_smts[d_lastWinner]->getInfo("status").getValue();
-}
-
 void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const {
   assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size());
   for(size_t i = 0; i < d_numThreads; ++i) {
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index f57d4f2d7..20a989106 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -297,13 +297,13 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       opts.set(options::replayStream, NULL);
     }
 
-    string result = "unknown";
+    Result result;
     if(status) {
-      result = pExecutor->getSmtEngineStatus();
+      result = pExecutor->getResult();
 
-      if(result == "sat") {
+      if(result.asSatisfiabilityResult() == Result::SAT) {
         returnValue = 10;
-      } else if(result == "unsat") {
+      } else if(result.asSatisfiabilityResult() == Result::UNSAT) {
         returnValue = 20;
       } else {
         returnValue = 0;