ADTRem (IJCAR 2020)

Note that this is the page for the IJCAR 2020 version of the paper.
The page for the revised and extended version of the paper can be accessed here.

This page contains supplementary material for the following paper

E. De Angelis, F. Fioravanti, A. Pettorossi, M. Proietti.
Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates.
10th International Joint Conference on Automated Reasoning (IJCAR 2020) Paris, France, June 29-July 5, 2020.

Abstract. We address the problem of proving the satisfiability of Constrained Horn Clauses (CHCs) with Algebraic Data Types (ADTs), such as lists and trees. We propose a technique that transforms sets of CHCs with ADTs into CHCs where predicates are defined over basic types, such as integers and booleans, only. We show that if the set of transformed clauses is satisfiable, then so is the set of the original clauses. Thus, our technique avoids the explicit use of inductive proof rules during satisfiability proofs. The main extension over previous techniques is that the transformation automatically generates new predicates corresponding to the lemmas that are often needed by inductive proofs. By an experimental evaluation, we show that our approach is competitive with respect to techniques that extend CHC solving with induction.

Benchmark suite and experiments

Our benchmark suite consists of 169 verification problems, over inductively defined data structures, such as lists, queues, heaps, and trees, which have been adapted from the benchmark suite considered by Reynolds and Kuncak in their VMCAI'15 paper.

These verification problems come from benchmarks used by various automated theorem provers and satisfiability checkers, and in particular:
(i) 53 problems from CLAM
(ii) 11 from HipSpec
(iii) 63 from IsaPlanner
(iv) 42 from Leon.

You can browse

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 after the application of the ADT removal algorithm
the original problems by Reynolds and Kuncak using the dtt encoding.

Alternatively, you can download an archive with all the problems.

A spreadsheet file with more detailed experimental results is available, too.

ADTRem tool

Instructions for running the tool on Linux 64bit.

Install SWI-Prolog. 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
             or
sudo apt-get install swi-prolog=8.0.3-0-xenialppa2 

export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/usr/lib/swi-prolog/lib/x86_64-linux/

Install Eldarica. We've tested ADTRem using Eldarica v2.0.1. Make sure that the eld command is on your PATH.

Alternatively, you can use Z3. For best results, however, you should use the CHC-COMP version of Z3-Spacer , make sure that z3 is on your PATH and that is a wrapper around the actual z3 binary invoking it using the parameters of the default configuration used in the CHC-COMP.
Download the ADTRem tool. Extract the archive and change directory by typing
```
tar xvzf ADTRem-linux_x86_64.tar.gz 
cd ADTRem-linux_x86_64
```

Run ADTRem on a CHC problem in Prolog format by typing

./ADTRem  <problem.pl>  eldarica 
             or
./ADTRem  <problem.pl>  z3

Run ADTRem on all CHC problems included in a directory by running

./run-all <directory>  eldarica
             or
./run-all <directory>  z3