Support for CVC5

[palmskog]

The CVC4 GitHub repo has been archived, seemingly indicating no new releases of CVC4 are planned, and by extension CVC4 may stop working completely in the future.

On the other hand CVC5 is actively developed and supported. Are there any plans to support CVC5? If not, maybe it would be useful to give some hints on what (if anything) might have to be added/changed in CoqHammer to support CVC5, in case a community member becomes interested in working on it.

[lukaszcz]

I'll take a look at CVC5 when I have some free time.

If CVC5 supports the TPTP format, then it should just be a matter of adjusting the command line invocations and maybe the output parsing. If CVC5 doesn't support TPTP, then the easiest way of integrating it with CoqHammer would be to add TPTP support to it, perhaps via a separate translator from TPTP to CVC5 input format.

In general, it is easy to integrate CoqHammer with any theorem prover which supports the TPTP format and outputs an easily parsable list of definitions used in the proof / unsat core.

[siraben]

Since v1.0.6 of cvc5, support for TPTP has been removed.