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.

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<CommandSequence*>(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