时间戳

首页 > 解决方案 > 我不明白如何在 Z3py 中开发长度方法

python - 我不明白如何在 Z3py 中开发长度方法

问题描述

我想开发一个函数来计算 Z3 中列表的长度，但我认为我做错了。我是使用 Z3 的新手，我不太了解。我做的：


def length(numbers):
    cont = 0
    x, length = Ints('x length')
    s = Solver()

    for x in numbers:
        cont +=1        

    dato = Implies(cont >0 , length == cont), Or(Implies(cont == 0, length == cont))
    s.add(dato)
    n = Solver()
    solve(dato)
    if s.check() == unsat:
        print(cont)
    else:
       # print("true")
        print(s.model())


if __name__ == '__main__':
    my_list = [1, 2,"p", 3,6,503]
    length([])
    length(my_list)

但是我认为我应该使用Z3的一个功能，因为如果我想制作更多方法（isNull，isEmpty ...）并同时调用它，那么Length for make axioms，但我现在不能执行。

标签： pythonz3z3py

解决方案

目前尚不清楚您要实现什么，但看起来您正在将 Python 列表与 Z3 序列混为一谈。当你有一个具体的列表时使用前者，而当列表本身可以是任意长度时使用后者。

对于后者，您还想使用序列逻辑，它已经定义了函数length、isNull等isEmpty，但名称不同。有关详细信息，请参见此处：https ://rise4fun.com/z3/tutorialcontent/sequences#h22

推荐阅读