Intermodular success policy

This module implements the policies to compute (possibly) temporary success patterns when modular analysis is performed.

Usage and interface

Library usage:
:- use_module(ciaopp(plai/intermod_success)).
Exports:
- Predicates:
  get_success_info/7, apply_success_policy/9.

Documentation on exports

PREDICATEget_success_info/7

Usage:get_success_info(Call,SgKey,Sg,Sv,AbsInt,Prime,PatternsApplied)

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. The predicate is allowed to fail if no patterns are found.

The following properties should hold at call time:
(nonvar/1)Call is currently a term which is not a free variable.
(nonvar/1)SgKey is currently a term which is not a free variable.
(nonvar/1)Sg is currently a term which is not a free variable.
(nonvar/1)Sv is currently a term which is not a free variable.
(nonvar/1)AbsInt is currently a term which is not a free variable.
(var/1)Prime is a free variable.
(var/1)PatternsApplied is a free variable.

PREDICATEapply_success_policy/9

Usage:apply_success_policy(SuccPolicy,AbsInt,SgKey,Sg,Sv,Proj,Patterns,Prime,PatternsApplied)

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.

The following properties should hold at call time:
(nonvar/1)SuccPolicy is currently a term which is not a free variable.
(nonvar/1)AbsInt is currently a term which is not a free variable.
(nonvar/1)SgKey is currently a term which is not a free variable.
(nonvar/1)Sg is currently a term which is not a free variable.
(nonvar/1)Sv is currently a term which is not a free variable.
(nonvar/1)Proj is currently a term which is not a free variable.
(nonvar/1)Patterns is currently a term which is not a free variable.
(var/1)Prime is a free variable.
(var/1)PatternsApplied is a free variable.

Documentation on imports

This module has the following direct dependencies:

Application modules:
intermod_ops, preprocess_flags, domains, fixpo_ops, intermod_db, intermod_punit.
System library modules:
datafacts_rt, terms_vars, aggregates, terms_check, lists, p_unit_db, program_keys.
Internal (engine) modules:
term_basic, arithmetic, atomic_basic, basiccontrol, exceptions, term_compare, term_typing, debugger_support, basic_props, hiord_rt.
Packages:
prelude, initial, condcomp, assertions, assertions/assertions_basic, isomodes, datafacts.