diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-12 12:23:57 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-12 12:23:57 -0500 |
| commit | af135825a60f917711d133828c9fdd6831e2142d (patch) | |
| tree | 20e9b46a027b8f8242901964fa360bb849f640df /src/theory/term_registration_visitor.cpp | |
| parent | 6b5b926f28b66c3812d77fd234e93b9eee03f71f (diff) | |
Fixes for free variables in assertions (#1762)
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; } |