mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

decl and rewriter support for Contains (WIP)

Browse source
This commit is contained in:
Murphy Berzish 2016-06-14 18:36:43 -04:00
parent 989d6b577b
commit a3986d6d0e
4 changed files with 34 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -91,6 +91,27 @@ br_status str_rewriter::mk_str_EndsWith(expr * haystack, expr * needle, expr_ref
}
}
br_status str_rewriter::mk_str_Contains(expr * haystack, expr * needle, expr_ref & result) {
TRACE("t_str_rw", tout << "rewrite (Contains " << mk_pp(haystack, m()) << " " << mk_pp(needle, m()) << ")" << std::endl;);
if (haystack == needle) {
TRACE("t_str_rw", tout << "eliminate (Contains) over identical terms" << std::endl;);
result = m().mk_true();
return BR_DONE;
} else if (m_strutil.is_string(haystack) && m_strutil.is_string(needle)) {
TRACE("t_str_rw", tout << "evaluating constant Contains predicate" << std::endl;);
std::string haystackStr = m_strutil.get_string_constant_value(haystack);
std::string needleStr = m_strutil.get_string_constant_value(needle);
if (haystackStr.find(needleStr) != std::string::npos) {
result = m().mk_true();
} else {
result = m().mk_false();
}
return BR_DONE;
} else {
return BR_FAILED;
}
}
br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(f->get_family_id() == get_fid());
@ -107,6 +128,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_STR_ENDSWITH:
SASSERT(num_args == 2);
return mk_str_EndsWith(args[0], args[1], result);
case OP_STR_CONTAINS:
SASSERT(num_args == 2);
return mk_str_Contains(args[0], args[1], result);
default:
return BR_FAILED;
}

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

@ -43,6 +43,7 @@ public:
br_status mk_str_CharAt(expr * arg0, expr * arg1, expr_ref & result);
br_status mk_str_StartsWith(expr * haystack, expr * needle, expr_ref & result);
br_status mk_str_EndsWith(expr * haystack, expr * needle, expr_ref & result);
br_status mk_str_Contains(expr * haystack, expr * needle, expr_ref & result);
bool reduce_eq(expr * l, expr * r, expr_ref_vector & lhs, expr_ref_vector & rhs, bool & change);
bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change);

7
src/ast/str_decl_plugin.cpp
View file

@ -29,6 +29,7 @@ str_decl_plugin::str_decl_plugin():
m_charat_decl(0),
m_startswith_decl(0),
m_endswith_decl(0),
m_contains_decl(0),
m_arith_plugin(0),
m_arith_fid(0),
m_int_sort(0){
@ -45,6 +46,7 @@ void str_decl_plugin::finalize(void) {
DEC_REF(m_charat_decl);
DEC_REF(m_startswith_decl);
DEC_REF(m_endswith_decl);
DEC_REF(m_contains_decl);
DEC_REF(m_int_sort);
}
@ -83,6 +85,9 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_endswith_decl = m->mk_func_decl(symbol("EndsWith"), s, s, boolT, func_decl_info(id, OP_STR_ENDSWITH));
m_manager->inc_ref(m_endswith_decl);
m_contains_decl = m->mk_func_decl(symbol("Contains"), s, s, boolT, func_decl_info(id, OP_STR_CONTAINS));
m_manager->inc_ref(m_contains_decl);
}
decl_plugin * str_decl_plugin::mk_fresh() {
@ -103,6 +108,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) {
case OP_STR_CHARAT: return m_charat_decl;
case OP_STR_STARTSWITH: return m_startswith_decl;
case OP_STR_ENDSWITH: return m_endswith_decl;
case OP_STR_CONTAINS: return m_contains_decl;
default: return 0;
}
}
@ -162,6 +168,7 @@ void str_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
op_names.push_back(builtin_name("CharAt", OP_STR_CHARAT));
op_names.push_back(builtin_name("StartsWith", OP_STR_STARTSWITH));
op_names.push_back(builtin_name("EndsWith", OP_STR_ENDSWITH));
op_names.push_back(builtin_name("Contains", OP_STR_CONTAINS));
}
void str_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {

2
src/ast/str_decl_plugin.h
View file

@ -34,6 +34,7 @@ enum str_op_kind {
OP_STR_CHARAT,
OP_STR_STARTSWITH,
OP_STR_ENDSWITH,
OP_STR_CONTAINS,
// end
LAST_STR_OP
};
@ -49,6 +50,7 @@ protected:
func_decl * m_charat_decl;
func_decl * m_startswith_decl;
func_decl * m_endswith_decl;
func_decl * m_contains_decl;
arith_decl_plugin * m_arith_plugin;
family_id m_arith_fid;