This page contains supplementary material for the following paper
- E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Satisfiability of Constrained Horn Clauses on Algebraic Data Types: A Transformation-based Approach
Submitted to Journal of Logic and Computation.
Abstract. We address the problem of checking the satisfiability of Constrained Horn Clauses (CHCs) defined on Algebraic Data Types (ADTs), such as lists and trees. We propose a new technique for transforming CHCs defined on ADTs into CHCs where the arguments of the pred- icates have only basic types, such as integers and booleans. Thus, our technique avoids, during satisfiability checking, the explicit use of proof rules based on induction over the ADTs. The main extension over previous techniques for ADT removal is a new transformation rule, called differential replacement, which allows us to introduce auxiliary predicates, whose definitions correspond to lemmas that are used when making inductive proofs. We present an algorithm that performs the automatic removal of ADTs by applying the new rule, together with the traditional folding/unfolding rules. We prove that, under suitable hypotheses, the set of the transformed clauses is satisfiable if and only if so is the set of the original clauses. By an experimental evaluation, we show that the use of the new rule significantly improves the effectiveness of ADT removal. We also show that our approach is competitive with respect to a state-of-the-art tool that extends the CVC4 solver with the use of inductive rules.
This paper is an improved, extended version of a paper the authors have presented at the International Joint Conference on Automated Reasoning (IJCAR 2020) and also at the 35th Italian Conference on Computational Logic 2020 (CILC 2020).
Besides detailed proofs and examples, the main, new contribution consists in addressing the problem of the completeness of the transformations. In our previous version, we proved only a soundness property, ensuring that if the transformed clauses are satisfiable, then so are the original clauses. In this paper, we identify some sufficient conditions, related to the functionality of the difference predicates introduced by the transformation algorithm R, which guarantee the converse of soundness, that is, if the transformed clauses are unsatisfiable, then so are the original ones. We have also extended our implementation and our benchmark, and we have shown that our sufficient conditions can indeed be checked in many interesting, non trivial examples.
The page for the supplementary material for the conference version of the paper can be accessed here.
Benchmark suite and experiments
Our benchmark suite consists of 251 verification problems over inductively defined data structures, such as lists, queues, heaps, and trees. 168 of these problems consider properties that do hold (valid properties) and the remaining 83 consider properties that do not hold (invalid properties). The 168 problems have been adapted from
the benchmark suite considered by Reynolds and Kuncak, and originate from benchmarks used by various theorem provers, such as CLAM, HipSpec, IsaPlanner, and Leon. Invalid properties have been obtained from valid properties by either negating the valid properties or introducing suitable bugs in the predicates on which the properties depend.
You can browse
Alternatively, you can download an archive with
all the problems.
the CHC problems in SMT-LIB2 format
before the application of the ADT removal algorithm
(also in Prolog format)
the CHC problems in SMT-LIB2 format obtained
the application of the ADT removal algorithm
the original problems
by Reynolds and Kuncak using the dtt encoding.
A spreadsheet file with more detailed experimental results is available, too.
Instructions for running the tool on Linux 64bit.
On Ubuntu 16.04 this can be done by running the following commands.
sudo add-apt-repository ppa:swi-prolog/stable
sudo apt-get update
sudo apt-get install swi-prolog
sudo apt-get install swi-prolog=8.0.3-0-xenialppa2
We've tested ADTRem using
Make sure that the eld command is on your PATH.
Download the ADTRem tool.
Extract the archive and change directory by typing
tar xvzf ADTRem-JLC-linux_x86_64.tar.gz
Run ADTRem on a CHC problem in Prolog format