☰

CLIQUE-sharing+freeness (abstract domain)

Author(s): Jorge Navas.

Stability: [prod] Apt for production use (but please report any bugs).


This file contains an extension (freeness) of the domain dependent abstract functions for the clique-sharing domain.

The representation of this domain augments the Clique-sharing domain with a third component that keep track of freeness.

The meaning of the variables is defined in sharefree.pl.

Documentation on exports

PREDICATEcall_to_entry/9

Usage:

  • The following properties should hold at call time:
    (nonvar/1)Arg1 is currently a term which is not a free variable.
    (nonvar/1)Arg2 is currently a term which is not a free variable.
    (nonvar/1)Arg3 is currently a term which is not a free variable.
    (nonvar/1)Arg4 is currently a term which is not a free variable.
    (nonvar/1)Arg5 is currently a term which is not a free variable.
    (nonvar/1)Arg6 is currently a term which is not a free variable.
    (nonvar/1)Arg7 is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)Arg8 is currently a term which is not a free variable.

PREDICATEexit_to_prime/7

Usage:

  • The following properties should hold at call time:
    (nonvar/1)Arg1 is currently a term which is not a free variable.
    (nonvar/1)Arg2 is currently a term which is not a free variable.
    (nonvar/1)Arg3 is currently a term which is not a free variable.
    (nonvar/1)Arg4 is currently a term which is not a free variable.
    (nonvar/1)Arg5 is currently a term which is not a free variable.
    (nonvar/1)Arg6 is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)Arg7 is currently a term which is not a free variable.

PREDICATEextend/5

Usage:extend(Sg,Prime,Sv,Call,Succ)

If Prime = bottom, Succ = bottom. If Sv = [], Call = Succ. Otherwise, Succ_sh is computed as in sharing_clique:extend/4, Call_fr is computed by:

  • obtainig in NewGv the set of variables which have becomed ground.
  • adding this NewGv variables to Prime_fr, obtaining Temp1_fr.
  • obtaining in BVars the set of nonground variables in Succ which do not belong to Sg (ar not in Sv).
  • Then it obtains in BVarsf the subset of BVars which are free w.r.t Call_fr, and in Temp2_fr, the result of adding X/nf to Temp1_fr for the rest of variables in BVars.
  • If BVarsf = [],

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

PREDICATEproject/5

Usage:project(Sg,Vars,HvFv_u,ASub,Proj)

  • The following properties should hold at call time:
    (nonvar/1)Sg is currently a term which is not a free variable.
    (nonvar/1)Vars is currently a term which is not a free variable.
    (nonvar/1)HvFv_u is currently a term which is not a free variable.
    (nonvar/1)ASub is currently a term which is not a free variable.
  • The following properties should hold upon exit:
    (nonvar/1)Proj is currently a term which is not a free variable.

PREDICATEabs_sort/2

Usage:abs_sort(Asub,Asub_s)

Sorts the set of set of variables ASub to obtaint the Asub_s.

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

PREDICATEidentical_abstract/2

Usage:identical_abstract(ASub0,ASub1)

Succeeds if the two abstract substitutions are defined on the same variables and are equivalent.

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

PREDICATEless_or_equal/2

Usage:less_or_equal(ASub0,ASub1)

Succeeds if ASub1 is more general or equal to ASub0.

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

PREDICATEcall_to_success_fact/9

Usage:

