From 1e0f71c97187c65548fbbb34d235980a12521fe8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 22 Jul 2022 09:35:25 -0700 Subject: [PATCH] add way to access range bounds directly #6186 Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 25 +++++++++++++++++++++++++ src/ast/seq_decl_plugin.h | 1 + 2 files changed, 26 insertions(+) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index bf377df43..54ef58e32 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1107,6 +1107,31 @@ unsigned seq_util::rex::max_length(expr* r) const { return UINT_MAX; } +/** + \brief determine if \c n is a range regular expression where the lower and upper bounds + are given by single characters. + Range expressions where lower and upper bounds are not single characters are either + the empty language (when a bound is a string but not a single character) or symbolic + (when both bounds are not ground strings). The general is_range can be used to process + range expressions for these cases, but they don't correspond to mainstream regex usage. + */ +bool seq_util::rex::is_range(expr const* n, unsigned& lo, unsigned& hi) const { + expr* _lo, *_hi; + zstring los, his; + if (!is_range(n, _lo, _hi)) + return false; + if (!u.str.is_string(_lo, los)) + return false; + if (!u.str.is_string(_hi, his)) + return false; + if (los.length() != 1 || his.length() != 1) + return false; + lo = los[0]; + hi = his[0]; + return true; +} + + sort* seq_util::rex::to_seq(sort* re) { (void)u; SASSERT(u.is_re(re)); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index b0c3ab3c6..d5c6da187 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -545,6 +545,7 @@ public: bool is_plus(expr const* n) const { return is_app_of(n, m_fid, OP_RE_PLUS); } bool is_opt(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OPTION); } bool is_range(expr const* n) const { return is_app_of(n, m_fid, OP_RE_RANGE); } + bool is_range(expr const* n, unsigned& lo, unsigned& hi) const; bool is_loop(expr const* n) const { return is_app_of(n, m_fid, OP_RE_LOOP); } bool is_empty(expr const* n) const { return is_app_of(n, m_fid, OP_RE_EMPTY_SET); } bool is_full_char(expr const* n) const { return is_app_of(n, m_fid, OP_RE_FULL_CHAR_SET); }