支持定點的SMT工具

Question

您是否知道除Z3以外的其他任何支持定點的smt工具？

Answer 1

通過不動點，我相信你的意思是求解霍恩子句的查詢。有許多工具可以解決類似性質的問題，但可能並不具有完全相同的格式。 Philippe Suter's Leon tool使用不同的算法，可以解決遞歸程序中的許多正確性查詢。 Andrey Rybalchenko的ARMC工具也使用線性實數算法解決了Horn公式。它也可以建立終止條件。帶有製表功能的CLP系統也應該能夠以與Z3類似的格式（都使用Horn公式作爲輸入格式）來解決查詢問題。還有很多符號模型檢查解算器可以根據您的上下文使用。