Specialized version of call_to_entry + exit_to_prime + extend for facts.

    PREDICATEcompute_lub_el/3
    No further documentation available for this predicate.

    PREDICATEglb/3

    Usage:glb(ASub0,ASub1,Lub)

    Glb is just intersection.

    • The following properties should hold at call time:
      (nonvar/1)ASub0 is currently a term which is not a free variable.
      (nonvar/1)ASub1 is currently a term which is not a free variable.
    • The following properties should hold upon exit:
      (nonvar/1)Lub is currently a term which is not a free variable.

    PREDICATEinput_user_interface/5

    Usage:input_user_interface(InputUser,Qv,ASub,Sg,MaybeCallASub)

    Obtaining the abstract substitution for Cl+Fr from the user supplied information just consists in taking the cliques first and the var(Fv) element of InputUser, and construct from them the Freeness.

    • The following properties should hold at call time:
      (nonvar/1)Qv 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)MaybeCallASub is currently a term which is not a free variable.
      (term/1)InputUser is any term.
      (list/1)Qv is a list.
      (term/1)ASub is any term.
      (term/1)Sg is any term.
      (term/1)MaybeCallASub is any term.
    • The following properties should hold upon exit:
      (nonvar/1)ASub is currently a term which is not a free variable.

    PREDICATEinput_interface/4
    No further documentation available for this predicate.

    PREDICATEunknown_call/4

    Usage:unknown_call(Sg,Vars,Call,Succ)

    • The following properties should hold at call time:
      (nonvar/1)Sg is currently a term which is not a free variable.
      (nonvar/1)Vars is currently a term which is not a free variable.
      (nonvar/1)Call is currently a term which is not a free variable.
    • The following properties should hold upon exit:
      (nonvar/1)Succ is currently a term which is not a free variable.

    PREDICATEempty_entry/3

    Usage:empty_entry(Sg,Vars,Entry)

    The empty value in Sh for a set of variables is the list of singletons, in Fr is X/f forall X in the set of variables.

    • The following properties should hold at call time:
      (nonvar/1)Sg is currently a term which is not a free variable.
      (nonvar/1)Vars is currently a term which is not a free variable.
    • The following properties should hold upon exit:
      (nonvar/1)Entry is currently a term which is not a free variable.

    PREDICATEspecial_builtin/5

    Usage:special_builtin(SgKey,Sg,Subgoal,Type,Condvars)

    Satisfied if the builtin does not need a very complex action. It divides builtins into groups determined by the flag returned in the second argument + some special handling for some builtins:

    • new_ground if the builtin makes all variables ground whithout imposing any condition on the previous freeness values of the variables.
    • old_ground if the builtin requires the variables to be ground.
    • old_new_ground if the builtin requires some variables to be ground and grounds the rest.
    • unchanged if we cannot infer anything from the builtin, the substitution remains unchanged and there are no conditions imposed on the previo.
    • some if it makes some variables ground without imposing conditions.
    • all_nonfree if the builtin makes all variables possible non free.
    • Sgkey, special handling of some particular builtins.

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

    Documentation on multifiles

    PREDICATEaidomain/1
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.init_abstract_domain/2
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.amgu/5
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.augment_asub/4
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.augment_two_asub/4
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.call_to_entry/10
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.exit_to_prime/8
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.project/6
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.widencall/4
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.needs/2
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.widen/4
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.compute_lub/3
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.compute_clauses_lub/4
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.compute_clauses_glb/4
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.fixpoint_covered/3
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.fixpoint_covered_gfp/3
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.identical_abstract/3
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.abs_sort/3
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.extend/6
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.less_or_equal/3
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.glb/4
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.eliminate_equivalent/3
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.abs_subset/3
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.call_to_success_fact/10
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.special_builtin/6
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.combined_special_builtin0/3
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.body_succ_builtin/9
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.split_combined_domain/4
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.success_builtin/7
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.call_to_success_builtin/7
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.obtain_info/5
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.input_interface/5
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.input_user_interface/6
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.asub_to_native/6
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.concrete/4
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.unknown_call/5
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.unknown_entry/4
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.empty_entry/4
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.part_conc/5
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.multi_part_conc/4
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.collect_auxinfo_asub/4
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.rename_auxinfo_asub/4
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.dom_statistics/2
    No further documentation available for this predicate. The predicate is multifile.

    PREDICATEaidom.contains_parameters/2
    No further documentation available for this predicate. The predicate is multifile.

    Generated with LPdoc using Ciao