Hash Calculations for Domains

[ArquintL]

The hash of a domain should not depend on the precise ordering of its domain functions and domain axioms. This is important when performing cache lookups as a cached verification result can still safely be used even if the some domain functions are in a slightly different order

[JonasAlaif]

Looks good to me, should we add a CI test that checks that the hash of two reordered domains stays the same?

[ArquintL]

How easy would this be? I already have a unit test in ViperServer that checks whether verifying two input programs that only differ in the order of domain functions and/or axioms results in the latter one being cached

[mschwerhoff]

As easy as adding another unit test to Silver:

• all: https://github.com/viperproject/silver/tree/master/src/test/scala
• e.g.: https://github.com/viperproject/silver/blob/master/src/test/scala/AstPositionsTests.scala

Since hashes are computed over the Silver AST, the Silver repo seems a more natural location for such tests than the ViperServer repo. But I'd keep the ViperServer test nonetheless, it probably has more of an end-to-end test flavour.