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

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"