Sound trigger-independent function encoding

[marcoeilers]

This PR solves the unsoundness from issue #376 and #369.
The solution (which Gaurav and I worked out based on earlier discussions by other people, and which Gaurav is in the process of implementing for Carbon) is, for every heap-dependent function with a precondition, to use a new boolean uninterpreted function on the SMT-level that represents whether the function's precondition holds, and make definitional and postcondition axioms conditional on that new function being true.
Then, we emit the information that a function's precondition holds in different places:

• When Silicon evaluates a function call, after checking that the precondition holds, it assumes that the precondition function holds for the given arguments and in the current state.
• If function f calls function g, then, after checking the well-definedness of f, we emit an additional axiom that states that, if f's precondition holds, then g's precondition will also hold when f calls g.
• When asserting quantifiers, after checking that they are well-defined, we assert that the asserted body holds under the assumption that for all function applications in its body, their respective preconditions hold.

The PreconditionPropagationTransformer (I'm very open to suggestions for better names and better places to put this code) takes a term that may contain applications of heap-dependent functions, and returns a term stating that the preconditions of all such function applications hold if the conditions under which they are called hold. That is, for a term t, after checking that it is well-defined, one may assume the transformed version of t.

[mschwerhoff]

Generally LGTM. I left a few comments, only the one about documentation would entail some work.

[mschwerhoff]

Assuming the transformer propagates preconditions, how about PreconditionPropagatingTransformer?

[marcoeilers]

After writing down what it actually does, I settled on FunctionPreconditionTransformer. While it doesn't transform function preconditions, it transforms terms to state that all function preconditions are fulfilled.