在正则表达式集中找到尽可能多的匹配正则表达式的字符串

Question

假设我有一个正则表达式集R，我怎样才能找到一个字符串s 匹配尽可能多的正则表达式？

例如，如果 R = {a\*b, b\*, c}，则 s 可能是 "b"。我不确定，也许 z3 求解器会有帮助？

Answer 1

是的，z3 可以通过正则表达式和优化来处理这个问题。您可以直接使用 SMTLib 或从其他语言绑定到 z3（C、C++、Java、Haskell 等）来执行此操作。在下面，找到 Python 和 Haskell 版本：

Python

使用 Python 绑定到 z3:

from z3 import *

re1 = Concat(Star(Re("a")), Re("b"))
re2 = Star(Re("b"))
re3 = Re("c")

s = String('s')

o = Optimize()
i = If(InRe(s, re1), 1, 0) + If(InRe(s, re2), 1, 0) + If(InRe(s, re3), 1, 0)
o.maximize(i)

r = o.check()
if r == sat:
    print(o.model())
else:
    print("Solver said: %s" % r)

当我运行这个时，我得到：

[s = "b"]

这会找到您描述的字符串 b。

Haskell

这是同一个示例，使用 Haskell 中的 SBV 库进行编码：

{-# LANGUAGE OverloadedStrings #-}

import Data.SBV
import Data.SBV.RegExp

find = optimize Lexicographic $ do
          s <- sString "s"

          let res = [KStar "a" * "b", KStar "b", KStar "c"]

              count :: SInteger
              count = sum [oneIf (s `match` re) | re <- res]

          maximize "matchCount" count

当运行时，会产生：

Optimal model:
  s          = "b" :: String
  matchCount =   2 :: Integer

这也显示了有多少正则表达式匹配。（你可以编程，这样它也可以准确地告诉你哪些匹配。）

在正则表达式集中找到尽可能多的匹配正则表达式的字符串

find a string match as many regular expressions as possible in a regular expression set

regex

z3

z3py

sbv

Python

Haskell