Как я могу узнать, является ли один массив ArEmpty в Z3py? - PullRequest
Новая
       8

Как я могу узнать, является ли один массив ArEmpty в Z3py?

0 голосов
/ 14 января 2020

Я начинаю использовать Z3py, и у меня так трудно понять, как это работает. Я должен знать, если массив isEmpty или нет, но я не знаю, как создать ссылку между "х" и "массив" 

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()

1 Ответ

2 голосов
/ 14 января 2020

Как ответил Кристоф в своем предыдущем вопросе ( как я могу узнать, сколько значений имеет массив в z3? ), массив в z3 имеет неограниченный размер. В этом смысле они больше похожи на функции. Для каждого целого числа x, (select A x) является значимым выражением.

Пожалуйста, просмотрите массив logi c в документе SMTLib (http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml). Таким образом, спрашивать, является ли массив пустым, бессмысленно. Если вы хотите связать размер с массивом, вам придется управлять этим отдельно, возможно, используя последовательность logi c (https://rise4fun.com/Z3/tutorial/sequences), где вы можете говорить о списках конечной длины; больше похоже на массивы, которые можно найти в таких языках программирования, как C или Java.

...