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

Question

在z3py中，我想在Z3py（https://z3prover.github.io/api/html/z3py_8py_source.html#l09944）中使用功能Empty

我试图使它像这样：

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

我还试图清空（iseq）仅向我返回空序列的任何内容，但对我没有用

Answer 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本质上是一种功能语言；一旦断言某些内容等于其他内容，就可以not修改该值，就像使用命令式语言（例如Python）一样。希望能有所帮助！