This page contains additional information about the experimental results reported in the paper, "An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types."

The test cases used can be downloaded here or browsed here. The test cases were built with a Windows program written by Igor Shikanian (one of the authors of the paper). You can download it here.

The test cases are all generated over the following recursive data type (given in CVC Lite syntax): 

DATATYPE
  nat = succ(pred : nat) | zero,
  list = cons(car : tree, cdr : list) | null,
  tree = node(children : list) | leaf(data : nat)
END;
The test cases are divided into two categories, typed and untyped. Untyped cases include all possible terms. Typed cases only include terms in which selectors are always applied to terms constructed with the matching constructor. The reason for this separation is that the first class of cases test the decision procedure in its fullest generality while the second class of cases are more like what would be expected in a real application. Interestingly, there does not seem to be a noticeable performance difference between the two classes. Within each class, test cases are divided by the maximum number of variables of each type. Cases were generated with (max) 1,2,3,5, and 10 variables of each type. Within each variable category, the number of literals tested ranged from 2 to 9, with 100 cases for each literal count.

A version of CVC Lite that supports data types with both eager and lazy splitting can be downloaded here. To run CVC Lite on any of the test cases, use the following syntax: 

cvcl -tcc filename
or 
cvcl -tcc +dt-lazy filename
The first runs the algorithm presented in the paper (eager splitting). The second runs the algorithm referred to as the lazy splitting algorithm (note that the "-tcc" switch disables type correctness condition checking: running with tcc's enabled adds an additional check which results in an error for many of the "untyped" tests and takes extra time for the "typed" tests). Though not reported here, results with tcc's enabled on the typed tests are similar to those reported when tcc's are disabled. To obtain statistics including number of splits, add the "+stats" flag.

The results of running CVC Lite on the test cases can be downloaded here and browsed here. A program that can be used to generate reports on the results is here. The report generator takes four command-line arguments: the name of the two directories to compare, the low number of splitters, and the high number of splitters. For example, to compare the performance of test cases whose worst-case number of splitters were between 20 and 30 (inclusive), use the following command: 

reports results/results.lazy/ results/results.eager/ 20 30
One additional test case of interest is the one discussed in Section 4 of the paper. It can be found here. If you have additional questions about these test results, feel free to contact barrett@cs.nyu.edu.