plai_db (library)

The predicate SgKey has a variant success pattern (Sg,Proj,Prime) on the domain AbsInt. The and-or graph node is Id, and is called from the program points in list Parents.

Usage:complete(SgKey,AbsInt,Sg,Proj,Prime,Id,Parents)

• The following properties should hold upon exit:
  (predkey/1)SgKey is an atom that uniquely identifies a program predicate.
  (atm/1)AbsInt is an atom.
  (term/1)Sg is any term.
  (term/1)Proj is any term.
  (list/2)Prime is a list of terms.
  (int/1)Id is an integer.
  (parents_complete/1)parents_complete(Parents)

The predicate SgKey has in all variants success pattern (Sg,Proj,Prime) on the domain AbsInt. If Lub is yes, Proj and Prime are substitutions, if Lub is no, they are lists of substitutions. The predicate is of type data.

Before calling the goal at program point PointKey, there is a variant in which Call on the domain AbsInt holds upon the program clause variables Vars_u. These variables need be sorted conveniently so that Call makes sense. The and-or graph node that causes this is Id and the call originated to the goal at this program point generates and-or graph node Child.

Usage:memo_table(LitKey,AbsInt,Id,Child,Vars_u,Call)

• The following properties should hold upon exit:
  (litkey/1)LitKey is an atom that uniquely identifies a program point of a program clause body literal.
  (atm/1)AbsInt is an atom.
  (int/1)Id is an integer.
  (int/1)Child is an integer.
  (term/1)Vars_u is any term.
  (list/2)Call is a list of terms.

Before calling the goal at program point PointKey, in all variants Call on the domain AbsInt holds upon the program clause variables Vars_u. If Lub is yes, Call is a substitution, if If Lub is no, Call is a list of substitutions. The predicate is of type data.

Used to keep the trace of the parents in the and-or graph for the dd/di fixpoints. The parents are used to choose previous aproximations to apply the widening operators on calls The and-or graph node is Id, and Parents is a list of couples of graph node and program points. The predicate is of type data.

Erases all data in this module for the analysis domain AbsInt.

Usage:get_parent_key(LitKey,Id,AbsInt,CKey)

CKey is the key that corresponds to Id, it may not correspong to the decoding LitKey because of how meta_calls are indexed in the fixpoints

• The following properties should hold upon exit:
  (litkey/1)LitKey is an atom that uniquely identifies a program point of a program clause body literal.
  (int/1)Id is an integer.
  (atm/1)AbsInt is an atom.
  (predkey/1)CKey is an atom that uniquely identifies a program predicate.

Usage:get_complete(SgKey,AbsInt,Sg,Proj,Prime,Id,Ps,Ref)

• The following properties should hold at call time:
  (nonvar/1)Id is currently a term which is not a free variable.
  (predkey/1)SgKey is an atom that uniquely identifies a program predicate.
  (atm/1)AbsInt is an atom.
  (plai_db_id/1)plai_db_id(Id)
• The following properties should hold globally:
  (is_det/1)All calls of the form get_complete(SgKey,AbsInt,Sg,Proj,Prime,Id,Ps,Ref) are deterministic.

Usage:get_memo_table(LitKey,AbsInt,Id,Child,Vars,Call,Ref)

• The following properties should hold at call time:
  (nonvar/1)LitKey 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)Id is currently a term which is not a free variable.
  (litkey/1)LitKey is an atom that uniquely identifies a program point of a program clause body literal.
  (atm/1)AbsInt is an atom.
  (plai_db_id/1)plai_db_id(Id)

Usage:get_raw_success(ClKey,AbsInt,Id,Sg,Proj,Prime,Ref)

• The following properties should hold at call time:
  (nonvar/1)ClKey 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)Id is currently a term which is not a free variable.
  (litkey/1)ClKey is an atom that uniquely identifies a program point of a program clause body literal.
  (atm/1)AbsInt is an atom.
  (plai_db_id/1)plai_db_id(Id)
• The following properties should hold upon exit:
  (nonvar/1)Sg 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)Prime is currently a term which is not a free variable.
  (nonvar/1)Ref is currently a term which is not a free variable.

Usage:add_parent_complete(SgKey,AbsInt,Id,PId,LitKey)

• The following properties should hold at call time:
  (nonvar/1)SgKey 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)Id is currently a term which is not a free variable.
  (nonvar/1)PId is currently a term which is not a free variable.
  (nonvar/1)LitKey is currently a term which is not a free variable.

