Dekker1/dekker-phd-thesis
Archived
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Change attaching symbol to one available in the font

Browse Source
This commit is contained in:
Jip J. Dekker 2021-05-19 13:29:46 +10:00
parent 1fe8190c14
commit ca60459058
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
1 changed files with 13 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
chapters/3_rewriting.tex
View File

@ -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).
<nzn-dom> ::= <constant> ".." <constant> | <constant>
\alt "bool" | "int" | "float" | "set of int"
<nzn-bind> ::= "└──" <nzn-con>
<nzn-bind> ::= "↳" <nzn-con>
\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}