10.9.13.1 Indexicals

An indexical has the syntax X in R, where R is a set of integers valued domain expression (see below). See Syntax of Indexicals for a grammar defining indexicals and domain expressions.

Indexicals can play one of two roles: propagating indexicals are used for constraint solving, and checking indexicals are used for entailment checking.

Let S be the constraint store, X in R a propagating indexical, and D(E,S) the domain of expression E in S. When it fires, the indexical prunes the domain of X by intersecting its domain with D(R,S). When a checking indexical fires, it checks if D(X,S) is contained in D(R,S), in which case the constraint corresponding to the indexical is detected as entailed.

The domain expression R of a propagating indexical should be contracting, i.e., as the constraint store S gets narrower and narrower, D(R,S) should get smaller and smaller; otherwise, the propagator would not be contracting. Dually, the domain expression R of a checking indexicals should be expanding, i.e., as the constraint store S gets narrower and narrower, D(R,S) should get larger and larger; otherwise, the entailment check would not work. The solver analyzes each domain expressions, and if it does not fulfill the contracting or expanding property, its evaluation is suspended until enough variables have been fixed to make the property hold.