Simplify approach for collapsed selectors over non-closed enumerable types (#5223)

This simplifies the approach for wrongly-applied selectors whose range type involves e.g. uninterpreted sorts. These cases are particularly tricky since uninterpreted constants should never appear in facts or lemmas.

Previously, the rewriter had special cases for either making a ground term or value, and a purify step was used to eliminate the occurrences of uninterpreted sorts afterwards.

This PR leverages mkGroundTerm in this inference instead, and makes the rewriter uniformly use mkGroundValue.

This also required making the type enumerator for datatypes more uniform. In particular, we require that the first value enumerated by the type enumerator is of the same shape as the term required by mkGroundTerm, or else debug-check-model will fail. This is due to the fact that now the inference for wrongly applied selectors uses terms while the rewriter uses values. The type enumerator is updated so that recursive codatatypes also first take mkGroundValue as the zero term, when they are well-founded. Previously this was skipped since the codatatype enumerator uses a different algorithm for computing its ground terms.

This is in preparation for further work on optimizations and proofs for datatypes.

0 files changed, 0 insertions, 0 deletions