diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp index 4b7ff9057..d6419ba4f 100644 --- a/src/ast/rewriter/str_rewriter.cpp +++ b/src/ast/rewriter/str_rewriter.cpp @@ -69,6 +69,28 @@ br_status str_rewriter::mk_str_StartsWith(expr * haystack, expr * needle, expr_r } } +br_status str_rewriter::mk_str_EndsWith(expr * haystack, expr * needle, expr_ref & result) { + TRACE("t_str_rw", tout << "rewrite (EndsWith " << 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 EndsWith 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(haystackStr.length() - needleStr.length(), needleStr.length()) == needleStr) { + 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()); @@ -82,6 +104,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_STR_STARTSWITH: SASSERT(num_args == 2); return mk_str_StartsWith(args[0], args[1], result); + case OP_STR_ENDSWITH: + SASSERT(num_args == 2); + return mk_str_EndsWith(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 8f12a75db..b179934c7 100644 --- a/src/ast/rewriter/str_rewriter.h +++ b/src/ast/rewriter/str_rewriter.h @@ -42,6 +42,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); 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 c6328d592..6453cb244 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/src/ast/str_decl_plugin.cpp @@ -28,6 +28,7 @@ str_decl_plugin::str_decl_plugin(): m_length_decl(0), m_charat_decl(0), m_startswith_decl(0), + m_endswith_decl(0), m_arith_plugin(0), m_arith_fid(0), m_int_sort(0){ @@ -43,6 +44,7 @@ void str_decl_plugin::finalize(void) { DEC_REF(m_length_decl); DEC_REF(m_charat_decl); DEC_REF(m_startswith_decl); + DEC_REF(m_endswith_decl); DEC_REF(m_int_sort); } @@ -78,6 +80,9 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) { 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); + + 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); } decl_plugin * str_decl_plugin::mk_fresh() { @@ -97,6 +102,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) { case OP_STRLEN: return m_length_decl; case OP_STR_CHARAT: return m_charat_decl; case OP_STR_STARTSWITH: return m_startswith_decl; + case OP_STR_ENDSWITH: return m_endswith_decl; default: return 0; } } @@ -155,6 +161,7 @@ void str_decl_plugin::get_op_names(svector & op_names, symbol cons 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)); + op_names.push_back(builtin_name("EndsWith", OP_STR_ENDSWITH)); } 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 d7bfcf172..4ce258c60 100644 --- a/src/ast/str_decl_plugin.h +++ b/src/ast/str_decl_plugin.h @@ -33,6 +33,7 @@ enum str_op_kind { // higher-level string functions -- these are reduced to basic operations OP_STR_CHARAT, OP_STR_STARTSWITH, + OP_STR_ENDSWITH, // end LAST_STR_OP }; @@ -47,6 +48,7 @@ protected: func_decl * m_charat_decl; func_decl * m_startswith_decl; + func_decl * m_endswith_decl; arith_decl_plugin * m_arith_plugin; family_id m_arith_fid; diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 7bdc9f197..76835c560 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -568,7 +568,7 @@ expr * theory_str::mk_concat(expr * n1, expr * n2) { bool theory_str::can_propagate() { return !m_basicstr_axiom_todo.empty() || !m_str_eq_todo.empty() || !m_concat_axiom_todo.empty() - || !m_axiom_CharAt_todo.empty() || !m_axiom_StartsWith_todo.empty() + || !m_axiom_CharAt_todo.empty() || !m_axiom_StartsWith_todo.empty() || !m_axiom_EndsWith_todo.empty() ; } @@ -602,6 +602,11 @@ void theory_str::propagate() { instantiate_axiom_StartsWith(m_axiom_StartsWith_todo[i]); } m_axiom_StartsWith_todo.reset(); + + for (unsigned i = 0; i < m_axiom_EndsWith_todo.size(); ++i) { + instantiate_axiom_EndsWith(m_axiom_EndsWith_todo[i]); + } + m_axiom_EndsWith_todo.reset(); } } @@ -832,6 +837,37 @@ void theory_str::instantiate_axiom_StartsWith(enode * e) { assert_axiom(finalAxiom); } +void theory_str::instantiate_axiom_EndsWith(enode * e) { + context & ctx = get_context(); + ast_manager & m = get_manager(); + + app * expr = e->get_owner(); + if (axiomatized_terms.contains(expr)) { + TRACE("t_str_detail", tout << "already set up EndsWith axiom for " << mk_pp(expr, m) << std::endl;); + return; + } + axiomatized_terms.insert(expr); + + TRACE("t_str_detail", tout << "instantiate EndsWith axiom for " << mk_pp(expr, m) << std::endl;); + + // TODO NEXT + NOT_IMPLEMENTED_YET(); + /* + Z3_ast resBoolVar = my_mk_internal_bool_var(t); + Z3_ast ts0 = my_mk_internal_string_var(t); + Z3_ast ts1 = my_mk_internal_string_var(t); + // boolVar = endswith(arg[0], arg[1]) + // -------------------------------------------- + std::vector innerItems; + innerItems.push_back( Z3_mk_eq(ctx, args[0], mk_concat(t, ts0, ts1)) ); + innerItems.push_back( Z3_mk_eq(ctx, mk_length(t, ts1), mk_length(t, args[1])) ); + innerItems.push_back( Z3_mk_ite(ctx, Z3_mk_eq(ctx, ts1, args[1]), Z3_mk_eq(ctx, resBoolVar, Z3_mk_true(ctx)), Z3_mk_eq(ctx, resBoolVar, Z3_mk_false(ctx) ) ) ); + Z3_ast then1 = mk_and_fromVector(t, innerItems); + breakdownAssert = Z3_mk_ite(ctx, Z3_mk_ge(ctx, mk_length(t, args[0]), mk_length(t, args[1])), then1, Z3_mk_eq(ctx, resBoolVar, Z3_mk_false(ctx) ) ); + reduceAst = resBoolVar; + */ +} + void theory_str::attach_new_th_var(enode * n) { context & ctx = get_context(); theory_var v = mk_var(n); @@ -3587,6 +3623,8 @@ void theory_str::set_up_axioms(expr * ex) { app * ap = to_app(ex); if (is_StartsWith(ap)) { m_axiom_StartsWith_todo.push_back(n); + } else if (is_EndsWith(ap)) { + m_axiom_EndsWith_todo.push_back(n); } } } else { diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 6debaad71..ae3cc5d52 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -109,6 +109,7 @@ namespace smt { // enode lists for term-specific axioms ptr_vector m_axiom_CharAt_todo; ptr_vector m_axiom_StartsWith_todo; + ptr_vector m_axiom_EndsWith_todo; // hashtable of all exprs for which we've already set up term-specific axioms -- // this prevents infinite recursive descent with respect to axioms that @@ -180,12 +181,16 @@ namespace smt { bool is_CharAt(enode const * n) const { return is_CharAt(n->get_owner()); } bool is_StartsWith(app const * a) const { return a->is_app_of(get_id(), OP_STR_STARTSWITH); } bool is_StartsWith(enode const * n) const { return is_StartsWith(n->get_owner()); } + bool is_EndsWith(app const * a) const { return a->is_app_of(get_id(), OP_STR_ENDSWITH); } + bool is_EndsWith(enode const * n) const { return is_EndsWith(n->get_owner()); } + void instantiate_concat_axiom(enode * cat); void instantiate_basic_string_axioms(enode * str); void instantiate_str_eq_length_axiom(enode * lhs, enode * rhs); void instantiate_axiom_CharAt(enode * e); void instantiate_axiom_StartsWith(enode * e); + void instantiate_axiom_EndsWith(enode * e); void set_up_axioms(expr * ex); void handle_equality(expr * lhs, expr * rhs);