From 7477b4d7a097e4590b21509afb3aa5f566f7110d Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Tue, 10 Nov 2015 08:43:32 +0100 Subject: [PATCH] started with a2 --- 1.tex => a1/1.tex | 0 2.tex => a1/2.tex | 0 3.tex => a1/3.tex | 0 4.tex => a1/4.tex | 0 Makefile => a1/Makefile | 0 README.md => a1/README.md | 0 ar.tex => a1/ar.tex | 0 pre.tex => a1/pre.tex | 0 {src => a1/src}/a1.bash | 0 {src => a1/src}/a1.py | 0 {src => a1/src}/a2.bash | 0 {src => a1/src}/a2.py | 0 {src => a1/src}/a3.bash | 0 {src => a1/src}/a3.py | 0 {src => a1/src}/a4.bash | 0 {src => a1/src}/a4.py | 0 a2/1.tex | 0 a2/2.tex | 0 a2/3.tex | 0 a2/4.tex | 0 a2/Makefile | 20 ++++++++++++++++++++ a2/ar.tex | 38 ++++++++++++++++++++++++++++++++++++++ a2/pre.tex | 28 ++++++++++++++++++++++++++++ 23 files changed, 86 insertions(+) rename 1.tex => a1/1.tex (100%) rename 2.tex => a1/2.tex (100%) rename 3.tex => a1/3.tex (100%) rename 4.tex => a1/4.tex (100%) rename Makefile => a1/Makefile (100%) rename README.md => a1/README.md (100%) rename ar.tex => a1/ar.tex (100%) rename pre.tex => a1/pre.tex (100%) rename {src => a1/src}/a1.bash (100%) rename {src => a1/src}/a1.py (100%) rename {src => a1/src}/a2.bash (100%) rename {src => a1/src}/a2.py (100%) rename {src => a1/src}/a3.bash (100%) rename {src => a1/src}/a3.py (100%) rename {src => a1/src}/a4.bash (100%) rename {src => a1/src}/a4.py (100%) create mode 100644 a2/1.tex create mode 100644 a2/2.tex create mode 100644 a2/3.tex create mode 100644 a2/4.tex create mode 100644 a2/Makefile create mode 100644 a2/ar.tex create mode 100644 a2/pre.tex 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 diff --git a/Makefile b/a1/Makefile similarity index 100% rename from Makefile rename to a1/Makefile diff --git a/README.md b/a1/README.md similarity index 100% rename from README.md rename to a1/README.md diff --git a/ar.tex b/a1/ar.tex similarity index 100% rename from ar.tex rename to a1/ar.tex diff --git a/pre.tex b/a1/pre.tex similarity index 100% rename from pre.tex rename to a1/pre.tex diff --git a/src/a1.bash b/a1/src/a1.bash similarity index 100% rename from src/a1.bash rename to a1/src/a1.bash diff --git a/src/a1.py b/a1/src/a1.py similarity index 100% rename from src/a1.py rename to a1/src/a1.py diff --git a/src/a2.bash b/a1/src/a2.bash similarity index 100% rename from src/a2.bash rename to a1/src/a2.bash diff --git a/src/a2.py b/a1/src/a2.py similarity index 100% rename from src/a2.py rename to a1/src/a2.py diff --git a/src/a3.bash b/a1/src/a3.bash similarity index 100% rename from src/a3.bash rename to a1/src/a3.bash diff --git a/src/a3.py b/a1/src/a3.py similarity index 100% rename from src/a3.py rename to a1/src/a3.py diff --git a/src/a4.bash b/a1/src/a4.bash similarity index 100% rename from src/a4.bash rename to a1/src/a4.bash diff --git a/src/a4.py b/a1/src/a4.py 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 index 0000000..e69de29 diff --git a/a2/2.tex b/a2/2.tex new file mode 100644 index 0000000..e69de29 diff --git a/a2/3.tex b/a2/3.tex new file mode 100644 index 0000000..e69de29 diff --git a/a2/4.tex b/a2/4.tex new file mode 100644 index 0000000..e69de29 diff --git a/a2/Makefile b/a2/Makefile new file mode 100644 index 0000000..5162ae9 --- /dev/null +++ b/a2/Makefile @@ -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 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 index 0000000..839423e --- /dev/null +++ b/a2/pre.tex @@ -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} -- 2.20.1