☰

*ON THIS PAGE*# Interval Domain

**Author(s):** Isabel Garcia-Contreras, Jose F. Morales.**Stability: [****devel****] **Currently the subject of active
development and/or research. Functionality may be limited and API
and/or functionality may change without warning or deprecation period. Not recommended yet for use in production.

## Usage and interface

## Documentation on multifiles

## Documentation on internals

## Documentation on imports

This module has the following direct dependencies:

A simple *intervals* abstract domain (non relational) derived from `nonrel_base.pl`.

This domain only uses closed intervals as abstractions, over-approximating the necessary builtins.

**Library usage:**`:- use_module(domain(nonrel_intervals)).`

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

PREDICATEnonrel_top/2

Usage:`nonrel_top(AbsInt,X)`

X is the representation of ``top'' in the abstract domain.

(implement in derived domain)

PREDICATEnonrel_bot/2

Usage:`nonrel_bot(AbsInt,X)`

X is the representation of ``bot'' in the abstract domain.

(implement in derived domain)

PREDICATEnonrel_var_elem/2

Usage:`nonrel_var_elem(AbsInt,X)`

X is the abstraction of a free variable in the abstract domain.

(implement in derived domain)

PREDICATEnonrel_less_or_equal_elem/3

Usage:`nonrel_less_or_equal_elem(AbsInt,E1,E2)`

Succeeds if E1 is smaller than E2.

(implement in derived domain)

PREDICATEnonrel_compute_glb_elem/4

Usage:`nonrel_compute_glb_elem(AbsInt,E1,E2,EG)`

EG is the *greatest lower bound* of E1 and E2.

(implement in derived domain)

PREDICATEnonrel_compute_lub_elem/4

Usage:`nonrel_compute_lub_elem(AbsInt,E1,E2,EL)`

EL is the *least upper bound* of E1 and E2.

(implement in derived domain)

PREDICATEnonrel_widen_elem/4

Usage:`nonrel_widen_elem(AbsInt,E1,E2,EW)`

EW is the *widening* of E1 and E2.

(implement in derived domain)

PREDICATEnonrel_amgu/5

Usage:`nonrel_amgu(AbsInt,Term1,Term2,ASub0,NASub)`

NASub is the abstract unification of Term1 and Term2, with ASub0 an abstract substitution that represents the state of both terms.

(implement in derived domain)

*The following properties should hold at call time:*

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

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

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

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

(`var/1`)NASub is a free variable.

PREDICATEnonrel_unknown_entry/4

Usage:`nonrel_unknown_entry(AbsInt,Sg,Vars,Call)`

Gives the ``top'' value for a given set of variables Vars, resulting in abstract constraint Call.

*The following properties should hold at call time:*

