Z3: реализация зависания решателя «Проверка модели с использованием SMT и теории списков» - PullRequest
Новая
       17

Z3: реализация зависания решателя «Проверка модели с использованием SMT и теории списков»

1 голос
/ 09 марта 2020

Я пытаюсь реализовать код из этой статьи: Проверка модели с использованием SMT и теории списков , чтобы доказать факты о простой машине. Я написал следующий код с использованием Python Z3 API, отражая код, описанный в статье: код и проблема были намеренно упрощены, чтобы лучше показать проблему: 

from z3 import *

MachineIntSort = BitVecSort(16)
MachineInt = lambda x: BitVec(x, 16)

def DeclareLinkedList(sort):
    LinkedList = Datatype(f'{sort.name()}_LinkedList')
    LinkedList.declare('nil')
    LinkedList.declare('cons', ('car', sort), ('cdr', LinkedList))
    return LinkedList.create()


State = Datatype('State')
State.declare('state',
    ('A', MachineIntSort),
    ('B', MachineIntSort),
    ('C', MachineIntSort),
    ('D', MachineIntSort))
State = State.create()

StateList = DeclareLinkedList(State)


def transition_condition(initial, next):
    return State.A(next) == State.A(initial) + 1

def final_condition(lst):
    return State.A(StateList.car(lst)) == 2

solver = Solver()
check_execution_trace = Function('check_execution_trace', StateList, BoolSort())
execution_list = Const('execution_list', StateList)


solver.add(ForAll(execution_list, check_execution_trace(execution_list) ==
    If(And(execution_list != StateList.nil, StateList.cdr(execution_list) != StateList.nil),
        And(
            transition_condition(StateList.car(execution_list), StateList.car(StateList.cdr(execution_list))),
            check_execution_trace(StateList.cdr(execution_list)),
            If(final_condition(StateList.cdr(execution_list)),
                StateList.nil == StateList.cdr(StateList.cdr(execution_list)),
                StateList.nil != StateList.cdr(StateList.cdr(execution_list))
            )
        ),
    True), # If False, unsat but incorrect. If True, it hangs
))

states = Const('states', StateList)

# Execution trace cannot be empty
solver.add(StateList.nil != states)

# Initial condition
solver.add(State.A(StateList.car(states)) == 0)

# Transition axiom
solver.add(check_execution_trace(states))

print(solver.check())
print(solver.model())

Проблема в том, что модель шаг висит вместо того, чтобы дать (тривиальное) решение. Я думаю, что, возможно, я не реализовал все, что описывает бумага: я не понимаю, что «Наконец, важно подчеркнуть цель шаблона создания экземпляров (PAT: {check tr (lst)}) в предложении FORALL. Эта аксиома заявляет что-то обо всех списках. Однако для решателя SMT было бы невозможно попытаться доказать, что утверждение действительно выполняется для всех возможных списков. Вместо этого, общий подход состоит в том, чтобы предоставить образец реализации, чтобы в основном сказать, в каких случаях аксиома должна быть инициатором и, следовательно, исполнителем решения ". значит, я его не реализовал.

Моя цель сейчас не в том, чтобы иметь красивый код (я знаю, что импорт звездочек уродлив, ...), а в том, чтобы иметь рабочий код.

1 Ответ

2 голосов
/ 10 марта 2020

Квантованным формулам сложно работать с SMT-решателями, так как они делают логику c полуразрешимой. Решатели SMT обычно полагаются на «эвристику» для решения таких проблем. Шаблоны являются одним из способов «помочь» этим эвристикам быстрее сходиться при работе с квантификаторами.

Возможно, вы захотите прочитать Раздел 13.2 из http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.225.8231&rep=rep1&type=pdf

Чтобы увидеть пример того, как добавить шаблоны в привязки z3py, посмотрите эту страницу: https://ericpony.github.io/z3py-tutorial/advanced-examples.htm (Поиск «шаблонов» при появлении страницы.)

...