正则表达式解释 smtlib2 格式答案

【问题标题】：Regex to interpret smtlib2 format正则表达式解释 smtlib2 格式
【发布时间】：2021-06-06 17:19:04
【问题描述】：

我正在尝试找出一个正则表达式，它可以匹配以 smtlib 格式输出的程序的结果。基本上，我的数据是这样的：

 (define-fun X_1 () Int
    281)
 (define-fun X_71 () Int
    104)
 (define-fun X_90 () Int
    21)
 (define-fun X_54 () Int
    250)
etc.

是否可以写一个匹配的表达式：

X_1 (...) 281
X_71 (...) 104
X_90 (...) 21
etc.

我目前的方法是使用\(define-fun[\w\s]+\) 查找单个事件，然后对于每个事件，删除(define-fun、Int、() 和)，然后读取数据，因为剩下的就是这样 1 281, 71 104

我只是想知道是否有更优雅的方式来做到这一点？

【问题讨论】：

不清楚你需要匹配什么。如果格式那么严格，您可能会使用\(define-fun\s+(\w+)\s*\([^()]*\)\s*([\w\W]*?)\s*(\d+)\)，请参阅demo。

标签： regex smt-lib

【解决方案1】：

捕获这些子字符串：

\(define-fun\s+(\S+).*\n\s*(\d+)\)

见regex proof。

解释

--------------------------------------------------------------------------------
  \(                       '('
--------------------------------------------------------------------------------
  define-fun               'define-fun'
--------------------------------------------------------------------------------
  \s+                      whitespace (\n, \r, \t, \f, and " ") (1 or
                           more times (matching the most amount
                           possible))
--------------------------------------------------------------------------------
  (                        group and capture to \1:
--------------------------------------------------------------------------------
    \S+                      non-whitespace (all but \n, \r, \t, \f,
                             and " ") (1 or more times (matching the
                             most amount possible))
--------------------------------------------------------------------------------
  )                        end of \1
--------------------------------------------------------------------------------
  .*                       any character except \n (0 or more times
                           (matching the most amount possible))
--------------------------------------------------------------------------------
  \n                       '\n' (newline)
--------------------------------------------------------------------------------
  \s*                      whitespace (\n, \r, \t, \f, and " ") (0 or
                           more times (matching the most amount
                           possible))
--------------------------------------------------------------------------------
  (                        group and capture to \2:
--------------------------------------------------------------------------------
    \d+                      digits (0-9) (1 or more times (matching
                             the most amount possible))
--------------------------------------------------------------------------------
  )                        end of \2
--------------------------------------------------------------------------------
  \)                       ')'

【讨论】：