From e80b93ca958bdbeb28959029868f6193b39a3f19 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 24 Jun 2013 19:58:37 -0400 Subject: 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. --- src/main/command_executor_portfolio.cpp | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) (limited to 'src/main/command_executor_portfolio.cpp') 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(cmd) != NULL || - dynamic_cast(cmd) != NULL) { + dynamic_cast(cmd) != NULL) { mode = 1; } else if(dynamic_cast(cmd) != NULL || dynamic_cast(cmd) != NULL || @@ -298,6 +298,16 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) d_lastWinner = portfolioReturn.first; + CheckSatCommand* cs = dynamic_cast(cmd); + if(cs != NULL) { + d_result = cs->getResult(); + } + QueryCommand* q = dynamic_cast(cmd); + if(q != NULL) { + d_result = q->getResult(); + } + dynamic_cast(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) { -- cgit v1.2.3