Conditional flyweight pattern for terms

[marcoeilers]

This PR implements the flyweight pattern for Silicon terms in a way that can be turned on or off (depending on the value of Verifier.config.useFlyweight).
The motivation is that the flyweight pattern is required to use the Z3 API in a fast way (since translating the same term multiple times slows down the Z3 API massively for large examples with many terms, so they need to be cached, which is too slow unless flyweight is used) but using the flyweight pattern slows down Silicon when using Z3 via StdIO. Thus, Verifier.config.useFlyweight is set to true nly if Z3 is used via its API.

The PR borrows code and ideas from the flyweight pattern implementation by Fabian Bösiger, but does not use Scala macros to avoid IDE issues.

Instead, it uses

• a trait ConditionalFlyweight that is implemented by all Term classes, which defines equality and hashCode either based on reference equality (if Verifier.config.useFlyweight is set) or otherwise on the values of a field equalityDefiningMembers, similar to the existing StructuralEquality trait.
• a trait GeneralCondFlyweightFactory (and some more specific subtraits), to be implemented by companion objects of all Term classes, which contains a TrieMap to cache all existing instances of the class, and defines functionality for conditionally creating new instances or first checking for existing ones in the cache, again based on the value of Verifier.config.useFlyweight.

(Also, the PR fixes parameter handling in the Z3 API.)

[marcoeilers]

I hereby request a review from @mschwerhoff :)

[mschwerhoff]

A few minor comments, but no objections to merging this PR.

[mschwerhoff]

I hereby request a review from @mschwerhoff :)

Ask, and it shall be given to you 😇