z3 - 如何使用 Z3 求解器比较两个解析树以在上下文无关语法中找到歧义？

Question

示例语法：

E ::= E + E | n

由于以下两条路径，我需要证明语法不明确：

E -> E + E -> E + E + E -> n + E + E
E -> E + E -> n + E -> n + E + E

这个想法是，人们将比较函数“集合”symbol1(symbol,index,time)（针对特定时间 t）和 symbol2(symbol,index,time) - 找出它们在哪里是等价的 - 但是有不同的前任（即在时间 t-1)

问题是我不知道如何比较两个函数 symbol1 和 symbol2

如果您有兴趣，我可以发布代码....（大约一页半的价值，但这可能太长了？）。

代码是用 Z3Py 编写的。

Answer 1

检查 CFG 是否模棱两可通常是无法确定的。但是，如果您将规则应用程序的数量限制为少量，那么您可以尝试使用那么多应用程序生成所有可能的字符串，并检查您是否可以使用不同数量的步骤达到相同的字符串。无论如何，我认为 SMT 求解器不适合解决此类问题，因为可导出的字符串数量会随着步数呈指数增长；这将要求您将步骤数保持在非常小的数量，从而使问题变得无趣。

当然，如果您事先知道语法的某些属性，那么您可以想出一个自定义算法来利用它。（假设它是 LALR(1) 可解析的。）但即使在这种情况下，与基于 SMT 的解决方案相比，其他算法方法也会更好。