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:
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
Eand semantic objects likeList.Furthermore, here is an example of synthesizing
max2in 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: