mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

add re.allchar support in z3str3

Browse source
This commit is contained in:
Murphy Berzish 2018-02-26 17:19:45 -05:00
parent 5d457c95aa
commit ac9b03528a
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! // trivially true for any string!
assert_axiom(ex); assert_axiom(ex);
} else if (u.re.is_full_char(regex)) { } else if (u.re.is_full_char(regex)) {
TRACE("str", tout << "ERROR: unknown regex expression " << mk_pp(regex, m) << "!" << std::endl;); // any char = any string of length 1
NOT_IMPLEMENTED_YET(); 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 { } 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();
@ -6327,6 +6330,13 @@ namespace smt {
make_transition(tmp, ch, tmp); make_transition(tmp, ch, tmp);
} }
TRACE("str", tout << "re.all NFA: start = " << start << ", end = " << end << std::endl;); 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 { } else {
TRACE("str", tout << "invalid regular expression" << std::endl;); TRACE("str", tout << "invalid regular expression" << std::endl;);
m_valid = false; m_valid = false;