diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-10 13:01:02 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-10 13:02:46 -0400 |
commit | 7f13c0713accdefa46ce2a43dbeae8c46255bea1 (patch) | |
tree | 13110353d5a45c0970e1fc4928f863e45c732e50 /src/theory/term_registration_visitor.cpp | |
parent | 315eb7e44cada64fd9b8a2b4ab9b9cac66758769 (diff) |
Fix erroneous results when the logic was incorrectly specified (by throwing LogicException). Also correct a case where sharing was doing some work during pure theory solving.
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 48d00130c..558975a72 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -127,15 +127,6 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { Assert(alreadyVisited(current, parent)); } -void PreRegisterVisitor::start(TNode node) { - d_multipleTheories = false; -} - -bool PreRegisterVisitor::done(TNode node) { - // We have multiple theories if removing the node theory from others is non-empty - return Theory::setRemove(Theory::theoryOf(node), d_theories); -} - std::string SharedTermsVisitor::toString() const { std::stringstream ss; TNodeVisitedMap::const_iterator it = d_visited.begin(); |