Add example from the half-reification section into the handling of undefined expressions

This commit is contained in:
Jip J. Dekker 2021-05-20 11:15:51 +10:00
parent ca60459058
commit 1946918038
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3

View File

@ -491,7 +491,26 @@ both contexts.
\label{subsec:back-mzn-partial}
Some expressions in the \cmls\ do not always have a well-defined result.
Examples of such expressions in \minizinc\ are:
\begin{example}\label{ex:back-undef}
Consider the following ``complex constraint''
\begin{mzn}
constraint i <= 4 -> a[i] * x >= 6;
\end{mzn}
which requires that if \mzninline{i} takes a value less or equal to four, then
the value in the \texttt{i}\(^{th}\) position of array \mzninline{a}
multiplied by \mzninline{x} must be at least 6.
Suppose the array \texttt{a} has index set \mzninline{1..5}, but \texttt{i}
takes the value \texttt{7}. The constraint \mzninline{element(i, a, t1)} will
fail and no solution will be found. However, intuitively if \mzninline{i = 7}
the constraint should be trivially true.
\end{example}
Part of the semantics of a \cmls\ is the choice as to how to treat these partial
functions. Examples of such expressions in \minizinc\ are:
\begin{itemize}
\item Division (or modulus) when the divisor is zero: