diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp index 76c0d25ae..4b7ff9057 100644 --- a/src/ast/rewriter/str_rewriter.cpp +++ b/src/ast/rewriter/str_rewriter.cpp @@ -42,24 +42,30 @@ br_status str_rewriter::mk_str_CharAt(expr * arg0, expr * arg1, expr_ref & resul result = m_strutil.mk_string(resultStr); return BR_DONE; } else { - // TODO if we ever figure out how to assert axioms in here, add this code + // TODO if we ever figure out how to assert axioms in here, add the axiom code from Z3str2's strAstReduce.cpp return BR_FAILED; - /* - Z3_ast ts0 = my_mk_internal_string_var(t); - Z3_ast ts1 = my_mk_internal_string_var(t); - Z3_ast ts2 = my_mk_internal_string_var(t); + } +} - Z3_ast cond = mk_2_and(t, Z3_mk_ge(ctx, args[1], mk_int(ctx, 0)), Z3_mk_lt(ctx, args[1], mk_length(t, args[0]))); - - Z3_ast and_item[3]; - and_item[0] = Z3_mk_eq(ctx, args[0], mk_concat(t, ts0, mk_concat(t, ts1, ts2))); - and_item[1] = Z3_mk_eq(ctx, args[1], mk_length(t, ts0)); - and_item[2] = Z3_mk_eq(ctx, mk_length(t, ts1), mk_int(ctx, 1)); - Z3_ast thenBranch = Z3_mk_and(ctx, 3, and_item); - Z3_ast elseBranch = Z3_mk_eq(ctx, ts1, my_mk_str_value(t, "")); - breakdownAssert = Z3_mk_ite(ctx, cond, thenBranch, elseBranch); - return ts1; - */ +br_status str_rewriter::mk_str_StartsWith(expr * haystack, expr * needle, expr_ref & result) { + TRACE("t_str_rw", tout << "rewrite (StartsWith " << mk_pp(haystack, m()) << " " << mk_pp(needle, m()) << ")" << std::endl;); + if (m_strutil.is_string(haystack) && m_strutil.is_string(needle)) { + TRACE("t_str_rw", tout << "evaluating constant StartsWith 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.length() < needleStr.length()) { + result = m().mk_false(); + return BR_DONE; + } else { + if (haystackStr.substr(0, needleStr.length()) == needleStr) { + result = m().mk_true(); + } else { + result = m().mk_false(); + } + return BR_DONE; + } + } else { + return BR_FAILED; } } @@ -73,6 +79,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_STR_CHARAT: SASSERT(num_args == 2); return mk_str_CharAt(args[0], args[1], result); + case OP_STR_STARTSWITH: + SASSERT(num_args == 2); + return mk_str_StartsWith(args[0], args[1], result); default: return BR_FAILED; } diff --git a/src/ast/rewriter/str_rewriter.h b/src/ast/rewriter/str_rewriter.h index 01ccde242..8f12a75db 100644 --- a/src/ast/rewriter/str_rewriter.h +++ b/src/ast/rewriter/str_rewriter.h @@ -41,6 +41,7 @@ public: br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); br_status mk_str_CharAt(expr * arg0, expr * arg1, expr_ref & result); + br_status mk_str_StartsWith(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); diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp index 03fde5aeb..c6328d592 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/src/ast/str_decl_plugin.cpp @@ -27,6 +27,7 @@ str_decl_plugin::str_decl_plugin(): m_concat_decl(0), m_length_decl(0), m_charat_decl(0), + m_startswith_decl(0), m_arith_plugin(0), m_arith_fid(0), m_int_sort(0){ @@ -41,6 +42,7 @@ void str_decl_plugin::finalize(void) { DEC_REF(m_concat_decl); DEC_REF(m_length_decl); DEC_REF(m_charat_decl); + DEC_REF(m_startswith_decl); DEC_REF(m_int_sort); } @@ -60,6 +62,8 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) { m_manager->inc_ref(m_int_sort); sort * i = m_int_sort; + sort* boolT = m_manager->mk_bool_sort(); + #define MK_OP(FIELD, NAME, KIND, SORT) \ FIELD = m->mk_func_decl(symbol(NAME), SORT, SORT, SORT, func_decl_info(id, KIND)); \ m->inc_ref(FIELD) @@ -71,6 +75,9 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) { m_charat_decl = m->mk_func_decl(symbol("CharAt"), s, i, s, func_decl_info(id, OP_STR_CHARAT)); m_manager->inc_ref(m_charat_decl); + + m_startswith_decl = m->mk_func_decl(symbol("StartsWith"), s, s, boolT, func_decl_info(id, OP_STR_STARTSWITH)); + m_manager->inc_ref(m_startswith_decl); } decl_plugin * str_decl_plugin::mk_fresh() { @@ -89,6 +96,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) { case OP_STRCAT: return m_concat_decl; case OP_STRLEN: return m_length_decl; case OP_STR_CHARAT: return m_charat_decl; + case OP_STR_STARTSWITH: return m_startswith_decl; default: return 0; } } @@ -146,6 +154,7 @@ void str_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("Concat", OP_STRCAT)); op_names.push_back(builtin_name("Length", OP_STRLEN)); op_names.push_back(builtin_name("CharAt", OP_STR_CHARAT)); + op_names.push_back(builtin_name("StartsWith", OP_STR_STARTSWITH)); } void str_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h index 049ef08ba..d7bfcf172 100644 --- a/src/ast/str_decl_plugin.h +++ b/src/ast/str_decl_plugin.h @@ -32,6 +32,7 @@ enum str_op_kind { OP_STRLEN, // higher-level string functions -- these are reduced to basic operations OP_STR_CHARAT, + OP_STR_STARTSWITH, // end LAST_STR_OP }; @@ -43,7 +44,9 @@ protected: func_decl * m_concat_decl; func_decl * m_length_decl; + func_decl * m_charat_decl; + func_decl * m_startswith_decl; arith_decl_plugin * m_arith_plugin; family_id m_arith_fid;