From b9f0e5df83a9e8cfd489112a385e4ee3520de771 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 15 Apr 2018 13:58:21 -0500 Subject: Fix type error with regexp (#1778) --- src/theory/strings/theory_strings.cpp | 35 ++++++++++------------------------- 1 file changed, 10 insertions(+), 25 deletions(-) (limited to 'src') 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 &nf_exp) { } break; } - case kind::REGEXP_CONCAT: { - std::vector< Node > vec_nodes; - for(unsigned i=0; i vec_nodes; - for(unsigned i=0; imkNode(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; imkNode(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: -- cgit v1.2.3