Replace fresh terms by abstract values in all subterms

[Halbaroth]

This PR fixes the issue #1270. More precisely,

1. Add a new argument to the function X.to_model_term. The purpose of to_model_term is to generate a model term from constant semantic values. Unfortunately, these model terms are not exactly the model values of the SMT-LIB standard because they can contain fresh terms. The new argument of X.to_model_term is a function of type E.t -> E.t that is used to create abstract values from fresh terms. A cache is hidden in the closure of this function to prevent from duplicating abstract values for the
   same fresh terms.
2. Improve and update some comments.
3. Remove the term_values field in Models. This field was only used to cache the result of model_repr_of_term in Uf.
   I replaced it by a local cache in the closure of extract_concrete_model.

Now the output of the example of #1270 is:

unknown
(
  (define-fun q ((arg_0 t)) Int
   (ite (= arg_0 (as @a2 t)) 1 (ite (= arg_0 (as @a4 t)) 0 (- 1))))
  (define-fun o ((arg_0 Int)) t
   (ite (= arg_0 1) (as @a3 t) (ite (= arg_0 0) (as @a5 t) (as @a7 t))))
) 

[Halbaroth]

I realized that the solution we found for #1213 should fix #1270 too without modifying the signature of any modules. I tested it on
the file of Matteo, it works! I will finish your patch. I keep this PR open.