Z3py模型返回空

Question

我将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())

密码有什么问题吗？

Answer 1

阿克塞尔解释了为什么这样的打印可能会令人困惑。如果要处理具有这些字符的字符串，处理它们的惯用方法是使用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

Answer 2

为了找出正在发生的事情，您可以分析解决方案：

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]
"

实际上，字符串有五个或更长的字符。