mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

Revert "fix indentation and add support for re.allchar"

Browse source 
This reverts commit cadde94017.
This commit is contained in:
Murphy Berzish 2017-08-09 15:37:52 -04:00
parent cadde94017
commit fce35fdb61
1 changed files with 26 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

70
src/smt/theory_str.cpp
View file

@ -1685,8 +1685,6 @@ namespace smt {
u.str.is_string(range1, range1val); u.str.is_string(range1, range1val);
u.str.is_string(range2, range2val); u.str.is_string(range2, range2val);
return zstring("[") + range1val + zstring("-") + range2val + zstring("]"); return zstring("[") + range1val + zstring("-") + range2val + zstring("]");
} else if (u.re.is_full(a_regex)) {
return zstring(".");
} else { } else {
TRACE("str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;); TRACE("str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;);
UNREACHABLE(); return zstring(""); UNREACHABLE(); return zstring("");
@ -1796,13 +1794,6 @@ namespace smt {
expr_ref finalAxiom(m.mk_iff(ex, rhs), m); expr_ref finalAxiom(m.mk_iff(ex, rhs), m);
SASSERT(finalAxiom); SASSERT(finalAxiom);
assert_axiom(finalAxiom); assert_axiom(finalAxiom);
} else if (u.re.is_full(regex)) {
// equivalent to regex "." operator, match any one character.
// we rewrite to expr IFF len(str) == 1
expr_ref rhs(ctx.mk_eq_atom(mk_strlen(str), m_autil.mk_numeral(rational::one(), true)), m);
expr_ref finalAxiom(m.mk_iff(ex, rhs), m);
SASSERT(finalAxiom);
assert_axiom(finalAxiom);
} else { } else {
TRACE("str", tout << "ERROR: unknown regex expression " << mk_pp(regex, m) << "!" << std::endl;); TRACE("str", tout << "ERROR: unknown regex expression " << mk_pp(regex, m) << "!" << std::endl;);
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
@ -6199,32 +6190,32 @@ namespace smt {
zstring str; zstring str;
if (u.str.is_string(arg_str, str)) { if (u.str.is_string(arg_str, str)) {
if (str.length() == 0) { if (str.length() == 0) {
// transitioning on the empty string is handled specially // transitioning on the empty string is handled specially
TRACE("str", tout << "empty string epsilon-move " << start << " --> " << end << std::endl;); TRACE("str", tout << "empty string epsilon-move " << start << " --> " << end << std::endl;);
make_epsilon_move(start, end); make_epsilon_move(start, end);
} else { } 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,
* labelled i_(0) through i_(n-2). * labelled i_(0) through i_(n-2).
* Then we construct the following transitions: * Then we construct the following transitions:
* start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final * start --str[0]--> i_(0) --str[1]--> i_(1) --...--> i_(n-2) --str[n-1]--> final
*/ */
unsigned last = start; unsigned last = start;
for (int i = 0; i <= ((int)str.length()) - 2; ++i) { for (int i = 0; i <= ((int)str.length()) - 2; ++i) {
unsigned i_state = next_id(); unsigned i_state = next_id();
make_transition(last, str[i], i_state); make_transition(last, str[i], i_state);
TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";); TRACE("str", tout << "string transition " << last << "--" << str[i] << "--> " << i_state << "\n";);
last = i_state; last = i_state;
} }
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 { // ! u.str.is_string(arg_str, str) } 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;
} }
} else if (u.re.is_concat(e)){ } else if (u.re.is_concat(e)){
app * a = to_app(e); app * a = to_app(e);
expr * re1 = a->get_arg(0); expr * re1 = a->get_arg(0);
@ -6293,15 +6284,6 @@ 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)) {
// equivalent to "transition on each character in the alphabet"
// TODO this hard-codes something about theory_str's char set here
for (unsigned i = 1; i <= 255; ++i) {
char ch = (char)i;
make_transition(start, ch, end);
}
} else { } else {
TRACE("str", tout << "invalid regular expression" << std::endl;); TRACE("str", tout << "invalid regular expression" << std::endl;);
m_valid = false; m_valid = false;