mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

seq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-07 15:01:46 -08:00
parent 34a0d7dfed
commit a9f5c2f864
2 changed files with 112 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -20,6 +20,7 @@ Notes:
#include"seq_rewriter.h"
#include"arith_decl_plugin.h"
#include"ast_pp.h"
#include"ast_util.h"
br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
@ -186,6 +187,21 @@ br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) {
result = m().mk_bool_val(0 != strstr(d.c_str(), c.c_str()));
return BR_DONE;
}
// check if subsequence of a is in b.
ptr_vector<expr> as, bs;
m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs);
bool found = false;
for (unsigned i = 0; !found && i < bs.size(); ++i) {
if (as.size() > bs.size() - i) break;
unsigned j = 0;
for (; j < as.size() && as[j] == bs[i+j]; ++j) {};
found = j == as.size();
}
if (found) {
result = m().mk_true();
return BR_DONE;
}
return BR_FAILED;
}
@ -275,6 +291,80 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
result = m().mk_true();
return BR_DONE;
}
expr* a1 = m_util.str.get_leftmost_concat(a);
expr* b1 = m_util.str.get_leftmost_concat(b);
isc1 = m_util.str.is_string(a1, s1);
isc2 = m_util.str.is_string(b1, s2);
ptr_vector<expr> as, bs;
if (a1 != b1 && isc1 && isc2) {
if (s1.length() <= s2.length()) {
if (strncmp(s1.c_str(), s2.c_str(), s1.length()) == 0) {
if (a == a1) {
result = m().mk_true();
return BR_DONE;
}
m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs);
SASSERT(as.size() > 1);
s2 = std::string(s2.c_str() + s1.length(), s2.length() - s1.length());
bs[0] = m_util.str.mk_string(s2);
m_util.str.mk_prefix(m_util.str.mk_concat(as.size()-1, as.c_ptr()+1),
m_util.str.mk_concat(bs.size(), bs.c_ptr()));
return BR_REWRITE_FULL;
}
else {
result = m().mk_false();
return BR_DONE;
}
}
else {
if (strncmp(s1.c_str(), s2.c_str(), s2.length()) == 0) {
if (b == b1) {
result = m().mk_false();
return BR_DONE;
}
m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs);
SASSERT(bs.size() > 1);
s1 = std::string(s1.c_str() + s2.length(), s1.length() - s2.length());
as[0] = m_util.str.mk_string(s1);
m_util.str.mk_prefix(m_util.str.mk_concat(as.size(), as.c_ptr()),
m_util.str.mk_concat(bs.size()-1, bs.c_ptr()+1));
return BR_REWRITE_FULL;
}
else {
result = m().mk_false();
return BR_DONE;
}
}
}
if (a1 != b1) {
return BR_FAILED;
}
m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs);
unsigned i = 0;
for (; i < as.size() && i < bs.size() && as[i] == bs[i]; ++i) {};
if (i == as.size()) {
result = m().mk_true();
return BR_DONE;
}
if (i == bs.size()) {
expr_ref_vector es(m());
for (unsigned j = i; j < as.size(); ++i) {
es.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j]));
}
result = mk_and(es);
return BR_REWRITE3;
}
if (i > 0) {
a = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i);
b = m_util.str.mk_concat(bs.size() - i, bs.c_ptr() + i);
result = m_util.str.mk_prefix(a, b);
return BR_DONE;
}
UNREACHABLE();
return BR_FAILED;
}
@ -293,6 +383,17 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
result = m().mk_true();
return BR_DONE;
}
if (m_util.str.is_empty(b)) {
result = m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), a);
return BR_REWRITE3;
}
// concatenation is left-associative, so a2, b2 are not concatenations
expr* a1, *a2, *b1, *b2;
if (m_util.str.is_concat(a, a1, a2) &&
m_util.str.is_concat(b, b1, b2) && a2 == b2) {
result = m_util.str.mk_suffix(a1, b1);
return BR_REWRITE1;
}
return BR_FAILED;
}

13
src/ast/seq_decl_plugin.h
View file

@ -164,13 +164,19 @@ public:
public:
str(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {}
sort* mk_seq(sort* s) { parameter param(s); return m.mk_sort(m_fid, SEQ_SORT, 1, &param); }
app* mk_empty(sort* s) { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, 0, 0, (expr*const*)0, s)); }
app* mk_string(symbol const& s);
app* mk_string(char const* s) { return mk_string(symbol(s)); }
app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); }
app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
expr* mk_concat(unsigned n, expr* const* es) { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); }
app* mk_length(expr* a) { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); }
app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); }
app* mk_strctn(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); }
app* mk_contains(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); }
app* mk_prefix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_PREFIX, 2, es); }
app* mk_suffix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_SUFFIX, 2, es); }
bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
@ -181,7 +187,9 @@ public:
return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true);
}
bool is_empty(expr const* n) const { symbol s; return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && strcmp(s.bare_str(),"") == 0); }
bool is_empty(expr const* n) const { symbol s;
return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0);
}
bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); }
bool is_length(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); }
bool is_extract(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_EXTRACT); }
@ -210,6 +218,7 @@ public:
MATCH_BINARY(is_in_re);
void get_concat(expr* e, ptr_vector<expr>& es) const;
expr* get_leftmost_concat(expr* e) const { expr* e1, *e2; while (is_concat(e, e1, e2)) e = e1; return e; }
};
class re {