(`nonvar/1`)AbsInt 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`)Vars is currently a term which is not a free variable.

(`var/1`)Call is a free variable.

(`atm/1`)AbsInt is an atom.

(`cgoal/1`)Sg is a term which represents a goal, i.e., an atom or a structure.

(`list/1`)Vars is a list.

(`term/1`)Call is any term.

PREDICATEnonrel_abs_sort/2

PREDICATEnonrel_project/5

Usage:`nonrel_project(Sg,Vars,HvFv_u,ASub,Proj)`

Proj is the result of eliminating from ASub all X/Value such that X is not in 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.

(`var/1`)Proj is a free variable.

(`term/1`)Sg is any term.

(`list/1`)Vars is a list.

(`list/1`)HvFv_u is a list.

(`term/1`)ASub is any term.

(`term/1`)Proj is any term.

PREDICATEnonrel_call_to_entry/10

Usage:`nonrel_call_to_entry(AbsInt,Sv,Sg,Hv,Head,K,Fv,Proj,Entry,ExtraInfo)`

It obtains the abstract substitution Entry which results from adding the abstraction of Sg = Head to Proj, later projecting the resulting substitution onto Hv.

In the general case, the steps are:

- Add to Proj the variables of Hv with a ``top'' value.
- Perform the abstract unification of Sg and Head.
- Add to the unification the variables of Fv with a ``top'' value.
- Project to the variables in Hv and Fv.

*The following properties should hold at call time:*

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

(`var/1`)Entry is a free variable.

(`var/1`)ExtraInfo is a free variable.

(`atm/1`)AbsInt is an atom.

(`list/1`)Sv is a list.

(`cgoal/1`)Sg is a term which represents a goal, i.e., an atom or a structure.

(`list/1`)Hv is a list.

(`cgoal/1`)Head is a term which represents a goal, i.e., an atom or a structure.

(`term/1`)K is any term.

(`list/1`)Fv is a list.

(`term/1`)Proj is any term.

(`term/1`)Entry is any term.

(`term/1`)ExtraInfo is any term.

PREDICATEnonrel_exit_to_prime/8

Usage:`nonrel_exit_to_prime(AbsInt,Sg,Hv,Head,Sv,Exit,ExtraInfo,Prime)`

*The following properties should hold at call time:*

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

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

(`var/1`)ExtraInfo is a free variable.

(`var/1`)Prime is a free variable.

(`atm/1`)AbsInt is an atom.

(`list/1`)Sg is a list.

(`list/1`)Hv is a list.

(`cgoal/1`)Head is a term which represents a goal, i.e., an atom or a structure.

(`cgoal/1`)Sv is a term which represents a goal, i.e., an atom or a structure.

(`term/1`)Exit is any term.

(`term/1`)ExtraInfo is any term.

(`term/1`)Prime is any term.

PREDICATEnonrel_compute_lub/3

Usage:`nonrel_compute_lub(AbsInt,ListASub,Lub)`

Lub is the *least upper bound* of the list of abstract substitutions ListASub.

PREDICATEnonrel_extend/6

Usage:`nonrel_extend(AbsInt,Sg,Prime,Sv,Call,Succ)`

*The following properties should hold at call time:*

(`nonvar/1`)AbsInt 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`)Prime is currently a term which is not a free variable.

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

(`var/1`)Succ is a free variable.

(`atm/1`)AbsInt is an atom.

(`term/1`)Sg is any term.

(`term/1`)Prime is any term.

(`list/1`)Sv is a list.

(`term/1`)Call is any term.

(`term/1`)Succ is any term.

PREDICATEnonrel_call_to_success_fact/10

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

Specialized version of `call_to_entry/9` + `exit_to_prime/7` + `extend/4` for facts

*The following properties should hold at call time:*

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

(`var/1`)Prime is a free variable.

(`var/1`)Succ is a free variable.

(`atm/1`)AbsInt is an atom.

(`cgoal/1`)Sg is a term which represents a goal, i.e., an atom or a structure.

(`list/1`)Hv is a list.

(`cgoal/1`)Head is a term which represents a goal, i.e., an atom or a structure.

(`list/1`)K is a list.

(`term/1`)Sv is any term.

(`term/1`)Call is any term.

(`term/1`)Proj is any term.

(`term/1`)Prime is any term.

(`term/1`)Succ is any term.

PREDICATEnonrel_special_builtin/6

Usage:`nonrel_special_builtin(AbsInt,SgKey,Sg,Subgoal,Type,Condvars)`

This predicate needs to be implemented by the user.

*The following properties should hold at call time:*

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

(`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`)Type is a free variable.

(`var/1`)Condvars is a free variable.

(`atm/1`)AbsInt is an atom.

(`predname/1`)SgKey is a predicate name.

(`cgoal/1`)Sg is a term which represents a goal, i.e., an atom or a structure.

(`cgoal/1`)Subgoal is a term which represents a goal, i.e., an atom or a structure.

(`atm/1`)Type is an atom.

(`term/1`)Condvars is any term.

PREDICATEnonrel_success_builtin/7

Usage:`nonrel_success_builtin(AbsInt,Sv_uns,Type,Condv,HvFv_u,Call,Succ)`

Obtains the success for some particular builtins.

*The following properties should hold at call time:*

