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/prop | |
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/prop')
-rw-r--r-- | src/prop/prop_engine.cpp | 16 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 4 | ||||
-rw-r--r-- | src/prop/sat.h | 2 |
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 |