mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

fix indentation

Browse source
This commit is contained in:
Murphy Berzish 2017-08-09 15:38:56 -04:00
parent fce35fdb61
commit 84abdae5f7
1 changed files with 26 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
src/smt/theory_str.cpp
View file

@ -6190,32 +6190,32 @@ namespace smt {
zstring 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";);
/*
* For an n-character string, we make (n-1) intermediate states,
* labelled i_(0) through i_(n-2).
* Then we construct the following transitions:
* start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final
*/
unsigned last = start;
for (int i = 0; i <= ((int)str.length()) - 2; ++i) {
unsigned i_state = next_id();
make_transition(last, str[i], i_state);
TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";);
last = i_state;
}
make_transition(last, str[(str.length() - 1)], end);
TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";);
}
} else { // ! u.str.is_string(arg_str, str)
TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;);
m_valid = false;
return;
}
// 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";);
/*
* For an n-character string, we make (n-1) intermediate states,
* labelled i_(0) through i_(n-2).
* Then we construct the following transitions:
* start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final
*/
unsigned last = start;
for (int i = 0; i <= ((int)str.length()) - 2; ++i) {
unsigned i_state = next_id();
make_transition(last, str[i], i_state);
TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";);
last = i_state;
}
make_transition(last, str[(str.length() - 1)], end);
TRACE("str", tout << "string transition " << last << "--" << str[(str.length() - 1)] << "--> " << end << "\n";);
}
} else { // ! u.str.is_string(arg_str, str)
TRACE("str", tout << "invalid string constant in Str2Reg" << std::endl;);
m_valid = false;
return;
}
} else if (u.re.is_concat(e)){
app * a = to_app(e);
expr * re1 = a->get_arg(0);