search

lukaszcz / coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Other
210 stars 31 forks source link

Support for CVC5 #171

Open palmskog opened 8 months ago

palmskog commented 8 months ago

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 commented 8 months ago

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.