<< Prev | - Up - | Next >> |
The operational semantics of some propagators is based on constructive disjunction which allows to lift common information from clauses of a disjunction.
In Oz, constructive disjunction is available through a syntax like the one for nondistributable disjunction or ... end
which uses the keyword condis
instead or or
.
Constructive disjunction adopts the operational semantics of the nondistributable disjunction concerning entailment and failure of clauses. It enriches 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 denote the local stores of the n clauses. Then the strongest constraint C consisting of basic constraints
with
for
is lifted and added to S.
As an example consider the store X, Y
and
condis X + 9 =<: Y
[] Y + 9 =<: X
end
Constructive disjunction narrows the domains of X
and Y
to .
<< Prev | - Up - | Next >> |