diff options
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 40 |
1 files changed, 22 insertions, 18 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 1e1a2e8e6..eae5578cf 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -35,15 +35,17 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; - if( ( parent.getKind() == kind::FORALL || - parent.getKind() == kind::EXISTS || - parent.getKind() == kind::REWRITE_RULE || - parent.getKind() == kind::SEP_STAR || - parent.getKind() == kind::SEP_WAND || - ( parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean() ) - // parent.getKind() == kind::CARDINALITY_CONSTRAINT - ) && - current != parent ) { + if ((parent.getKind() == kind::FORALL || parent.getKind() == kind::EXISTS + || parent.getKind() == kind::LAMBDA + || parent.getKind() == kind::CHOICE + || parent.getKind() == kind::REWRITE_RULE + || parent.getKind() == kind::SEP_STAR + || parent.getKind() == kind::SEP_WAND + || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean()) + // parent.getKind() == kind::CARDINALITY_CONSTRAINT + ) + && current != parent) + { Debug("register::internal") << "quantifier:true" << std::endl; return true; } @@ -179,15 +181,17 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl; - if( ( parent.getKind() == kind::FORALL || - parent.getKind() == kind::EXISTS || - parent.getKind() == kind::REWRITE_RULE || - parent.getKind() == kind::SEP_STAR || - parent.getKind() == kind::SEP_WAND || - ( parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean() ) - // parent.getKind() == kind::CARDINALITY_CONSTRAINT - ) && - current != parent ) { + if ((parent.getKind() == kind::FORALL || parent.getKind() == kind::EXISTS + || parent.getKind() == kind::LAMBDA + || parent.getKind() == kind::CHOICE + || parent.getKind() == kind::REWRITE_RULE + || parent.getKind() == kind::SEP_STAR + || parent.getKind() == kind::SEP_WAND + || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean()) + // parent.getKind() == kind::CARDINALITY_CONSTRAINT + ) + && current != parent) + { Debug("register::internal") << "quantifier:true" << std::endl; return true; } |