etermsvar: eterms with variables (abstract domain)

Author(s): Claudio Vaucheret, Francisco Bueno, Alejandro Serrano (etermsvar), Ciao Development Team.

This module implements an (experimental) variant of the eterms domain with vr elements in the lattice.

Usage and interface

Documentation on exports

No further documentation available for this predicate.

Usage:etermsvar_compute_lub(ListASub,Lub)

  • The following properties should hold at call time:
    (nonvar/1)ListASub is currently a term which is not a free variable.
    (var/1)Lub is a free variable.
    (list/2)ListASub is a list of absus.
    (absu/1)Lub is an abstract substitution

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

Usage:etermsvar_widen(Prime0,Prime1,NewPrime)

  • The following properties should hold at call time:
    (nonvar/1)Prime0 is currently a term which is not a free variable.
    (nonvar/1)Prime1 is currently a term which is not a free variable.
    (var/1)NewPrime is a free variable.
    (absu/1)Prime0 is an abstract substitution
    (absu/1)Prime1 is an abstract substitution
    (absu/1)NewPrime is an abstract substitution

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

  • 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.
    (var/1)Entry is a free variable.
    (var/1)ExtraInfo is a free variable.
    (term/1)Sv is any term.
    (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.
    (absu/1)Proj is an abstract substitution
    (absu/1)Entry is an abstract substitution
    (extrainfo/1)extrainfo(ExtraInfo)

Usage:etermsvar_exit_to_prime(Sg,Hv,Head,Sv,Exit,ExtraInfo,Prime)

  • 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.
    (var/1)ExtraInfo is a free variable.
    (var/1)Prime is a free variable.
    (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.
    (absu/1)Exit is an abstract substitution
    (extrainfo/1)extrainfo(ExtraInfo)
    (absu/1)Prime is an abstract substitution

Usage:etermsvar_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.
    (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.
    (absu/1)Asub is an abstract substitution
    (absu/1)Proj is an abstract substitution

Usage:etermsvar_abs_sort(Asub,Asub_s)

  • The following properties should hold at call time:
    (nonvar/1)Asub is currently a term which is not a free variable.
    (var/1)Asub_s is a free variable.
    (absu/1)Asub is an abstract substitution
    (absu/1)Asub_s is an abstract substitution

Usage:etermsvar_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.
    (var/1)Succ is a free variable.
    (term/1)Sg is any term.
    (absu/1)Prime is an abstract substitution
    (list/1)Sv is a list.
    (absu/1)Call is an abstract substitution
    (absu/1)Succ is an abstract substitution

Usage:etermsvar_less_or_equal(ASub0,ASub1)

  • 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.
    (absu/1)ASub0 is an abstract substitution
    (absu/1)ASub1 is an abstract substitution

Usage:etermsvar_glb(ASub0,ASub1,Glb)

  • 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.
    (var/1)Glb is a free variable.
    (absu/1)ASub0 is an abstract substitution
    (absu/1)ASub1 is an abstract substitution
    (absu/1)Glb is an abstract substitution

No further documentation available for this predicate.

Usage:etermsvar_unknown_entry(Sg,Qv,Call)

  • 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.
    (var/1)Call is a free variable.
    (cgoal/1)Sg is a term which represents a goal, i.e., an atom or a structure.
    (list/1)Qv is a list.
    (absu/1)Call is an abstract substitution

Usage:etermsvar_empty_entry(Sg,Vars,Entry)

  • 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.
    (var/1)Entry is a free variable.
    (cgoal/1)Sg is a term which represents a goal, i.e., an atom or a structure.
    (list/1)Vars is a list.
    (absu/1)Entry is an abstract substitution

Usage:etermsvar_unknown_call(Sg,Vars,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)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.
    (cgoal/1)Sg is a term which represents a goal, i.e., an atom or a structure.
    (list/1)Vars is a list.
    (absu/1)Call is an abstract substitution
    (absu/1)Succ is an abstract substitution

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

  • 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.
    (var/1)Prime is a free variable.
    (var/1)Succ is a free variable.
    (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)Sv is a list.
    (absu/1)Call is an abstract substitution
    (absu/1)Proj is an abstract substitution
    (absu/1)Prime is an abstract substitution
    (absu/1)Succ is an abstract substitution

Usage:etermsvar_special_builtin(SgKey,Sg,Subgoal,Type,Condvars)

  • 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)Type is a free variable.
    (var/1)Condvars is a free variable.

Usage:etermsvar_success_builtin(Type,Sv_uns,Condvars,HvFv_u,Call,Succ)

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

No further documentation available for this predicate.

Usage:etermsvar_call_to_success_builtin(SgKey,Sg,Sv,Call,Proj,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.
    (var/1)Succ is a free variable.

No further documentation available for this predicate.

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

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

No further documentation available for this predicate.

No further documentation available for this predicate.

Usage:etermsvar_output_interface(ASub,Output)

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

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

No further documentation available for this predicate.

Documentation on multifiles

PREDICATEaidomain/1
No further documentation available for this predicate. The predicate is multifile.

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.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

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.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

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.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.

No further documentation available for this predicate. The predicate is multifile.