diff --git a/chapters/3_rewriting.tex b/chapters/3_rewriting.tex index 6aa71f3..53cad0c 100644 --- a/chapters/3_rewriting.tex +++ b/chapters/3_rewriting.tex @@ -122,7 +122,7 @@ and where expressions have \mzninline{par} type. A \nanozinc\ program, defined in \cref{fig:4-nzn-syntax}, is simply a list of variable declaration and constraints in the form of calls. The syntax -``\texttt{└──}'' will be used to track dependent constraints (this will be +``\texttt{↳}'' will be used to track dependent constraints (this will be explained in detail in \cref{sec:4-nanozinc}, for now you can ignore them). \begin{figure} @@ -138,7 +138,7 @@ explained in detail in \cref{sec:4-nanozinc}, for now you can ignore them). ::= ".." | \alt "bool" | "int" | "float" | "set of int" - ::= "└──" + ::= "↳" \end{grammar} \caption{\label{fig:4-nzn-syntax}Syntax of \nanozinc{}.} \end{figure} @@ -384,7 +384,7 @@ can only define the function result. var -10..10: x; var -10..10: y; var int: z; - └── constraint int_abs(x, z); + ↳ constraint int_abs(x, z); constraint int_gt(z, y); \end{nzn} @@ -457,7 +457,7 @@ considered primitives, and as such simply need to be transferred into the \bigskip \begin{prooftree} \hypo{\Sem{\(\mathbf{X}\)}{\Prog, \{ t : x \} \cup{} \Env} \Rightarrow \tuple{x, \{ t: x \} \cup{} \Env'}} - \infer1[(Item0)]{\Sem{\(\epsilon{} \mid{} \mathbf{X}\)}{\Prog, \{ t: x \}\cup{}\Env, \Ctx} \Rightarrow{} \tuple{x, \{ t: x_{\texttt{~└──~}} \Ctx{} \} \cup{} \Env'}} + \infer1[(Item0)]{\Sem{\(\epsilon{} \mid{} \mathbf{X}\)}{\Prog, \{ t: x \}\cup{}\Env, \Ctx} \Rightarrow{} \tuple{x, \{ t: x \texttt{~↳~} \Ctx{} \} \cup{} \Env'}} \end{prooftree} \\ \bigskip \begin{prooftree} @@ -509,7 +509,7 @@ notation. \centering \begin{prooftree} \hypo{x \in \langle \text{ident} \rangle} - \hypo{\{t: x_{\texttt{~└──~}} \phi\ \} \in \Env} + \hypo{\{t: x \texttt{~↳~} \phi\ \} \in \Env} \infer2[(IdX)]{\Sem{\(x\)}{\Prog, \Env} \Rightarrow{} \tuple{x, \Env}} \end{prooftree} \\ \bigskip @@ -623,7 +623,7 @@ therefore equisatisfiable with the original model. Consider now the case where a variable in \nanozinc\ is only used in its own auxiliary definitions (the constraints directly succeeding the declaration -prepended by \texttt{└── }). +prepended by \texttt{↳}). \begin{example}\label{ex:4-absreif} The following is a slight variation on the \minizinc\ fragment in @@ -648,9 +648,9 @@ prepended by \texttt{└── }). var -10..10: x; var -10..10: y; var int: z; - └── constraint int_abs(x, z); + ↳ constraint int_abs(x, z); var bool: b; - └── constraint int_gt_reif(z, y, b); + ↳ constraint int_gt_reif(z, y, b); constraint bool_or(b, c); \end{nzn} @@ -802,9 +802,9 @@ corresponding \nanozinc\ code looks like this: \begin{nzn} var int: x; - └── constraint f_rel(a, x); + ↳ constraint f_rel(a, x); var int: y; - └── constraint g_rel(b, y); + ↳ constraint g_rel(b, y); constraint int_eq(x, y); \end{nzn} @@ -821,7 +821,7 @@ resulting \nanozinc\ looks like this: \begin{nzn} var int: x; - └── constraint f_rel(a, x); + ↳ constraint f_rel(a, x); constraint g_rel(x, y); constraint int_eq(x, y); \end{nzn} @@ -1035,9 +1035,9 @@ operators. For example the evaluation of the linear constraint \mzninline{x + var int: y; var int: z; var int: i1; - └── constraint int_times(y, 2); + ↳ constraint int_times(y, 2); var int: i2; - └── constraint int_plus(x, i1); + ↳ constraint int_plus(x, i1); constraint int_le(i2, z); \end{nzn}