diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp index 5e61ee3a2..30dcb1d95 100644 --- a/src/ast/rewriter/str_rewriter.cpp +++ b/src/ast/rewriter/str_rewriter.cpp @@ -130,6 +130,34 @@ br_status str_rewriter::mk_str_Indexof(expr * haystack, expr * needle, expr_ref } } +br_status str_rewriter::mk_str_Indexof2(expr * arg0, expr * arg1, expr * arg2, expr_ref & result) { + TRACE("t_str_rw", tout << "rewrite (Indexof2 " << mk_pp(arg0, m()) << " " << mk_pp(arg1, m()) << " " << mk_pp(arg2, m()) << ")" << std::endl;); + //if (getNodeType(t, args[0]) == my_Z3_ConstStr && getNodeType(t, args[1]) == my_Z3_ConstStr && getNodeType(t, args[2]) == my_Z3_Num) { + rational arg2Int; + if (m_strutil.is_string(arg0) && m_strutil.is_string(arg1) && m_autil.is_numeral(arg2, arg2Int)) { + TRACE("t_str_rw", tout << "evaluating constant Indexof2 expression" << std::endl;); + std::string arg0str = m_strutil.get_string_constant_value(arg0); + std::string arg1str = m_strutil.get_string_constant_value(arg1); + if (arg2Int >= rational((unsigned)arg0str.length())) { + result = m_autil.mk_numeral(rational(-1), true); + } else if (arg2Int < rational(0)) { + int index = arg0str.find(arg1str); + result = m_autil.mk_numeral(rational(index), true); + } else { + std::string suffixStr = arg0str.substr(arg2Int.get_unsigned(), arg0str.length() - arg2Int.get_unsigned()); + if (suffixStr.find(arg1str) != std::string::npos) { + int index = suffixStr.find(arg1str) + arg2Int.get_unsigned(); + result = m_autil.mk_numeral(rational(index), true); + } else { + result = m_autil.mk_numeral(rational(-1), true); + } + } + 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()); @@ -152,6 +180,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_STR_INDEXOF: SASSERT(num_args == 2); return mk_str_Indexof(args[0], args[1], result); + case OP_STR_INDEXOF2: + SASSERT(num_args == 3); + return mk_str_Indexof2(args[0], args[1], args[2], result); default: return BR_FAILED; } diff --git a/src/ast/rewriter/str_rewriter.h b/src/ast/rewriter/str_rewriter.h index f22ac31a7..c0bae2881 100644 --- a/src/ast/rewriter/str_rewriter.h +++ b/src/ast/rewriter/str_rewriter.h @@ -45,6 +45,7 @@ public: br_status mk_str_EndsWith(expr * haystack, expr * needle, expr_ref & result); br_status mk_str_Contains(expr * haystack, expr * needle, expr_ref & result); br_status mk_str_Indexof(expr * haystack, expr * needle, expr_ref & result); + br_status mk_str_Indexof2(expr * arg0, expr * arg1, expr * arg2, 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 ea4b0c6d0..f6e458fbd 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/src/ast/str_decl_plugin.cpp @@ -31,6 +31,7 @@ str_decl_plugin::str_decl_plugin(): m_endswith_decl(0), m_contains_decl(0), m_indexof_decl(0), + m_indexof2_decl(0), m_arith_plugin(0), m_arith_fid(0), m_int_sort(0){ @@ -49,6 +50,7 @@ void str_decl_plugin::finalize(void) { DEC_REF(m_endswith_decl); DEC_REF(m_contains_decl); DEC_REF(m_indexof_decl); + DEC_REF(m_indexof2_decl); DEC_REF(m_int_sort); } @@ -93,6 +95,12 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) { m_indexof_decl = m->mk_func_decl(symbol("Indexof"), s, s, i, func_decl_info(id, OP_STR_INDEXOF)); m_manager->inc_ref(m_indexof_decl); + + { + sort * d[3] = { s, s, i }; + m_indexof2_decl = m->mk_func_decl(symbol("Indexof2"), 3, d, i, func_decl_info(id, OP_STR_INDEXOF2)); + m_manager->inc_ref(m_indexof2_decl); + } } decl_plugin * str_decl_plugin::mk_fresh() { @@ -115,6 +123,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) { case OP_STR_ENDSWITH: return m_endswith_decl; case OP_STR_CONTAINS: return m_contains_decl; case OP_STR_INDEXOF: return m_indexof_decl; + case OP_STR_INDEXOF2: return m_indexof2_decl; default: return 0; } } @@ -176,6 +185,7 @@ void str_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("EndsWith", OP_STR_ENDSWITH)); op_names.push_back(builtin_name("Contains", OP_STR_CONTAINS)); op_names.push_back(builtin_name("Indexof", OP_STR_INDEXOF)); + op_names.push_back(builtin_name("Indexof2", OP_STR_INDEXOF2)); } 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 a2a355ba2..54762f6b9 100644 --- a/src/ast/str_decl_plugin.h +++ b/src/ast/str_decl_plugin.h @@ -36,6 +36,7 @@ enum str_op_kind { OP_STR_ENDSWITH, OP_STR_CONTAINS, OP_STR_INDEXOF, + OP_STR_INDEXOF2, // end LAST_STR_OP }; @@ -53,6 +54,7 @@ protected: func_decl * m_endswith_decl; func_decl * m_contains_decl; func_decl * m_indexof_decl; + func_decl * m_indexof2_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 df77018e9..a5244f7bb 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -531,6 +531,15 @@ app * theory_str::mk_contains(expr * haystack, expr * needle) { return contains; } +app * theory_str::mk_indexof(expr * haystack, expr * needle) { + expr * args[2] = {haystack, needle}; + app * indexof = get_manager().mk_app(get_id(), OP_STR_INDEXOF, 0, 0, 2, args); + // immediately force internalization so that axiom setup does not fail + get_context().internalize(indexof, false); + set_up_axioms(indexof); + return indexof; +} + app * theory_str::mk_strlen(expr * e) { /*if (m_strutil.is_string(e)) {*/ if (false) { const char * strval = 0; @@ -602,7 +611,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_EndsWith_todo.empty() - || !m_axiom_Contains_todo.empty() || !m_axiom_Indexof_todo.empty() + || !m_axiom_Contains_todo.empty() || !m_axiom_Indexof_todo.empty() || !m_axiom_Indexof2_todo.empty() ; } @@ -651,6 +660,11 @@ void theory_str::propagate() { instantiate_axiom_Indexof(m_axiom_Indexof_todo[i]); } m_axiom_Indexof_todo.reset(); + + for (unsigned i = 0; i < m_axiom_Indexof2_todo.size(); ++i) { + instantiate_axiom_Indexof2(m_axiom_Indexof2_todo[i]); + } + m_axiom_Indexof2_todo.reset(); } } @@ -994,6 +1008,74 @@ void theory_str::instantiate_axiom_Indexof(enode * e) { assert_axiom(finalAxiom); } +void theory_str::instantiate_axiom_Indexof2(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 Indexof2 axiom for " << mk_pp(expr, m) << std::endl;); + return; + } + axiomatized_terms.insert(expr); + + TRACE("t_str_detail", tout << "instantiate Indexof2 axiom for " << mk_pp(expr, m) << std::endl;); + + // ------------------------------------------------------------------------------- + // if (arg[2] >= length(arg[0])) // ite2 + // resAst = -1 + // else + // args[0] = prefix . suffix + // /\ indexAst = indexof(suffix, arg[1]) + // /\ args[2] = len(prefix) + // /\ if (indexAst == -1) resAst = indexAst // ite3 + // else resAst = args[2] + indexAst + // ------------------------------------------------------------------------------- + + expr_ref resAst(mk_int_var("res"), m); + expr_ref indexAst(mk_int_var("index"), m); + expr_ref prefix(mk_str_var("prefix"), m); + expr_ref suffix(mk_str_var("suffix"), m); + expr_ref prefixLen(mk_strlen(prefix), m); + expr_ref zeroAst(mk_int(0), m); + expr_ref negOneAst(mk_int(-1), m); + + expr_ref ite3(m.mk_ite( + ctx.mk_eq_atom(indexAst, negOneAst), + ctx.mk_eq_atom(resAst, negOneAst), + ctx.mk_eq_atom(resAst, m_autil.mk_add(expr->get_arg(2), indexAst)) + ),m); + + expr_ref_vector ite2ElseItems(m); + ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(prefix, suffix))); + ite2ElseItems.push_back(ctx.mk_eq_atom(indexAst, mk_indexof(suffix, expr->get_arg(1)))); + ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(2), prefixLen)); + ite2ElseItems.push_back(ite3); + expr_ref ite2Else(m.mk_and(ite2ElseItems.size(), ite2ElseItems.c_ptr()), m); + SASSERT(ite2Else); + + expr_ref ite2(m.mk_ite( + //m_autil.mk_ge(expr->get_arg(2), mk_strlen(expr->get_arg(0))), + m_autil.mk_ge(m_autil.mk_add(expr->get_arg(2), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(0)))), zeroAst), + ctx.mk_eq_atom(resAst, negOneAst), + ite2Else + ), m); + SASSERT(ite2); + + expr_ref ite1(m.mk_ite( + //m_autil.mk_lt(expr->get_arg(2), zeroAst), + m.mk_not(m_autil.mk_ge(expr->get_arg(2), zeroAst)), + ctx.mk_eq_atom(resAst, mk_indexof(expr->get_arg(0), expr->get_arg(1))), + ite2 + ), m); + SASSERT(ite1); + assert_axiom(ite1); + + expr_ref reduceTerm(ctx.mk_eq_atom(expr, resAst), m); + SASSERT(reduceTerm); + assert_axiom(reduceTerm); +} + void theory_str::attach_new_th_var(enode * n) { context & ctx = get_context(); theory_var v = mk_var(n); diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index bf0fef38b..c652a3faf 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -107,11 +107,13 @@ namespace smt { ptr_vector m_string_constant_length_todo; // enode lists for term-specific axioms + // TODO maybe refactor this into a generic "library_aware_axiom_todo" list ptr_vector m_axiom_CharAt_todo; ptr_vector m_axiom_StartsWith_todo; ptr_vector m_axiom_EndsWith_todo; ptr_vector m_axiom_Contains_todo; ptr_vector m_axiom_Indexof_todo; + ptr_vector m_axiom_Indexof2_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 @@ -158,6 +160,7 @@ namespace smt { expr * mk_concat(expr * n1, expr * n2); expr * mk_concat_const_str(expr * n1, expr * n2); app * mk_contains(expr * haystack, expr * needle); + app * mk_indexof(expr * haystack, expr * needle); literal mk_literal(expr* _e); app * mk_int(int n); @@ -191,6 +194,8 @@ namespace smt { bool is_Contains(enode const * n) const { return is_Contains(n->get_owner()); } bool is_Indexof(app const * a) const { return a->is_app_of(get_id(), OP_STR_INDEXOF); } bool is_Indexof(enode const * n) const { return is_Indexof(n->get_owner()); } + bool is_Indexof2(app const * a) const { return a->is_app_of(get_id(), OP_STR_INDEXOF2); } + bool is_Indexof2(enode const * n) const { return is_Indexof2(n->get_owner()); } void instantiate_concat_axiom(enode * cat); void instantiate_basic_string_axioms(enode * str); @@ -201,6 +206,7 @@ namespace smt { void instantiate_axiom_EndsWith(enode * e); void instantiate_axiom_Contains(enode * e); void instantiate_axiom_Indexof(enode * e); + void instantiate_axiom_Indexof2(enode * e); void set_up_axioms(expr * ex); void handle_equality(expr * lhs, expr * rhs);