CLIQUE-sharing (abstract domain)

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.

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.
• The following properties should hold upon exit:
  (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.

Usage:amgu(Sg,Head,ASub,AMGU)

AMGU is the abstract unification between Sg and Head.

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

Usage:extend(Sg,Prime,Sv,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)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:

Augments the abstract subtitution with fresh variables

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

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.

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.

Usage:eliminate_equivalent(TmpLSucc,LSucc)

The list LSucc is reduced wrt the list TmpLSucc in that it does not contain abstract substitutions which are equivalent. Note that new clique groups can be introduced because of the use of normalization process.

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

Specialized version of call_to_entry + exit_to_prime + extend for facts.

Note that if the success is computed (instead of the prime) and then we compose the information and project it, we can loose information since the extension is the step in which more information is lost Note that if we use Proj we need to call explicitly the function extend, so we can loose information.

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 merging the ASub1 and ASub2.

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

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.

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

Obtaining the abstract substitution for Sharing from the user supplied information just consists in taking the mshare(Sharing) and clique(Clique) element of InputUser and sorting it. If there is no such element, get the top sharing for the variables involved.

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

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

The user friendly format consists in extracting the ground variables.

• 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:unknown_call(Sg,Vars,Call,Succ)

Gives the top value for the variables involved in a literal whose definition is not present, and adds this top value to Call.

• 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:empty_entry(Sg,Vars,Entry)

Gives the empty value in this domain for a given set of variables Vars, resulting in the abstract substitution Entry. I.e., obtains the abstraction of a substitution in which all variables Vars are unbound: free and unaliased. In this domain is the list of singleton lists of variables in the sharing part. The clique part is initialized to empty list.

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

Usage:unknown_entry(Sg,Qv,Call)

The top value in Clique for a set of variables is the powerset. It consits of putting Qv directly in the clique part.

• 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:widen(Who,ASub1,ExtraInfo,ASub)

ASub is the result of widening the abstract substitution ASub1. This interface is only defined for sake of clarity. Who defines what operation has called to widen. The actions depend on this argument.

• if Who = amgu then the value of widen is amgu.
• if Who = extend then the value of widen is not off.
• if Who = plai_op then the value of widen is plai_op.

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

Usage:widen(TCond,TWid,ASub1,ExtraInfo,ASub)

ASub is the result of widening the abstract substitution ASub1. TCond is the type of condition used and TWid is the type of widening.

Compute the number of widening done. Note that it should be removed if time measuring is required.

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

Handles those builtins for which computing Prime is easier than Succ.

• 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:clique_make_decomposition(Eqs,Cl,Ground,NewGround,NewSH)

It gives the adecuate abstract substitution resulting of the unification of A and `B `when ==(A,B) was called. If neither X nor Term in one binding is ground, since they have to be identicals (==), each set C of the clique domain have to satisfied that X is an element of C if and only if at least one variable in Term appears also in C. Therefore, we have to decompose the initial clique in subcliques and sharing sets such that either only X or only variables of Term cannot appear. The difference wrt share_make_reduction/5 is that clique_make_decomposition/5 returns the final elements and share_make_reduction/5 returns the sharing sets that have to be eliminated.

• The following properties should hold at call time:
  (nonvar/1)Eqs is currently a term which is not a free variable.
  (nonvar/1)Cl is currently a term which is not a free variable.
  (nonvar/1)Ground is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)NewGround is currently a term which is not a free variable.
  (nonvar/1)NewSH is currently a term which is not a free variable.

Usage:eliminate_couples_clique(Cl,Xv,Yv,NewCl)

All arguments ordered

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

Usage:share_make_reduction(Eqs,Lambda,Ground,NewGround,Eliminate)

It gives the adecuate abstract substitution resulting of the unification of A and B when ==(A,B) was called. If neither X nor Term in one binding is ground, since they have to be identicals (==), each set S of the sharing domain have to satisfied that X is an element of S if and only if at least one variable in Term appears also in S. Therefore, each set in which either only X or only variables of Term appear, has to be eliminated.

• The following properties should hold at call time:
  (nonvar/1)Eqs is currently a term which is not a free variable.
  (nonvar/1)Lambda is currently a term which is not a free variable.
  (nonvar/1)Ground is currently a term which is not a free variable.
• The following properties should hold upon exit:
  (nonvar/1)NewGround is currently a term which is not a free variable.
  (nonvar/1)Eliminate is currently a term which is not a free variable.