z3 - 支持定点的SMT工具

Question

你知道除了Z3之外还有什么smt工具支持fixpoint吗？

Answer 1

通过定点，我认为您的意思是解决 Horn 子句查询。有许多工具可以解决类似性质的问题，但格式可能不完全相同。 Philippe Suter 的 Leon 工具使用不同的算法，可以解决递归程序上的许多正确性查询。Andrey Rybalchenko 的 ARMC 工具也可以使用线性实数算术求解 Horn 公式。它还可以建立终止条件。带有表格的 CLP 系统也应该能够以类似于 Z3 的格式解决查询（两者都使用 Horn 公式作为其输入格式）。还有许多符号模型检查求解器可以根据您的上下文使用。