Z3：实现"Model Checking Using SMT and Theory of Lists"求解器挂起

Question

我试图实现本文中的一些代码：使用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(｝(。这条公理说明了一切列表。然而，SMT求解器不可能试图证明这句话确实适用于所有可能的列表。相反，常见的方法是提供一个实例化模式，基本上说明公理在哪些情况下应该被实例化并因此由解算器强制执行。"意思是，所以我没有实现它。

我现在的目标不是拥有漂亮的代码(我知道星形导入很难看，…(，而是拥有可工作的代码。

Answer 1

SMT求解器很难处理量化公式，因为它们使逻辑具有半决定性。SMT求解器通常依靠"启发式"来处理此类问题。在处理量词时，模式是"帮助"这些启发式算法更快收敛的一种方法。

您可能想阅读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(当页面出现时，搜索"图案"。(