Update plai_db after clause deletion (incremental analysis)

Author(s): Isabel Garcia-Contreras (ported from ciaopp-0.8).

This module contains predicates for removing completes and related memo_table data from analysis necessary for recomputing correctly analysis after removing clauses or modifying the answers of the analysis.

Usage and interface

Documentation on exports

Usage:remove_clauses_and_related_info_collect_preds(ClKeys,AbsInt,Preds,Keys)

Cls is a set of clauses which has have been eliminated from the program. Thus, they must be deleted from the database of clauses used by the analyzer. In addition to the clause, we delete all the memo_tables and memo_lubs for the clauses. In Preds and Keys we collect the name,arity and keys of predicates for which clauses have been deleted. This will later be used for updating the SCCs.

  • The following properties should hold at call time:
    (nonvar/1)ClKeys 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)Preds is a free variable.
    (var/1)Keys is a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form remove_clauses_and_related_info_collect_preds(ClKeys,AbsInt,Preds,Keys) do not fail.
    (is_det/1)All calls of the form remove_clauses_and_related_info_collect_preds(ClKeys,AbsInt,Preds,Keys) are deterministic.

Usage:bottom_up_delete_completes_preds(Keys,SCCs,AbsInt,ExtCompletes)

Keys is the list of keys of predicates for which clauses have been deleted. The completes for such predicates may no longer be accurate enough. Thus we collect the external calls in ExtCompletes and erase the corresponding completes from the analysis database.

  • The following properties should hold at call time:
    (nonvar/1)Keys 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)ExtCompletes is a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form bottom_up_delete_completes_preds(Keys,SCCs,AbsInt,ExtCompletes) do not fail.

Usage:bottom_up_delete_complete(SgKey,Id,SCC,AbsInt,ExtCompletes)

  • The following properties should hold at call time:
    (nonvar/1)SgKey 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)SCC 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)ExtCompletes is a free variable.
  • The following properties should hold globally:
    (not_fails/1)All the calls of the form bottom_up_delete_complete(SgKey,Id,SCC,AbsInt,ExtCompletes) do not fail.

No further documentation available for this predicate.