From 7c8b882ae6603b5908d6aa6d3ce5b48422c73cb4 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 15 Jun 2016 18:04:33 -0400 Subject: [PATCH] decl and rewriter support for LastIndexof in theory_str (WIP) --- src/ast/rewriter/str_rewriter.cpp | 21 +++++++++++++++++++++ src/ast/rewriter/str_rewriter.h | 1 + src/ast/str_decl_plugin.cpp | 7 +++++++ src/ast/str_decl_plugin.h | 2 ++ 4 files changed, 31 insertions(+) diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp index 30dcb1d95..c4f2e634e 100644 --- a/src/ast/rewriter/str_rewriter.cpp +++ b/src/ast/rewriter/str_rewriter.cpp @@ -158,6 +158,24 @@ br_status str_rewriter::mk_str_Indexof2(expr * arg0, expr * arg1, expr * arg2, e } } +br_status str_rewriter::mk_str_LastIndexof(expr * haystack, expr * needle, expr_ref & result) { + TRACE("t_str_rw", tout << "rewrite (LastIndexof " << 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 LastIndexof expression" << std::endl;); + std::string arg0Str = m_strutil.get_string_constant_value(haystack); + std::string arg1Str = m_strutil.get_string_constant_value(needle); + if (arg0Str.rfind(arg1Str) != std::string::npos) { + int index = arg0Str.rfind(arg1Str); + 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()); @@ -183,6 +201,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_STR_INDEXOF2: SASSERT(num_args == 3); return mk_str_Indexof2(args[0], args[1], args[2], result); + case OP_STR_LASTINDEXOF: + SASSERT(num_args == 2); + return mk_str_LastIndexof(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 c0bae2881..de399acba 100644 --- a/src/ast/rewriter/str_rewriter.h +++ b/src/ast/rewriter/str_rewriter.h @@ -46,6 +46,7 @@ public: 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); + br_status mk_str_LastIndexof(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 f6e458fbd..fbdb10263 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/src/ast/str_decl_plugin.cpp @@ -32,6 +32,7 @@ str_decl_plugin::str_decl_plugin(): m_contains_decl(0), m_indexof_decl(0), m_indexof2_decl(0), + m_lastindexof_decl(0), m_arith_plugin(0), m_arith_fid(0), m_int_sort(0){ @@ -51,6 +52,7 @@ void str_decl_plugin::finalize(void) { DEC_REF(m_contains_decl); DEC_REF(m_indexof_decl); DEC_REF(m_indexof2_decl); + DEC_REF(m_lastindexof_decl); DEC_REF(m_int_sort); } @@ -101,6 +103,9 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) { 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); } + + 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); } decl_plugin * str_decl_plugin::mk_fresh() { @@ -124,6 +129,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) { case OP_STR_CONTAINS: return m_contains_decl; case OP_STR_INDEXOF: return m_indexof_decl; case OP_STR_INDEXOF2: return m_indexof2_decl; + case OP_STR_LASTINDEXOF: return m_lastindexof_decl; default: return 0; } } @@ -186,6 +192,7 @@ void str_decl_plugin::get_op_names(svector & op_names, symbol cons 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)); + op_names.push_back(builtin_name("LastIndexof", OP_STR_LASTINDEXOF)); } 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 54762f6b9..3e9a1d8f5 100644 --- a/src/ast/str_decl_plugin.h +++ b/src/ast/str_decl_plugin.h @@ -37,6 +37,7 @@ enum str_op_kind { OP_STR_CONTAINS, OP_STR_INDEXOF, OP_STR_INDEXOF2, + OP_STR_LASTINDEXOF, // end LAST_STR_OP }; @@ -55,6 +56,7 @@ protected: func_decl * m_contains_decl; func_decl * m_indexof_decl; func_decl * m_indexof2_decl; + func_decl * m_lastindexof_decl; arith_decl_plugin * m_arith_plugin; family_id m_arith_fid;