\documentclass[a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage{fullpage}
\setlength{\topmargin}{0mm}
\usepackage{amsmath,amssymb,stmaryrd}
\usepackage{enumitem}
\setlist[enumerate,1]{label={\alph*)}}
\usepackage[retainorgcmds]{IEEEtrantools}
\usepackage{tikz}

\newcommand{\Z}{\mathbb{Z}}
\newcommand{\D}{\mathbb{D}}
\newcommand{\symbeq}{\odot}
\newcommand{\symblt}{\olessthan}
\newcommand{\symbgt}{\ogreaterthan}
\newcommand{\symble}{\ominus}
\newcommand{\symbge}{\oplus}
\newcommand{\symtop}{\top}
\newcommand{\symbot}{\bot}
\newcommand{\aplus}{\mathop{+^\sharp}}
\newcommand{\amult}{\mathop{\ast^\sharp}}

\title{Solutions to Exercise Sheet 4}   

\author{Your Name}
  
\begin{document}

\maketitle

\section{Constant Propagation}
\begin{enumerate}
  %(The symbols for join & meet are \sqcup and \sqcap.)
  \item The constraint system:
    \begin{align*}
      x_0 &\sqsupseteq \top \\
      x_1 &\sqsupseteq 
        \begin{cases}
          \bot & \text{if $?$} \\
          ?    & \text{otherwise}
        \end{cases} \\
      x_2 &\sqsupseteq 
        \begin{cases}
          \bot & \text{if $?$} \\
          ?    & \text{otherwise}
        \end{cases} \\
      x_3 &\sqsupseteq ? \\
      x_3 &\sqsupseteq ? \\
    \end{align*}
  \item $x_0 = ?, x_1 = ?, x_2 = ?, x_3 = ?$.
\end{enumerate}

\section{Assertion Checking}
\begin{enumerate}
  \item The values at each program point:
    \begin{equation*}
      \begin{array}[c]{c|c|c}
          & x    & y \\ \hline
        0 & \top & \top \\
        1 & ?    & ?    \\
        2 & ?    & ?    \\
        3 & ?    & ?    \\
        4 & ?    & ?    \\
      \end{array}
    \end{equation*}
  \item WP computation starting from $x + y = 8$ at $4$:
    \begin{align*}
      \phi_4 &= \{ x + y = 8 \} \\
      \phi_3 &= ? \\
      \phi_2 &= ? \\
      \phi_1 &= ? \\
      \phi_0 &= ? \\
    \end{align*}
\end{enumerate}

\section{Value Domain}

\begin{enumerate}
\item 
We define the lattice $\D = \{ \bot, \symblt, \symble, \symbeq, \symbge,
  \symbgt, \top \}$, where the ordering and the concretization is as follows:\\
\begin{minipage}[c]{0.4\linewidth}\centering
  \begin{tikzpicture}[node distance=2cm]
  \node (T) {$\top$};
  \node (1) [below left of=T]  {$?$};
  \node (2) [below right of=T] {$?$};
  \node (3) [below left of=1]  {$?$};
  \node (4) [below right of=1] {$?$};
  \node (5) [below right of=2] {$?$};
  \node (B) [below of=4,yshift=1cm] {$\bot$};

  \path[-] 
    (B) edge (3)
    (B) edge (4)
    (B) edge (5)
    (3)  edge (1)
    (4)  edge (1)
    (4)  edge (2)
    (5)  edge (2)
    (1)  edge (T)
    (2)  edge (T)
  ;
\end{tikzpicture}
\end{minipage}
\begin{minipage}[c]{0.6\linewidth}
  \begin{align*}
    \gamma(\top) &= \mathbb Z \\
    \gamma(\symble) &= \{ x \mid x \leq 0 \} \\
    \gamma(\symbge) &= \{ x \mid x \geq 0 \} \\
    \gamma(\symblt) &= \{ x \mid x < 0 \} \\
    \gamma(\symbeq) &= \{ x \mid x = 0 \} \\
    \gamma(\symbgt) &= \{ x \mid x > 0 \}\\
    \gamma(\bot) &= \emptyset \\
  \end{align*}
\end{minipage}
\item The addition \& multiplication tables:
\begin{equation*}
  \begin{array}[c]{c|cccccc}
    +^\sharp & \symblt & \symble & \symbeq & \symbge & \symbgt & \symtop \\
    \hline                                                     
    \symblt  &         &         &         &         &         &         \\
    \symble  &         &         &         &         &         &         \\
    \symbeq  &         &         &         &         &         &         \\
    \symbge  &         &         &         &         &         &         \\
    \symbgt  &         &         &         &         &         &         \\
    \symtop  &         &         &         &         &         &         \\
  \end{array}
  \qquad
  \begin{array}[c]{c|cccccc}
    \ast^\sharp & \symblt & \symble & \symbeq & \symbge & \symbgt & \symtop \\
    \hline                                              
    \symblt     &         &         &         &         &         &         \\
    \symble     &         &         &         &         &         &         \\
    \symbeq     &         &         &         &         &         &         \\
    \symbge     &         &         &         &         &         &         \\
    \symbgt     &         &         &         &         &         &         \\
    \symtop     &         &         &         &         &         &         \\
  \end{array}\\[1em]
\end{equation*}
\end{enumerate}

\end{document}
