☰

*ON THIS PAGE*# def: definiteness (abstract domain)

**Author(s):** Maria Garcia de la Banda, Manuel Hermenegildo. **Meaning of the Program Variables**

## Usage and interface

## Documentation on exports

## Documentation on multifiles

## Documentation on imports

This module has the following direct dependencies:

- The CiaoPP Program Processor »

- PART I - Using CiaoPP »

- Available abstract domains »

**def: definiteness (abstract domain)**

**Stability: [****beta****] **Most of the functionality is there but it is still missing some testing and/or verification.

This file contains the definiteness abstract domain and abstract unctions for CLP languages.

The abstract constraint is kept as `a(Ground,Set)` in which:

- Ground is a sorted list of uniquely defined variables
- Set is a sorted list of elements with format (X,SS) in which X is a variable and SS is a sorted set of set of variables such that for each S in SS, uniquely defining all variables in S, uniquely defines X, and there is no
`S'`in SS, such that`S'`subseteq S. - Not that
*top variables*(variables from which nothing is known) cannot appear in Ground but can appear in some SS.

- AbsInt : identifier of the abstract interpreter being used.
- Sg : Subgoal being analysed.
- SgKey : Subgoal key (represented by functor/arity).
- Sv : Subgoal variables.
- Call : Abstract call constraint.
- Proj : Call projected onto Sv.
- Head : Head of one of the clauses which define the Sg predicate.
- Hv : Head variables.
- Fv : Free variables in the body of the clause being considered
- Entry : Abstract entry constraint (i.e. the abstract subtitution obtained after the abstract unification of Sg and Head projected onto Hv + Fv).
- BothEntry: Similar to the abstract entry constraint: the abstract subtitution obtained after the abstract unification of Sg and Head but without being projected onto Hv + Fv).
- Exit : Abstract exit constraint (i.e. the abstract subtitution obtained after the analysis of the clause being considered projected onto Hv).
- Prime : Abstract prime constraint (i.e. the abstract subtitution obtained after the analysis of the clause being considered projected onto Sv).
- BPrime : similar to the abstract prime constraint: abstract subtitution obtained after the analysis of the clause being considered still projected onto Hv (i.e. just before going Sv and thus, to Prime).
- Succ : Abstract success constraint (i.e. the abstract subtitution obtained after the analysis of the clause being considered extended to the variables of the clause in which Sg appears).
- Constr : Any abstract constraint.

**Library usage:**`:- use_module(domain(def)).`**Exports:***Predicates:*`call_to_entry/9`,`exit_to_prime/7`,`project/5`,`project_vars/4`,`compute_lub/2`,`compute_lub_el/3`,`glb/3`,`abs_sort/2`,`extend/5`,`call_to_success_fact/9`,`special_builtin/5`,`success_builtin/6`,`input_user_interface/5`,`input_interface/4`,`asub_to_native/5`,`unknown_call/4`,`unknown_entry/3`,`empty_entry/3`,`less_or_equal/2`.*Multifiles:*`aidomain/1`,`aidom.init_abstract_domain/2`,`aidom.amgu/5`,`aidom.augment_asub/4`,`aidom.augment_two_asub/4`,`aidom.call_to_entry/10`,`aidom.exit_to_prime/8`,`aidom.project/6`,`aidom.widencall/4`,`aidom.needs/2`,`aidom.widen/4`,`aidom.compute_lub/3`,`aidom.compute_clauses_lub/4`,`aidom.compute_clauses_glb/4`,`aidom.fixpoint_covered/3`,`aidom.fixpoint_covered_gfp/3`,`aidom.identical_abstract/3`,`aidom.abs_sort/3`,`aidom.extend/6`,`aidom.less_or_equal/3`,`aidom.glb/4`,`aidom.eliminate_equivalent/3`,`aidom.abs_subset/3`,`aidom.call_to_success_fact/10`,`aidom.special_builtin/6`,`aidom.combined_special_builtin0/3`,`aidom.body_succ_builtin/9`,`aidom.split_combined_domain/4`,`aidom.success_builtin/7`,`aidom.call_to_success_builtin/7`,`aidom.obtain_info/5`,`aidom.input_interface/5`,`aidom.input_user_interface/6`,`aidom.asub_to_native/6`,`aidom.concrete/4`,`aidom.unknown_call/5`,`aidom.unknown_entry/4`,`aidom.empty_entry/4`,`aidom.part_conc/5`,`aidom.multi_part_conc/4`,`aidom.collect_auxinfo_asub/4`,`aidom.rename_auxinfo_asub/4`,`aidom.dom_statistics/2`,`aidom.contains_parameters/2`.

