ReTHFL

A nuHFL(Z) (aka higher-order CHC) solver based on refinement types.

Install and Build

Creating an opam switch

We use opam for install and build.

If you already have opam, create a new switch for ReTHFL:

opam switch create rethfl 4.14.1
eval $(opam env)

Even if you have a switch for OCaml 4.14.1 we recommend you to create a new switch to avoid dependency hell.

If this is your first time using opam, then initialize opam as follows before running the above commands:

opam init

Install

After you've set up an opam swtich, running the following command will install rethfl:

opam pin add rethfl https://github.com/hopv/rethfl.git#master

Manual build

First, clone this repository

git clone git@github.com:hopv/rethfl.git
cd rethfl

and then, let opam install all packages that are needed

opam install --deps-only .

Once the dependent packages have been installed, ReTHFL can be compiled by the following command:

dune build

An alternative way to obtain a reproducible build is to use the lock file.

git clone git@github.com:hopv/rethfl.git
cd rethfl
opam switch create . --deps-only --locked
dune build

(Note that this creates an opam switch.)

External Dependencies

ReTHFL uses (extended) CHC solvers for constraint solving. For most cases, the constraints are of the form of CHCs, so having CHC solvers such as HoIce or Z3 (Spacer) installed is enough. The default backend is HoICE. For some instances (and if the users specify to do so), ReTHFL generates constraints of the form of extended CHC, and to handle these cases PCSat is needed. (The PCSat backend is not actively maintained, so we don't recommend users to use it.) Another optional dependency is Eldarica, which is needed for counterexample generation.

To summarize, here is the list of external dependencies

HoIce
(Optional) Z3 (Spacer)
(Optional) Eldarica
(Optional; Unmaintained) PCSat

How to Run

rethfl <filename>

See rethfl --help for more information.

If you want to run a manually built executable, run the following command instead:

dune exec rethfl -- <filename>

hopv / rethfl