diff options
Diffstat (limited to 'src/main/main.cpp')
-rw-r--r-- | src/main/main.cpp | 39 |
1 files changed, 26 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; } |