From 9468dec9f3c041e4996df2f703f2c2ba4ba8dd91 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 2 Dec 2011 00:35:32 +0000 Subject: [PATCH] Error detection is different now---with new Command infrastructure, exceptions are not thrown outside the library. Reflect this in the exit code of the driver. Fixes a bug found by Tim among the nightly regressions. Also improved error reporting if antlr is unavailable and the parsers need to be generated. --- src/main/main.cpp | 39 ++++++++++++++++++++++++------------- src/parser/cvc/Makefile.am | 1 + src/parser/smt/Makefile.am | 1 + src/parser/smt2/Makefile.am | 1 + 4 files changed, 29 insertions(+), 13 deletions(-) diff --git a/src/main/main.cpp b/src/main/main.cpp index ba5d06672..76ca7a925 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -47,7 +47,7 @@ using namespace CVC4::parser; using namespace CVC4::main; static int runCvc4(int argc, char* argv[]); -static void doCommand(SmtEngine&, Command*); +static bool doCommand(SmtEngine&, Command*); static void printUsage(bool full = false); namespace CVC4 { @@ -277,6 +277,7 @@ static int runCvc4(int argc, char* argv[]) { // Parse and execute commands until we are done Command* cmd; + bool status = true; if( options.interactive ) { InteractiveShell shell(exprMgr, options); Message() << Configuration::getPackageName() @@ -293,7 +294,7 @@ static int runCvc4(int argc, char* argv[]) { replayParser->useDeclarationsFrom(shell.getParser()); } while((cmd = shell.readCommand())) { - doCommand(smt,cmd); + status = status && doCommand(smt, cmd); delete cmd; } } else { @@ -309,7 +310,7 @@ static int runCvc4(int argc, char* argv[]) { replayParser->useDeclarationsFrom(parser); } while((cmd = parser->nextCommand())) { - doCommand(smt, cmd); + status = status && doCommand(smt, cmd); delete cmd; } // Remove the parser @@ -322,15 +323,21 @@ static int runCvc4(int argc, char* argv[]) { options.replayStream = NULL; } - string result = smt.getInfo(":status").getValue(); int returnValue; - - if(result == "sat") { - returnValue = 10; - } else if(result == "unsat") { - returnValue = 20; + string result = "unknown"; + if(status) { + result = smt.getInfo(":status").getValue(); + + if(result == "sat") { + returnValue = 10; + } else if(result == "unsat") { + returnValue = 20; + } else { + returnValue = 0; + } } else { - returnValue = 0; + // there was some kind of error + returnValue = 1; } #ifdef CVC4_COMPETITION_MODE @@ -350,17 +357,20 @@ static int runCvc4(int argc, char* argv[]) { } /** Executes a command. Deletes the command after execution. */ -static void doCommand(SmtEngine& smt, Command* cmd) { +static bool doCommand(SmtEngine& smt, Command* cmd) { if( options.parseOnly ) { - return; + return true; } + // assume no error + bool status = true; + CommandSequence *seq = dynamic_cast(cmd); if(seq != NULL) { for(CommandSequence::iterator subcmd = seq->begin(); subcmd != seq->end(); ++subcmd) { - doCommand(smt, *subcmd); + status = status && doCommand(smt, *subcmd); } } else { if(options.verbosity > 0) { @@ -372,5 +382,8 @@ static void doCommand(SmtEngine& smt, Command* cmd) { } else { cmd->invoke(&smt); } + status = status && cmd->ok(); } + + return status; } diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index c5dab0cd2..15a572745 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -51,6 +51,7 @@ maintainer-clean-local: # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. @srcdir@/generated/CvcLexer.h: Cvc.g @srcdir@/stamp-generated -$(AM_V_at)rm -f $(ANTLR_STUFF) + @if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@srcdir@/generated" "@srcdir@/Cvc.g" # These don't actually depend on CvcLexer.h, but if we're doing parallel diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index 46926da8f..975a90b72 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -51,6 +51,7 @@ maintainer-clean-local: # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. @srcdir@/generated/SmtLexer.h: Smt.g @srcdir@/stamp-generated -$(AM_V_at)rm -f $(ANTLR_STUFF) + @if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@srcdir@/generated" "@srcdir@/Smt.g" # These don't actually depend on SmtLexer.h, but if we're doing parallel diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am index 9def4c85b..75ceec43a 100644 --- a/src/parser/smt2/Makefile.am +++ b/src/parser/smt2/Makefile.am @@ -51,6 +51,7 @@ maintainer-clean-local: # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. @srcdir@/generated/Smt2Lexer.h: Smt2.g @srcdir@/stamp-generated -$(AM_V_at)rm -f $(ANTLR_STUFF) + @if test -z "$(ANTLR)"; then echo "ERROR: antlr parser generator cannot be found, cannot generate the parser" >&2; exit 1; fi $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -fo "@srcdir@/generated" "@srcdir@/Smt2.g" # These don't actually depend on SmtLexer.h, but if we're doing parallel -- 2.30.2