From a879b240114e75938ac2668ccd8f178a87c94ad4 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 27 Jan 2017 16:26:30 -0500 Subject: [PATCH] add str.prefixof, str.suffixof in theory_str --- src/ast/rewriter/str_rewriter.cpp | 18 ++++++++++++++++++ src/ast/rewriter/str_rewriter.h | 2 ++ src/ast/str_decl_plugin.cpp | 14 ++++++++++++++ src/ast/str_decl_plugin.h | 15 +++++++++++++++ 4 files changed, 49 insertions(+) diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp index 2e3c82613..3926e66e1 100644 --- a/src/ast/rewriter/str_rewriter.cpp +++ b/src/ast/rewriter/str_rewriter.cpp @@ -375,6 +375,18 @@ br_status str_rewriter::mk_str_Replace(expr * base, expr * source, expr * target } } +br_status str_rewriter::mk_str_prefixof(expr * pre, expr * full, expr_ref & result) { + TRACE("t_str_rw", tout << "rewrite (str.prefixof " << mk_pp(pre, m()) << " " << mk_pp(full, m()) << ")" << std::endl;); + result = m_strutil.mk_str_StartsWith(full, pre); + return BR_REWRITE_FULL; +} + +br_status str_rewriter::mk_str_suffixof(expr * post, expr * full, expr_ref & result) { + TRACE("t_str_rw", tout << "rewrite (str.suffixof" << mk_pp(post, m()) << " " << mk_pp(full, m()) << ")" << std::endl;); + result = m_strutil.mk_str_EndsWith(full, post); + return BR_REWRITE_FULL; +} + br_status str_rewriter::mk_str_to_int(expr * arg0, expr_ref & result) { TRACE("t_str_rw", tout << "rewrite (str.to-int " << mk_pp(arg0, m()) << ")" << std::endl;); @@ -623,6 +635,12 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_STR_REPLACE: SASSERT(num_args == 3); return mk_str_Replace(args[0], args[1], args[2], result); + case OP_STR_PREFIXOF: + SASSERT(num_args == 2); + return mk_str_prefixof(args[0], args[1], result); + case OP_STR_SUFFIXOF: + SASSERT(num_args == 2); + return mk_str_suffixof(args[0], args[1], result); case OP_STR_STR2INT: SASSERT(num_args == 1); return mk_str_to_int(args[0], result); diff --git a/src/ast/rewriter/str_rewriter.h b/src/ast/rewriter/str_rewriter.h index 145c0193e..0494d4d1b 100644 --- a/src/ast/rewriter/str_rewriter.h +++ b/src/ast/rewriter/str_rewriter.h @@ -53,6 +53,8 @@ public: br_status mk_str_LastIndexof(expr * haystack, expr * needle, expr_ref & result); br_status mk_str_Replace(expr * base, expr * source, expr * target, expr_ref & result); br_status mk_str_Substr(expr * base, expr * start, expr * len, expr_ref & result); + br_status mk_str_prefixof(expr * pre, expr * full, expr_ref & result); + br_status mk_str_suffixof(expr * post, expr * full, expr_ref & result); br_status mk_str_to_int(expr * arg0, expr_ref & result); br_status mk_str_from_int(expr * arg0, expr_ref & result); diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp index 8ac1f722f..60f50b5c4 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/src/ast/str_decl_plugin.cpp @@ -38,6 +38,8 @@ str_decl_plugin::str_decl_plugin(): m_replace_decl(0), m_str2int_decl(0), m_int2str_decl(0), + m_prefixof_decl(0), + m_suffixof_decl(0), m_re_str2regex_decl(0), m_re_regexin_decl(0), m_re_regexconcat_decl(0), @@ -69,6 +71,8 @@ void str_decl_plugin::finalize(void) { DEC_REF(m_lastindexof_decl); DEC_REF(m_substr_decl); DEC_REF(m_replace_decl); + DEC_REF(m_prefixof_decl); + DEC_REF(m_suffixof_decl); DEC_REF(m_str2int_decl); DEC_REF(m_int2str_decl); DEC_REF(m_re_str2regex_decl); @@ -149,6 +153,12 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) { m_manager->inc_ref(m_replace_decl); } + m_prefixof_decl = m->mk_func_decl(symbol("str.prefixof"), s, s, boolT, func_decl_info(id, OP_STR_PREFIXOF)); + m_manager->inc_ref(m_prefixof_decl); + + m_suffixof_decl = m->mk_func_decl(symbol("str.suffixof"), s, s, boolT, func_decl_info(id, OP_STR_SUFFIXOF)); + m_manager->inc_ref(m_suffixof_decl); + m_str2int_decl = m->mk_func_decl(symbol("str.to-int"), s, i, func_decl_info(id, OP_STR_STR2INT)); m_manager->inc_ref(m_str2int_decl); @@ -206,6 +216,8 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) { case OP_STR_LASTINDEXOF: return m_lastindexof_decl; case OP_STR_SUBSTR: return m_substr_decl; case OP_STR_REPLACE: return m_replace_decl; + case OP_STR_PREFIXOF: return m_prefixof_decl; + case OP_STR_SUFFIXOF: return m_suffixof_decl; case OP_STR_STR2INT: return m_str2int_decl; case OP_STR_INT2STR: return m_int2str_decl; case OP_RE_STR2REGEX: return m_re_str2regex_decl; @@ -281,6 +293,8 @@ void str_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("LastIndexof", OP_STR_LASTINDEXOF)); op_names.push_back(builtin_name("Substring", OP_STR_SUBSTR)); op_names.push_back(builtin_name("Replace", OP_STR_REPLACE)); + op_names.push_back(builtin_name("str.prefixof", OP_STR_PREFIXOF)); + op_names.push_back(builtin_name("str.suffixof", OP_STR_SUFFIXOF)); op_names.push_back(builtin_name("str.to-int", OP_STR_STR2INT)); op_names.push_back(builtin_name("str.from-int", OP_STR_INT2STR)); op_names.push_back(builtin_name("Str2Reg", OP_RE_STR2REGEX)); diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h index ff531e942..3ae034b45 100644 --- a/src/ast/str_decl_plugin.h +++ b/src/ast/str_decl_plugin.h @@ -41,6 +41,9 @@ enum str_op_kind { OP_STR_LASTINDEXOF, OP_STR_SUBSTR, OP_STR_REPLACE, + // SMT-LIB 2.5 standard operators -- these are rewritten to internal ones + OP_STR_PREFIXOF, + OP_STR_SUFFIXOF, // string-integer conversion OP_STR_STR2INT, OP_STR_INT2STR, OP_STR_PLACEHOLDER1, OP_STR_PLACEHOLDER2, @@ -78,6 +81,8 @@ protected: func_decl * m_replace_decl; func_decl * m_str2int_decl; func_decl * m_int2str_decl; + func_decl * m_prefixof_decl; + func_decl * m_suffixof_decl; func_decl * m_re_str2regex_decl; func_decl * m_re_regexin_decl; @@ -167,6 +172,16 @@ public: } app * mk_string_with_escape_characters(std::string & val); + app * mk_str_StartsWith(expr * haystack, expr * needle) { + expr * es[2] = {haystack, needle}; + return m_manager.mk_app(get_fid(), OP_STR_STARTSWITH, 2, es); + } + + app * mk_str_EndsWith(expr * haystack, expr * needle) { + expr * es[2] = {haystack, needle}; + return m_manager.mk_app(get_fid(), OP_STR_ENDSWITH, 2, es); + } + app * mk_re_Str2Reg(expr * s) { expr * es[1] = {s}; return m_manager.mk_app(get_fid(), OP_RE_STR2REGEX, 1, es);