Usage:del_parent_complete(SgKey,AbsInt,Id,PId,LitKey,NPs)

• The following properties should hold at call time:
  (nonvar/1)SgKey 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)Id is currently a term which is not a free variable.
  (nonvar/1)PId is currently a term which is not a free variable.
  (nonvar/1)LitKey is currently a term which is not a free variable.
  (var/1)NPs is a free variable.

Usage:patch_parents(Ref,Memo,Key,Id,NewFs,Fs)

• The following properties should hold at call time:
  (nonvar/1)Ref is currently a term which is not a free variable.
  (nonvar/1)Memo is currently a term which is not a free variable.
  (nonvar/1)Key is currently a term which is not a free variable.
  (nonvar/1)Id is currently a term which is not a free variable.
  (nonvar/1)Fs is currently a term which is not a free variable.
  (list/1)Fs is a list.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form patch_parents(Ref,Memo,Key,Id,NewFs,Fs) do not fail.

Usage:delete_complete(SgKey,AbsInt,Id)

Deletes the information of the complete with Id. This predicate does not delete recursively following its parents.

• The following properties should hold at call time:
  (nonvar/1)SgKey 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)Id is currently a term which is not a free variable.
  (atm/1)SgKey is an atom.
  (atm/1)AbsInt is an atom.
  (plai_db_id/1)plai_db_id(Id)

Usage:delete_plai_db_one_clause(PredKey,ClKey,Id,AbsInt)

Removes from plai_db the information relative to the clause ClKey of complete Id for the domain AbsInt

• The following properties should hold at call time:
  (nonvar/1)PredKey is currently a term which is not a free variable.
  (nonvar/1)ClKey is currently a term which is not a free variable.
  (nonvar/1)Id is currently a term which is not a free variable.
  (nonvar/1)AbsInt is currently a term which is not a free variable.
  (atm/1)PredKey is an atom.
  (atm/1)ClKey is an atom.
  (plai_db_id/1)plai_db_id(Id)
  (atm/1)AbsInt is an atom.

Usage:erase_previous_memo_tables_and_parents(Body,AbsInt,ClKey,Id)

We use Body to erase all the memo_tables and all the pointers in the dependency graph that are not longer valid

• The following properties should hold at call time:
  (nonvar/1)Body 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)ClKey is currently a term which is not a free variable.
  (nonvar/1)Id is currently a term which is not a free variable.

Usage:erase_last_memo_table(AbsInt,ClKey,Id)

• The following properties should hold at call time:
  (nonvar/1)AbsInt is currently a term which is not a free variable.
  (nonvar/1)ClKey is currently a term which is not a free variable.
  (nonvar/1)Id is currently a term which is not a free variable.
• The following properties should hold globally:
  (not_fails/1)All the calls of the form erase_last_memo_table(AbsInt,ClKey,Id) do not fail.

Usage:erase_previous_memo_lubs(Body,ClKey)

This predicate traverses Body and removes the existing memo_lubs. When Body is finished, we also remove the memo-lub for the end of the clause using ClKey.

• The following properties should hold at call time:
  (nonvar/1)Body is currently a term which is not a free variable.
  (nonvar/1)ClKey is currently a term which is not a free variable.

Usage:erase_previous_parents_info(Id,Goal,AbsInt,Key,NewN)

Id is the node identifier of the complete that has this Goal in its list of parents. If Id is no then nothing needs to be done (it is a builtin)

• The following properties should hold at call time:
  (nonvar/1)Id is currently a term which is not a free variable.
  (nonvar/1)Goal 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)Key is currently a term which is not a free variable.
  (nonvar/1)NewN is currently a term which is not a free variable.

Usage:add_invalid_call(SgKey,AbsInt,LitKey,Id,Sg,Proj)

• The following properties should hold at call time:
  (nonvar/1)SgKey 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)LitKey is currently a term which is not a free variable.
  (nonvar/1)Id 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)Proj is currently a term which is not a free variable.

Usage:store_raw_success(ClKey,AbsInt,Id,Sg,Proj,LPrime)

• The following properties should hold at call time:
  (nonvar/1)ClKey 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)Id 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)Proj is currently a term which is not a free variable.
  (nonvar/1)LPrime is currently a term which is not a free variable.

Usage:get_raw_success(ClKey,AbsInt,Id,Sg,Proj,LPrime)

• The following properties should hold at call time:
  (nonvar/1)ClKey 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)Id is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (list/1)LPrime is a list.

plai_db_id(no).
plai_db_id(X) :-
    int(X).