Inverting abstract unification for set-sharing
Xuan Li, Lunjin Lu · 2005
This paper presents an inversion of the abstract unification operator for forward set-sharing analysis of logic programs. The inverted operator, called a backward abstract unification operator, computes all maximal pre-conditions for a given equation and its post-condition. It is a key operator in a backward analysis. The maximal preconditions are obtained by first calculating a superset of all preconditions and then generating all maximal pre-conditions from the superset. The latter step is transformed to the problem of finding all maximal models of a Boolean formula.