(`nonvar/1`)AbsInt 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`)Type is currently a term which is not a free variable.

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

(`var/1`)Succ is a free variable.

(`atm/1`)AbsInt is an atom.

(`term/1`)Sv_uns is any term.

(`atm/1`)Type is an atom.

(`term/1`)Condv is any term.

(`term/1`)HvFv_u is any term.

(`term/1`)Call is any term.

(`term/1`)Succ is any term.

PREDICATEnonrel_call_to_success_builtin/7

Usage:`nonrel_call_to_success_builtin(AbsInt,SgKey,Sg,Sv,Call,Proj,Succ)`

Handles those builtins for which computing Proj is easier than Succ. Currently only builtins `=/2` and `==/2` are implemented. More builtins can be added by the user.

*The following properties should hold at call time:*

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

(`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.

(`var/1`)Succ is a free variable.

(`atm/1`)AbsInt is an atom.

(`predname/1`)SgKey is a predicate name.

(`cgoal/1`)Sg is a term which represents a goal, i.e., an atom or a structure.

(`list/1`)Sv is a list.

(`term/1`)Call is any term.

(`term/1`)Proj is any term.

(`term/1`)Succ is any term.

PREDICATEnonrel_input_user_interface/6

Usage:`nonrel_input_user_interface(AbsInt,InputUser,Qv,ASub,Sg,MaybeCallASub)`

Obtains the abstract substitution from the native properties found in the user supplied info.

*The following properties should hold at call time:*

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

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

PREDICATEnonrel_input_interface/5

Usage:`nonrel_input_interface(AbsInt,Prop,Kind,Struc0,Struc1)`

Adds native property Prop to the structure accumulating the properties relevant to this domain.

*The following properties should hold at call time:*

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

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

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

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

PREDICATEnonrel_asub_to_native/6

Usage:`nonrel_asub_to_native(AbsInt,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`)AbsInt is currently a term which is not a free variable.

(`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.

(`var/1`)ASub_user is a free variable.

(`var/1`)Comps is a free variable.

(`atm/1`)AbsInt is an atom.

(`term/1`)ASub is any term.

(`term/1`)Qv is any term.

(`term/1`)OutFlag is any term.

(`term/1`)ASub_user is any term.

(`term/1`)Comps is any term.

PREDICATEnonrel_unknown_call/5

Usage:`nonrel_unknown_call(AbsInt,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`)AbsInt 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`)Vars is currently a term which is not a free variable.

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

(`var/1`)Succ is a free variable.

(`atm/1`)AbsInt is an atom.

(`cgoal/1`)Sg is a term which represents a goal, i.e., an atom or a structure.

(`list/1`)Vars is a list.

(`term/1`)Call is any term.

(`term/1`)Succ is any term.

PREDICATEnonrel_less_or_equal/3

Usage:`nonrel_less_or_equal(AbsInt,ASub0,ASub1)`

Succeeds if ASub1 is more general or equal to ASub0. it is assumed the two abstract substitutions are defined on the same variables

*The following properties should hold at call time:*

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

(`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.

(`atm/1`)AbsInt is an atom.

(`term/1`)ASub0 is any term.

(`term/1`)ASub1 is any term.

PREDICATEnonrel_glb/4

Usage:`nonrel_glb(AbsInt,ASub0,ASub1,Glb)`

Glb is the great lower bound of ASub0 and ASub1, two substitutions that describe the same set of variables.

*The following properties should hold at call time:*

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

(`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.

(`var/1`)Glb is a free variable.

(`atm/1`)AbsInt is an atom.

(`list/1`)ASub0 is a list.

(`list/1`)ASub1 is a list.

(`var/1`)Glb is a free variable.

PREDICATEnonrel_identical_abstract/2

PREDICATEnonrel_widen/4

Usage:`nonrel_widen(AbsInt,Asub1,ASub2,WAsub)`

PREDICATEnonrel_widencall/4

Usage:`nonrel_widencall(AbsInt,Asub1,ASub2,WAsub)`

*Application modules:*`preprocess_flags`,`domains`.*System library modules:*`sets`,`sort`,`terms_check`,`terms_vars`.*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`,`regtypes`,`basicmodes`,`aidomain`.

Generated with LPdoc using Ciao