我在尝试将Java布尔表达式转换为Z3能够理解的格式时遇到一些问题。由于项目的某些要求，我无法使用任何其他工具来评估表达式。表达式中只能使用标识符，而不能使用函数或更复杂的类型。
我考虑的可能性是：
使用parboiled或类似工具构建解析器。这样做的缺点是，在将运算符转换为等效的SMT并可能加上括号之后，我只想移动运算符所在的位置，因此这种解决方案以及涉及AST处理的工作对我来说似乎工作过度。此外，我发现定义一个适合所有嵌套层的语法有点复杂。
使用词法分析器或其他类型的工具获取令牌，然后使用类似于Shunting-yard算法的算法对令牌进行重新排序。在这种情况下，可能应该要求输入具有所有括号，以避免出现一些问题。
使用可以解析表达式并对其进行编辑的库。到目前为止，除了让您评估表达式的工具外，我什么都没有找到。
使用可以在符号之间直接转换的内容。我一直在搜索，但找不到。不过，这会让我感到高兴。
我一直在寻找类似的问题，但没有发现任何问题。我会很感激您可能有的任何想法。提前致谢！
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句