z3 - 使用 SMT 简化术语

Question

我一直在使用 Z3 来检查是否可以满足条款。但除此之外，我需要简化人类消费的术语，例如当 n 是 Int 时，将 And(n>4 , n != 5) 简化为 n > 5。有人知道如何在 Z3 中或通过其他工具执行此操作吗？

Answer 1

您可能已经注意到 Z3 在 API 上公开了一个简化器，您也可以从 SMT-LIB 使用它。来自rise4fun.com/z3 和rise4fun.com/z3py 的Z3 教程给出了几个简化器的例子。但是，简化器不会尝试任何正常的形式转换，因此它不太可能产生您暗示想要的样式的结果。特别是它不会将合取 And(n > 4, n != 5) 简化为 n > 5。

Answer 2

可能的答案：

n = Int('n')

antecedent = And(n >4, n != 5)
claim1 = n > 5

prove(Implies(antecedent, claim1))

输出：

proved