Регулярное выражение для интерпретации формата smtlib2

Question

Я пытаюсь вычислить регулярное выражение, которое могло бы соответствовать результатам программы, которая выводит в формате 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

Мне просто интересно, есть ли более элегантный способ сделать это?

Answer 1

Захватите эти подстроки:

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

См. Доказательство регулярного выражения .

ОБЪЯСНЕНИЕ

      --------------------------------------------------------------------------------
  \(                       '('
--------------------------------------------------------------------------------
  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
--------------------------------------------------------------------------------
  \)                       ')'