时间戳

首页 > 解决方案 > 如何在 Z3Py 的列表中使用 Empty 方法？

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

问题描述

在 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) 只支持我一个空序列，但它对我没有用

标签： pythonz3z3py

解决方案

这里发生了一些事情：

  • 您正在通过 声明求解器对象s = Solver ()，但随后您正在调用该solve函数。solve创建自己的求解器。只需使用即可s.add。

  • Empty给定排序，创建一个序列。你不能调用它iseq。这就是您收到的错误消息。

我猜你想说的是： declare 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；它不是空的，它满足我们提出的约束。

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）中所做的那样。希望有帮助！

推荐阅读