How to check if two predicates are equivalent?

Question

I have two different inplementations for certain predicate and I want to check if both of them return the same instance, how can I achive that?

Thanks.

Answer 1

I'd assert that the two predicates are always either both true or both false, and check the assertion.

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

If the predicates take arguments, then of course you need to check them on the same arguments:

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