some changes to make CVC4 work nicely with trace executor for application track;...

diff --git a/Makefile b/Makefile
index 97b47b812532b32bda352846a3c1fced3c84190f..e720e2db8671d5c64ce48b958f5f00f798582aeb 100644 (file)
--- 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 ae24f4984e4da563c16e9c234c830a9ce2ca43da..6d934c3fd6e79f09c2a51d8c26be9cd6145f60f3 100644 (file)
--- 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 00072d6d9fbb47b1b626232b0a7987e4df712692..5ecfed3a6784fa35fed7e2a0314bf63af39eef6e 100644 (file)
--- 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 1908d3e90fe32e39e7ce4ba421cab47cc45c7ef2..7972cd94d3bde080c744f79efddd3dd215523848 100644 (file)
--- 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 ebec370312e6d9001a24785125ec80114f2da2fb..e032a942644d1e967046a3827f36e7d722a05af6 100644 (file)
--- 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 91c43a1deffb9c47dc10843720a8539a0464a3b3..5e51900a942cbbcd8008ab6e0d8a07adae044b46 100644 (file)
--- 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") {