add RegexPlus to theory_str

src/ast/rewriter/str_rewriter.cpp

@@ -219,6 +219,27 @@ br_status str_rewriter::mk_re_RegexIn(expr * str, expr * re, expr_ref & result)
 	return BR_FAILED;
 }
 
+br_status str_rewriter::mk_re_RegexPlus(expr * re, expr_ref & result) {
+    /*
+     * Two optimizations are possible if we inspect 're'.
+     * If 're' is (RegexPlus X), then reduce to 're'.
+     * If 're' is (RegexStar X), then reduce to 're'.
+     * Otherwise, reduce to (RegexConcat re (RegexStar re)).
+     */
+
+    if (m_strutil.is_re_RegexPlus(re)) {
+        result = re;
+        return BR_REWRITE_FULL;
+    } else if (m_strutil.is_re_RegexStar(re)) {
+        // Z3str2 re-created the AST under 're' here, but I don't think we need to do that
+        result = re;
+        return BR_REWRITE_FULL;
+    } else {
+        result = m_strutil.mk_re_RegexConcat(re, m_strutil.mk_re_RegexStar(re));
+        return BR_REWRITE_FULL;
+    }
+}
+
 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());
 
@@ -256,6 +277,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_RE_REGEXIN:
     	SASSERT(num_args == 2);
     	return mk_re_RegexIn(args[0], args[1], result);
+    case OP_RE_REGEXPLUS:
+        SASSERT(num_args == 1);
+        return mk_re_RegexPlus(args[0], result);
     default:
         return BR_FAILED;
     }

src/ast/rewriter/str_rewriter.h

@@ -51,6 +51,7 @@ public:
 
     br_status mk_re_Str2Reg(expr * str, expr_ref & result);
     br_status mk_re_RegexIn(expr * str, expr * re, expr_ref & result);
+    br_status mk_re_RegexPlus(expr * re, 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

@@ -42,6 +42,7 @@ str_decl_plugin::str_decl_plugin():
 	m_re_regexstar_decl(0),
 	m_re_regexunion_decl(0),
 	m_re_unroll_decl(0),
+    m_re_regexplus_decl(0),
     m_arith_plugin(0),
     m_arith_fid(0),
     m_int_sort(0){
@@ -70,6 +71,7 @@ void str_decl_plugin::finalize(void) {
     DEC_REF(m_re_regexconcat_decl);
     DEC_REF(m_re_regexstar_decl);
     DEC_REF(m_re_regexunion_decl);
+    DEC_REF(m_re_regexplus_decl);
     DEC_REF(m_re_unroll_decl);
     DEC_REF(m_int_sort);
 }
@@ -153,6 +155,9 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
     m_re_regexstar_decl = m->mk_func_decl(symbol("RegexStar"), re, re, func_decl_info(id, OP_RE_REGEXSTAR));
     m_manager->inc_ref(m_re_regexstar_decl);
 
+    m_re_regexplus_decl = m->mk_func_decl(symbol("RegexPlus"), re, re, func_decl_info(id, OP_RE_REGEXPLUS));
+    m_manager->inc_ref(m_re_regexplus_decl);
+
     m_re_regexunion_decl = m->mk_func_decl(symbol("RegexUnion"), re, re, re, func_decl_info(id, OP_RE_REGEXUNION));
     m_manager->inc_ref(m_re_regexunion_decl);
 
@@ -190,6 +195,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) {
     case OP_RE_REGEXIN: return m_re_regexin_decl;
     case OP_RE_REGEXCONCAT: return m_re_regexconcat_decl;
     case OP_RE_REGEXSTAR: return m_re_regexstar_decl;
+    case OP_RE_REGEXPLUS: return m_re_regexplus_decl;
     case OP_RE_REGEXUNION: return m_re_regexunion_decl;
     case OP_RE_UNROLL: return m_re_unroll_decl;
     default: return 0;
@@ -262,6 +268,7 @@ void str_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
     op_names.push_back(builtin_name("RegexConcat", OP_RE_REGEXCONCAT));
     op_names.push_back(builtin_name("RegexStar", OP_RE_REGEXSTAR));
     op_names.push_back(builtin_name("RegexUnion", OP_RE_REGEXUNION));
+    op_names.push_back(builtin_name("RegexPlus", OP_RE_REGEXPLUS));
     op_names.push_back(builtin_name("Unroll", OP_RE_UNROLL));
 }
 

src/ast/str_decl_plugin.h

@@ -48,6 +48,8 @@ enum str_op_kind {
 	OP_RE_REGEXSTAR,
 	OP_RE_REGEXUNION,
 	OP_RE_UNROLL,
+	// higher-level regex operators
+	OP_RE_REGEXPLUS,
     // end
     LAST_STR_OP
 };
@@ -77,6 +79,7 @@ protected:
     func_decl * m_re_regexstar_decl;
     func_decl * m_re_regexunion_decl;
     func_decl * m_re_unroll_decl;
+    func_decl * m_re_regexplus_decl;
 
     arith_decl_plugin * m_arith_plugin;
     family_id           m_arith_fid;
@@ -120,6 +123,8 @@ public:
     bool is_string(expr const * n) const;
 
     bool is_re_Str2Reg(expr const * n) const { return is_app_of(n, get_fid(), OP_RE_STR2REGEX); }
+    bool is_re_RegexStar(expr const * n) const { return is_app_of(n, get_fid(), OP_RE_REGEXSTAR); }
+    bool is_re_RegexPlus(expr const * n) const { return is_app_of(n, get_fid(), OP_RE_REGEXPLUS); }
 
     std::string get_string_constant_value(expr const *n) const;
     // TODO
@@ -142,7 +147,17 @@ public:
     app * mk_fresh_string() {
         return m_plugin->mk_fresh_string();
     }
-    // TODO
+
+    app * mk_re_RegexConcat(expr * e1, expr * e2) {
+        expr * es[2] = {e1, e2};
+        return m_manager.mk_app(get_fid(), OP_RE_REGEXCONCAT, 2, es);
+    }
+
+    app * mk_re_RegexStar(expr * r) {
+        expr * es[1] = {r};
+        return m_manager.mk_app(get_fid(), OP_RE_REGEXSTAR, 1, es);
+    }
+
 };
 
 #endif /* _STR_DECL_PLUGIN_H_ */