PREDICATEcall_to_entry/9

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

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

- It will add to Call the information corresponding to the set of equations
`=`(ArgSg,ArgHead) resulting from the unification Sg = Head by calling to`def_herbrand_equation/6`, obtaining NewProj. - If NewProj is
`$bottom`(i.e. if Sg and Head are not unifiables) then Entry =`bottom`. Otherwise, it will project NewProj onto Hv and it will add the free variables in the body of the clause to the projected constraint, obtaining Entry.

*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`)BothEntry is currently a term which is not a free variable.

PREDICATEexit_to_prime/7

Usage:`exit_to_prime(Sg,Hv,Head,Sv,Exit,BothEntry,Prime)`

It computes the prime abstract constraint Prime, i.e. the result of going from the abstract constraint over the head variables (Exit), to the abstract constraint over the variables in the subgoal. If Exit is `$bottom`, Prime will be also `$bottom`. Otherwise Prime is the result of projecting Exit onto Hv obtaining BPrime, then adding the information in BPrime to the BothEntry (the abstract constraint obtained during the call to entry over all variables in Sg and Head and later projecting onto Sv.

*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`)Sv 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`)BothEntry 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.

PREDICATEproject/5

Usage:`project(Sg,Vars,HvFv_u,Constr,Projected)`

It projects the ordered abstract subtitution given in the first argument on the ordered list of variables Vars in the second argument. All the variables in the second argument are assumed to appear also in the abstract constraint.

- If the abstract constraint is
`$bottom`the projected abstract constraint will be also`$bottom` - Otherwise: let a(Ground,Set) be the abstract constraint and a(PGround, PSet) be the result of the projection
- PGround will be the intersection of Ground and Vars
- PSet will be the result of for each (X,SS) in Set s.t.X in Vars remove from SS those sets which are not subsetseq of Vars obtaining NewSS. This will be done by calling
`project_vars/5`. Note that if NewSS is [], (X,NewSS) will not be in PSet

*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`)Constr is currently a term which is not a free variable.*The following properties should hold upon exit:*

(`nonvar/1`)Projected is currently a term which is not a free variable.

PREDICATEproject_vars/4

Usage:`project_vars(Vars1,Set,Vars2,PSet)`

It will project the list of (X,SS) in Set onto Vars2 obtaining PSet. This will be done in the following way, for each (X,SS) in Set:

- If X not in Vars1, (X,SS) will be eliminated.
- Otherwise, we will compute NewSS =
`{`S in SS| S in Vars2`}`.- If NewSS = [], X becomes
*top*and it will be ignored. - Otherwise, (X,NewSS) will be added to PSet.

- If NewSS = [], X becomes

*The following properties should hold at call time:*

(`nonvar/1`)Vars1 is currently a term which is not a free variable.

(`nonvar/1`)Set is currently a term which is not a free variable.

(`nonvar/1`)Vars2 is currently a term which is not a free variable.*The following properties should hold upon exit:*

(`nonvar/1`)PSet is currently a term which is not a free variable.

PREDICATEcompute_lub/2

Usage:`compute_lub(ListConstr,Lub)`

It obtains the *lub* between all abstract constraints which are elements of the list given in the first argument. We assume that the abstract constraints are ordered and defined over the same set of variables. It will be computed recursively by obtaining the *lub* of 2 abstract constraints in each iteration in the following way:

- The lub between two abstract constraints one of which is
`$bottom`will result in the other abstract constraint - Otherwise, let Constr1 = a(G1,T1,S1) and Constr2 = a(G2,T2,S2)
- NewG will be the intersection between G1 and G2.
- NewT will be the union of T1 and T2.
- NewS will be computed by
`lub_set/4`.

PREDICATEcompute_lub_el/3

No further documentation available for this predicate.

PREDICATEglb/3

Usage:`glb(Constr1,Constr2,Constr)`

*The following properties should hold at call time:*

(`nonvar/1`)Constr1 is currently a term which is not a free variable.

(`nonvar/1`)Constr2 is currently a term which is not a free variable.*The following properties should hold upon exit:*

(`nonvar/1`)Constr is currently a term which is not a free variable.

PREDICATEabs_sort/2

