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/theory/theory_engine.cpp | |
parent | 587520ce888b88294fb9e4ca476e2425d8bf026e (diff) |
merge from symmetry branch
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index fa885590b..4237e0992 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -286,6 +286,12 @@ Node TheoryEngine::getValue(TNode node) { }/* TheoryEngine::getValue(TNode node) */ bool TheoryEngine::presolve() { + // NOTE that we don't look at d_theoryIsActive[] here. First of + // all, we haven't done any pre-registration yet, so we don't know + // which theories are active. Second, let's give each theory a shot + // at doing something with the input formula, even if it wouldn't + // otherwise be active. + d_theoryOut.d_conflictNode = Node::null(); d_theoryOut.d_propagatedLiterals.clear(); @@ -295,7 +301,7 @@ bool TheoryEngine::presolve() { #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasPresolve && d_theoryIsActive[THEORY]) { \ + if (theory::TheoryTraits<THEORY>::hasPresolve) { \ reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->presolve(); \ if(!d_theoryOut.d_conflictNode.get().isNull()) { \ return true; \ |