Difference between term types and datatypes

[sanpoyur]

Recently I started to continue the sketch-based solver project, and I noticed the newly added datatypes feature.

Initially I was a little confused, but I gradually sensed that there are some subtle differences between program terms like E and semantic objects like List.

Furthermore, here is an example of synthesizing max2 in SyGuS (max2-sygus.sl) using datatypes as term types. CVC5 is able to yield the following result:

However, the SemGuS parser is not able to parse it: