A Haskell implementation of the algorithm described in "Higher-Order Constrained Horn Clauses for Verification"(Cathcart Burn, Ramsey, Ong). See section 5.4 for details. Transforms a higher-order Horn clause problem into a first order one. A web demo is available at http://mjolnir.cs.ox.ac.uk/horus/.
The project can be built with the tools cabal or stack:
stack install
(this will create the executables horus and thoth on PATH)
or
cabal configure
cabal install --bindir=.
Z3, which can be obtained from https://github.com/Z3Prover/z3/releases is needed for some test cases.
horus inputFile outputFile is the easiest way to call the program.
horus -h gives more information about command line options.
For an example of a complete input file, see tests/test1.inp. Each new formula or type declaration must begin on a new line and not start with whitespace. Lines starting with whitespace are assumed to be continuations of the previous line, allowing multi-line definitions.
The environment section must consist of a list of variable names with a correct sort for each. The last line may end in a semicolon.
The program section must consist of a list of Horn clauses with the last terminated by a semicolon.
There must be at least one clause where the head begins with X for each variable X in the environment.
The last line may end in a semicolon.
The goal section must consist of a single formula. The line may end in a semicolon.
Variables should not be of the form x_<number> as this could interfere with the fresh variables generated by the program.
The program accepts unicode input, but unicode symbols may be used interchangeably with the following ascii versions.
^ ∧
\/ ∨
=> ⇒
A ∀
E ∃
<=> ⇔
<= ≤
>= ≥
- −
-> →
/= ≠
Comments begin with # and end at the end of a line.
The output consists of a list of first order Horn clauses of with heads of the form X a b c.
This represents a conjunction of clauses where the variables a, b and c are bound under universal quantifiers.
There is another line giving a first order goal clause.
The -z option outputs in the SMT-LIB2 format with the extensions described in http://rise4fun.com/Z3/tutorial/fixedpoints.
The -x option outputs in unextended SMT-LIB2 format which works with all tested versions of Z3. It has not been tested with any SMT-LIB solvers other than Z3 (those that have been tried don't have the required fixpoint engine). Z3 version 4.4.2 produces simpler output with -z than with -x.
Tests are in the form of bash scripts which should be called from the base directory. If stack build has been used but not stack install then stack exec may be used e.g. stack exec tests/test.sh.
tests/test.sh runs a small number of simple tests (2 of which require z3).
git diff is used to check the output. It will produce no output if it runs without errors (beyond differences between versions of z3).
tests/mochi.sh creates or modifies the file tests/allmochi.out. This demonstrates the cases where we can solve the first order problem arising from the transformation and agree with those obtained by mochi (amax-e is an exception since the original code is identical to amax).
Now also includes a program to translate ML-like or Haskell-like programs with assertions into a system of higher-order Horn clauses.