mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

indexof

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-05 16:36:11 -08:00
parent 5296009f46
commit 4fe0e07080
3 changed files with 23 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -79,8 +79,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
SASSERT(num_args == 2);
return mk_str_charat(args[0], args[1], result);
case OP_STRING_STRIDOF:
SASSERT(num_args == 2);
return mk_str_stridof(args[0], args[1], result);
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);
@ -135,7 +135,7 @@ br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& resul
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) &&
pos.is_unsigned() && len.is_unsigned() && !pos.is_neg() && !len.is_neg() && pos.get_unsigned() <= s.length()) {
pos.is_unsigned() && len.is_unsigned() && pos.get_unsigned() <= s.length()) {
unsigned _pos = pos.get_unsigned();
unsigned _len = len.get_unsigned();
result = m_util.str.mk_string(s.substr(_pos, _len));
@ -166,7 +166,23 @@ br_status seq_rewriter::mk_str_charat(expr* a, expr* b, expr_ref& result) {
}
return BR_FAILED;
}
br_status seq_rewriter::mk_str_stridof(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;
if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2) && m_autil.is_numeral(c, r) && r.is_unsigned()) {
for (unsigned i = r.get_unsigned(); i < s1.length(); ++i) {
if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) {
result = m_autil.mk_numeral(rational(i) - r, true);
return BR_DONE;
}
}
result = m_autil.mk_numeral(rational(-1), true);
return BR_DONE;
}
if (m_util.str.is_const(b, s2) && s2.length() == 0) {
result = c;
return BR_DONE;
}
return BR_FAILED;
}
br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result) {

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

@ -38,7 +38,7 @@ class seq_rewriter {
br_status mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result);
br_status mk_str_strctn(expr* a, expr* b, expr_ref& result);
br_status mk_str_charat(expr* a, expr* b, expr_ref& result);
br_status mk_str_stridof(expr* a, expr* b, expr_ref& result);
br_status mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result);
br_status mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result);
br_status mk_str_prefix(expr* a, expr* b, expr_ref& result);
br_status mk_str_suffix(expr* a, expr* b, expr_ref& result);

3
src/ast/seq_decl_plugin.cpp
View file

@ -146,6 +146,7 @@ void seq_decl_plugin::init() {
sort* strTint2T[3] = { strT, intT, intT };
sort* re2T[2] = { reT, reT };
sort* strTreT[2] = { strT, reT };
sort* str2TintT[3] = { strT, strT, intT };
m_sigs.resize(LAST_SEQ_OP);
// TBD: have (par ..) construct and load parameterized signature from premable.
m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq-unit", 1, 1, &A, seqA);
@ -185,7 +186,7 @@ void seq_decl_plugin::init() {
m_sigs[OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, boolT);
m_sigs[OP_STRING_STRCTN] = alloc(psig, m, "str.contains", 0, 2, str2T, boolT);
m_sigs[OP_STRING_CHARAT] = alloc(psig, m, "str.at", 0, 2, strTint2T, strT);
m_sigs[OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 2, str2T, intT);
m_sigs[OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT);
m_sigs[OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT);
m_sigs[OP_STRING_PREFIX] = alloc(psig, m, "str.prefixof", 0, 2, str2T, boolT);
m_sigs[OP_STRING_SUFFIX] = alloc(psig, m, "str.suffixof", 0, 2, str2T, boolT);