diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-06-17 15:55:56 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-06-17 15:57:28 -0500 |
| commit | 1a2547995acc5a98c8969e628ac5e1c45b0efe94 (patch) | |
| tree | 0d9abd19ba7b3b742da3e745da00c0457237f84b /src/theory/term_registration_visitor.cpp | |
| parent | 0348b525a951a8709f9dc4b5757ce0bcb48a9472 (diff) | |
Support for separation logic. Enable cbqi by default for pure BV.
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
| -rw-r--r-- | src/theory/term_registration_visitor.cpp | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 6b268805a..7b9786247 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -37,8 +37,13 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { if( ( parent.getKind() == kind::FORALL || parent.getKind() == kind::EXISTS || - parent.getKind() == kind::REWRITE_RULE /*|| - parent.getKind() == kind::CARDINALITY_CONSTRAINT*/ ) && + parent.getKind() == kind::REWRITE_RULE || + parent.getKind() == kind::SEP_NIL || + 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; @@ -177,8 +182,13 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { if( ( parent.getKind() == kind::FORALL || parent.getKind() == kind::EXISTS || - parent.getKind() == kind::REWRITE_RULE /*|| - parent.getKind() == kind::CARDINALITY_CONSTRAINT*/ ) && + parent.getKind() == kind::REWRITE_RULE || + parent.getKind() == kind::SEP_NIL || + 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; |