Как я могу проверить, содержится ли Const в Списке в Z3Py? - PullRequest
Новая
       10

Как я могу проверить, содержится ли Const в Списке в Z3Py?

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

В Z3Py мне нужно проверить, содержится ли тип Const в List, я определяю список типов данных и Const, я пытался использовать метод Contain (https://z3prover.github.io/api/html/namespacez3py.html#ada058544efbae7608acaef3233aa4422), но он только доступен для строкового типа данных, и мне нужно для всех. 

def funList(sort):
    List = Datatype('List')
    #insert: (Int, List) -> List
    List.declare('insert', ('head', sort), ('tail', List)) 
    List.declare('nil')
    return List.create() 

IntList = funList(IntSort())
l1 = Const('l1', IntList)

Я пытался сделать все oop в Z3, но это не работает: S

1 Ответ

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

Ваш вопрос не совсем понятен. Вы пытаетесь закодировать какое-то членство в списке? (Как найти элемент в списке.)

Если это ваша цель, я бы рекомендовал не использовать кодирование на основе Datatype. Потому что любая функция, которую вы напишите об этом (например, elem, length, et c.), Должна быть рекурсивной. И решатели SMT плохо справляются с рекурсивными определениями этой формы; поскольку это помещает логи c в неразрешимый фрагмент. Кроме того, отладка и кодирование довольно сложны, когда присутствуют рекурсивные типы, подобные этим, поскольку поддержка инструмента не так уж велика.

Если ваша цель - использовать структуры, подобные списку, я бы рекомендовал использовать встроенные вместо sequence logi c. Вот пример: 

from z3 import *

s = Solver()

# declare a sequence of integers
iseq = Const('iseq', SeqSort(IntSort()))

# assert 3 is somewhere in this sequence
s.add(Contains(iseq, Unit(IntVal(3))))

# assert the sequence has at least 5 elements
s.add(Length(iseq) >= 5)

# get a model and print it:
if s.check() == sat:
    print s.model()

Когда я запускаю это, я получаю: 

$ python a.py
[iseq = Concat(Unit(9),
               Concat(Unit(10),
                      Concat(Unit(3),
                             Concat(Unit(16), Unit(17)))))]

Возможно, это немного сложно прочитать, но, по сути, говорит, что iseq - это последовательность, которая является конкатенацией (Concat) группы синглетонов (Unit). В более удобной записи это будет: 

iseq = [9, 10, 3, 16, 17]

И, как вы можете видеть, оно имеет 5 элементов, и 3 действительно является этой последовательностью, как того требуют наши ограничения.

Последовательность логики Z3 c довольно богат и содержит много функций, которые вы хотели бы выполнить. Смотрите здесь: https://z3prover.github.io/api/html/z3py_8py_source.html#l09944

...