diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-06-25 19:36:59 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-25 21:36:59 -0500 |
| commit | ccd4500c03685952ebf571b3539bd9e29c829cb5 (patch) | |
| tree | d4ae6bac75d458a0eb2d7b5887175d258fcb3368 /src/expr | |
| parent | 23aa2a0868027527469f2293952f038c66db23e1 (diff) | |
fix and test (#4658)
This PR adds support for indexed operators (such as extract) to getOperatorsMap in node_algorithm.cpp. The corresponding test is augmented accordingly.
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/node_algorithm.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 52c5165a6..be436bf8b 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -491,7 +491,13 @@ void getOperatorsMap( // add the current operator to the result if (cur.hasOperator()) { - ops[tn].insert(NodeManager::currentNM()->operatorOf(cur.getKind())); + Node o; + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) { + o = cur.getOperator(); + } else { + o = NodeManager::currentNM()->operatorOf(cur.getKind()); + } + ops[tn].insert(o); } // add children to visit in the future for (TNode cn : cur) |