From: Mart Lubbers Date: Mon, 26 Oct 2015 19:53:12 +0000 (+0100) Subject: remove typo X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=1b2f865a854eba3546a475a24e5fa1bd3b7c4265;p=ar1516.git remove typo --- diff --git a/2.tex b/2.tex index a8fdc66..d266aad 100644 --- a/2.tex +++ b/2.tex @@ -99,9 +99,9 @@ power components and only regular components. \subsection{SMT format solution} The formula is easily convertable via a Python script to SMT format by literal conversion and said script is listed in Listing~\ref{listing:a2.bash}. The -Python script optimizes a little bit from the original formula by leaving out -the overlap checking between the same components. The solution is calculated -using the command shown in Listing~\ref{listing:2.bash} and visualized with the +script optimizes a little bit from the original formula by leaving out the +overlap checking between the same components. The solution is calculated using +the command shown in Listing~\ref{listing:2.bash} and visualized with the python script shown in Listing~\ref{listing:a2.py} \lstinputlisting[language=bash, diff --git a/4.tex b/4.tex index 0ddc5de..f2a929c 100644 --- a/4.tex +++ b/4.tex @@ -47,10 +47,10 @@ postcondition. \subsection{SMT format solution} The formula is easily convertable via a Python script to SMT format by literal conversion and said script is listed in Listing~\ref{listing:a4.bash}. The -Python script optimizes a little bit from the original formula by leaving out -the $i=j$ comparison in subformula 17 and 18 by removing them from the set -looped over. The script also optimizes by not checking variables $a_0^n$ and -$a_I^n$ since they always stay the same anyways. The minimization is done by +script optimizes a little bit from the original formula by leaving out the +$i=j$ comparison in subformula 17 and 18 by removing them from the set looped +over. The script also optimizes by not checking variables $a_0^n$ and $a_I^n$ +since they always stay the same anyways. The minimization is done by incrementing variable $N$ every time the current $N$ yields unsat with a bash script shown in Listing~\ref{listing:4.bash} and visualized with the python script shown in Listing~\ref{listing:a4.py}.