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 | |
parent | 587520ce888b88294fb9e4ca476e2425d8bf026e (diff) |
merge from symmetry branch
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 14 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 22 |
2 files changed, 31 insertions, 5 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 8e98f32c0..0c4f00875 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -240,8 +240,18 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type) if (ps.size() == 0) return ok = false; else if (ps.size() == 1){ - assert(type != CLAUSE_LEMMA); - assert(value(ps[0]) == l_Undef); + if(in_solve) { + assert(type != CLAUSE_LEMMA); + assert(value(ps[0]) == l_Undef); + } else { + // [MGD] at "pre-solve" time we allow unit T-lemmas + if(value(ps[0]) == l_True) { + // this unit T-lemma is extraneous (perhaps it was + // discovered twice at presolve time) + return true; + } + assert(value(ps[0]) == l_Undef); + } uncheckedEnqueue(ps[0]); return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef); }else{ 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(); |