Case splits on enum domains

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo

https://alt-ergo.ocamlpro.com/

Other

131 stars 33 forks source link

Case splits on enum domains #1138

Closed Halbaroth closed 3 months ago

Halbaroth commented 4 months ago

This PR changes the way we perform split on ADT domains. Before this PR, after asserting formulas, we can split on ADT semantic values of enum type, that is all its constructors have no payload. After this patch, we can split on an ADT domain if all its constructors are enum constructors, that is they have no payload.