0

对于非确定性规则，有没有办法在应用其他规则之前对某些规则进行优先级排序，直到它们无法再应用？

例如在以下规则中（在伪代码中）

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)。即，如果允许负模式匹配，则仅适用 (2) 和 (3) 如果没有任何S形式是P|Q. 如果我没记错的话，我可以使用函数来达到类似的效果，但我想知道是否有更直接的方法。

此外，与上述规则有些相关，以下是查找表单多个元素的正确语法A + _吗？

<myset> ... SetItem(A + B) SetItem(A + C)... </myset>

那么是否可以更新它们？

<myset> ... (SetItem(A + B)=>SetItem(B)) (SetItem(A + C)=>SetItem(C))... </myset>
4

1 回答 1

1

只是为了确保该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)]

这将确保规则one总是在规则之前two尝试或被three尝试。这适用于 LLVM（具体执行）和 Haskell（符号执行）后端，并且适用于普通规则和函数规则。请注意，由于 Haskell 后端必须在状态空间中进行详尽的搜索，如果它不能证明较低优先级的规则涵盖了所有可能的行为，它仍然会在较低优先级规则未涵盖的其余部分上尝试较高优先级的规则.

优先级可以介于0和200（包括）之间。

您也可以使用owise属性，它基本上是priority(200).

大多数规则的默认优先级是50。一些特定的自动生成的规则获得优先权100。

于 2020-05-16T11:10:47.970 回答