使用SMT简化术语

Question

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

Answer 1

正如您可能已经注意到的，Z3有一个通过API公开的简化程序，您也可以在SMT-LIB中使用它。rise4fun.com/z3和rise4fun.com/z3py上的Z3教程提供了几个简化程序的示例。但是，简化程序不会尝试任何范式转换，因此它不太可能产生您所暗示的所需样式的结果。特别是，它没有将合取和(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