Tech Report CS-94-17
Cardinality Analysis of Prolog
C. Braem, B. Le Charlier, S. Modart, and P. Van Hentenryck
This paper proposes a novel analysis called cardinality analysis to approximate the number of solutions to a goal. The analysis is an instantiation of a new abstract interpretation framework for full Prolog (without dynamic predicates) based on sequences of substitutions. The abstract domain captures not only modes and types but also lower and upper bounds on the number of solutions and information about arithmetic and meta predicates, the cut, and termination. Experimental results show that the approach has a number of desirable properties wrt efficiency, accuracy, and simplicity not available in previous work. In particular, all aspects of the analysis are captured in a single framework, the mode/type analysis and the cardinality analysis are performed simultaneously and improve each other's accuracy, input/output patterns, cut, termination, and abstractions of arithmetic and meta-predicates are used to achieve great precision, and the overhead of the approach is small compared to traditional mode/type analyses.