diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-07-11 03:33:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-07-11 03:33:14 +0000 |
commit | 25e9c72dd689d3b621b901220794c652a3ba589a (patch) | |
tree | 58b14dd3818f3e7a8ca3311a0457716e7753a95e /src/prop/prop_engine.cpp | |
parent | 587520ce888b88294fb9e4ca476e2425d8bf026e (diff) |
merge from symmetry branch
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r-- | src/prop/prop_engine.cpp | 22 |
1 files changed, 19 insertions, 3 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index cbec9faea..4c9b66020 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -16,9 +16,9 @@ ** Implementation of the propositional engine of CVC4. **/ -#include "cnf_stream.h" -#include "prop_engine.h" -#include "sat.h" +#include "prop/cnf_stream.h" +#include "prop/prop_engine.h" +#include "prop/sat.h" #include "theory/theory_engine.h" #include "theory/registrar.h" @@ -26,6 +26,8 @@ #include "util/options.h" #include "util/output.h" #include "util/result.h" +#include "expr/expr.h" +#include "expr/command.h" #include <utility> #include <map> @@ -88,6 +90,16 @@ void PropEngine::assertLemma(TNode node) { //Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; + if(Options::current()->preprocessOnly) { + if(Message.isOn()) { + // If "preprocess only" mode is in effect, the lemmas we get + // here are due to theory reasoning during preprocessing. So + // push the lemma to the Message() stream. + expr::ExprSetDepth::Scope sdScope(Message.getStream(), -1); + Message() << AssertCommand(BoolExpr(node.toExpr())) << endl; + } + } + //TODO This comment is now false // Assert as removable d_cnfStream->convertAndAssert(node, true, false); @@ -124,6 +136,10 @@ Result PropEngine::checkSat() { // TODO This currently ignores conflicts (a dangerous practice). d_theoryEngine->presolve(); + if(Options::current()->preprocessOnly) { + return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK); + } + // Check the problem bool result = d_satSolver->solve(); |