Andrew Reynolds 6c2dc6e78f Add option to make regular expressions first class (#12049) ...

This adds an expert option to allow regular expressions to appear
anywhere in constraints, including in datatype fields, or as arguments
to uninterpreted functions.

This is required for reasoning about the correctness of CPC for proof
rules involving regular expressions.

2025-08-23 16:48:07 +00:00

41 KiB

Raw Permalink Blame History

View Raw