☰

Intervals (abstract 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.


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.

Usage and interface

  • Library usage:
    :- use_module(domain(nonrel_intervals)).

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.

Documentation on internals

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)

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

        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)

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

        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)

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

        PREDICATEnonrel_widen_elem/4

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

        EW is the widening of E1 and E2.

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

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

        PREDICATEnonrel_abs_sort/2

        Usage:nonrel_abs_sort(Asub,Asub_s)

        It sorts the set of X/Values in Asub obtaining Asub_s

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

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

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

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

        PREDICATEnonrel_compute_lub/3

        Usage:nonrel_compute_lub(AbsInt,ListASub,Lub)

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

        • The following properties should hold at call time:
          (nonvar/1)AbsInt is currently a term which is not a free variable.
          (nonvar/1)ListASub is currently a term which is not a free variable.
          (atm/1)AbsInt is an atom.
          (list/1)ListASub is a list.
          (term/1)Lub is any term.
        • The following properties should hold upon exit:
          (nonvar/1)Lub is currently a term which is not a free variable.

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

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

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

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

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

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

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

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

        PREDICATEnonrel_identical_abstract/2

        Usage:nonrel_identical_abstract(ASub1,ASub2)

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

        PREDICATEnonrel_widen/4

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

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

        PREDICATEnonrel_widencall/4

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

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

        Documentation on imports

        This module has the following direct dependencies:
        Generated with LPdoc using Ciao