Next: , Previous: , Up: Defining Primitive Constraints   [Contents][Index]

#### 10.9.10.9 Execution of Checking Indexicals

Consider the definition of a constraint C containing a checking indexical `X in R`. Let FV(X,C,S) denote the set of values for X that can make C false in some ground extension of the store S. Then the indexical should obey the following coding rules:

• all arguments of C except X should occur in R
• if R is ground in S, S(R) = TV(X,C,S)

If the coding rules are observed, then S(R) can be proven to exclude FV(X,C,S) for all stores in which R is anti-monotone. Hence it is natural for the implementation to wait until R becomes anti-monotone before admitting the checking indexical for execution. The execution of `X in R` thus involves the following:

• If D(X,S) is contained in S(R), then none of the possible values for X can make C false, and so C is detected as entailed.
• Otherwise, if D(X,S) is disjoint from S(R) and R is ground in S, then all possible values for X will make C false, and so C is detected as disentailed.
• Otherwise, D(X,S) contains some values that could make C true and some that could make C false, and the indexical suspends.

A checking indexical is scheduled for execution as follows:

• it is evaluated initially as soon as it has become anti-monotone
• it is re-evaluated when one of the following conditions occurs:
1. the domain of X has been pruned, or X has been assigned
2. the domain of a variable Y that occurs as `dom(Y)` or `card(Y)` in R has been pruned
3. the lower bound of a variable Y that occurs as `min(Y)` in R has been increased
4. the upper bound of a variable Y that occurs as `max(Y)` in R has been decreased

Send feedback on this subject.