diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-12-14 09:31:21 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-12-14 09:31:21 +0000 |
| commit | ee64b3fa49a22b89ffb3e62d8d7144fc9b99754e (patch) | |
| tree | eb972e4e0c0c61e3b1e1ddfc3637dec80e038d51 /src/theory/theory_engine.cpp | |
| parent | 6d04f19e1c1fbf7714fbb95dc62648ac44b419dd (diff) | |
some more bug fixes (TNode -> Node, normalize literals in explanations)
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 4c289b5c1..d08e79c8e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -570,16 +570,16 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { d_propagatedLiterals.push_back(literal); } else { // Otherwise it might be a shared-term (dis-)equality - Node normalizedEquality = Rewriter::rewrite(literal); - if (d_propEngine->isSatLiteral(normalizedEquality)) { + Node normalizedLiteral = Rewriter::rewrite(literal); + if (d_propEngine->isSatLiteral(normalizedLiteral)) { // If there is a literal, just enqueue it, same as above bool value; - if (d_propEngine->hasValue(normalizedEquality, value)) { + if (d_propEngine->hasValue(normalizedLiteral, value)) { // if we are propagting something that already has a sat value we better be the same - Debug("theory") << "literal " << literal << " (" << normalizedEquality << ") propagated by " << theory << " but already has a sat value" << std::endl; - Assert((value && (literal.getKind() != kind::NOT)) || (!value && literal.getKind() == kind::NOT)); + Debug("theory") << "literal " << literal << " (" << normalizedLiteral << ") propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl; + Assert(value); } else { - d_propagatedLiterals.push_back(normalizedEquality); + d_propagatedLiterals.push_back(normalizedLiteral); } } // Otherwise, we assert it to all interested theories @@ -708,7 +708,7 @@ void TheoryEngine::explainEquality(TheoryId theoryId, TNode eqLiteral, NodeBuild SharedAssertionsMap::iterator find = d_sharedAssertions.find(NodeTheoryPair(eqLiteral, theoryId)); if (find == d_sharedAssertions.end()) { // Not a shared assertion, just add it since it must be SAT literal - builder << eqLiteral; + builder << Rewriter::rewrite(eqLiteral); } else { TheoryId explainingTheory = (*find).second.theory; if (explainingTheory == theory::THEORY_LAST) { @@ -721,4 +721,3 @@ void TheoryEngine::explainEquality(TheoryId theoryId, TNode eqLiteral, NodeBuild } } } - |