Make smt-lib2 printer not drop (as ...) on applied symbols

[hra687261]

Before (as ...) was only printed for polymorphic symbols with a 0-arity, but in some cases its needed for polymorphic symbols with arguments, notably when the type variable appears in the return type and not in the types of the arguments. Here for example:

(declare-fun f (par (t1) (Int) t1))
(declare-fun p (par (t2) (t2) Bool))
(assert (par (t3) (forall ((_x t3)) (p ((as f t3) 0)))))

Where the type-checking does not work if we don't manually bind cast the return type of f (t1) to t3.

[Gbury]

Thanks, that's a very nice fix !

While we're at it, I was wondering whether we should use the same (or a similar system) for other places where we need to print type annotations. More specifically, when applying polymorphic maps (i.e. encodings of higher-order functions), there is some logic to add an as type annotation when a polymorphic map is applied partially, and it seems like that check could miss some cases and could maybe be rewritten using the same kind of logic of whether the provided arguments are enough to fully decide the type of the application ?

[hra687261]

Indeed, so I tried to do something similar for the HO case in 568ff69
But in the implementation it seemed that it was when HO maps where fully applied that the "as" was skipped (when the symbol is applied directly without the "@"), so now a similar check is done for the HO type to determine whether an "as" is needed or not.
When maps are partially applied on the other hand, it seems that the printer simply passes the application symbol and its arguments to the standard printer for applications which takes care of determining if an "as" is needed or not.

[hra687261]

I also noticed that type variables are not bound when printing polymorphic function definitions in the psmt2 format, fixed it in abf073f