mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 01:18:45 +00:00
Code Activity

z3str3: add str.is_digit support (#5038)

Browse source
This commit is contained in:
Murphy Berzish 2021-02-23 10:36:01 -06:00 • committed by GitHub
parent c3b7fa941a
commit 5599387a34
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 33 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/smt/theory_str.cpp
View file

@ -831,6 +831,8 @@ namespace smt {
instantiate_axiom_Replace(e); instantiate_axiom_Replace(e);
} else if (u.str.is_in_re(a)) { } else if (u.str.is_in_re(a)) {
instantiate_axiom_RegexIn(e); instantiate_axiom_RegexIn(e);
} else if (u.str.is_is_digit(a)) {
instantiate_axiom_is_digit(e);
} else if (u.str.is_from_code(a)) { } else if (u.str.is_from_code(a)) {
instantiate_axiom_str_from_code(e); instantiate_axiom_str_from_code(e);
} else if (u.str.is_to_code(a)) { } else if (u.str.is_to_code(a)) {
@ -1828,6 +1830,34 @@ namespace smt {
} }
} }
void theory_str::instantiate_axiom_is_digit(enode * e) {
ast_manager & m = get_manager();
app * ex = e->get_owner();
if (axiomatized_terms.contains(ex)) {
TRACE("str", tout << "already set up str.is_digit axiom for " << mk_pp(ex, m) << std::endl;);
return;
}
axiomatized_terms.insert(ex);
TRACE("str", tout << "instantiate str.is_digit axiom for " << mk_pp(ex, m) << std::endl;);
expr * string_term = nullptr;
u.str.is_is_digit(ex, string_term);
SASSERT(string_term);
expr_ref_vector rhs_terms(m);
for (unsigned c = 0x30; c <= 0x39; ++c) {
zstring ch(c);
expr_ref rhs_term(ctx.mk_eq_atom(string_term, mk_string(ch)), m);
rhs_terms.push_back(rhs_term);
}
expr_ref rhs(mk_or(rhs_terms), m);
expr_ref axiom(ctx.mk_eq_atom(ex, rhs), m);
assert_axiom_rw(axiom);
}
void theory_str::instantiate_axiom_str_from_code(enode * e) { void theory_str::instantiate_axiom_str_from_code(enode * e) {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
@ -6867,7 +6897,7 @@ namespace smt {
sort * int_sort = m.mk_sort(m_arith_fid, INT_SORT); sort * int_sort = m.mk_sort(m_arith_fid, INT_SORT);
// reject unhandled expressions // reject unhandled expressions
if (u.str.is_replace_all(ex) || u.str.is_replace_re(ex) || u.str.is_replace_re_all(ex) || u.str.is_is_digit(ex)) { if (u.str.is_replace_all(ex) || u.str.is_replace_re(ex) || u.str.is_replace_re_all(ex)) {
TRACE("str", tout << "ERROR: Z3str3 has encountered an unsupported operator. Aborting." << std::endl;); TRACE("str", tout << "ERROR: Z3str3 has encountered an unsupported operator. Aborting." << std::endl;);
m.raise_exception("Z3str3 encountered an unsupported operator."); m.raise_exception("Z3str3 encountered an unsupported operator.");
} }
@ -6926,7 +6956,7 @@ namespace smt {
if (is_app(ex)) { if (is_app(ex)) {
app * ap = to_app(ex); app * ap = to_app(ex);
if (u.str.is_prefix(ap) || u.str.is_suffix(ap) || u.str.is_contains(ap) || u.str.is_in_re(ap)) { if (u.str.is_prefix(ap) || u.str.is_suffix(ap) || u.str.is_contains(ap) || u.str.is_in_re(ap) || u.str.is_is_digit(ap)) {
m_library_aware_axiom_todo.push_back(n); m_library_aware_axiom_todo.push_back(n);
m_library_aware_trail_stack.push(push_back_trail<enode*, false>(m_library_aware_axiom_todo)); m_library_aware_trail_stack.push(push_back_trail<enode*, false>(m_library_aware_axiom_todo));
} }

1
src/smt/theory_str.h
View file

@ -606,6 +606,7 @@ protected:
void instantiate_axiom_Replace(enode * e); void instantiate_axiom_Replace(enode * e);
void instantiate_axiom_str_to_int(enode * e); void instantiate_axiom_str_to_int(enode * e);
void instantiate_axiom_int_to_str(enode * e); void instantiate_axiom_int_to_str(enode * e);
void instantiate_axiom_is_digit(enode * e);
void instantiate_axiom_str_to_code(enode * e); void instantiate_axiom_str_to_code(enode * e);
void instantiate_axiom_str_from_code(enode * e); void instantiate_axiom_str_from_code(enode * e);