From adae32f7efeb5c4bcf4777792f04e53c03e1e564 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Sat, 19 Aug 2017 23:25:34 -0400 Subject: [PATCH] add re.all to NFA in theory_str --- src/smt/theory_str.cpp | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 7fbc15e8a..127409efe 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -6297,9 +6297,18 @@ namespace smt { TRACE("str", tout << "range NFA: start = " << start << ", end = " << end << std::endl;); } else if (u.re.is_full(e)) { - NOT_IMPLEMENTED_YET(); - m_valid = false; - return; + // effectively the same as .* where . can be any single character + // start --e--> tmp + // tmp --e--> end + // tmp --C--> tmp for every character C + unsigned tmp = next_id(); + make_epsilon_move(start, tmp); + make_epsilon_move(tmp, end); + for (unsigned int i = 0; i < 256; ++i) { + char ch = (char)i; + make_transition(tmp, ch, tmp); + } + TRACE("str", tout << "re.all NFA: start = " << start << ", end = " << end << std::endl;); } else { TRACE("str", tout << "invalid regular expression" << std::endl;); m_valid = false;