diff options
Diffstat (limited to 'src/prop/prop_engine.cpp')
| -rw-r--r-- | src/prop/prop_engine.cpp | 16 |
1 files changed, 9 insertions, 7 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 */ |