z3 - 线性整数算术中量词消除的工具

Question

除了 Z3 之外，是否还有其他可用（并且仍然受支持）的 SMT 工具可以为线性整数算术执行量词消除？

谢谢。

Answer 1

你可以试试Philipp Rümmer 的Princess。它支持量词消除并得到积极维护。