Adding a SMT-LIB compliant printer for Expr

We plan to use expression from `Expr` to store model values but we
haven't appropriate printer for it in the SMT-LIB format. Indeed, the current
SMT-LIB printer of `Expr` is wrong, both on formula and simple symbols as
rational numbers or bitvector literals.

This commit changes the SMT-LIB printer of `Expr` in order to always
print SMT-LIB format.

The new SMT-LIB printer have only two limitations:
1. it doesn't print the triggers of lemmas when the verbose flag is up
   because there is no appropriate syntax in the SMT-LIB standard.
2. it doesn't print the detail of the semantic trigger `In`.

Notice that multi-trigger are now printed as DNF formulae.

After discussion, we decide to keep the actual printer of `Symbols` as
we need it for debugging messages. Instead I split it in several
printers in module's implementation and I expose a new printer
`pp_operator` for sake of code factorisation.

Notice that printing names and literal constants should be sufficient to
output models but for sake of completeness, this commit refactors
completely the SMT-LIB printer of `Expr`.

I also clean up the code of both `Symbols` and `Expr` printers in the
following way:
- I use everywhere `Fmt` and in particular `Fmt.list` and `Fmt.iter`.
- I rename some functions but I keep the previous API. I just add a new
  function `pp_operator` to the signature of `Symbols`.
- I remove some useless test with `Options.get_output_smtlib`.

src/lib/frontend/models.ml

@@ -312,10 +312,19 @@ module SmtlibCounterExample = struct
     | [Ty.Trecord _r, _arg] -> begin
         match xs_values with
         | [record_name,_] ->
+          (* HOTFIX: this fix is temporary. The current implementation of
+             model generation for records relies on string representants,
+             which means the printer for access symbols has to agree with
+             the name of the field in the type trecord. As the printer
+             [Symbols.print] will always output AE native format, this
+             doesn't agree when the output format is SMT-LIB. But the
+             printer of expression will output the right string if we don't
+             give the arguments of the field. *)
+          let access = Fmt.str "%a" Expr.print (Expr.mk_term f [] ty) in
           add_records_destr
             records
             (asprintf "%a" Expr.print record_name)
-            (Sy.to_string f)
+            access
             rep
         | [] | _ -> records
       end