Error detection is different now---with new Command infrastructure, exceptions are...

Also improved error reporting if antlr is unavailable and the parsers need to be generated.

diff --git a/src/main/main.cpp b/src/main/main.cpp
index ba5d06672ffb57eb9953ae48f6edfac7b9fe8456..76ca7a9252fea299cb89ac64588e76091ff3ed94 100644 (file)
--- 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 c5dab0cd2c82937033368bfa7b23c2d32ae3c3d5..15a572745f5d429806888e4c65bdfc988e749899 100644 (file)
--- 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 46926da8f90e6e127513007d735cc66e8734f2d4..975a90b72ce30275980bf8d9fee16ce64a723f4e 100644 (file)
--- 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 9def4c85ba65b880a1dcb470e232c5d5244cd4d8..75ceec43a12467cf023a114574e9440e0f8ab8a3 100644 (file)
--- 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