diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 10 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 16 |
3 files changed, 5 insertions, 25 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 4a2a5f135..e1ef51d09 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -30,7 +30,7 @@ std::string PreRegisterVisitor::toString() const { bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { - Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ") => "; + Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; TheoryId currentTheoryId = Theory::theoryOf(current); @@ -134,7 +134,7 @@ std::string SharedTermsVisitor::toString() const { bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { - Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ") => "; + Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; TNodeVisitedMap::const_iterator find = d_visited.find(current); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5a8a75aab..0ab188dc4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -772,14 +772,8 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { Node normalizedLiteral = Rewriter::rewrite(literal); if (d_propEngine->isSatLiteral(normalizedLiteral)) { // If there is a literal, propagate it to SAT - 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 << ", normalized = " << normalizedLiteral << ", propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl; - Assert(value); - } else { - SharedLiteral sharedLiteral(normalizedLiteral, literal, theory::THEORY_LAST); - d_propagatedSharedLiterals.push_back(sharedLiteral); - } + SharedLiteral sharedLiteral(normalizedLiteral, literal, theory::THEORY_LAST); + d_propagatedSharedLiterals.push_back(sharedLiteral); } // Assert to interested theories Debug("shared-in") << "TheoryEngine::propagate: asserting shared node: " << literal << std::endl; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index cddd01b07..7f173a0c4 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -112,21 +112,7 @@ void TheoryUF::propagate(Effort level) { for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl; - bool satValue; - Node normalized = Rewriter::rewrite(literal); - if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { - d_out->propagate(literal); - } else { - Debug("uf") << "TheoryUF::propagate(): in conflict, normalized = " << normalized << std::endl; - Node negatedLiteral; - std::vector<TNode> assumptions; - negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); - assumptions.push_back(negatedLiteral); - explain(literal, assumptions); - d_conflictNode = mkAnd(assumptions); - d_conflict = true; - break; - } + d_out->propagate(literal); } } }/* TheoryUF::propagate(Effort) */ |