Hermes is a termination and complexity analyzer for innermost first-order rewriting.
Currently, v1.0.0, it implements techniques from the paper https://doi.org/10.4204/EPTCS.376.5 which describes the complexity analysis of such systems in the framework of tuple interpretations.
We use opam to build Hermes. See opam installation instruction page for installation instructions for your system.
Here's the package dependency list,
which can be installed using opam
.
- ocaml, v4.14.0 or higher, the ocaml compiler.
- dune v3.5.0 or higher, the building tool.
- menhir v20230608 or higher, the parser generator.
- z3 v4.12.2-1 or higher, the SMT solver.
- Note: z3
opam
package will require the following system dependencies: libgmp and python3. Make sure those are installed on your system before proceeding.
- Note: z3
We recommend creating a fresh opam switch
with OCaml v4.14.1 or higher.
opam switch create hermes 4.14.1
eval $(opam env)
After creating the Hermes switch
, we switch to it using:
opam switch hermes
opam install dune menhir z3
With all the above dependencies installed in your opam switch
,
run the following from the root of the repository:
dune build
This will use dune
to build the source code.
We recommend users install the binaries for Hermes locally in their system.
This can be done via the command:
dune install
This will install Hermes locally on your system as an opam package.
Hermes then is called using the name hermes
in the command line.
Hermes receives as input a file describing the term rewriting system to be analyzed.
This version, v1.0.0, only accepts file in the onijn
format.
The file format is explained in the API.
We assume Hermes' binaries are installed locally. Then simply run:
hermes /path/to/input/input/file.onijn
The output is a human-readable description of the tuple interpretation found (if any).
Hermes can also be run in isolation from a docker image builder provided. We assume you have docker properly installed in your system. From the root of this repository simply run:
# Build the Dockerfile.
docker build -t hermes_img .
# Run the docker image interactively
docker run -i -it hermes_img:latest