son: sondergaard (abstract domain)

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

Proj_gr will the the intersection among Vars and Gv. Proj_sh will be { Xs in Sh | Xs $\subseteq$ Vars }.

• 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.

Usage:call_to_entry(Sv,Sg,Hv,Head,K,Fv,Proj,Entry,ExtraInfo)

It obtains the abstract substitution (Entry) which results from adding the abstraction of the Sg = Head to Proj, later projecting the resulting substitution onto Hv. This is done as follows:

• If Sg and Head are identical up to renaming it is just a question or renaming Proj.
• If Hv = [], Entry is just ([],[]).
• Otherwise, it will
  • Obtain in Binds the set of primitive equations corresponding to the equation Sg = Head.
  • obtain Gv1 (variables in Sg or Head involved in a primitive equation with a ground term).
  • propagate the groundnes of Gv1 to Proj through Binds obtaining NewBinds (grounding bindings eliminated) TempSh (sharing part of thee abstract domain) and GvAll (ground variables in both Sg and head).
  • Entry_gr will be the result of intersecting GvAll and Hv.
  • obtain in NonLinear the set of possibly non linear variables w.r.t. TempSh.
  • perform the abstract unification for each binding given in Binds starting from Sh and the list of non linear variables NonLinear in Sh, obtaining NewSh.
  • Entry_sh will be the result of projeecting NewSh onto Hv.

• The following properties should hold at call time:
  (nonvar/1)Sv 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)Hv is currently a term which is not a free variable.
  (nonvar/1)Head is currently a term which is not a free variable.
  (nonvar/1)K is currently a term which is not a free variable.
  (nonvar/1)Fv is currently a term which is not a free variable.
  (nonvar/1)Proj 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.
  (nonvar/1)ExtraInfo is currently a term which is not a free variable.

Usage:exit_to_prime(Sg,Hv,Head,Arg4,Exit,ExtraInfo,Prime)

• If Exit is $bottom, Prime will be also $bottom.
• If Flag = yes (Head and Sg identical up to renaming) it is just a question or renaming Exit.
• If Hv = [], Sh_Prime = [] and Prime_gr = Sv.
• Otherwise:
  • Projects Exit onto Hv obtaining (Gv and Sh).
  • Propagates through Binds the groundness of Gv and Gv_1 (all variables ground after abstracting Sg = Head) to Sh, obtaining NewBinds (grounding bindings eliminated) TempSh (sharing part of thee abstract domain) and GvAll (ground variables in both Sg and head).
  • Entry_gr will be the result of intersecting GvAll and Hv.
  • obtains in NonLinear the set of possibly non linear variables w.r.t. TempSh.
  • perform the abstract unification for each binding given in Binds starting from Sh and the list of non linear variablesm NonLinear in Sh, obtaining NewSh.
  • Entry_sh will be the result of projecting NewSh onto Hv.

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

Usage:abs_sort(ASub_u,ASub)

First sorts the set of variables in Gr, then it sorts the set of set of variables Sh.

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

Usage:compute_lub(ListASub,Lub)

It computes the lub of a set of Asub. For each two abstract substitutions ASub1 and ASub2 in ListASub, obtaining the lub is just

• intersecting Gr1 and Gr2.
• merging Sh1 and Sh2.

• The following properties should hold at call time:
  (nonvar/1)ListASub 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.

Usage:glb(ASub0,ASub1,Lub)

• 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.

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

If Prime = bottom, Succ = bottom. If Sv = [], Call = Succ. Otherwise:

• Succ_gr is the result of merging Prime_gr and Call_gr.
• Then, it obtains in Temp_sh the result of eliminating the couples in Sh in which a ground variables appears.
• Projects Temp_sh onto Sv and obtaining Temp1.

• 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.

Usage:

Specialized version of call_to_entry + exit_to_prime + extend for facts

Usage:

Obtains the abstract prime substitution from the lambda for a fact. (it is a combination of the call_to_entry and exit_to_prime functions) only needed in the combinations of domains.

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

Succ_gr is identical to Call_gr. Succ_sh is obtained by selecting the non ground variables in Vars, and obtaining all possible couples and singletons.

• 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.

Usage:unknown_entry(Sg,Qv,Call)

The top value in Sh for a set of variables is the powerset, in Fr is X/nf 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)Qv is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)Call is currently a term which is not a free variable.

Usage:

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. So, here, all linear and independent: i.e., [].

• 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.
• The following properties should hold upon exit:
  (nonvar/1)Arg3 is currently a term which is not a free variable.

Usage:asub_to_native(ASub,Qv,OutFlag,ASub_user,Comps)

The user friendly format consists in extracting the ground variables (Gr) the linear variables (those which do not appear as singletons in Sh). The rest is the way in which pair sharing is transformed into set sharing

• The following properties should hold at call time:
  (nonvar/1)ASub is currently a term which is not a free variable.
  (nonvar/1)Qv is currently a term which is not a free variable.
  (nonvar/1)OutFlag is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)ASub_user is currently a term which is not a free variable.
  (nonvar/1)Comps is currently a term which is not a free variable.

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

Gr is the set of variables which are in Qv but not in Sharing (share(Sharing) given by the user). Sh is computed as follows:

• Linear is the set of linear variables given by the user (if any)
• a first approximation to the non linear variables is Qv minus Linear.
• Then (since the ground and free variables are also linear) they are also subtracted in order to allow the user not to explicit them, obtaining the final NonLinear.
• Those nonlinear variables are transformed into singletons.
• Finally the (set) Sharing given by the user is transformed into our (pair) sharing Sh.

• 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.
• The following properties should hold upon exit:
  (nonvar/1)ASub is currently a term which is not a free variable.

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.

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:

• ground : if the builtin makes all variables ground whithout imposing any condition on the previous freeness values of the variables.
• bottom : if the abstract execution of the builtin returns bottom.
• unchanged : if we cannot infer anything from the builtin, the substitution remains unchanged and there are no conditions imposed on the previous freeness values of the variables.
• some : if it makes some variables ground without imposing conditions.
• 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.

Usage:success_builtin(Type,Sv_u,Condv,_HvFv_u,Call,Succ)

Obtains the success for some particular builtins:

• If Type = ground, it updates Call making all vars in Sv_u ground.
• If Type = bottom, Succ = $bottom.
• If Type = unchanged, Succ = Call.
• If Type = some, it updates Call making all vars in Condv ground
• Otherwise Type is the SgKey of a particular builtin for each the Succ is computed.

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

Usage:call_to_success_builtin(SgKey,Sg,Sv,Call,Proj,Succ)

If it gets here, the call for the builtin is bound to fail, so ...

• 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)Sv is currently a term which is not a free variable.
  (nonvar/1)Call is currently a term which is not a free variable.
  (nonvar/1)Proj 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.

Usage:propagate_to_sh(ASub_sh,SSon,NewASub_sh,Allowed_sh)

Eliminates the redundancies in ASub_sh using SSon. This is done by for each set Xs in ASub_sh:

• obtaining in NewXss_a the sorted set of all sorted couples in Xs.
• If NewXss_s subseteq SSon, Xs is not redundant and thus it is added to NewASub_sh and to Allowed_sh. Otherwise it is eliminated.

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

Usage:propagate_to_son(SSon,Allowed_sh,NewGSon,NewSSon)

Eliminates the redundancies in SSon using Allowed_sh and NewGSon. This is done by for each set Xs in SSon:

• if Xs is a singleton [X] and X is ground, Xs is eliminated.
• If Xs is a couple and is not in Allowed_sh it is eliminated.
• Otherwise Xs will be added to NewSSon.

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