Given a call pattern for an imported predicate defined by Call call and Sg abstract substitution, Prime is the success substitution resulting from the application of the success policy for imported predicates. PatternsApplied is instatiated to no if there are no applicable patterns.
Provides on backtracking the call and success patterns Call and Succ of exported predicates of a given goal Sg on a given abstract domain AbsInt. It uses SuccessPolicy to check which marked patterns can be used.
This predicate is called by the analysis procedure to get info about imported predicates. For performance reasons, when an external predicate of an imported module is requested, all the exported predicates of the imported module are loaded into memory.
Applies the success policy given as first argument to the list of triples (SgProj,Proj,Succ) Patterns w.r.t. Proj. If there are no applicable patterns in Patterns, it returns either '$bottom' or the topmost substitution, depending on the type of the success policy (either it is underapproximating or overapproximating, respectively.) PatternsApplied is instatiated to no if there are no applicable patterns.