Z3：实现“使用SMT和列表理论进行模型检查”求解器挂起

Question

我正在尝试实现本文中的一些代码：Model Checking Using SMT and Theory of Lists以证明有关简单机器的事实。我使用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：在FORALL子句中{check tr（lst）}）。这个公理陈述了所有事情列表。但是，SMT求解器不可能尝试证明声明确实适用于所有可能的列表。相反，常见的方法是提供一种实例化模式，以基本说出在什么情况下公理应该被实例化，因此由求解程序强制执行。”意味着，所以我没有实现它。

我现在的目标不是拥有漂亮的代码（我知道星级导入很丑，...），而是拥有有效的代码。

Answer 1

SMT求解器很难处理量化公式，因为它们会使逻辑变得不可确定。 SMT求解器通常依靠“启发式”来解决此类问题。模式是处理量词时“帮助”启发式算法更快收敛的一种方法。