mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

add str.prefixof, str.suffixof in theory_str

Browse source
This commit is contained in:
Murphy Berzish 2017-01-27 16:26:30 -05:00
parent 09ac5645e4
commit a879b24011
4 changed files with 49 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/ast/rewriter/str_rewriter.cpp
View file

@ -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);

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

@ -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);

14
src/ast/str_decl_plugin.cpp
View file

@ -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<builtin_name> & 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));

15
src/ast/str_decl_plugin.h
View file

@ -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);