The later uses only ASCII letters instead of Unicode characters. This
currently leads to a build issue with the Java headers on FreeBSD:
https://github.com/cvc5/cvc5/issues/11145
This PR implements one approach to exposing DSL Proof rules to the user: by making the DSL rule enum public.
Notes:
The safe toString method is not included in safe_print.h because it's generated by the RARE parser.
To test the hash and toString, for all enum values, a "last" enum value is needed. However, the current last enum value (DISTINCT_BINARY_ELIM) used in the test is generated by the RARE parser and may change in the future. Potential fixes include: adding LAST enum value, moving NONE to the end, or defining a LAST whose value is generated by the RARE parser.
This pull requests makes the enum that lists all proof rules a part of the API.
It also renames the enum from PfRule to ProofRule. It also renames some unrelated types and function names that share the PfRule name (such as DslPfRule).
This rename unfortunately touches many files since PfRule is not an uncommon type. (second to last commit)