python - 为字符串约束设置求解器

Question

我正在尝试在 python 中使用 z3 为问题(需要字符串操作)实现求解器。我试过阅读 documentation ，但没有足够的信息。我也尝试阅读 z3str documentation，但我找不到让我的示例正常工作的方法。

我想设置:

len(string) = 8
string[6] = 'a'
string_possible_characters = '3456789a'
string.count("6") = 2

在这种情况下使用 itertools(排列 + 组合)之类的东西更好吗？

Answer 1

z3 可以相对轻松地解决此类问题。 API 的使用有点学习曲线，但值得投资。话虽如此，如果您的约束相对简单且字符串较短，则使用常规编程枚举它们并检查约束可能是一种快速且有效的方法有效的替代品。但对于更长的字符串和更复杂的约束，z3 将是解决此类问题的绝佳选择。

以下是我如何用 Python 编写您的示例代码:

# Bring z3 to scope
from z3 import *

# Grab a solver
s = Solver ()

# Create a symbolic string
string = String('string')

# len(string) = 8
s.add(Length(string) == 8)

# string[6] = 'a'
s.add(SubSeq(string, 6, 1) == StringVal('a'))

# string_possible_characters = '3456789a'
chars    = Union([Re(StringVal(c)) for c in '345789a'])   # Note I left 6 out on purpose!
six      = Re(StringVal('6'))

# string.count("6") = 2
# Create a regular expression that matches exactly two occurences
# of 6's and any other allowed character in other positions
template = Concat(Star(chars), six, Star(chars), six, Star(chars))

# Assert our string matches the template
s.add(InRe(string, template))

# Get a model
res = s.check()
if res == sat:
    print s.model()
else:
    print "Solver said:",
    print res

当我运行它时，我得到:

[string = "634436a9"]

它满足您的所有约束。您可以在此模板上进行构建以对其他约束进行建模。 API的相关部分在这里:https://z3prover.github.io/api/html/z3py_8py_source.html#l10190

请注意，Python 并不是唯一提供对 Z3 正则表达式和字符串的访问的 API；几乎所有其他 z3 的高级绑定(bind)都包括某种级别的支持，包括 C/C++/Java/Haskell 等。并且根据这些绑定(bind)提供的抽象，这些约束甚至可能更容易编程。例如，这是使用 SBV Haskell 包编码的同一问题，它使用 z3 作为底层求解器:

{-# LANGUAGE OverloadedStrings #-}

import Data.SBV

import qualified Data.SBV.String as S
import           Data.SBV.RegExp

p :: IO SatResult
p = sat $ do s <- sString "string"

             let others   = KStar $ oneOf "345789a"
                 template = others * "6" * others * "6" * others

             constrain $ S.length s        .== 8
             constrain $ S.strToCharAt s 6 .== literal 'a'
             constrain $ s `match` template

运行时，该程序产生:

*Main> p
Satisfiable. Model:
  string = "649576a8" :: String

如您所见，Haskell 编码相当简洁易读，而其他语言(如 C、Java 等)的编码可能更冗长。当然，您应该选择一种最适合您的宿主语言，但如果您可以自由选择，我建议您使用易于使用的 Haskell 绑定(bind)。详情在这里:http://hackage.haskell.org/package/sbv