mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 21:50:52 +00:00
Code Activity

fix indentation and add support for re.allchar

Browse source
This commit is contained in:
Murphy Berzish 2017-08-07 23:02:55 -04:00
parent f4c0e0b28d
commit cadde94017
1 changed files with 44 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/smt/theory_str.cpp
View file

@ -1685,6 +1685,8 @@ 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("");
@ -1794,6 +1796,13 @@ 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();
@ -6284,6 +6293,15 @@ 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;