diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp index fbdb10263..7bd4ec154 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/src/ast/str_decl_plugin.cpp @@ -33,6 +33,7 @@ str_decl_plugin::str_decl_plugin(): m_indexof_decl(0), m_indexof2_decl(0), m_lastindexof_decl(0), + m_substr_decl(0), m_arith_plugin(0), m_arith_fid(0), m_int_sort(0){ @@ -53,6 +54,7 @@ void str_decl_plugin::finalize(void) { DEC_REF(m_indexof_decl); DEC_REF(m_indexof2_decl); DEC_REF(m_lastindexof_decl); + DEC_REF(m_substr_decl); DEC_REF(m_int_sort); } @@ -106,6 +108,12 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) { m_lastindexof_decl = m->mk_func_decl(symbol("LastIndexof"), s, s, i, func_decl_info(id, OP_STR_LASTINDEXOF)); m_manager->inc_ref(m_lastindexof_decl); + + { + sort * d[3] = {s, i, i }; + m_substr_decl = m->mk_func_decl(symbol("Substring"), 3, d, s, func_decl_info(id, OP_STR_SUBSTR)); + m_manager->inc_ref(m_substr_decl); + } } decl_plugin * str_decl_plugin::mk_fresh() { @@ -130,6 +138,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) { case OP_STR_INDEXOF: return m_indexof_decl; case OP_STR_INDEXOF2: return m_indexof2_decl; case OP_STR_LASTINDEXOF: return m_lastindexof_decl; + case OP_STR_SUBSTR: return m_substr_decl; default: return 0; } } @@ -193,6 +202,7 @@ void str_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("Indexof", OP_STR_INDEXOF)); op_names.push_back(builtin_name("Indexof2", OP_STR_INDEXOF2)); op_names.push_back(builtin_name("LastIndexof", OP_STR_LASTINDEXOF)); + op_names.push_back(builtin_name("Substring", OP_STR_SUBSTR)); } 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 3e9a1d8f5..bd2a70a1e 100644 --- a/src/ast/str_decl_plugin.h +++ b/src/ast/str_decl_plugin.h @@ -38,6 +38,7 @@ enum str_op_kind { OP_STR_INDEXOF, OP_STR_INDEXOF2, OP_STR_LASTINDEXOF, + OP_STR_SUBSTR, // end LAST_STR_OP }; @@ -57,6 +58,7 @@ protected: func_decl * m_indexof_decl; func_decl * m_indexof2_decl; func_decl * m_lastindexof_decl; + func_decl * m_substr_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 727048c11..4f04ede23 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -612,6 +612,7 @@ 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_Indexof2_todo.empty() || !m_axiom_LastIndexof_todo.empty() + || !m_axiom_Substr_todo.empty() ; } @@ -670,6 +671,11 @@ void theory_str::propagate() { instantiate_axiom_LastIndexof(m_axiom_LastIndexof_todo[i]); } m_axiom_LastIndexof_todo.reset(); + + for (unsigned i = 0; i < m_axiom_Substr_todo.size(); ++i) { + instantiate_axiom_Substr(m_axiom_Substr_todo[i]); + } + m_axiom_Substr_todo.reset(); } } @@ -1150,6 +1156,42 @@ void theory_str::instantiate_axiom_LastIndexof(enode * e) { assert_axiom(finalAxiom); } +void theory_str::instantiate_axiom_Substr(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 Substr axiom for " << mk_pp(expr, m) << std::endl;); + return; + } + axiomatized_terms.insert(expr); + + TRACE("t_str_detail", tout << "instantiate Substr axiom for " << mk_pp(expr, m) << std::endl;); + + expr_ref ts0(mk_str_var("ts0"), m); + expr_ref ts1(mk_str_var("ts1"), m); + expr_ref ts2(mk_str_var("ts2"), m); + + expr_ref ts0_contains_ts1(mk_contains(expr->get_arg(0), ts1), m); + + expr_ref_vector and_item(m); + and_item.push_back(ts0_contains_ts1); + and_item.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(ts0, mk_concat(ts1, ts2)))); + and_item.push_back(ctx.mk_eq_atom(expr->get_arg(1), mk_strlen(ts0))); + and_item.push_back(ctx.mk_eq_atom(expr->get_arg(2), mk_strlen(ts1))); + + expr_ref breakdownAssert(m.mk_and(and_item.size(), and_item.c_ptr()), m); + SASSERT(breakdownAssert); + + expr_ref reduceToVar(ctx.mk_eq_atom(expr, ts1), m); + SASSERT(reduceToVar); + + expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToVar), m); + SASSERT(finalAxiom); + assert_axiom(finalAxiom); +} + 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 70878b45f..35a6fe91b 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -115,6 +115,7 @@ namespace smt { ptr_vector m_axiom_Indexof_todo; ptr_vector m_axiom_Indexof2_todo; ptr_vector m_axiom_LastIndexof_todo; + ptr_vector m_axiom_Substr_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 @@ -199,6 +200,8 @@ namespace smt { bool is_Indexof2(enode const * n) const { return is_Indexof2(n->get_owner()); } bool is_LastIndexof(app const * a) const { return a->is_app_of(get_id(), OP_STR_LASTINDEXOF); } bool is_LastIndexof(enode const * n) const { return is_LastIndexof(n->get_owner()); } + bool is_Substr(app const * a) const { return a->is_app_of(get_id(), OP_STR_SUBSTR); } + bool is_Substr(enode const * n) const { return is_Substr(n->get_owner()); } void instantiate_concat_axiom(enode * cat); void instantiate_basic_string_axioms(enode * str); @@ -211,6 +214,7 @@ namespace smt { void instantiate_axiom_Indexof(enode * e); void instantiate_axiom_Indexof2(enode * e); void instantiate_axiom_LastIndexof(enode * e); + void instantiate_axiom_Substr(enode * e); void set_up_axioms(expr * ex); void handle_equality(expr * lhs, expr * rhs);