Я не понимаю, как я могу разработать метод длины в Z3py - PullRequest
Новая
       3

Я не понимаю, как я могу разработать метод длины в Z3py

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

Я хочу разработать функцию для вычисления длины в 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 ...) и вызывать их одновременно, Длина для создания аксиом, но я не могу для текущей реализации.

1 Ответ

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

Не совсем понятно, чего вы пытаетесь достичь, но похоже, что вы объединяете списки Python с последовательностями Z3. Используйте первое, когда у вас есть конкретный список, а второе, когда список может иметь произвольную длину.

Для последнего вы также хотите использовать последовательность logi c, которая уже определяет функции length, isNull, isEmpty et c., Но с разными именами. Подробности смотрите здесь: https://rise4fun.com/z3/tutorialcontent/sequences#h22

...