dekker.one
+1
.vscode/ltex.dictionary.en-GB.txt
+1
.vscode/ltex.dictionary.en-GB.txt
+1
-1
assets/listing/rew_elem_safe.mzn
+1
-1
assets/listing/rew_elem_safe.mzn
···
12
12
% Otherwise, give xs the value m instead to avoid a free variable
13
13
constraint not total -> xs = m;
14
14
% element constraint that is guaranteed to be total
15
-
tuple(var bool, var int): res = (total, element(a, xs));
15
+
tuple(var bool, var int): ret = (total, element(a, xs));
16
16
} in ret;
+1
-1
chapters/3_rewriting.tex
+1
-1
chapters/3_rewriting.tex
···
72
72
Function declarations without an expression body are used to mark functions that are \gls{native} to the target \solver{}.
73
73
We have omitted the definitions of \syntax{<mzn-type-inst>} and \syntax{<ident>}, which can be assumed to be the same as the definition of \syntax{<type-inst>} and \syntax{<ident>} in the \minizinc{} grammar, see \cref{ch:minizinc-grammar}.
74
74
While we omit the typing rules here for space reasons, we will assume that in well-typed \microzinc{} programs conditions of expressions are \parameters{}.
75
-
This means that the where conditions \syntax{<exp>} in \glspl{comprehension}, the conditions \syntax{<exp>} in \gls{conditional} expressions, and the \syntax{<literal>} index in \gls{array} accesses must have parametric type.
75
+
This means that the where conditions \syntax{<exp>} in \glspl{comprehension}, the conditions \syntax{<exp>} in \gls{conditional} expressions, and the \syntax{<literal>} index in \gls{array} accesses must have \mzninline{par} type.
76
76
In \minizinc{} the use of \variables{} in these positions is allowed, and these expressions are rewritten to function calls.
77
77
We will discuss how the same transformation takes place when translating \minizinc{} to \microzinc{}.
78
78
+3
-3
chapters/4_half_reif.tex
+3
-3
chapters/4_half_reif.tex
···
65
65
\end{mzn}
66
66
67
67
However, independent of the value of \mzninline{x = 5}, if \mzninline{y = 5} takes the value \true{}, then it can never make the disjunction \false{}.
68
-
Therefore, all \glspl{sol} is still a \gls{sol} when \mzninline{y = 5} (or \mzninline{x = 5}) is replaced by \true{}.
68
+
Therefore, all \glspl{sol} are still \glspl{sol} when \mzninline{y = 5} (or \mzninline{x = 5}) is replaced by \true{}.
69
69
Consequently, this means using \gls{half-reif} is \gls{eqsat}.
70
70
\Gls{rewriting} using \gls{half-reif} will result in the following model.
71
71
···
90
90
\end{mzn}
91
91
92
92
Making the left-hand side of the \constraint{} larger will only ever help satisfy the \constraint{}.
93
-
This means that all \glspl{sol} will still be \glspl{sol} if any expression \mzninline{x = 5} is replaced by \true{}.
93
+
This means that all \glspl{sol} will still be \glspl{sol} if any expression \mzninline{x = 5} is replaced by \true{}.
94
94
Similar to \cref{ex:hr-disjunction}, the \gls{rewriting} process can thus use \glspl{half-reif} instead of \glspl{reif} for the \mzninline{x = 5} expressions.
95
95
\end{example}
96
96
···
247
247
Similarly, in \negc{} context we can make the \gls{propagator} \mzninline{b -> pred(@...@)} run at the lowest priority.
248
248
This means that the \glspl{cvar} are still \gls{fixed} at the same time, but there is less overhead.
249
249
250
-
In \cref{sec:half-experiments} we assess \glspl{propagator} implementations for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element} based on these principles.
250
+
In \cref{sec:half-experiments} we assess \gls{propagator} implementations for the \glspl{half-reif} of \mzninline{all_different} and \mzninline{element} based on these principles.
251
251
252
252
\section{Decomposition and Half-Reification}%
253
253
\label{sec:half-decomposition}