diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-04-17 12:42:11 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-04-17 12:42:11 -0500 |
commit | d0c44a9e048558887ab75aaec4c493696c67b456 (patch) | |
tree | ba64a48d289a7d2cde5ff2a2e5886a4babfb441f /src/theory | |
parent | 5b00f8d6804bf9f71d6169634341011f99d59b8b (diff) |
More use of isClosure (#2959)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 | ||||
-rw-r--r-- | src/theory/substitutions.cpp | 4 | ||||
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 10 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory_model_builder.cpp | 2 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 3 |
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(); |