diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-15 13:58:21 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-15 13:58:21 -0500 |
| commit | b9f0e5df83a9e8cfd489112a385e4ee3520de771 (patch) | |
| tree | 772c800e7fafa528fd14720561ca80fc13b8148f /src | |
| parent | c22c31b0dfab057cd41cd276852d27d905274c9a (diff) | |
Fix type error with regexp (#1778)
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 35 |
1 files changed, 10 insertions, 25 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 142695b9d..713c346e0 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -4621,33 +4621,18 @@ Node TheoryStrings::getNormalSymRegExp(Node r, std::vector<Node> &nf_exp) { } break; } - case kind::REGEXP_CONCAT: { - std::vector< Node > vec_nodes; - for(unsigned i=0; i<r.getNumChildren(); ++i) { - vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) ); - } - ret = mkConcat(vec_nodes); - break; - } - case kind::REGEXP_UNION: { - std::vector< Node > vec_nodes; - for(unsigned i=0; i<r.getNumChildren(); ++i) { - vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) ); - } - ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes) ); - break; - } - case kind::REGEXP_INTER: { + case kind::REGEXP_CONCAT: + case kind::REGEXP_UNION: + case kind::REGEXP_INTER: + case kind::REGEXP_STAR: + { std::vector< Node > vec_nodes; - for(unsigned i=0; i<r.getNumChildren(); ++i) { - vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) ); + for (const Node& cr : r) + { + vec_nodes.push_back(getNormalSymRegExp(cr, nf_exp)); } - ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_INTER, vec_nodes) ); - break; - } - case kind::REGEXP_STAR: { - ret = getNormalSymRegExp( r[0], nf_exp ); - ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, ret) ); + ret = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(r.getKind(), vec_nodes)); break; } //case kind::REGEXP_PLUS: |