diff options
Diffstat (limited to 'src/main/main.cpp')
-rw-r--r-- | src/main/main.cpp | 47 |
1 files changed, 41 insertions, 6 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp index 4731c536e..387d5ca97 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -26,6 +26,7 @@ #include "expr/expr_manager.h" #include "smt/smt_engine.h" #include "util/command.h" +#include "util/result.h" #include "util/Assert.h" #include "util/output.h" #include "util/options.h" @@ -35,9 +36,12 @@ using namespace CVC4; using namespace CVC4::parser; using namespace CVC4::main; -int main(int argc, char *argv[]) { +static Result lastResult; +static struct Options options; + +void doCommand(SmtEngine&, Command*); - struct Options options; +int main(int argc, char *argv[]) { try { @@ -110,10 +114,7 @@ int main(int argc, char *argv[]) { // Parse and execute commands until we are done Command* cmd; while((cmd = parser->parseNextCommand())) { - if(options.verbosity > 0) { - cout << "Invoking: " << *cmd << endl; - } - cmd->invoke(&smt); + doCommand(smt, cmd); delete cmd; } @@ -147,5 +148,39 @@ int main(int argc, char *argv[]) { abort(); } + // TODO: adjust return value based on lastResult return 0; } + +void doCommand(SmtEngine& smt, Command* cmd) { + CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd); + if(seq != NULL) { + for(CommandSequence::iterator subcmd = seq->begin(); + subcmd != seq->end(); + ++subcmd) { + doCommand(smt, *subcmd); + } + } else { + if(options.verbosity > 0) { + cout << "Invoking: " << *cmd << endl; + } + + cmd->invoke(&smt); + + QueryCommand *qc = dynamic_cast<QueryCommand*>(cmd); + if(qc != NULL) { + lastResult = qc->getResult(); + if(options.verbosity >= 0) { + cout << lastResult << endl; + } + } else { + CheckSatCommand *csc = dynamic_cast<CheckSatCommand*>(cmd); + if(csc != NULL) { + lastResult = csc->getResult(); + if(options.verbosity >= 0) { + cout << lastResult << endl; + } + } + } + } +} |