我怎么知道Z3py中是否有一个数组为空？

Question

我开始使用Z3py，并且我很难理解它的功能。我必须知道数组是否为isEmpty，但是我不知道如何在“ x”和“ array”之间创建引用。

def isEmpty():
    x = Int('x')
    y = Int('y')
    array = Array('array', IntSort(), IntSort())

    empty = Bool('isEmpty')
    s = Solver()
    #s.add(x==0)
    dato = Implies(x>0,empty == False),Or(Implies(x<=0,empty == True))
    s.add(dato)

    if s.check() == sat:
        #print("0")
        #print(s.model())
        return s.model()


if __name__ == '__main__':
     isEmpty()

我开始使用Z3py，并且我很难理解它的功能。我必须知道数组是否为isEmpty，但是我不知道如何在“ x”和“ array” def之间创建引用...

Answer 1

正如Christoph在您上一个问题（how I can to know how many values have a array in z3?）中回答的那样，z3中的数组的大小无限制。从这个意义上讲，它们更像是函数。对于每个整数x，(select A x)是一个有意义的表达式。