对于非确定性规则，有没有办法在应用其他规则之前优先考虑某些规则，直到它们无法再应用？
例如，在以下规则中(伪代码(
1. (S U {P | Q}) => (S U {P, Q}) [prioritise]
2. (S U {P + Q}) => (S U {P}) [transition]
3. (S U {P + Q}) => (S U {Q}) [transition]
目的是在不确定地应用规则(2(和(3(之前优先考虑非确定性结构规则，例如(1(。 即，如果允许负模式匹配，则仅当S中没有任何形式是P|Q时应用 (2( 和 (3(。如果我没记错的话，我可以使用函数实现类似的效果，但我想知道是否有更直接的方法。
另外，与上面的规则有些相关，以下语法是否正确，可以找到表单A + _的多个元素？
<myset> ... SetItem(A + B) SetItem(A + C)... </myset>
那么可以更新它们吗？
<myset> ... (SetItem(A + B)=>SetItem(B)) (SetItem(A + C)=>SetItem(C))... </myset>
只是为了确保，transition属性已被弃用，因此在现代 K 后端没有任何意义。
我们通过priority(...)属性支持您的需求。你可以做：
rule [one]: (S U {P | Q}) => (S U {P, Q}) [priority(25)]
rule [two]: (S U {P + Q}) => (S U {P}) [priority(26)]
rule [three]: (S U {P + Q}) => (S U {Q}) [priority(26)]
这将确保始终在尝试规则two或three之前尝试规则one。这适用于LLVM(具体执行(和Haskell(符号执行(后端，并且适用于普通规则和函数规则。请注意，由于 Haskell 后端必须对状态空间进行详尽的搜索，如果它无法证明较低优先级规则涵盖所有可能的行为，它仍将对较低优先级规则未涵盖的其余部分尝试较高优先级的规则。
优先级可以在0和200(含(之间。
您还可以使用owise属性，它基本上是priority(200)的同义词。
大多数规则的默认优先级为50。某些特定的自动生成的规则获得优先级100。