An Interpolation Method for CLP Traversal
Joxan Jaffar, Andrew Santosa and Razvan Voicu
Abstract
We consider the problem of exploring the search tree of a CLP goal in
pursuit of a target property. Essential to such a process is a method
of tabling to prevent duplicate exploration. Typically, only actually
traversed goals are memoed in the table. In this paper we present a
method where, upon the successful traversal of a subgoal, a {\em
generalization} of the subgoal is memoed. This enlarges the record of
already traversed goals, thus providing more pruning in the subsequent
search process. The key feature is that the abstraction computed is
guaranteed not to give rise to a spurious path that might violate the
target property.
A driving application area is the use of CLP to model the behavior of
other programs. We demonstrate the performance of our method on a
benchmark of program verfication problems.