diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/node_algorithm.cpp | 59 | ||||
-rw-r--r-- | src/expr/node_algorithm.h | 14 |
2 files changed, 48 insertions, 25 deletions
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index f41bef37b..2439e28b6 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -328,8 +328,16 @@ bool getFreeVariables(TNode n, std::unordered_set<Node, NodeHashFunction>& fvs, bool computeFv) { - std::unordered_set<TNode, TNodeHashFunction> bound_var; - std::unordered_map<TNode, bool, TNodeHashFunction> visited; + std::unordered_set<TNode, TNodeHashFunction> scope; + return getFreeVariablesScope(n, fvs, scope, computeFv); +} + +bool getFreeVariablesScope(TNode n, + std::unordered_set<Node, NodeHashFunction>& fvs, + std::unordered_set<TNode, TNodeHashFunction>& scope, + bool computeFv) +{ + std::unordered_set<TNode, TNodeHashFunction> visited; std::vector<TNode> visit; TNode cur; visit.push_back(n); @@ -342,15 +350,14 @@ bool getFreeVariables(TNode n, { continue; } - Kind k = cur.getKind(); - bool isQuant = cur.isClosure(); - std::unordered_map<TNode, bool, TNodeHashFunction>::iterator itv = + std::unordered_set<TNode, TNodeHashFunction>::iterator itv = visited.find(cur); if (itv == visited.end()) { - if (k == kind::BOUND_VARIABLE) + visited.insert(cur); + if (cur.getKind() == kind::BOUND_VARIABLE) { - if (bound_var.find(cur) == bound_var.end()) + if (scope.find(cur) == scope.end()) { if (computeFv) { @@ -362,32 +369,34 @@ bool getFreeVariables(TNode n, } } } - else if (isQuant) + else if (cur.isClosure()) { + // add to scope for (const TNode& cn : cur[0]) { // should not shadow - Assert(bound_var.find(cn) == bound_var.end()); - bound_var.insert(cn); + Assert(scope.find(cn) == scope.end()); + scope.insert(cn); + } + // must make recursive call to use separate cache + if (getFreeVariablesScope(cur[1], fvs, scope, computeFv) && !computeFv) + { + return true; + } + // cleanup + for (const TNode& cn : cur[0]) + { + scope.erase(cn); } - visit.push_back(cur); - } - // must visit quantifiers again to clean up below - visited[cur] = !isQuant; - if (cur.hasOperator()) - { - visit.push_back(cur.getOperator()); } - visit.insert(visit.end(), cur.begin(), cur.end()); - } - else if (!itv->second) - { - Assert(isQuant); - for (const TNode& cn : cur[0]) + else { - bound_var.erase(cn); + if (cur.hasOperator()) + { + visit.push_back(cur.getOperator()); + } + visit.insert(visit.end(), cur.begin(), cur.end()); } - visited[cur] = true; } } while (!visit.empty()); diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 7b6dd4f8c..f5d9f6516 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -105,6 +105,20 @@ bool hasClosure(Node n); bool getFreeVariables(TNode n, std::unordered_set<Node, NodeHashFunction>& fvs, bool computeFv = true); +/** + * Get the free variables in n, that is, the subterms of n of kind + * BOUND_VARIABLE that are not bound in n or occur in scope, adds these to fvs. + * @param n The node under investigation + * @param fvs The set which free variables are added to + * @param scope The scope we are considering. + * @param computeFv If this flag is false, then we only return true/false and + * do not add to fvs. + * @return true iff this node contains a free variable. + */ +bool getFreeVariablesScope(TNode n, + std::unordered_set<Node, NodeHashFunction>& fvs, + std::unordered_set<TNode, TNodeHashFunction>& scope, + bool computeFv = true); /** * Get all variables in n. |