More use of isClosure (#2959)

6 files changed, 9 insertions, 16 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 472e2561f..51cc15c12 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -228,7 +228,7 @@ void TermDb::addTerm(Node n,
     d_iclosure_processed.insert(n);
     rec = true;
   }
-  if (rec && n.getKind() != FORALL)
+  if (rec && !n.isClosure())
   {
     for (const Node& nc : n)
     {
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 7d0adab96..9007386c4 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -57,8 +57,8 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
       continue;
     }
 
-    if (!d_substituteUnderQuantifiers &&
-        (current.getKind() == kind::FORALL || current.getKind() == kind::EXISTS)) {
+    if (!d_substituteUnderQuantifiers && current.isClosure())
+    {
       Debug("substitution::internal") << "--not substituting under quantifier" << endl;
       cache[current] = current;
       toVisit.pop_back();
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 8733c2e20..3b11d8e54 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -35,10 +35,7 @@ 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::LAMBDA
-       || parent.getKind() == kind::CHOICE
-       || parent.getKind() == kind::REWRITE_RULE
+  if ((parent.isClosure() || parent.getKind() == kind::REWRITE_RULE
        || parent.getKind() == kind::SEP_STAR
        || parent.getKind() == kind::SEP_WAND
        || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
@@ -181,10 +178,7 @@ 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::LAMBDA
-       || parent.getKind() == kind::CHOICE
-       || parent.getKind() == kind::REWRITE_RULE
+  if ((parent.isClosure() || parent.getKind() == kind::REWRITE_RULE
        || parent.getKind() == kind::SEP_STAR
        || parent.getKind() == kind::SEP_WAND
        || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index dceeeae7a..78db1718e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1061,9 +1061,7 @@ Node TheoryEngine::ppTheoryRewrite(TNode term) {
 
   Node newTerm;
   // do not rewrite inside quantifiers
-  if (term.getKind() == kind::FORALL || term.getKind() == kind::EXISTS
-      || term.getKind() == kind::CHOICE
-      || term.getKind() == kind::LAMBDA)
+  if (term.isClosure())
   {
     newTerm = Rewriter::rewrite(term);
   }
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 7a4a0f041..b032dfec4 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -80,7 +80,7 @@ void TheoryEngineModelBuilder::addAssignableSubterms(TNode n,
                                                      TheoryModel* tm,
                                                      NodeSet& cache)
 {
-  if (n.getKind() == FORALL || n.getKind() == EXISTS)
+  if (n.isClosure())
   {
     return;
   }
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index ddc0e1b90..508bd5002 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -455,7 +455,8 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
   while(!workList.empty()) {
     n = workList.back();
 
-    if(n.getKind() == kind::FORALL || n.getKind() == kind::EXISTS) {
+    if (n.isClosure())
+    {
       // unsafe to go under quantifiers; we might pull bound vars out of scope!
       processed.insert(n);
       workList.pop_back();