使用SMT簡化術語

Question

我一直在使用Z3來檢查是否可以滿足條件。但是，另外，我需要簡化人類消費的術語，例如當n是一個Int時，簡化和（n> 4，n！= 5）到n> 5。劑量任何人知道如何在Z3或通過其他工具做到這一點？

Answer 1

正如您可能已經注意到的那樣，Z3在API上有一個簡化器，您也可以在SMT-LIB中使用它。來自rise4fun.com/z3和rise4fun.com/z3py的Z3教程給出了幾個簡化器的例子。但是，簡化器不會嘗試任何正常的表單轉換，所以它不可能產生您想要的樣式的結果。特別是它不簡化結合並以N> 5

Answer 2

可能的答案（N> 4，N = 5！）：

n = Int('n') 

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

prove(Implies(antecedent, claim1)) 

輸出：

proved