найти строку, соответствующую как можно большему количеству регулярных выражений в наборе регулярных выражений

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

Вот тот же пример, кодированный с использованием библиотеки SBV в Haskell:

{-# 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

который также показывает, сколько совпадений соответствует. (Вы можете запрограммировать так, чтобы он также точно сообщал вам, какие из них совпадают.)