如何在 Z3Py 的列表中使用 Empty 方法？答案

【问题标题】：How I can to use Empty method in a List in Z3Py?如何在 Z3Py 的列表中使用 Empty 方法？
【发布时间】：2020-01-29 21:40:53
【问题描述】：

在 z3py 中我想在 Z3py 中使用 Empty 函数 (https://z3prover.github.io/api/html/z3py_8py_source.html#l09944)

我尝试过这样：

s = Solver()

# declare a sequence of integers
iseq = Const('iseq', SeqSort(IntSort()))
solve(Empty(iseq)!= True)


# get a model and print it:
if s.check() == sat:
    print (s.model())

但我返回“Z3Exception：传递给 Empty 的非序列、非正则表达式排序”

我也尝试 Empty(iseq) 只支持我一个空序列，但它对我没有用

【问题讨论】：

标签： python z3 z3py

【解决方案1】：

这里发生了一些事情：

您通过s = Solver () 声明了一个求解器对象，但随后您调用了solve 函数。 solve 创建自己的求解器。只需改用s.add。
Empty 根据排序创建一个序列。您不能在iseq 上调用它。这就是您收到的错误消息。

我猜你想说的是：声明iseq，确保它不为空。您可以编写如下代码：

from z3 import *

s = Solver()

# declare a sequence of integers
iseq = Const('iseq', SeqSort(IntSort()))

# assert it's not empty
s.add (Length(iseq) != 0)

# get a model and print it:
if s.check() == sat:
    print (s.model())

z3 说：

$ python a.py
[iseq = Unit(2)]

所以，它给了你一个模型，其中iseq 是包含数字2 的单例序列； not 为空，满足我们提出的约束。

这是一个使用Empty 创建空序列的示例：

from z3 import *

s = Solver()

# Give a name to integer sequences
ISeq = SeqSort(IntSort())

# declare a sequence of integers
iseq = Const('iseq', ISeq)

# make sure it's empty!
s.add (iseq == Empty(ISeq))

# get a model and print it:
if s.check() == sat:
    print (s.model())

z3 说：

[iseq = Empty(Seq(Int))]

请注意，z3py 本质上是一种函数式语言；一旦您断言某事等于其他某事，您就可以不修改该值，就像您在命令式语言（例如 Python）中所做的那样。希望对您有所帮助！

【讨论】：

非常感谢您的帮助。我只是想尝试一个 Empty 的例子来更好地理解什么是有效的，感谢你的帮助我知道 Empty 方法会生成一个空序列，但我想知道我必须把 s.add (..) 生成它。
添加了一个示例来展示如何使用Empty。我仍然不清楚您要达到的目标。