Z3py 模型返回 EMPTY

如何解决Z3py 模型返回 EMPTY

我将 z3 格式转换为 z3py 但模型返回空字符串。它应该给我等于或大于 5 个字母的字符串。

(declare-const z String)
(assert (>= (str.len z) 5))
(check-sat)
(get-model)

from z3 import *
s = Solver()
a = String('a')
s.add(Length(a) >= 5)
print(s.check())
print(s.model())

代码有什么问题？

解决方法

要了解发生了什么，您可以分析解决方案：

from z3 import *
s = Solver()
a = String('a')

s.add(Length(a) >= 5)

print(s.check())
m = s.model()

def showChar(c):
    return c if ord(c) > 20 else "[" + str(ord(c)) + "]"

for c in str(m[a]):
    print(showChar(c))

结果输出：

sat
"
[0]
[0]
[0]
[0]
[0]
"

字符串实际上是五个或更多字符长。

,

Axel 解释了为什么此类打印输出会令人困惑。如果您正在处理具有此类字符的字符串，处理它们的惯用方法是使用 encode 方法：

from z3 import *
s = Solver()
a = String('a')
s.add(Length(a) >= 5)
print(s.check())
print(s.model()[a].as_string().encode('unicode_escape'))

打印：

sat
\x00\x00\x00\x00\x00