diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-11 23:56:10 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-19 19:09:28 -0400 |
commit | 4fc1fe120fd570f8e49da2fefa7b8a0bfed9df48 (patch) | |
tree | ad538771d8c2162de578b89b5947a02e4047fae5 /src/theory/term_registration_visitor.cpp | |
parent | 4ea1dce10aa9648b695c1249fbafc1255deadb1e (diff) |
Minor cleanup of sources
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index b41089b80..61b7209f6 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -171,9 +171,6 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { TheoryId parentTheoryId = Theory::theoryOf(parent); // Should we use the theory of the type -#if 0 - bool useType = current != parent && currentTheoryId != parentTheoryId; -#else bool useType = false; TheoryId typeTheoryId = THEORY_LAST; @@ -199,12 +196,10 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { } } } -#endif if (Theory::setContains(currentTheoryId, theories)) { if (Theory::setContains(parentTheoryId, theories)) { if (useType) { - ////TheoryId typeTheoryId = Theory::theoryOf(current.getType()); return Theory::setContains(typeTheoryId, theories); } else { return true; @@ -228,9 +223,6 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { TheoryId currentTheoryId = Theory::theoryOf(current); TheoryId parentTheoryId = Theory::theoryOf(parent); -#if 0 - bool useType = current != parent && currentTheoryId != parentTheoryId; -#else // Should we use the theory of the type bool useType = false; TheoryId typeTheoryId = THEORY_LAST; @@ -257,7 +249,6 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { } } } -#endif Theory::Set visitedTheories = d_visited[current]; Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl; @@ -270,7 +261,6 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } if (useType) { - //////TheoryId typeTheoryId = Theory::theoryOf(current.getType()); if (!Theory::setContains(typeTheoryId, visitedTheories)) { visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories); Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << typeTheoryId << std::endl; |