) Operational Model
We now precisely but informally define the operational model of CLP( ).
A goal G is written in the form C, D ?- E where
C is a satisfiable collection of constraints,
D a collection of nonlinear constraints
called the delayed constraints, and
E a sequence of atoms and constraints.
In what follows, we define how such a goal
is reduced into another in the context of an ongoing derivation.
In reducing a goal C, D ?- E,
CLP( ) either selects an element from E,
call this a forward reduction, or selects a
constraint from D, call this
a wakeup reduction. Initially,
C and D are empty, and CLP( ) attempts to
make a forward reduction.
Forward reductions
If E is empty, then we say that the goal is terminal, and no more reduction of the goal is possible. If D is also empty, then the derivation is successful; otherwise, the derivation is conditionally successful (depending on the nonlinear constraints).
Now consider the case where E is nonempty; let E0 denote the first element of E and let E2 denote the remaining subsequence of E.
If E0 is an atom, then E0 will be selected for atom reduction in the manner described above. First, an appropriate program rule will be selected. The atom and rule head will then be matched, giving rise to a collection of constraints, which we will write as M1 & M2 where M1 consists only of linear constraints and M2 only of nonlinear ones. The new goal consists of (a) C & M1 in its first component; (b) D & M2 in its second component, and (c) the body of the rule and E2, sequenced in this order, in its third component.
If E0 is a linear constraint, then the reduced goal is C & E0, D ?- E2 providing C & E0 is satisfiable; otherwise there is no reduced goal and the derivation is finitely failed.
Finally, if E0 is a nonlinear constraint, then the reduced goal is C, D & E0 ?- E2. That is, the constraint E0 is simply delayed.
Wakeup reductions
Let the goal at hand be C, D ?- E. This reduction step starts by considering whether there is a delayed constraint D0 in D which is in fact linear. That is, C implies that D0 is equivalent to a linear constraint. If there is no such delayed constraint, then no reduction is performed.
Otherwise, consider the case in which C is inconsistent with this linear constraint. Here reduction is not possible and a finitely failed derivation is obtained. However, if C is consistent with the linear constraint, then the reduced goal is C & D0, D2 ?- E where D2 is result of deleting D0 from D.