From f9b4f21683c19cf629dbc7f6d49793788c87f696 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 31 Aug 2016 19:22:04 -0400 Subject: [PATCH] add rewrite for theory_str rewriter RegexPlus fixes regex-013.smt2 --- src/ast/rewriter/str_rewriter.cpp | 12 ++++++++++++ src/ast/rewriter/str_rewriter.h | 1 + 2 files changed, 13 insertions(+) diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp index c644ecd46..015898a64 100644 --- a/src/ast/rewriter/str_rewriter.cpp +++ b/src/ast/rewriter/str_rewriter.cpp @@ -425,6 +425,15 @@ br_status str_rewriter::mk_re_RegexIn(expr * str, expr * re, expr_ref & result) return BR_FAILED; } +br_status str_rewriter::mk_re_RegexStar(expr * re, expr_ref & result) { + if (m_strutil.is_re_RegexStar(re)) { + result = re; + return BR_REWRITE_FULL; + } else { + return BR_FAILED; + } +} + br_status str_rewriter::mk_re_RegexPlus(expr * re, expr_ref & result) { /* * Two optimizations are possible if we inspect 're'. @@ -523,6 +532,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_RE_REGEXPLUS: SASSERT(num_args == 1); return mk_re_RegexPlus(args[0], result); + case OP_RE_REGEXSTAR: + SASSERT(num_args == 1); + return mk_re_RegexStar(args[0], result); case OP_RE_REGEXCHARRANGE: SASSERT(num_args == 2); return mk_re_RegexCharRange(args[0], args[1], result); diff --git a/src/ast/rewriter/str_rewriter.h b/src/ast/rewriter/str_rewriter.h index c64d086f9..d147e82e8 100644 --- a/src/ast/rewriter/str_rewriter.h +++ b/src/ast/rewriter/str_rewriter.h @@ -57,6 +57,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); + br_status mk_re_RegexStar(expr * re, expr_ref & result); br_status mk_re_RegexCharRange(expr * start, expr * end, expr_ref & result); bool reduce_eq(expr * l, expr * r, expr_ref_vector & lhs, expr_ref_vector & rhs, bool & change);