2

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

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

4

1 回答 1

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 中的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

它还向您显示了匹配的正则表达式的数量。（您可以编程，这样它也可以准确地告诉您哪些匹配。）

于 2020-07-29T07:35:36.497 回答