A nuHFL(Z) (aka higher-order CHC) solver based on refinement types.
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 initAfter you've set up an opam swtich, running the following command will install rethfl:
opam pin add rethfl https://github.com/hopv/rethfl.git#masterFirst, clone this repository
git clone git@github.com:hopv/rethfl.git
cd rethfland 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 buildAn 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.)
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
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>