Tech Report CS-92-49

Groundness Analysis for Prolog: Implementation and Evaluation of the Domain Prop

Baudouin Le Charlier and Pascal Van Hentenryck

October 1992

Abstract:

The domain Prop is a conceptually simple and elegant abstract domain to compute groundness information for Prolog programs. In particular, abstract substitutions are represented by Boolean functions built using and, or, and equivalence. Prop has raised much theoretical interest recently but little is known about the practical accuracy and efficiency of this domain. Experimental evaluation of Prop is particularly important since Prop theoretically needs to solve a co-NP-complete problem. However, this complexity issue may not matter much in practice because the size of the abstract substitutions is bounded, since Prop would work only on the clause variables in many frameworks.

In this paper, we describe an implementation of the domain Prop and use it to instantiate a generic abstract interpretation algorithm. A key feature of the implementation is the use of ordered binary decision graphs to provide a compact representation of many Boolean functions. The implementation (about 6000 lines of C) has been evaluated systematically and its efficiency and accuracy has been compared with two other abstract domains: the domain Mode (mode, same-value, sharing) and the domain Pattern (mode, same-value, sharing, pattern). A comparison with a reexecution algorithm over the domain Mode, denoted Mode-Reex, is also given. The benchmark programs include symbolic equation-solvers, peephole optimizers, cutting-stock programs, and parsers. This is, to our knowledge, the first implementation and evaluation of Prop.

The experimental results are particularly interesting. The accuracy results for groundness inference indicate that, on our benchmark programs, Prop compares well in accuracy with Pattern, outperforms Mode by an order of magnitude, and is exactly as accurate as Mode-Reex. The efficiency results are even more surprising. They indicate that Prop is only twice as slow as Mode in the average, takes 70% of the time taken by Pattern and 138% of the time taken by Mode-Reex. Results on on-line analysis are also reported.

(complete text in pdf or gzipped postscript)