mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

filter length limits to be non-skolems and under concat/""/unit

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-09-15 07:41:00 -07:00
parent af258d1720
commit 088898834c
3 changed files with 43 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/ast/rewriter/seq_skolem.cpp
View file

@ -26,10 +26,14 @@ skolem::skolem(ast_manager& m, th_rewriter& rw):
m_suffix = "seq.s.prefix";
m_accept = "aut.accept";
m_tail = "seq.tail";
m_left = "seq.left";
m_right = "seq.right";
m_seq_first = "seq.first";
m_seq_last = "seq.last";
m_indexof_left = "seq.idx.l";
m_indexof_right = "seq.idx.r";
m_lindexof_left = "seq.lidx.l";
m_lindexof_right = "seq.lidx.r";
m_aut_step = "aut.step";
m_pre = "seq.pre"; // (seq.pre s l): prefix of string s of length l
m_post = "seq.post"; // (seq.post s l): suffix of string s of length k, based on extract starting at index i of length l
@ -155,6 +159,20 @@ bool skolem::is_tail(expr* e, expr*& s, expr*& idx) const {
return is_tail(e) && (s = to_app(e)->get_arg(0), idx = to_app(e)->get_arg(1), true);
}
bool skolem::is_left_or_right(expr* e, expr*& x, expr*& y, expr*& z) {
if (!is_skolem(m_left, e) && !is_skolem(m_right, e))
return false;
x = nullptr;
y = nullptr;
z = nullptr;
unsigned sz = to_app(e)->get_num_args();
if (sz > 0) x = to_app(e)->get_arg(0);
if (sz > 1) y = to_app(e)->get_arg(1);
if (sz > 2) z = to_app(e)->get_arg(2);
return true;
}
bool skolem::is_eq(expr* e, expr*& a, expr*& b) const {
return is_skolem(m_eq, e) && (a = to_app(e)->get_arg(0), b = to_app(e)->get_arg(1), true);
}

15
src/ast/rewriter/seq_skolem.h
View file

@ -32,8 +32,10 @@ namespace seq {
symbol m_prefix, m_suffix;
symbol m_tail;
symbol m_left, m_right;
symbol m_seq_first, m_seq_last;
symbol m_indexof_left, m_indexof_right; // inverse of indexof: (indexof_left s t) + s + (indexof_right s t) = t, for s in t.
symbol m_indexof_left, m_indexof_right; // inverse of indexof: (indexof_left s t) + s + (indexof_right s t) = t, for s in t.
symbol m_lindexof_left, m_lindexof_right; // inverse of indexof: (indexof_left s t) + s + (indexof_right s t) = t, for s in t.
symbol m_aut_step; // regex unfolding state
symbol m_accept; // regex
symbol m_is_empty; // regex emptiness check
@ -81,8 +83,8 @@ namespace seq {
expr_ref mk_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_right, t, s, offset); }
expr_ref mk_contains_left(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.cnt.l", t, s, offset); }
expr_ref mk_contains_right(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.cnt.r", t, s, offset); }
expr_ref mk_last_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.lidx.l", t, s, offset); }
expr_ref mk_last_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.lidx.r", t, s, offset); }
expr_ref mk_last_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk(m_lindexof_left, t, s, offset); }
expr_ref mk_last_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk(m_lindexof_right, t, s, offset); }
expr_ref mk_tail(expr* s, expr* i) { return mk(m_tail, s, i); }
expr_ref mk_post(expr* s, expr* i) { return mk(m_post, s, i); }
@ -100,8 +102,8 @@ namespace seq {
expr_ref mk_digit2int(expr* ch) { return mk(symbol("seq.digit2int"), ch, nullptr, nullptr, nullptr, a.mk_int()); }
expr_ref mk_digit2bv(expr* ch, sort* bv_sort);
expr_ref mk_ubv2ch(expr* b) { return mk(symbol("seq.ubv2ch"), b, nullptr, nullptr, nullptr, seq.mk_char_sort()); }
expr_ref mk_left(expr* x, expr* y, expr* z = nullptr) { return mk("seq.left", x, y, z); }
expr_ref mk_right(expr* x, expr* y, expr* z = nullptr) { return mk("seq.right", x, y, z); }
expr_ref mk_left(expr* x, expr* y, expr* z = nullptr) { return mk(m_left, x, y, z); }
expr_ref mk_right(expr* x, expr* y, expr* z = nullptr) { return mk(m_right, x, y, z); }
expr_ref mk_max_unfolding_depth(unsigned d);
expr_ref mk_length_limit(expr* e, unsigned d);
@ -117,6 +119,8 @@ namespace seq {
bool is_seq_first(expr* e) const { return is_skolem(m_seq_first, e); }
bool is_indexof_left(expr* e) const { return is_skolem(m_indexof_left, e); }
bool is_indexof_right(expr* e) const { return is_skolem(m_indexof_right, e); }
bool is_last_indexof_left(expr* e) const { return is_skolem(m_lindexof_left, e); }
bool is_last_indexof_right(expr* e) const { return is_skolem(m_lindexof_right, e); }
bool is_indexof_left(expr* e, expr*& x, expr*& y) const {
return is_indexof_left(e) && (x = to_app(e)->get_arg(0), y = to_app(e)->get_arg(1), true);
}
@ -124,6 +128,7 @@ namespace seq {
return is_indexof_right(e) && (x = to_app(e)->get_arg(0), y = to_app(e)->get_arg(1), true);
}
bool is_left_or_right(expr* e, expr*& x, expr*& y, expr*& z);
bool is_step(expr* e) const { return is_skolem(m_aut_step, e); }
bool is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, expr*& j, expr*& t) const;
bool is_accept(expr* acc) const { return is_skolem(m_accept, acc); }

17
src/smt/theory_seq.cpp
View file

@ -1538,10 +1538,23 @@ void theory_seq::add_length(expr* l) {
Add length limit restrictions to sequence s.
*/
void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) {
if (m_sk.is_indexof_left(s))
if (m_util.str.is_concat(s)) {
for (expr* e : *to_app(s))
add_length_limit(e, k, is_searching);
return;
if (m_sk.is_indexof_right(s))
}
if (m_util.str.is_unit(s))
return;
if (m_util.str.is_empty(s))
return;
if (m_sk.is_skolem(s)) {
for (expr* e : *to_app(s))
if (m_util.is_seq(e) || m_sk.is_skolem(e))
add_length_limit(e, k, is_searching);
return;
}
expr_ref lim_e = m_ax.add_length_limit(s, k);
unsigned k0 = 0;
if (m_length_limit_map.find(s, k0)) {