Avoid linear scan in isKnownToBeTrue

[fpoli]

From a sampled profiling of Silicon, the following line is reported to be in the stacktrace of 5.5% of the samples:

https://github.com/viperproject/silicon/blob/c8d4c9677d956604ec0d580e6d44f92c3c00b7ef/src/main/scala/decider/Decider.scala#L228

It's a linear search over a list of terms, which could be optimized by using a set type (e.g. with an additional assumptionsSet field). However, I'm not sure whether Viper terms already implement the hashCode method properly.

[mschwerhoff]

AFAIK, Silicon's terms implement hashCode and equals as expected, so using a set here should work. Adding a second, set-typed collection of terms incurs additional bookkeeping costs, though (add/remove terms to/from two collections), and might not be the best choice here. Any solution attempt should be carefully benchmarked.

On a related note: a long time ago, I've experimented with memoizing term factories, since this allows to compare terms, e.g. when accessing collections, by identity rather than equality. The latter is particularly costly for deep terms (and ASTs) because we use structural equality everywhere (default for case classes). The experiment was inconclusive, if I remember correctly, but since our test suite back then consisted of quickly verifying examples only, this might not be the case any more.