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

add nullable, get-head-tail with Caleb

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-18 19:10:00 -07:00
parent c40c4313a4
commit f8d328b1fb
3 changed files with 78 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast_util.h
View file

@ -102,6 +102,7 @@ expr * get_clause_literal(ast_manager & m, expr * cls, unsigned idx);
*/
expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args);
app * mk_and(ast_manager & m, unsigned num_args, app * const * args);
inline expr * mk_and(ast_manager & m, expr* a, expr* b) { expr* args[2] = { a, b }; return mk_and(m, 2, args); }
inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
@ -123,6 +124,7 @@ app_ref operator+(expr_ref& a, expr_ref& b);
*/
expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args);
app * mk_or(ast_manager & m, unsigned num_args, app * const * args);
inline expr * mk_or(ast_manager & m, expr* a, expr* b) { expr* args[2] = { a, b }; return mk_or(m, 2, args); }
inline app_ref mk_or(app_ref_vector const& args) { return app_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }

73
src/ast/rewriter/seq_rewriter.cpp
View file

@ -1963,6 +1963,79 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
return true;
}
bool seq_rewriter::get_head_tail(expr* s, expr_ref& head, expr_ref& tail) {
expr* h = nullptr, *t = nullptr;
zstring s1;
if (m_util.str.is_unit(s, h)) {
head = h;
tail = m_util.str.mk_empty(m().get_sort(s));
return true;
}
if (m_util.str.is_string(s, s1) && s1.length() > 0) {
head = m_util.str.mk_string(s1.extract(0, 1));
tail = m_util.str.mk_string(s1.extract(1, s1.length()));
return true;
}
if (m_util.str.is_concat(s, h, t) && get_head_tail(h, head, tail)) {
tail = m_util.str.mk_concat(tail, t);
return true;
}
return false;
}
expr_ref seq_rewriter::is_nullable(expr* r) {
SASSERT(m_util.is_re(r));
expr* r1 = nullptr, *r2 = nullptr;
unsigned lo = 0, hi = 0;
if (m_util.re.is_concat(r, r1, r2)) {
return expr_ref(mk_and(m(), is_nullable(r1), is_nullable(r2)), m());
}
if (m_util.re.is_union(r, r1, r2)) {
return expr_ref(mk_or(m(), is_nullable(r1), is_nullable(r2)), m());
}
if (m_util.re.is_intersection(r, r1, r2)) {
return expr_ref(mk_and(m(), is_nullable(r1), is_nullable(r2)), m());
}
if (m_util.re.is_star(r) ||
m_util.re.is_opt(r) ||
m_util.re.is_full_seq(r)) {
return expr_ref(m().mk_true(), m());
}
if (m_util.re.is_full_char(r) ||
m_util.re.is_empty(r) ||
m_util.re.is_of_pred(r)) {
return expr_ref(m().mk_false(), m());
}
if (m_util.re.is_plus(r, r1)) {
return is_nullable(r1);
}
if (m_util.re.is_range(r, r1, r2)) {
if (m_util.is_const_char(r1, lo) && m_util.is_const_char(r2, hi)) {
return expr_ref(m().mk_bool_val(lo > hi), m());
}
else {
return expr_ref(m_util.mk_lt(r2, r1), m());
}
}
if (m_util.re.is_complement(r, r1)) {
return expr_ref(mk_not(m(), is_nullable(r1)), m());
}
if (m_util.re.is_loop(r, r1, lo) || m_util.re.is_loop(r, r1, lo, hi)) {
if (lo == 0) {
return expr_ref(m().mk_true(), m());
}
else if (hi == 0) {
return expr_ref(m().mk_false(), m());
}
else {
return is_nullable(r1);
}
}
sort* seq_sort = nullptr;
VERIFY(m_util.is_re(r, seq_sort));
return expr_ref(m_util.re.mk_in_re(m_util.str.mk_empty(seq_sort), r), m());
}
br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
if (m_util.re.is_empty(b)) {
result = m().mk_false();

3
src/ast/rewriter/seq_rewriter.h
View file

@ -132,6 +132,9 @@ class seq_rewriter {
}
length_comparison compare_lengths(unsigned sza, expr* const* as, unsigned szb, expr* const* bs);
bool get_head_tail(expr* e, expr_ref& head, expr_ref& tail);
expr_ref is_nullable(expr* r);
br_status mk_seq_unit(expr* e, expr_ref& result);
br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
br_status mk_seq_length(expr* a, expr_ref& result);