LHornSolver uses an abstraction-refinement algorithm for solving non-linear Horn clauses using only a linear Horn clause solver.
LHornSolver is written in Ciao and is interfaced with Yices SMT solver and Parma polyhedra library for handling constraints. LHornSolver uses several reusable components such as linear Horn clause solver, dimension bounded program generator, Horn clause linearisers etc.
Ciao 1.16 or newer (installed
from git repository with
Build and installation
You can automatically fetch, build, and install LHornSolver using:
ciao get github.com/bishoksan/LHornSolver
The following dependendencies (including third-party code) will be installed automatically:
- Ciao bindings for
Parma Polyhedra Library
ciao get ciao_ppl)
- Ciao bindings for
Yices SMT solver (
ciao get github.com/jfmc/ciao_yices)
- Partial evaluator Logen
(install the Ciao port with
ciao get github.com/jfmc/logen).
All code will be downloaded and built under the first directory
specified in the
CIAOPATH environment variable or
For developing it is recommended to define your own
workspace directory and clone this repository. E.g.,
export CIAOPATH=~/ciao and update your
The dependencies can be cloned manually or fetched automatically by
ciao fetch at the source directory.
lhornsolver <input file containing a set of Horn clauses>
a set of (non)-linear Horn clauses written using Prolog
h(X):- C, b1(X1),...,bn(Xn).
solved | unsolved | unknown if the clauses are solvable
| unsolvable | unknown.
Generate a standalone binary distribution
mkdir dist; cd dist
This creates a platform specific binary
directory, together with the collection of shared libraries for the
dependencies. Note: you may need to include a standalone copy of
logen binary and related files.
Programs and benchmarks for TPLP paper "Tree dimension in verification of constrained Horn clauses"
The programs are in directory TPLP-Alg1 and are run using a shell script. There is a short file README.txt in that directory giving instructions for use. The benchmarks used in that paper are found in directory bench-tplp17-kdim.