如何检查两个谓词是否相等？

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