java - 将 java boolean 表达式转换为 SMTlib

Question

我在尝试将 java boolean 表达式转换为 Z3 能够理解的格式时遇到一些问题。由于项目的某些要求，我无法使用任何其他工具来评估表达式。表达式中只能使用标识符，不能使用函数或更复杂的类型。

我考虑过的可能性是:

• 使用 parboiled 或类似工具构建解析器。这样做的缺点是，我只想在将其转换为 SMT 等效项后移动操作符所在的位置，并且可能添加括号，因此这个解决方案和涉及 AST 处理的工作对我来说似乎过度劳累。此外，我发现定义一个适合所有嵌套级别的语法有点复杂。

• 使用词法分析器或其他类型的工具来获取标记，然后使用类似于 Shunting-yard algorithm 的算法对它们重新排序。 。在这种情况下，也许应该要求输入包含所有括号，以避免出现一些问题。

• 使用可以解析表达式并进行编辑的库。到目前为止，除了可以让您评估表达式的工具之外，我还没有找到任何东西。

• 使用可以在符号之间直接转换的东西。我一直在寻找，但没能找到。不过，这会让我很开心。

我查过类似的问题，但没有找到任何东西。我将不胜感激您的任何想法。提前致谢!

Answer 1

您考虑过TXL ？TXL 提供对解析文件、对抽象语法树应用转换并打印结果的支持。它很容易使用，而且他们有很多文档和一个大的 library语法(包括 Java)。