diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-10 22:15:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-10 22:15:38 +0000 |
commit | d6b37239a2e525e7878d3bb0b4372a8dabc340a9 (patch) | |
tree | 3db6b54c8b5873db1e6c91b1577d431d74632c66 /src/main | |
parent | 7a059452ebf5729723f610da9258a47007e38253 (diff) |
additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/getopt.cpp | 2 | ||||
-rw-r--r-- | src/main/main.cpp | 29 | ||||
-rw-r--r-- | src/main/util.cpp | 2 |
3 files changed, 8 insertions, 25 deletions
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 8faaefac4..57aa84a57 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -29,7 +29,7 @@ #include "util/exception.h" #include "util/configuration.h" #include "util/output.h" -#include "util/options.h" +#include "smt/options.h" #include "util/language.h" #include "expr/expr.h" 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(); - } - } } } diff --git a/src/main/util.cpp b/src/main/util.cpp index 760bd5258..70cb85c93 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -24,7 +24,7 @@ #include <signal.h> #include "util/exception.h" -#include "util/options.h" +#include "smt/options.h" #include "util/Assert.h" #include "util/stats.h" |