This module implements the top-down fixpoint algorithm of PLAI, both in its mono-variant and multi-variant on successes versions. It is always multi-variant on calls. The algorithm is parametric on the particular analysis domain.
The success pattern of Query with Call is Succ in the analysis domain AbsInt. The predicate called is identified by QKey, and RFlag says if it is recursive or not. The goal Query has variables Qv, and the call pattern is uniquely identified by N.
Cleanups the database of analysis of temporary information.
Cleans up the database of analysis, of both temporary as well as permanent information regarding abstract domain AbsInt.