From 2a17d4066ae336583ca268a8ba7cd4d442f1613d Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Mon, 8 Nov 2021 19:50:07 +1100 Subject: [PATCH] Fix last errors spotted by Guido --- .vscode/ltex.dictionary.en-GB.txt | 1 + .vscode/ltex.hiddenFalsePositives.en-GB.txt | 9 +++++++++ assets/listing/rew_elem_safe.mzn | 2 +- chapters/3_rewriting.tex | 2 +- chapters/4_half_reif.tex | 6 +++--- 5 files changed, 15 insertions(+), 5 deletions(-) diff --git a/.vscode/ltex.dictionary.en-GB.txt b/.vscode/ltex.dictionary.en-GB.txt index 26736c6..6fe6aa4 100644 --- a/.vscode/ltex.dictionary.en-GB.txt +++ b/.vscode/ltex.dictionary.en-GB.txt @@ -53,3 +53,4 @@ Stuckey Schutt Banda Gange +Half-Reifications diff --git a/.vscode/ltex.hiddenFalsePositives.en-GB.txt b/.vscode/ltex.hiddenFalsePositives.en-GB.txt index 7b9e072..f18bf77 100644 --- a/.vscode/ltex.hiddenFalsePositives.en-GB.txt +++ b/.vscode/ltex.hiddenFalsePositives.en-GB.txt @@ -382,3 +382,12 @@ {"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\QThe function [fontsize=]minizinc set2bool is used to transform the set decision variable into an array of Boolean variables that represent whether an element is present in the set.\\E$"} {"rule":"EN_A_VS_AN","sentence":"^\\QAn \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q graph \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q where chained implications have been removed.\\E$"} {"rule":"EN_A_VS_AN","sentence":"^\\QAn expression \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q can be \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q when every to the \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is also a if \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q is replaced by \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qscip name=SCIP, description=A well-known open source MIP \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qsicstus name=SICStus Prolog, description=A well-known implementation of the Prolog CLP language and constraint modelling environment \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qgls-opl name=optimization modelling language (OPL), description=A \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q aimed at combining the powers of mathematical programming and CP.\\E$"} +{"rule":"MORFOLOGIK_RULE_EN_GB","sentence":"^\\Qopenwbo name=OpenWBO, description=A well-known MaxSAT \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qcplex name=CPLEX, description=A well-known proprietary MIP \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q developed by IBM \\E(?:Dummy|Ina|Jimmy-)[0-9]+\\Q.,\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qaccap amaze city-position community-detection depot-placement freepizza groupsplitter kidney-exchange multi-knapsack nonogram nside rcpsp-wet road-cons roster stack-cuttingstock steelmillslab triangular\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qaccap amaze code-generator fox-geese-corn groupsplitter hrc kidney-exchange liner-sf-repositioning lot-sizing median-string multi-knapsack nside ptv rcpsp-wet-diverse rotating-workforce stack-cuttingstock steelmillslab stochastic-vrp triangular zephyrus\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qbnn-planner cabletreewiring code-generator collaborative-construction gbac hoist-benchmark is lot-sizing minimal-decision-sets p1f-pjs pentominoes pillars-and-planks racp radiation sdn-change skill-allocation soccer-computational stable-goods towerchallenge whirlpool\\E$"} +{"rule":"UPPERCASE_SENTENCE_START","sentence":"^\\Qgbac radiation steelmillslab rcpsp-wet\\E$"} diff --git a/assets/listing/rew_elem_safe.mzn b/assets/listing/rew_elem_safe.mzn index 84ae1f8..f55ac5c 100644 --- a/assets/listing/rew_elem_safe.mzn +++ b/assets/listing/rew_elem_safe.mzn @@ -12,5 +12,5 @@ function tuple(var bool, var int): element_safe( % Otherwise, give xs the value m instead to avoid a free variable constraint not total -> xs = m; % element constraint that is guaranteed to be total - tuple(var bool, var int): res = (total, element(a, xs)); + tuple(var bool, var int): ret = (total, element(a, xs)); } in ret; diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex index 65e11db..346b279 100644 --- a/chapters/3_rewriting.tex +++ b/chapters/3_rewriting.tex @@ -72,7 +72,7 @@ The core of the syntax of \microzinc{} is defined in \cref{fig:rew-uzn-syntax}. Function declarations without an expression body are used to mark functions that are \gls{native} to the target \solver{}. We have omitted the definitions of \syntax{} and \syntax{}, which can be assumed to be the same as the definition of \syntax{} and \syntax{} in the \minizinc{} grammar, see \cref{ch:minizinc-grammar}. While we omit the typing rules here for space reasons, we will assume that in well-typed \microzinc{} programs conditions of expressions are \parameters{}. -This means that the where conditions \syntax{} in \glspl{comprehension}, the conditions \syntax{} in \gls{conditional} expressions, and the \syntax{} index in \gls{array} accesses must have parametric type. +This means that the where conditions \syntax{} in \glspl{comprehension}, the conditions \syntax{} in \gls{conditional} expressions, and the \syntax{} index in \gls{array} accesses must have \mzninline{par} type. In \minizinc{} the use of \variables{} in these positions is allowed, and these expressions are rewritten to function calls. We will discuss how the same transformation takes place when translating \minizinc{} to \microzinc{}. diff --git a/chapters/4_half_reif.tex b/chapters/4_half_reif.tex index 9de8b56..0fd6cc1 100644 --- a/chapters/4_half_reif.tex +++ b/chapters/4_half_reif.tex @@ -65,7 +65,7 @@ A possible downside of \gls{half-reif} is thus that its \gls{cvar} might need to \end{mzn} 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{}. - Therefore, all \glspl{sol} is still a \gls{sol} when \mzninline{y = 5} (or \mzninline{x = 5}) is replaced by \true{}. + Therefore, all \glspl{sol} are still \glspl{sol} when \mzninline{y = 5} (or \mzninline{x = 5}) is replaced by \true{}. Consequently, this means using \gls{half-reif} is \gls{eqsat}. \Gls{rewriting} using \gls{half-reif} will result in the following model. @@ -90,7 +90,7 @@ Since Boolean expressions in \minizinc{} can be used in, for example, integer ex \end{mzn} Making the left-hand side of the \constraint{} larger will only ever help satisfy the \constraint{}. - This means that all \glspl{sol} will still be \glspl{sol} if any expression \mzninline{x = 5} is replaced by \true{}. + This means that all \glspl{sol} will still be \glspl{sol} if any expression \mzninline{x = 5} is replaced by \true{}. 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. \end{example} @@ -247,7 +247,7 @@ For Booleans appearing in \posc{} context we can make the \gls{propagator} of th Similarly, in \negc{} context we can make the \gls{propagator} \mzninline{b -> pred(@...@)} run at the lowest priority. This means that the \glspl{cvar} are still \gls{fixed} at the same time, but there is less overhead. -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. +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. \section{Decomposition and Half-Reification}% \label{sec:half-decomposition}