More use of isClosure (#2959)

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 71f41354a073aa324606a20514068ad80bd435ba..2e68328409c91fffadbafcc09d86c1ad8f96c87d 100644 (file)
--- 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 5456f32858c7af17500a9b11ed2c239a700f3c34..cd7a1f839fa9776e1addac3cfc60b7e8d72e1d36 100644 (file)
--- 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 4e62bc9ad0327c4ca84c263078e11fb10e5bbbb5..25ffb077894f0a700dddb7d5878096d68d984ca5 100644 (file)
--- 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 f83cb7f31cdcec0a7c390d794b7a218863dcb269..9fb9fc9f56e8008ace14709eec5b4c9dc91b2dcf 100644 (file)
--- 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 d3cfc043852150798fc8f78b593b008828c3c450..cf5f354572224a304a10b8e1eaf620715075ac8e 100644 (file)
--- 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 f610cc7df5fdfbf3471b5cbbc56f68488b37c4f6..d37ed05e159199418d13f16658581d9ff89f5e3e 100644 (file)
--- 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 472e2561f0b1638635f077e64f0f998b1b90c48b..51cc15c124d915d0f95b8c116bf3b05d3e5b4892 100644 (file)
--- 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 7d0adab96b72a65a600a1c39b068a6480b9bf592..9007386c442535d264ebf953bb39bd36376cb996 100644 (file)
--- 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 8733c2e20ba5452de1792401baf086ca96385755..3b11d8e546712d272d00f1aec266d61a82fd3ed8 100644 (file)
--- 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 dceeeae7ac1c1e522d9071d2ef5ea98bd82c610b..78db1718ef7aa404fda886885b9ef2a79de35789 100644 (file)
--- 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 7a4a0f04145606c8099c06369826ad8b1e2afa40..b032dfec4386d928179cbbbb6e8f1d9eabff79a1 100644 (file)
--- 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 ddc0e1b905730c090fc486bf507dfad634de16cd..508bd50021d31f47bb4ad50d15658fe050715bee 100644 (file)
--- 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();