From 4fe0e07080bbc4aa006be03112892fe6007b22e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 5 Dec 2015 16:36:11 -0800 Subject: [PATCH] indexof Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 24 ++++++++++++++++++++---- src/ast/rewriter/seq_rewriter.h | 2 +- src/ast/seq_decl_plugin.cpp | 3 ++- 3 files changed, 23 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 741e6077e..2568639c3 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -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) { diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 04363c766..f2a152640 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -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); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 5962af658..19b5b3321 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -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);