More use of isClosure (#2959)

12 files changed, 20 insertions, 29 deletions

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 71f41354a..2e6832840 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -520,7 +520,7 @@ public:
 
   /**
    * Create a new, fresh variable for use in a binder expression
-   * (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA).  It is
+   * (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or CHOICE).  It is
    * an error for this bound variable to exist outside of a binder,
    * and it should also only be used in a single binder expression.
    * That is, two distinct FORALL expressions should use entirely
@@ -539,7 +539,7 @@ public:
 
   /**
    * Create a (nameless) new, fresh variable for use in a binder
-   * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA).
+   * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or CHOICE).
    * It is an error for this bound variable to exist outside of a
    * binder, and it should also only be used in a single binder
    * expression.  That is, two distinct FORALL expressions should use
diff --git a/src/expr/node.h b/src/expr/node.h
index 5456f3285..cd7a1f839 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -468,6 +468,10 @@ public:
     return getMetaKind() == kind::metakind::NULLARY_OPERATOR;
   }
 
+  /**
+   * Returns true if this node represents a closure, that is an expression
+   * that binds variables.
+   */
   inline bool isClosure() const {
     assertTNodeNotExpired();
     return getKind() == kind::LAMBDA || getKind() == kind::FORALL
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 4e62bc9ad..25ffb0778 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -182,8 +182,7 @@ bool getFreeVariables(TNode n,
       continue;
     }
     Kind k = cur.getKind();
-    bool isQuant = k == kind::FORALL || k == kind::EXISTS || k == kind::LAMBDA
-                   || k == kind::CHOICE;
+    bool isQuant = cur.isClosure();
     std::unordered_map<TNode, bool, TNodeHashFunction>::iterator itv =
         visited.find(cur);
     if (itv == visited.end())
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index f83cb7f31..9fb9fc9f5 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -80,7 +80,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
         Trace("srs-input-debug") << "...preprocess " << cur << std::endl;
         visited[cur] = false;
         Kind k = cur.getKind();
-        bool isQuant = k == FORALL || k == EXISTS || k == LAMBDA || k == CHOICE;
+        bool isQuant = cur.isClosure();
         // we recurse on this node if it is not a quantified formula
         if (!isQuant)
         {
diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
index d3cfc0438..cf5f35457 100644
--- a/src/printer/dagification_visitor.cpp
+++ b/src/printer/dagification_visitor.cpp
@@ -47,8 +47,7 @@ DagificationVisitor::~DagificationVisitor() {
 
 bool DagificationVisitor::alreadyVisited(TNode current, TNode parent) {
   Kind ck = current.getKind();
-  if (ck == kind::FORALL || ck == kind::EXISTS || ck == kind::LAMBDA
-      || ck == kind::CHOICE)
+  if (current.isClosure())
   {
     // for quantifiers, we visit them but we don't recurse on them
     visit(current, parent);
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index f610cc7df..d37ed05e1 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -207,9 +207,7 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
     return skolem;
   }
 
-  if (node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS
-      || node.getKind() == kind::LAMBDA
-      || node.getKind() == kind::CHOICE)
+  if (node.isClosure())
   {
     // Remember if we're inside a quantifier
     inQuant = true;
@@ -269,9 +267,7 @@ Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const {
     return cached.isNull() ? Node(node) : cached;
   }
 
-  if (node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS
-      || node.getKind() == kind::LAMBDA
-      || node.getKind() == kind::CHOICE)
+  if (node.isClosure())
   {
     // Remember if we're inside a quantifier
     inQuant = true;
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();