Replace dummy values in Model by abstract values

[Halbaroth]

This PR uses abstract values of the SMTLIB standard instead of printing dummy values.

Notice I use Hstring.fresh_string to produce fresh names. For instance, the test

(set-logic ALL)
(set-option :produce-models true)
(declare-datatype Pair
((pair (first Int) (second Int))))
(declare-const a Pair)
(assert (= (first a) 5))
(check-sat)
(get-model)

will produce the model

(
  (define-fun a () Pair (pair 5 (as @!k3 Int)))
)

I checked that @!... are valid identifiers in SMT-LIB.

[bclement-ocp]

I was a bit uneasy about using the function/constant name as the name for the abstract value due to the possibility of confusion (printing twice the same abstract value even though it could be different), but I don't think it can actually happen, so we might as well have the nicer models :)

[Halbaroth]

After merging my future PR that outputs exactly declared terms by the user, this cannot happen as Dolmen refuses input file in which you declare several times the same symbol.

But if a user decides to declare a term whose the name is of the form !k..., it could happen. I will check.

[bclement-ocp]

But if a user decides to declare a term whose the name is of the form !k..., it could happen. I will check.

You are right, this is another case of a mismatch between Alt-Ergo and SMT-LIB constraints — !kXXX are invalid identifiers for Alt-Ergo, but valid identifiers in SMT-LIB syntax. It is safer to always use a fresh_string then.

[bclement-ocp]

By the way we probably have a problem with quoted identifiers as well… This is unrelated to this PR however.

[bclement-ocp]

Quoted identifiers are unrelated to the PR but identifiers of the form !kXXX very much are, as you noted, and so we should use fresh_string everywhere. This should not have been merged, apologies for not removing the approval.

[bclement-ocp]

(No biggie though, we'll just make another PR to use fresh_string)