#1258 Updated hash code of `Pair`

Closes #1258 (closed).

This is a suggestion for an update of Pair#hashCode. Note that coming up with a good way to combine hash values is not easy. The proposal in this MR is based on the hash code of java.awt.geom.Point2D. But I see that it isn't perfect, for example when used with Pair<Integer, Integer> with small integers. Then bits will probably have a lot of leading binary 0-s. So you can also get quite some hash collisions still.

I also tried the 'multiply and XOR' mix method that's proposed by rapidhash and is also used in JavaDD at the moment:

@Override
public int hashCode() {
  long leftHash = Objects.hashCode(left);
  long rightHash = Objects.hashCode(right);

  long low = leftHash * rightHash;
  long high = Math.multiplyHigh(leftHash, rightHash) + ((leftHash >> 63) & rightHash) + ((rightHash >> 63) & leftHash);

  leftHash ^= low;
  rightHash ^= high;

  return (int)(low ^ high);
}

That method seems to perform better for creating the graph for variable ordering than the one proposed in this MR. Then the times it took to populate graphEdges became:

• First call to VarOrderHelper#createGraph: 4076.6568ms
• Second call to VarOrderHelper#createGraph: 4230.3638ms
• Third call to VarOrderHelper#createGraph: 4151.4202ms
• Fourth call to VarOrderHelper#createGraph: 3776.8559ms

There are probably many other ways of combining hash functions, some of which may be better than others in certain situations. The suggestion in this MR is a proposal for one of these, which seems to perform better on a concrete case.

---

End-user visible changes: Improves the performance of CIF data-based synthesis and CIF controller properties checker (for BDD-based checks) in case BDD variable ordering for models with many linearized edges and variable relations.