diff options
Diffstat (limited to 'src/main/main.cpp')
-rw-r--r-- | src/main/main.cpp | 29 |
1 files changed, 6 insertions, 23 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp index 7fd866112..f78637d82 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -33,7 +33,7 @@ #include "util/Assert.h" #include "util/configuration.h" #include "util/output.h" -#include "util/options.h" +#include "smt/options.h" #include "util/result.h" #include "util/stats.h" @@ -42,8 +42,6 @@ using namespace CVC4; using namespace CVC4::parser; using namespace CVC4::main; -static Result lastResult; - namespace CVC4 { namespace main { struct Options options; @@ -203,20 +201,15 @@ int runCvc4(int argc, char* argv[]) { delete cmd; } - Result asSatResult = lastResult.asSatisfiabilityResult(); + string result = smt.getInfo(":status").getValue(); int returnValue; - switch(asSatResult.isSAT()) { - - case Result::SAT: + if(result == "sat") { returnValue = 10; - break; - case Result::UNSAT: + } else if(result == "unsat") { returnValue = 20; - break; - default: + } else { returnValue = 0; - break; } #ifdef CVC4_COMPETITION_MODE @@ -228,7 +221,7 @@ int runCvc4(int argc, char* argv[]) { // Remove the parser delete parser; - ReferenceStat< Result > s_statSatResult("sat/unsat", asSatResult); + ReferenceStat< Result > s_statSatResult("sat/unsat", result); StatisticsRegistry::registerStat(&s_statSatResult); if(options.statistics){ @@ -259,15 +252,5 @@ void doCommand(SmtEngine& smt, Command* cmd) { } else { cmd->invoke(&smt); } - - QueryCommand *qc = dynamic_cast<QueryCommand*>(cmd); - if(qc != NULL) { - lastResult = qc->getResult(); - } else { - CheckSatCommand *csc = dynamic_cast<CheckSatCommand*>(cmd); - if(csc != NULL) { - lastResult = csc->getResult(); - } - } } } |