started with a2
authorMart Lubbers <mart@martlubbers.net>
Tue, 10 Nov 2015 07:43:32 +0000 (08:43 +0100)
committerMart Lubbers <mart@martlubbers.net>
Tue, 10 Nov 2015 07:43:32 +0000 (08:43 +0100)
23 files changed:
a1/1.tex [moved from 1.tex with 100% similarity]
a1/2.tex [moved from 2.tex with 100% similarity]
a1/3.tex [moved from 3.tex with 100% similarity]
a1/4.tex [moved from 4.tex with 100% similarity]
a1/Makefile [moved from Makefile with 100% similarity]
a1/README.md [moved from README.md with 100% similarity]
a1/ar.tex [moved from ar.tex with 100% similarity]
a1/pre.tex [moved from pre.tex with 100% similarity]
a1/src/a1.bash [moved from src/a1.bash with 100% similarity]
a1/src/a1.py [moved from src/a1.py with 100% similarity]
a1/src/a2.bash [moved from src/a2.bash with 100% similarity]
a1/src/a2.py [moved from src/a2.py with 100% similarity]
a1/src/a3.bash [moved from src/a3.bash with 100% similarity]
a1/src/a3.py [moved from src/a3.py with 100% similarity]
a1/src/a4.bash [moved from src/a4.bash with 100% similarity]
a1/src/a4.py [moved from src/a4.py with 100% similarity]
a2/1.tex [new file with mode: 0644]
a2/2.tex [new file with mode: 0644]
a2/3.tex [new file with mode: 0644]
a2/4.tex [new file with mode: 0644]
a2/Makefile [new file with mode: 0644]
a2/ar.tex [new file with mode: 0644]
a2/pre.tex [new file with mode: 0644]

diff --git a/1.tex b/a1/1.tex
similarity index 100%
rename from 1.tex
rename to a1/1.tex
diff --git a/2.tex b/a1/2.tex
similarity index 100%
rename from 2.tex
rename to a1/2.tex
diff --git a/3.tex b/a1/3.tex
similarity index 100%
rename from 3.tex
rename to a1/3.tex
diff --git a/4.tex b/a1/4.tex
similarity index 100%
rename from 4.tex
rename to a1/4.tex
similarity index 100%
rename from Makefile
rename to a1/Makefile
similarity index 100%
rename from README.md
rename to a1/README.md
similarity index 100%
rename from ar.tex
rename to a1/ar.tex
similarity index 100%
rename from pre.tex
rename to a1/pre.tex
similarity index 100%
rename from src/a1.bash
rename to a1/src/a1.bash
similarity index 100%
rename from src/a1.py
rename to a1/src/a1.py
similarity index 100%
rename from src/a2.bash
rename to a1/src/a2.bash
similarity index 100%
rename from src/a2.py
rename to a1/src/a2.py
similarity index 100%
rename from src/a3.bash
rename to a1/src/a3.bash
similarity index 100%
rename from src/a3.py
rename to a1/src/a3.py
similarity index 100%
rename from src/a4.bash
rename to a1/src/a4.bash
similarity index 100%
rename from src/a4.py
rename to a1/src/a4.py
diff --git a/a2/1.tex b/a2/1.tex
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/a2/2.tex b/a2/2.tex
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/a2/3.tex b/a2/3.tex
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/a2/4.tex b/a2/4.tex
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/a2/Makefile b/a2/Makefile
new file mode 100644 (file)
index 0000000..5162ae9
--- /dev/null
@@ -0,0 +1,20 @@
+LATEX:=pdflatex
+
+DOCUMENT:=ar
+PROBLEMS:=1 2 3 4
+
+SOURCES:=$(DOCUMENT).tex $(addsuffix .tex,$(PROBLEMS))
+
+.SECONDARY: $(DOCUMENT).fmt $(SOLUTIONS)
+
+all: $(DOCUMENT).pdf
+
+%.pdf: %.tex %.fmt $(SOURCES)
+       $(LATEX) $<
+       $(LATEX) $<
+
+%.fmt: pre.tex
+       $(LATEX) -ini -jobname="$(basename $@)" "&$(LATEX) $<\dump"
+
+clean:
+       $(RM) -v $(addprefix $(DOCUMENT).,fmt aux log out toc pdf)
diff --git a/a2/ar.tex b/a2/ar.tex
new file mode 100644 (file)
index 0000000..7b5d21e
--- /dev/null
+++ b/a2/ar.tex
@@ -0,0 +1,38 @@
+%&ar
+\begin{document}
+\maketitle
+\tableofcontents
+
+\setcounter{section}{-1}
+\section{General approach}
+Implementing all the problems by hand in SMT-Lib format would be too much work
+and therefore all problems have an accompanying bash script contains a function
+\lstinline{generate} that generates the SMT-Lib format. The script feeds the
+SMT-Lib format to yices after which the output is feeded to a Python script
+that visualizes the solution. This means that for all problems $p$ for $p\in
+\{1,\ldots, 4\}$ there exist $2$ files. \texttt{ap.bash} that generates the
+solution and \texttt{ap.py} that visualizes the solution. All solving is done
+on the benchmark system listed in Listing~\ref{listing:benchmark}.
+
+\begin{lstlisting}[caption={Benchmark system},label={listing:benchmark}]
+CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor
+RAM: 8GB
+
+Yices: 2.4.1
+SMT-Lib: 1.2
+Bash: 4.3.30(1)
+\end{lstlisting}
+
+\newpage
+\input{1.tex}
+
+\newpage
+\input{2.tex}
+
+\newpage
+\input{3.tex}
+
+\newpage
+\input{4.tex}
+
+\end{document}
diff --git a/a2/pre.tex b/a2/pre.tex
new file mode 100644 (file)
index 0000000..839423e
--- /dev/null
@@ -0,0 +1,28 @@
+\documentclass{article}
+
+\usepackage{hyperref}  % For clickable links
+\usepackage{a4wide}    % For better page usage
+\usepackage{float}     % For better placement of tables/figures
+\usepackage{amsmath}   % For align
+\usepackage{listings}  % For code snippets
+\usepackage{booktabs}  % For nice tables
+
+\everymath{\displaystyle\allowdisplaybreaks}
+
+\lstset{%
+  basicstyle=\scriptsize,
+  breakatwhitespace=true,
+  breaklines=true,
+  keepspaces=true,
+  numbers=left,
+  numberstyle=\tiny,
+  frame=L,
+  showspaces=false,
+  showstringspaces=false,
+  showtabs=false,
+  tabsize=2
+}
+
+\author{Mart Lubbers (s4109503)}
+\title{Automated reasoning Assignment 2} 
+\date{\today}