我在尝试将 java 布尔表达式转换为 Z3 能够理解的格式时遇到了一些问题。由于项目的某些要求，我不能使用任何其他工具来评估表达式。表达式中只能使用标识符，不能使用函数或更复杂的类型。
我考虑过的可能性是：
使用 parboiled 或类似工具构建解析器。这样做的缺点是，我只想在将运算符转换为等效的 SMT 之后移动运算符所在的位置，并且可能添加括号，所以这个解决方案和涉及 AST 处理的工作对我来说似乎工作过度。此外，我发现定义一个适合所有嵌套级别的语法有点复杂。
使用词法分析器或其他类型的工具获取标记，然后使用类似于Shunting-yard 算法的算法对它们重新排序。在这种情况下，也许应该要求输入包含所有括号以避免一些问题。
使用可以解析表达式并对其进行编辑的库。到目前为止，除了可以让您评估表达式的工具之外，我还没有找到任何东西。
使用可以直接在符号之间转换的东西。我一直在寻找，但我找不到。不过，这会让我很开心。
我已经查找了类似的问题，但我没有找到任何东西。我会很感激你有任何想法。提前致谢！