some changes to make CVC4 work nicely with trace executor for application track; (set-option :print-success true) supported, (exit) causes immediate exit regardless of EOF, etc.

6 files changed, 36 insertions, 5 deletions

diff --git a/Makefile b/Makefile
index 97b47b812..e720e2db8 100644
--- a/Makefile
+++ b/Makefile
@@ -59,7 +59,7 @@ submission:
 	mkdir -p cvc4-smtcomp-$(YEAR)
 	cp -p builds/bin/cvc4 cvc4-smtcomp-$(YEAR)/cvc4
 	( echo '#!/bin/sh'; \
-	  echo 'exec ./cvc4 -L smt2 --no-interactive' ) > cvc4-smtcomp-$(YEAR)/run
+	  echo 'exec ./cvc4 -L smt2 --no-checking --no-interactive' ) > cvc4-smtcomp-$(YEAR)/run
 	chmod 755 cvc4-smtcomp-$(YEAR)/run
 	tar cf cvc4-smtcomp-$(YEAR).tar cvc4-smtcomp-$(YEAR)
 	# application track is a separate build too :-(
@@ -74,7 +74,7 @@ submission:
 	mkdir -p cvc4-application-smtcomp-$(YEAR)
 	cp -p builds/bin/cvc4 cvc4-application-smtcomp-$(YEAR)/cvc4
 	( echo '#!/bin/sh'; \
-	  echo 'exec ./cvc4 -L smt2 --no-interactive --incremental' ) > cvc4-application-smtcomp-$(YEAR)/run
+	  echo 'exec ./cvc4 -L smt2 --no-checking --no-interactive --incremental' ) > cvc4-application-smtcomp-$(YEAR)/run
 	chmod 755 cvc4-application-smtcomp-$(YEAR)/run
 	tar cf cvc4-application-smtcomp-$(YEAR).tar cvc4-application-smtcomp-$(YEAR)
 	# parallel track can't be built with -cln, so it's a separate build
@@ -90,6 +90,6 @@ submission:
 	mkdir -p cvc4-parallel-smtcomp-$(YEAR)
 	cp -p builds/bin/pcvc4 cvc4-parallel-smtcomp-$(YEAR)/pcvc4
 	( echo '#!/bin/sh'; \
-	  echo 'exec ./pcvc4 --threads 2 -L smt2 --no-interactive' ) > cvc4-parallel-smtcomp-$(YEAR)/run
+	  echo 'exec ./pcvc4 --threads 2 -L smt2 --no-checking --no-interactive' ) > cvc4-parallel-smtcomp-$(YEAR)/run
 	chmod 755 cvc4-parallel-smtcomp-$(YEAR)/run
 	tar cf cvc4-parallel-smtcomp-$(YEAR).tar cvc4-parallel-smtcomp-$(YEAR)
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index ae24f4984..6d934c3fd 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -467,6 +467,7 @@ Type DeclareFunctionCommand::getType() const throw() {
 
 void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this;
+  d_commandStatus = CommandSuccess::instance();
 }
 
 Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager,
@@ -497,6 +498,7 @@ Type DeclareTypeCommand::getType() const throw() {
 
 void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this;
+  d_commandStatus = CommandSuccess::instance();
 }
 
 Command* DeclareTypeCommand::exportTo(ExprManager* exprManager,
diff --git a/src/main/driver.cpp b/src/main/driver.cpp
index 00072d6d9..5ecfed3a6 100644
--- a/src/main/driver.cpp
+++ b/src/main/driver.cpp
@@ -242,6 +242,9 @@ int runCvc4(int argc, char* argv[], Options& options) {
     *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1);
   }
 
+  // important even for muzzled builds (to get result output right)
+  *options.out << Expr::setlanguage(options.outputLanguage);
+
   // Parse and execute commands until we are done
   Command* cmd;
   bool status = true;
@@ -281,6 +284,10 @@ int runCvc4(int argc, char* argv[], Options& options) {
       replayParser->useDeclarationsFrom(parser);
     }
     while((cmd = parser->nextCommand())) {
+      if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
+        delete cmd;
+        break;
+      }
       status = doCommand(smt, cmd, options) && status;
       delete cmd;
     }
diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
index 1908d3e90..7972cd94d 100644
--- a/src/main/driver_portfolio.cpp
+++ b/src/main/driver_portfolio.cpp
@@ -301,6 +301,9 @@ int runCvc4(int argc, char *argv[], Options& options) {
                      << Expr::printtypes(false);
   }
 
+  // important even for muzzled builds (to get result output right)
+  *options.out << Expr::setlanguage(options.outputLanguage);
+
   vector<Options> threadOptions;
   for(int i = 0; i < numThreads; ++i) {
     threadOptions.push_back(options);
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index ebec37031..e032a9426 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -748,7 +748,14 @@ static void toStream(std::ostream& out, const CommandSuccess* s) throw() {
 }
 
 static void toStream(std::ostream& out, const CommandUnsupported* s) throw() {
+#ifdef CVC4_COMPETITION_MODE
+  // if in competition mode, lie and say we're ok
+  // (we have nothing to lose by saying success, and everything to lose
+  // if we say "unsupported")
+  out << "success" << endl;
+#else /* CVC4_COMPETITION_MODE */
   out << "unsupported" << endl;
+#endif /* CVC4_COMPETITION_MODE */
 }
 
 static void toStream(std::ostream& out, const CommandFailure* s) throw() {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 91c43a1de..5e51900a9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -650,6 +650,9 @@ SExpr SmtEngine::getInfo(const std::string& key) const
 
 void SmtEngine::setOption(const std::string& key, const SExpr& value)
   throw(BadOptionException, ModalException) {
+
+  NodeManagerScope nms(d_nodeManager);
+
   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << SetOptionCommand(key, value);
@@ -657,7 +660,9 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value)
 
   if(key == ":print-success") {
     if(value.isAtom() && value.getValue() == "false") {
-      // fine; don't need to do anything
+      *Options::current()->out << Command::printsuccess(false);
+    } else if(value.isAtom() && value.getValue() == "true") {
+      *Options::current()->out << Command::printsuccess(true);
     } else {
       throw BadOptionException();
     }
@@ -696,12 +701,19 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value)
 
 SExpr SmtEngine::getOption(const std::string& key) const
   throw(BadOptionException) {
+
+  NodeManagerScope nms(d_nodeManager);
+
   Trace("smt") << "SMT getOption(" << key << ")" << endl;
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetOptionCommand(key);
   }
   if(key == ":print-success") {
-    return SExpr("true");
+    if(Command::printsuccess::getPrintSuccess(*Options::current()->out)) {
+      return SExpr("true");
+    } else {
+      return SExpr("false");
+    }
   } else if(key == ":expand-definitions") {
     throw BadOptionException();
   } else if(key == ":interactive-mode") {