From 1f8b08108c039ef1956e8e37926822af9b85b09a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 26 Jul 2025 14:02:34 -0700 Subject: [PATCH] #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. --- src/ast/rewriter/seq_rewriter.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index cd7b56865..ba544e854 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -6021,6 +6021,12 @@ bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) { result = m_autil.mk_lt(s, zero()); return true; } + // at(s, offset) = "" <=> len(s) <= offset or offset < 0 + if (str().is_at(r, s, offset)) { + expr_ref len_s(str().mk_length(s), m()); + result = m().mk_or(m_autil.mk_le(len_s, offset), m_autil.mk_lt(offset, zero())); + return true; + } return false; }