decl and rewriter support for LastIndexof in theory_str (WIP)

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;
     }

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);

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<builtin_name> & 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<builtin_name> & sort_names, symbol const & logic) {

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;