vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
282 stars 49 forks source link

GREATER_EQ and LESS_EQ have to go #582

Closed mezpusz closed 1 month ago

mezpusz commented 1 month ago

I have finally got annoyed enough to remove the two enum values that annoyed many Vampire developers before me (based on comments in the code).

There were probably earlier Ordering implementations which used these values but now nothing returns them on the term level, and literal-level comparisons like Ordering_Equality only used them when they were returned from the term level. Removing them gives a cleaner code and will hopefully allow more optimisations down the road.

I know only of ArgumentOrderVals which relies on the exact layout of Ordering, please let me know if there are more of these somewhere.