5.2 The Concept of Constructive Disjunction

The operational semantics of some propagators is based on the concept of constructive disjunction which allows to lift common information from different clauses of a disjunctive constraint.

Constructive disjunction is not available as program combinator in Oz. Anyway, we use it in Oz program fragments (by the keyword condis) to describe the operational semantics of certain propagators. For example such propagators are FD.tasksOverlap and FD.disjoint.

Constructive disjunction adopts the operational semantics of the nondistributable disjunction of Oz (or ... end) concerning entailment and failure of clauses. Furthermore, it extends the semantics as follows: Assume a disjunction with n clauses and let S be the constraint store of the computation space in which it resides. Let S_1,\ldots,S_n denote the local stores of the n clauses. Then the strongest constraint C consisting of basic constraints X\in D with S_i\models C for 1\leq i
\leq n is lifted and added to S.

As an example consider the store X, Y\in\{0,\ldots,10\} and

condis X + 9 =<: Y
[] Y + 9 =<: X

Constructive disjunction narrows the domains of X and Y to \{0,1,9,10\}.

Denys Duchier, Leif Kornstaedt, Martin Homik, Tobias Müller, Christian Schulte and Peter Van Roy
Version 1.4.0 (20080702)