This updates the proof output of cvc5 to the new Eunoia syntax when
applicable.
It furthermore renames the signature files *.smt3 to *.eo and moves them
to the new appropriate directories.
The ethos version is update to one that generates a binary named ethos.
Further PRs will update the internal namings e.g. src/proofs/alf ->
src/proofs/eo, although this is lower priority.
This is the first step towards renaming our default proof format to
`cpc` and renaming the proof checker `alfc` to `ethos`.
The following things are TODO and will be done shortly after this PR is
merged:
- [external] Update alfc repo link to ethos
- [external] Update alfc repo to naming conventions of Eunoia, update
binary name.
- Update signatures *.smt3 to *.eo, directories in `proof/`
- Update `src/proof/alf` to `src/proof/eo`.
- Update cvc5 proof support to match new Eunoia format.
---------
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
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)
This PR initializes some documentation for our proofs. It adds some almost empty files and makes sure that we can show documentation for the PfRule enum.
