From: Andrew Reynolds Date: Wed, 17 Apr 2019 17:42:11 +0000 (-0500) Subject: More use of isClosure (#2959) X-Git-Tag: cvc5-1.0.0~4174 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d0c44a9e048558887ab75aaec4c493696c67b456;p=cvc5.git More use of isClosure (#2959) --- 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::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& 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();