From d6b37239a2e525e7878d3bb0b4372a8dabc340a9 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Sun, 10 Oct 2010 22:15:38 +0000
Subject: 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

---
 src/prop/prop_engine.cpp | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

(limited to 'src/prop/prop_engine.cpp')

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 */
-- 
cgit v1.2.3