如何檢查兩個謂詞是否相等？

Question

對於某些謂詞，我有兩種不同的實現方式，我想檢查它們是否都返回相同的實例，我如何執行此操作？

謝謝。

Answer 1

我斷言這兩個謂詞總是或者都是真的，或者都是假的，並檢查斷言。

pred P1 { ... } 
pred P2 { ... } 
assert P1_equiv_P2 { P1 iff P2 } 
check P1_equiv_P2 

如果謂詞獲取參數，那麼你當然需要檢查他們在相同的參數：

pred P1[x : univ] { ... } 
pred P2[x : univ] { ... } 
assert P1_equiv_P2 { all x : univ | P1[x] iff P2[x] } 
check P1_equiv_P2