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, 12 insertions, 10 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 961a18bdb..de60b5f7d 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -24,7 +24,7 @@
 #include "util/decision_engine.h"
 #include "util/Assert.h"
 #include "util/output.h"
-#include "util/options.h"
+#include "smt/options.h"
 #include "util/result.h"
 
 #include <utility>
@@ -93,9 +93,11 @@ void PropEngine::assertLemma(TNode node) {
 
 
 void PropEngine::printSatisfyingAssignment(){
-  const CnfStream::TranslationCache& transCache = d_cnfStream->getTranslationCache();
+  const CnfStream::TranslationCache& transCache =
+    d_cnfStream->getTranslationCache();
   Debug("prop-value") << "Literal | Value | Expr" << endl
-                      << "---------------------------------------------------------" << endl;
+                      << "----------------------------------------"
+                      << "-----------------" << endl;
   for(CnfStream::TranslationCache::const_iterator i = transCache.begin(),
       end = transCache.end();
       i != end;
@@ -105,8 +107,7 @@ void PropEngine::printSatisfyingAssignment(){
     if(!sign(l)) {
       Node n = curr.first;
       SatLiteralValue value = d_satSolver->value(l);
-      Debug("prop-value") << /*setw(4) << */ "'" << l << "' " /*<< setw(4)*/ << value << " " << n
-            << endl;
+      Debug("prop-value") << "'" << l << "' " << value << " " << n << endl;
     }
   }
 }
@@ -126,7 +127,8 @@ Result PropEngine::checkSat() {
     printSatisfyingAssignment();
   }
 
-  Debug("prop") << "PropEngine::checkSat() => " << (result ? "true" : "false") << endl;
+  Debug("prop") << "PropEngine::checkSat() => "
+                << (result ? "true" : "false") << endl;
   return Result(result ? Result::SAT : Result::UNSAT);
 }
 
@@ -154,5 +156,5 @@ void PropEngine::pop() {
   Debug("prop") << "pop()" << endl;
 }
 
-}/* prop namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 7eb903180..1dada2e69 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -25,12 +25,12 @@
 
 #include "expr/node.h"
 #include "util/result.h"
-#include "util/options.h"
 #include "util/decision_engine.h"
 
 namespace CVC4 {
 
 class TheoryEngine;
+class Options;
 
 namespace prop {
 
@@ -133,7 +133,7 @@ public:
 
 };/* class PropEngine */
 
-}/* prop namespace */
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PROP_ENGINE_H */
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 776895b4c..a335b733b 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -25,9 +25,9 @@
 // Optional blocks below will be unconditionally included
 #define __CVC4_USE_MINISAT
 
-#include "util/options.h"
 #include "util/stats.h"
 #include "theory/theory.h"
+#include "smt/options.h"
 
 #ifdef __CVC4_USE_MINISAT