From f5f980fa381f16ee92b284c4fb87435cbbf6bfbf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Dec 2020 21:28:23 -0800 Subject: [PATCH] add rewrite rule --- src/ast/rewriter/seq_rewriter.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 0b65454cd..6725c263c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1428,6 +1428,7 @@ br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) { indexof("", b, r) -> if b = "" and r = 0 then 0 else -1 indexof(unit(x)+a, b, r+1) -> indexof(a, b, r) indexof(unit(x)+a, unit(y)+b, 0) -> indexof(a,unit(y)+b, 0) if x != y + indexof(substr(x,y,len1), z, len2) -> -1 if len2 > len1 */ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result) { zstring s1, s2; @@ -1468,6 +1469,13 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result return BR_REWRITE2; } } + expr* x = nullptr, *y = nullptr, *len1 = nullptr; + rational r1, r2; + if (str().is_extract(a, x, y, len1) && m_autil.is_numeral(len1, r1) && + m_autil.is_numeral(c, r2) && r2 > r1) { + result = minus_one(); + return BR_DONE; + } expr_ref_vector as(m()), bs(m()); str().get_concat_units(a, as);