Usage 1:`abs_sort(Constr,SortedConstr)`

It sorts the abstract constraint a(Ground,Set) received as first argument. In doing this it will:

- sort the list of variables in Ground
- for each (X,SS) in Set:
- sort each S in SS obtaining TempSet.
- sort TempSet.

*The following properties should hold at call time:*

(`nonvar/1`)Constr is currently a term which is not a free variable.*The following properties should hold upon exit:*

(`nonvar/1`)SortedConstr is currently a term which is not a free variable.

Usage 2:`abs_sort(Set1,Set2)`

PREDICATEextend/5

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

It extends the information given by the new abstract constraint on the subgoal Prime (first argument) to the original information about all the clause variables which is contained in Call, obtaining Succ.

- If Prime is
`$bottom`, Succ =`$bottom`. - Otherwise, the result will be the same as conjunting the new abstract constraint Prime with Call.

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

PREDICATEcall_to_success_fact/9

Usage:`call_to_success_fact(Sg,Hv,Head,K,Sv,Call,Proj,Prime,Succ)`

It obtains the prime and success constraint for a fact. However, since the program are assumed to be normilised, a fact should have all their arguments as voids, and therefore Prime = Proj, and Succ = Call.

*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`)K 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`)Prime is currently a term which is not a free variable.

(`nonvar/1`)Succ is currently a term which is not a free variable.

PREDICATEspecial_builtin/5

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

The predicate succeeds if the Sgkey indicates a builtin or a constraint Type indicates the kind of builtin and Condvars contains the info needed for their abstraction.

- Type:
`'$fd_=/2'`| Condvars: Sg | Meaning:`=/2`builtin - Type:
`'$fd_comp/2'`| Condvars: _ | Meaning: comparisons like`<`,`>`,etc - Type:
`'$fd_piii/2'`| Condvars: Sg | Meaning: PrologIII list - Type:
`'$fd_fail'`| Condvars: _ | Meaning: fail, abort,etc - Type:
`'$fd_unchanged'`| Condvars: _ | Meaning: does not affect the info - ....

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

PREDICATEsuccess_builtin/6

Usage:`success_builtin(Type,Sv_uns,Term,HvFv_u,Call,Succ)`

By now, it is tricky since it assumes the following things:

- booleans are still not allowed

*The following properties should hold at call time:*

(`nonvar/1`)Type is currently a term which is not a free variable.

(`nonvar/1`)Sv_uns 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.

PREDICATEinput_user_interface/5

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

It translate the query mode given by the user into the internal structure.

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

PREDICATEasub_to_native/5

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

It translates an internal abstract constraint into something friendly for the user.

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

PREDICATEunknown_call/4

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

Gives the *top* value for the variables Vars involved in a literal whose definition is not present, and adds this *top* value to Call (it is like conjunting the information in Call with the *top* for a subset of variables) In the definiteness analyser, nothing needs to be done.

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

PREDICATEunknown_entry/3

Usage:`unknown_entry(Sg,Vars,Call)`

Gives the *top* value for a given set of variables, resulting in the abstract constraint Call. In the definiteeness domain the *top* abstraction for a set of variables Vars is T = a({},{}).

PREDICATEempty_entry/3

Usage:`empty_entry(Sg,Vars,Entry)`

PREDICATEless_or_equal/2

Usage:`less_or_equal(ASub0,ASub1)`

Succeeds if ASub0 = (G0,T0,R0) is less or equal than ASub1 = a(G1,T1,R1) i.e. if ASub0 is more concrete or equal than ASub1. This will be true if either ASub0 is *bottom* or:

- G1 subseteq G0.
- forall (X,SS1) in R1, X in G0, or exists (X,SS0) in R0, such that forall S1 in SS1, exists S0 in SS0 such that S0 in S1.

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

*Application modules:*`preprocess_flags`,`domains`,`deftools`.*System library modules:*`datafacts_rt`,`sets`,`sort`,`terms_check`,`terms_vars`,`p_unit`.*Internal (engine) modules:*`term_basic`,`arithmetic`,`atomic_basic`,`basiccontrol`,`exceptions`,`term_compare`,`term_typing`,`debugger_support`,`basic_props`,`hiord_rt`.*Packages:*`prelude`,`initial`,`condcomp`,`assertions`,`assertions/assertions_basic`,`datafacts`,`modes_extra`,`modes`,`aidomain`.

Generated with LPdoc using Ciao