diff options
Diffstat (limited to 'src/expr/node.cpp')
-rw-r--r-- | src/expr/node.cpp | 98 |
1 files changed, 0 insertions, 98 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp index fdb1e4d90..b983c81f5 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -73,13 +73,8 @@ UnknownTypeException::UnknownTypeException(TNode n) /** Is this node constant? (and has that been computed yet?) */ struct IsConstTag { }; struct IsConstComputedTag { }; -struct HasBoundVarTag { }; -struct HasBoundVarComputedTag { }; typedef expr::Attribute<IsConstTag, bool> IsConstAttr; typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr; -/** Attribute true for expressions with bound variables in them */ -typedef expr::Attribute<HasBoundVarTag, bool> HasBoundVarAttr; -typedef expr::Attribute<HasBoundVarComputedTag, bool> HasBoundVarComputedAttr; template <bool ref_count> bool NodeTemplate<ref_count>::isConst() const { @@ -114,100 +109,7 @@ bool NodeTemplate<ref_count>::isConst() const { } } -template <bool ref_count> -bool NodeTemplate<ref_count>::hasBoundVar() { - assertTNodeNotExpired(); - if(! getAttribute(HasBoundVarComputedAttr())) { - bool hasBv = false; - if(getKind() == kind::BOUND_VARIABLE) { - hasBv = true; - } else { - for(iterator i = begin(); i != end() && !hasBv; ++i) { - hasBv = (*i).hasBoundVar(); - } - } - if (!hasBv && hasOperator()) { - hasBv = getOperator().hasBoundVar(); - } - setAttribute(HasBoundVarAttr(), hasBv); - setAttribute(HasBoundVarComputedAttr(), true); - Debug("bva") << *this << " has bva : " << getAttribute(HasBoundVarAttr()) << std::endl; - return hasBv; - } - return getAttribute(HasBoundVarAttr()); -} - -template <bool ref_count> -bool NodeTemplate<ref_count>::hasFreeVar() -{ - assertTNodeNotExpired(); - std::unordered_set<TNode, TNodeHashFunction> bound_var; - std::unordered_map<TNode, bool, TNodeHashFunction> visited; - std::vector<TNode> visit; - TNode cur; - visit.push_back(*this); - do - { - cur = visit.back(); - visit.pop_back(); - // can skip if it doesn't have a bound variable - if (!cur.hasBoundVar()) - { - continue; - } - Kind k = cur.getKind(); - bool isQuant = k == kind::FORALL || k == kind::EXISTS || k == kind::LAMBDA - || k == kind::CHOICE; - std::unordered_map<TNode, bool, TNodeHashFunction>::iterator itv = - visited.find(cur); - if (itv == visited.end()) - { - if (k == kind::BOUND_VARIABLE) - { - if (bound_var.find(cur) == bound_var.end()) - { - return true; - } - } - else if (isQuant) - { - for (const TNode& cn : cur[0]) - { - // should not shadow - Assert(bound_var.find(cn) == bound_var.end()); - bound_var.insert(cn); - } - visit.push_back(cur); - } - // must visit quantifiers again to clean up below - visited[cur] = !isQuant; - if (cur.hasOperator()) - { - visit.push_back(cur.getOperator()); - } - for (const TNode& cn : cur) - { - visit.push_back(cn); - } - } - else if (!itv->second) - { - Assert(isQuant); - for (const TNode& cn : cur[0]) - { - bound_var.erase(cn); - } - visited[cur] = true; - } - } while (!visit.empty()); - return false; -} - template bool NodeTemplate<true>::isConst() const; template bool NodeTemplate<false>::isConst() const; -template bool NodeTemplate<true>::hasBoundVar(); -template bool NodeTemplate<false>::hasBoundVar(); -template bool NodeTemplate<true>::hasFreeVar(); -template bool NodeTemplate<false>::hasFreeVar(); }/* CVC4 namespace */ |