This looks like what CVC4's SyGuS component is useful for, especially since their optimization criteria is "smallest program"