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

Merge pull request #1508 from mtrberzi/regex-allchar

Browse source 
add re.allchar support in z3str3
This commit is contained in:
Nikolaj Bjorner 2018-02-27 09:12:13 +09:00 • committed by GitHub
commit fbbc57168d
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 12 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/smt/theory_str.cpp
View file

@ -1812,8 +1812,11 @@ namespace smt {
// trivially true for any string!
assert_axiom(ex);
} else if (u.re.is_full_char(regex)) {
TRACE("str", tout << "ERROR: unknown regex expression " << mk_pp(regex, m) << "!" << std::endl;);
NOT_IMPLEMENTED_YET();
// any char = any string of length 1
expr_ref rhs(ctx.mk_eq_atom(mk_strlen(str), mk_int(1)), m);
expr_ref finalAxiom(m.mk_iff(ex, rhs), m);
SASSERT(finalAxiom);
assert_axiom(finalAxiom);
} else {
TRACE("str", tout << "ERROR: unknown regex expression " << mk_pp(regex, m) << "!" << std::endl;);
NOT_IMPLEMENTED_YET();
@ -6327,6 +6330,13 @@ namespace smt {
make_transition(tmp, ch, tmp);
}
TRACE("str", tout << "re.all NFA: start = " << start << ", end = " << end << std::endl;);
} else if (u.re.is_full_char(e)) {
// effectively . (match any one character)
for (unsigned int i = 0; i < 256; ++i) {
char ch = (char)i;
make_transition(start, ch, end);
}
TRACE("str", tout << "re.allchar NFA: start = " << start << ", end = " << end << std::endl;);
} else {
TRACE("str", tout << "invalid regular expression" << std::endl;);
m_valid = false;