mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

add re.all to NFA in theory_str

Browse source
This commit is contained in:
Murphy Berzish 2017-08-19 23:25:34 -04:00
parent 1e445a62d4
commit adae32f7ef
1 changed files with 12 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/theory_str.cpp
View file

@ -6297,9 +6297,18 @@ namespace smt {
TRACE("str", tout << "range NFA: start = " << start << ", end = " << end << std::endl;); TRACE("str", tout << "range NFA: start = " << start << ", end = " << end << std::endl;);
} else if (u.re.is_full(e)) { } else if (u.re.is_full(e)) {
NOT_IMPLEMENTED_YET(); // effectively the same as .* where . can be any single character
m_valid = false; // start --e--> tmp
return; // 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 { } else {
TRACE("str", tout << "invalid regular expression" << std::endl;); TRACE("str", tout << "invalid regular expression" << std::endl;);
m_valid = false; m_valid = false;