mirror of
https://github.com/Z3Prover/z3
synced 2025-07-18 02:16:40 +00:00
merge seq and string operators
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
70b10d53cf
commit
8bb73c8eae
6 changed files with 186 additions and 145 deletions
|
|
@ -29,12 +29,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
|
||||
case OP_SEQ_UNIT:
|
||||
case OP_SEQ_EMPTY:
|
||||
case OP_SEQ_PREFIX_OF:
|
||||
case OP_SEQ_SUFFIX_OF:
|
||||
case OP_SEQ_SUBSEQ_OF:
|
||||
case OP_SEQ_EXTRACT:
|
||||
case OP_SEQ_NTH:
|
||||
case OP_SEQ_LENGTH:
|
||||
|
||||
case OP_RE_PLUS:
|
||||
case OP_RE_STAR:
|
||||
|
|
@ -47,52 +41,60 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
case OP_RE_EMPTY_SET:
|
||||
case OP_RE_FULL_SET:
|
||||
case OP_RE_EMPTY_SEQ:
|
||||
case OP_RE_OF_SEQ:
|
||||
case OP_RE_OF_PRED:
|
||||
case OP_RE_MEMBER:
|
||||
return BR_FAILED;
|
||||
|
||||
// string specific operators.
|
||||
case OP_STRING_CONST:
|
||||
return BR_FAILED;
|
||||
case OP_SEQ_CONCAT:
|
||||
case _OP_STRING_CONCAT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_seq_concat(args[0], args[1], result);
|
||||
case OP_STRING_LENGTH:
|
||||
case OP_SEQ_LENGTH:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_str_length(args[0], result);
|
||||
case OP_STRING_SUBSTR:
|
||||
case OP_SEQ_EXTRACT:
|
||||
SASSERT(num_args == 3);
|
||||
return mk_str_substr(args[0], args[1], args[2], result);
|
||||
case OP_STRING_STRCTN:
|
||||
case OP_SEQ_CONTAINS:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_str_strctn(args[0], args[1], result);
|
||||
case OP_STRING_CHARAT:
|
||||
case OP_SEQ_AT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_str_charat(args[0], args[1], result);
|
||||
return mk_str_at(args[0], args[1], result);
|
||||
case OP_STRING_STRIDOF:
|
||||
SASSERT(num_args == 3);
|
||||
return mk_str_stridof(args[0], args[1], args[2], result);
|
||||
case OP_STRING_STRREPL:
|
||||
SASSERT(num_args == 3);
|
||||
return mk_str_strrepl(args[0], args[1], args[2], result);
|
||||
case OP_STRING_PREFIX:
|
||||
case OP_SEQ_PREFIX:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_str_prefix(args[0], args[1], result);
|
||||
case OP_STRING_SUFFIX:
|
||||
return mk_seq_prefix(args[0], args[1], result);
|
||||
case OP_SEQ_SUFFIX:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_str_suffix(args[0], args[1], result);
|
||||
return mk_seq_suffix(args[0], args[1], result);
|
||||
case OP_STRING_ITOS:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_str_itos(args[0], result);
|
||||
case OP_STRING_STOI:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_str_stoi(args[0], result);
|
||||
case OP_STRING_IN_REGEXP:
|
||||
case OP_STRING_TO_REGEXP:
|
||||
case OP_SEQ_TO_RE:
|
||||
case OP_SEQ_IN_RE:
|
||||
case OP_REGEXP_LOOP:
|
||||
return BR_FAILED;
|
||||
case _OP_STRING_CONCAT:
|
||||
case _OP_STRING_PREFIX:
|
||||
case _OP_STRING_SUFFIX:
|
||||
case _OP_STRING_STRCTN:
|
||||
case _OP_STRING_LENGTH:
|
||||
case _OP_STRING_CHARAT:
|
||||
case _OP_STRING_IN_REGEXP:
|
||||
case _OP_STRING_TO_REGEXP:
|
||||
case _OP_STRING_SUBSTR:
|
||||
|
||||
UNREACHABLE();
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
|
@ -107,8 +109,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
|
||||
std::string s1, s2;
|
||||
expr* c, *d;
|
||||
bool isc1 = m_util.str.is_const(a, s1);
|
||||
bool isc2 = m_util.str.is_const(b, s2);
|
||||
bool isc1 = m_util.str.is_string(a, s1);
|
||||
bool isc2 = m_util.str.is_string(b, s2);
|
||||
if (isc1 && isc2) {
|
||||
result = m_util.str.mk_string(s1 + s2);
|
||||
return BR_DONE;
|
||||
|
|
@ -117,16 +119,16 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
|
|||
result = m_util.str.mk_concat(m_util.str.mk_concat(a, c), d);
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
if (isc1 && s1.length() == 0) {
|
||||
if (m_util.str.is_empty(a)) {
|
||||
result = b;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (isc2 && s2.length() == 0) {
|
||||
if (m_util.str.is_empty(b)) {
|
||||
result = a;
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.str.is_concat(a, c, d) &&
|
||||
m_util.str.is_const(d, s1) && isc2) {
|
||||
m_util.str.is_string(d, s1) && isc2) {
|
||||
result = m_util.str.mk_concat(c, m_util.str.mk_string(s1 + s2));
|
||||
return BR_DONE;
|
||||
}
|
||||
|
|
@ -140,7 +142,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
|
|||
unsigned len = 0;
|
||||
size_t j = 0;
|
||||
for (unsigned i = 0; i < m_es.size(); ++i) {
|
||||
if (m_util.str.is_const(m_es[i], b)) {
|
||||
if (m_util.str.is_string(m_es[i], b)) {
|
||||
len += b.length();
|
||||
}
|
||||
else {
|
||||
|
|
@ -169,7 +171,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
|
|||
br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result) {
|
||||
std::string s;
|
||||
rational pos, len;
|
||||
if (m_util.str.is_const(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) &&
|
||||
if (m_util.str.is_string(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) &&
|
||||
pos.is_unsigned() && len.is_unsigned() && pos.get_unsigned() <= s.length()) {
|
||||
unsigned _pos = pos.get_unsigned();
|
||||
unsigned _len = len.get_unsigned();
|
||||
|
|
@ -180,17 +182,17 @@ br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& resul
|
|||
}
|
||||
br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) {
|
||||
std::string c, d;
|
||||
if (m_util.str.is_const(a, c) && m_util.str.is_const(b, d)) {
|
||||
if (m_util.str.is_string(a, c) && m_util.str.is_string(b, d)) {
|
||||
result = m().mk_bool_val(0 != strstr(d.c_str(), c.c_str()));
|
||||
return BR_DONE;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status seq_rewriter::mk_str_charat(expr* a, expr* b, expr_ref& result) {
|
||||
br_status seq_rewriter::mk_str_at(expr* a, expr* b, expr_ref& result) {
|
||||
std::string c;
|
||||
rational r;
|
||||
if (m_util.str.is_const(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) {
|
||||
if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) {
|
||||
unsigned j = r.get_unsigned();
|
||||
if (j < c.length()) {
|
||||
char ch = c[j];
|
||||
|
|
@ -206,8 +208,8 @@ br_status seq_rewriter::mk_str_charat(expr* a, expr* b, expr_ref& result) {
|
|||
br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result) {
|
||||
std::string s1, s2;
|
||||
rational r;
|
||||
bool isc1 = m_util.str.is_const(a, s1);
|
||||
bool isc2 = m_util.str.is_const(b, s2);
|
||||
bool isc1 = m_util.str.is_string(a, s1);
|
||||
bool isc2 = m_util.str.is_string(b, s2);
|
||||
|
||||
if (isc1 && isc2 && m_autil.is_numeral(c, r) && r.is_unsigned()) {
|
||||
for (unsigned i = r.get_unsigned(); i < s1.length(); ++i) {
|
||||
|
|
@ -224,7 +226,7 @@ br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& resu
|
|||
return BR_DONE;
|
||||
}
|
||||
|
||||
if (isc2 && s2.length() == 0) {
|
||||
if (m_util.str.is_empty(b)) {
|
||||
result = c;
|
||||
return BR_DONE;
|
||||
}
|
||||
|
|
@ -234,8 +236,8 @@ br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& resu
|
|||
|
||||
br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result) {
|
||||
std::string s1, s2, s3;
|
||||
if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2) &&
|
||||
m_util.str.is_const(c, s3)) {
|
||||
if (m_util.str.is_string(a, s1) && m_util.str.is_string(b, s2) &&
|
||||
m_util.str.is_string(c, s3)) {
|
||||
std::ostringstream buffer;
|
||||
for (size_t i = 0; i < s1.length(); ) {
|
||||
if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) {
|
||||
|
|
@ -257,10 +259,10 @@ br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& resu
|
|||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status seq_rewriter::mk_str_prefix(expr* a, expr* b, expr_ref& result) {
|
||||
br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
|
||||
std::string s1, s2;
|
||||
bool isc1 = m_util.str.is_const(a, s1);
|
||||
bool isc2 = m_util.str.is_const(b, s2);
|
||||
bool isc1 = m_util.str.is_string(a, s1);
|
||||
bool isc2 = m_util.str.is_string(b, s2);
|
||||
if (isc1 && isc2) {
|
||||
bool prefix = s1.length() <= s2.length();
|
||||
for (unsigned i = 0; i < s1.length() && prefix; ++i) {
|
||||
|
|
@ -269,17 +271,17 @@ br_status seq_rewriter::mk_str_prefix(expr* a, expr* b, expr_ref& result) {
|
|||
result = m().mk_bool_val(prefix);
|
||||
return BR_DONE;
|
||||
}
|
||||
if (isc1 && s1.length() == 0) {
|
||||
if (m_util.str.is_empty(a)) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status seq_rewriter::mk_str_suffix(expr* a, expr* b, expr_ref& result) {
|
||||
br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
|
||||
std::string s1, s2;
|
||||
bool isc1 = m_util.str.is_const(a, s1);
|
||||
if (isc1 && m_util.str.is_const(b, s2)) {
|
||||
bool isc1 = m_util.str.is_string(a, s1);
|
||||
if (isc1 && m_util.str.is_string(b, s2)) {
|
||||
bool suffix = s1.length() <= s2.length();
|
||||
for (unsigned i = 0; i < s1.length() && suffix; ++i) {
|
||||
suffix = s1[s1.length() - i - 1] == s2[s2.length() - i - 1];
|
||||
|
|
@ -287,7 +289,7 @@ br_status seq_rewriter::mk_str_suffix(expr* a, expr* b, expr_ref& result) {
|
|||
result = m().mk_bool_val(suffix);
|
||||
return BR_DONE;
|
||||
}
|
||||
if (isc1 && s1.length() == 0) {
|
||||
if (m_util.str.is_empty(a)) {
|
||||
result = m().mk_true();
|
||||
return BR_DONE;
|
||||
}
|
||||
|
|
@ -304,7 +306,7 @@ br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
|
|||
}
|
||||
br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
|
||||
std::string s;
|
||||
if (m_util.str.is_const(a, s)) {
|
||||
if (m_util.str.is_string(a, s)) {
|
||||
for (unsigned i = 0; i < s.length(); ++i) {
|
||||
if (s[i] == '-') { if (i != 0) return BR_FAILED; }
|
||||
else if ('0' <= s[i] && s[i] <= '9') continue;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue