Node:Execution of Checking Indexicals, Next:Goal Expanded Constraints, Previous:Execution of Propagating Indexicals, Up:Defining Primitive Constraints
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:
If the coding rules are observed, 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:
A checking indexical is scheduled for execution as follows:
dom(Y)
or card(Y)
in R has been pruned
min(Y)
in R has been increased
max(Y)
in R has been decreased