mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-22 19:17:53 +00:00
Code Activity

fix regex bug in theory_str for empty string match. need to fix indents

Browse source
This commit is contained in:
Murphy Berzish 2017-08-06 17:17:04 -04:00
parent 9d6be286d0
commit f4c0e0b28d
1 changed files with 27 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_str.cpp
View file

@ -6189,6 +6189,11 @@ namespace smt {
expr * arg_str = a->get_arg(0); expr * arg_str = a->get_arg(0);
zstring str; zstring str;
if (u.str.is_string(arg_str, str)) { if (u.str.is_string(arg_str, str)) {
if (str.length() == 0) {
// transitioning on the empty string is handled specially
TRACE("str", tout << "empty string epsilon-move " << start << " --> " << end << std::endl;);
make_epsilon_move(start, end);
} else {
TRACE("str", tout << "build NFA for '" << str << "'" << "\n";); TRACE("str", tout << "build NFA for '" << str << "'" << "\n";);
/* /*
* For an n-character string, we make (n-1) intermediate states, * For an n-character string, we make (n-1) intermediate states,
@ -6205,7 +6210,8 @@ namespace smt {
} }
make_transition(last, str[(str.length() - 1)], end); make_transition(last, str[(str.length() - 1)], end);
TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";); TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";);
} else { }
} else { // ! u.str.is_string(arg_str, str)
TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;); TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;);
m_valid = false; m_valid = false;
return; return;