Consider the definition of a constraint C containing a
propagating indexical X in
R. Let
TV(X,C,S) denote the set of values for X that can make
C true in some ground extension of the store S.
Then the indexical should obey the following coding rules:
If the coding rules are observed, S(R) can be proven to contain
TV(X,C,S) for all stores in which R is monotone. Hence
it is natural for the implementation to wait until R becomes
monotone before admitting the propagating indexical for execution. The
execution of X in
R thus involves the following:
::
S(R) is
added to the store (X is pruned), and the indexical
suspends, unless R is ground in S, in which case
C is detected as entailed.
A propagating indexical is scheduled for execution as follows:
dom(
Y)
or card(
Y)
in R has been updated
min(
Y)
in R has been updated
max(
Y)
in R has been updated