Precise pair-sharing analysis of logic programs

The paper presents a novel approach to pair-sharing analysis of logic programs. The pair-sharing domain ASub of Søndergaard is known to be more efficient than the setsharing domain Sharing of Jacobs and Langen and gains accuracy because of linearity tracking. However, it is less accurate because of weaker groundness information, and the fact that it loses track of where new groundness eliminates sharing. In this paper we present a new domain which inherits the advantages of both ASub and Sharing and is uniformly more accurate in terms of pair-sharing than each of the two domains. The proposed domain expresses pair-sharing in terms of existence of traversable paths in relation graphs derived from program constraints. Each edge of a relation graph has an attached groundness formula which defines under what groundness conditions it still causes sharing. This allows the domain to maintain information about when groundness can eliminate sharing. Relation graphs are augmented by separate groundness information (usually Def or Pos). The groundness analysis and groundness formulae can be represented using efficient ROBDD methods.