From 4c956f292906c59ba77c000084a08a4e7888e49b Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 14 Jun 2012 17:42:47 +0000 Subject: [PATCH] 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. --- Makefile | 6 +++--- src/expr/command.cpp | 2 ++ src/main/driver.cpp | 7 +++++++ src/main/driver_portfolio.cpp | 3 +++ src/printer/smt2/smt2_printer.cpp | 7 +++++++ src/smt/smt_engine.cpp | 16 ++++++++++++++-- 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(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 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") { -- 2.30.2