A simple intervals abstract domain (non relational) derived from nonrel_base.pl.
X is the representation of “top” in the abstract domain.
X is the representation of “bot” in the abstract domain.
X is the abstraction of a free variable in the abstract domain.
Succeeds if E1 is smaller than E2.
EG is the greatest lower bound of E1 and E2.
EL is the least upper bound of E1 and E2.
EW is the widening of E1 and E2.
NASub is the abstract unification of Term1 and Term2, with ASub0 an abstract substitution that represents the state of both terms.
Gives the “top” value for a given set of variables Vars, resulting in abstract constraint Call.
Proj is the result of eliminating from ASub all X/Value such that X is not in Vars
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:
Lub is the least upper bound of the list of abstract substitutions ListASub.
Specialized version of call_to_entry/9 + exit_to_prime/7 + extend/4 for facts
Obtains the success for some particular builtins.
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.
Obtains the abstract substitution from the native properties found in the user supplied info.
Adds native property Prop to the structure accumulating the properties relevant to this domain.
It translates an internal abstract constraint into something friendly for the user.
Gives the “top” value for the variables involved in a literal whose definition is not present, and adds this top value to Call
Succeeds if ASub1 is more general or equal to ASub0. it is assumed the two abstract substitutions are defined on the same variables
Glb is the great lower bound of ASub0 and ASub1, two substitutions that describe the same set of variables.