search

leoprover / Leo-III

An Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
http://inf.fu-berlin.de/~lex/leo3
BSD 3-Clause "New" or "Revised" License
41 stars 10 forks source link

HashCode in Clause not Matching Equals #38

Closed Ryugoron closed 7 years ago

Ryugoron commented 7 years ago

The function hashCode() in Clause is not matchin the equals function.

In more detail: equal is defined as mutual inclusion of the literals, whereas hashCode is defined as a fold with XOR.

As long as the clause is always in the simplified form, this is no problem, but since a Clause is a MultiSet of Literals they do not match always

lex-lex commented 7 years ago

Fixed in 79102151b05d2f3b46dd63e1a273ae93bf9edf51