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 end

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