diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-05 12:41:47 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-05 12:41:47 -0500 |
commit | 4e4068f1d29ddc1ffe0bde8e6f2cf3094fd6bd40 (patch) | |
tree | 49c496d78643921bbb0cdbf436b49965ce5a5161 /src/expr | |
parent | 1752aeb263a986bf437bb04029474b41987450d2 (diff) |
Finer-grained inference of substitutions in incremental mode (#2403)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_algorithm.cpp | 36 | ||||
-rw-r--r-- | src/expr/node_algorithm.h | 19 |
2 files changed, 52 insertions, 3 deletions
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 5443a3a2a..9240e4a8e 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -166,5 +166,41 @@ bool hasFreeVar(TNode n) return false; } +void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms) +{ + std::unordered_set<TNode, TNodeHashFunction> visited; + getSymbols(n, syms); +} + +void getSymbols(TNode n, + std::unordered_set<Node, NodeHashFunction>& syms, + std::unordered_set<TNode, TNodeHashFunction>& visited) +{ + std::vector<TNode> visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.isVar() && cur.getKind() != kind::BOUND_VARIABLE) + { + syms.insert(cur); + } + if (cur.hasOperator()) + { + visit.push_back(cur.getOperator()); + } + for (TNode cn : cur) + { + visit.push_back(cn); + } + } + } while (!visit.empty()); +} + } // namespace expr } // namespace CVC4 diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 61e81c4c2..7453bc292 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -39,20 +39,33 @@ namespace expr { bool hasSubterm(TNode n, TNode t, bool strict = false); /** - * Returns true iff the node n contains a bound variable. This bound - * variable may or may not be free. + * Returns true iff the node n contains a bound variable, that is a node of + * kind BOUND_VARIABLE. This bound variable may or may not be free. * @param n The node under investigation * @return true iff this node contains a bound variable */ bool hasBoundVar(TNode n); /** - * Returns true iff the node n contains a free variable. + * Returns true iff the node n contains a free variable, that is, a node + * of kind BOUND_VARIABLE that is not bound in n. * @param n The node under investigation * @return true iff this node contains a free variable. */ bool hasFreeVar(TNode n); +/** + * For term n, this function collects the symbols that occur as a subterms + * of n. A symbol is a variable that does not have kind BOUND_VARIABLE. + * @param n The node under investigation + * @param syms The set which the symbols of n are added to + */ +void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms); +/** Same as above, with a visited cache */ +void getSymbols(TNode n, + std::unordered_set<Node, NodeHashFunction>& syms, + std::unordered_set<TNode, TNodeHashFunction>& visited); + } // namespace expr } // namespace CVC4 |