支持定点SMT工具

Question

您知道除了Z3之外，还有其他支持固定点的工具吗？

Answer 1

所谓固定点，我假设你是指解决Horn子句查询。有许多工具可以解决类似性质的问题，但格式可能并不完全相同。Philippe Suter's Leon tool使用不同的算法，可以解决递归程序上的许多正确性查询。Andrey Rybalchenko的ARMC工具也使用线性实数解决Horn公式。它还可以建立终止条件。带有列表的CLP系统也应该能够以类似于Z3的格式(两者都使用Horn公式作为其输入格式)来解决查询。还有许多符号模型检查解算器，可以根据您的上下文使用。