Z3py 模型返回 EMPTY答案

【问题标题】：Z3py model returned EMPTYZ3py 模型返回 EMPTY
【发布时间】：2020-12-30 19:13:08
【问题描述】：

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

代码有什么问题？

【问题讨论】：

标签： string z3 z3py

【解决方案1】：

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

【讨论】：

【解决方案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]
"

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

【讨论】：