Simplify internal representation of instantiated sorts (#8620)

Simplify internal representation of instantiated sorts (#8620)

Previously, sort constructors were stored as underlying operator of the NodeValue of instantiated sorts. This made it very difficult to access what sort constructor was used to construct the uninterpreted sort. Moreover, this representation made it virtually impossible to have a clean implementation of the LFSC printer for instantiated uninterpreted sorts, which requires renaming sort constructors.

This introduces a new kind INSTANTIATED_SORT_TYPE, which acts as an uninterpreted sort. The sort constructor is stored as the first child in its AST, which is analogous to parametric datatypes. It furthermore restricts SORT_TYPE to 0 children.

This is work towards having correct LFSC proof output when the input contains instantiated uninterpreted sorts.