From 4fd1e6d32c31e87a255dd7b651d1ad1fb64d7265 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Sun, 25 Jul 2021 09:51:48 -0700 Subject: [PATCH] added derivative support for (str.to_re (str.from_int ...)) (#5431) --- src/ast/rewriter/seq_rewriter.cpp | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 513180bac..99de59aec 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3339,6 +3339,26 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { //while mk_empty() = [], because deriv(epsilon) = [] = nothing return mk_empty(); } + else if (str().is_itos(r1, r2)) + { + //here r1 = (str.from_int r2) and r2 is non-ground + //or else the expression would have been simplified earlier + //so r1 must be nonempty and must consists of decimal digits + //'0' = char(48) <= elem <= char(57) = '9' + m_br.mk_and(u().mk_le(m_util.mk_char(48), ele), u().mk_le(ele, m_util.mk_char(57)), result); + if (m().is_false(result)) + return mk_empty(); + + hd = str().mk_nth_i(r1, m_autil.mk_int(0)); + m_br.mk_and(result, m().mk_eq(hd, ele), result); // result := result & ele = (hd r1) + if (m().is_false(result)) + return mk_empty(); + + tl = str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1))); + //if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else [] + result = re_and(result, re().mk_to_re(tl)); + return result; + } #if 0 else { hd = str().mk_nth_i(r1, m_autil.mk_int(0));