Available abstract domains

Meaning of Variables in CiaoPP

Both in the PLAI fixpoints and domains, for simplicity, we use the following variable names meaning:

  • AbsInt : identifier of the abstract interpreter being used.
  • Sg : Subgoal being analysed.
  • SgKey : Subgoal key (represented by functor/arity).
  • Head : Head of the clause being analysed.
  • Sv : Subgoal variables.
  • Hv : Head variables.
  • Fv : Free variables in the body of the clause being considered.
  • Vars : Any possible set of variables.
  • Call : Abstract call substitution.
  • Proj : Call projected onto Sv.
  • Entry : Abstract entry substitution (i.e. the abstract subtitution obtained after the abstract unification of Sg and Head projected onto Hv + Fv).
  • Exit : Abstract exit substitution (i.e. the abstract subtitution obtained after the analysis of the clause being considered projected onto Hv).
  • Prime : Abstract prime substitution (i.e. the abstract subtitution obtained after the analysis of the clause being considered projected onto Sv).
  • Succ : Abstract success substitution (i.e. the abstract subtitution obtained after the analysis of the clause being considered extended to the variables of the clause in which Sg appears).
  • ASub : Any possible abstract substitution.
  • R_flag : Flag which represents the recursive characteristics of a predicate. It will be “nr” in case the predicate be non recursive. Otherwise it will be r (recursive).
  • List : (can be represented as OldList,List,AddList,IdList,NewList) current the list of nodes which a given node depends on.
  • _s : The suffix _s means that the term to which the variable is bound to has been sorted. By default they are always sorted thus _s is added only when it appears neccessary to say it explicitely.
  • _uns : The suffix _uns means that the term to which the variable is bound is not sorted.
  • ExtraInfo: Info computed during the call_to_entry that can be reused during the exit_to_prime step.

Subparts