hoice is an ICE-based Constrained Horn Clause (CHC) solver.
Given some CHCs mentioning some undefined predicates, hoice infers definitions for these predicate
that respect all CHCs or prove none exist. Hoice supports the
Real sorts. It
also supports user-defined ADTs, although it is still in an experimental stage.
Hoice generally uses the latest rust features available. Make sure the rust ecosystem is up to date by running the following command before building hoice.
rustup update stable
Installing hoice with
cargo install --git https://github.com/hopv/hoice
To build hoice manually, clone this repository,
cd in the directory and run
cargo build --release
The binary file will be in
To get the fastest version, compile hoice with
cargo build --release --features "bench"
Note that this disables some features such as verbose output, profiling...
hoice relies on the z3 SMT-solver. Make sure you have a relatively recent version of the z3 binary in your path.
Consult the wiki for a description of
- (mutually recursive) ADTs
- user-specified qualifiers through
Checking the result
hoice can check its own results. The code performing this feature is completely separated from the code doing the actual inference so that the check is meaningful.
In fact, the code for this is almost implemented as some string substitutions followed by an SMT query for each clause of the problem.
For now, this feature is completely off-line. Put
hoice's result in a file, for instance with
hoice <horn_clause_file> | tee <output_file>
and use the
--check option to verify that the predicates inferred verify all the horn clauses:
hoice --check <output_file> <horn_clause_file>
This repository hosts the latest stable version of hoice. See the main developer's fork for a cutting edge, although unstable, version.
We welcome any help, please the contribution guidelines if you are not familiar with the github pull request workflow to get started.