Proving with Hets¶
Online¶
In order to use the online version run gavel with the following environment variables:
- HETS_HOST: rest.hets.eu
- HETS_PORT: 80
following options parameters:
eprover –hets <problem_path>
Offline¶
Follow the instructions in the “hets documentation”:https://github.com/spechub/Hets and start hets –server or run “the docker container”:https://github.com/spechub/Hets/wiki/How-to-use-the-Hets-Docker-Container (the mount option is not necessary as gavel uses the rest interface instead of shared files).
- HETS_HOST: localhost
- HETS_PORT: The port your docker container is forwarding
following options parameters:
eprover –hets <problem_path>
Python interface¶
Hets is just a layer around a number of provers. The latest version of gavel only supports EProver. In order to use any Proverinterface with hets, you have to pass it to the constructor:
from gavel.prover.hets.interface import HetsEngine, HetsSession, HetsProve
from gavel.prover.eprover.interface import EProverInterface
internal_prover = EProverInterface()
# Or any other subclass or anything that quacks like BaseProverInterface
hets_engine = HetsEngine()
hets_session = HetsSession(hets_engine)
prover = HetsProve(internal_prover, hets_session)