diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-03-15 17:01:42 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-15 17:01:42 -0500 |
commit | e8f23236b7f797fd3cd8900df0422d44f1a6a7e0 (patch) | |
tree | d0f8f1167e34509b15797e2a3b78cd21d9dff82f /src/expr/node_algorithm.h | |
parent | a74e32e26d33e18b84edee4b27e352afc5271eef (diff) |
Adding capture avoiding substitution (#2867)
Diffstat (limited to 'src/expr/node_algorithm.h')
-rw-r--r-- | src/expr/node_algorithm.h | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index bf2cb5877..7cc12b664 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -83,6 +83,19 @@ void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms); void getSymbols(TNode n, std::unordered_set<Node, NodeHashFunction>& syms, std::unordered_set<TNode, TNodeHashFunction>& visited); +/** + * Substitution of Nodes in a capture avoiding way. + */ +Node substituteCaptureAvoiding(TNode n, Node src, Node dest); + +/** + * Simultaneous substitution of Nodes in a capture avoiding way. Elements in + * source will be replaced by their corresponding element in dest. Both + * vectors should have the same size. + */ +Node substituteCaptureAvoiding(TNode n, + std::vector<Node>& src, + std::vector<Node>& dest); } // namespace expr } // namespace CVC4 |