...

CA/GoL/main_EN.tex

@@ -202,11 +202,11 @@ \subsubsection{Reversing back the state of ``Game of Life''}
 ...
 \end{lstlisting}
 
-( \url{.../GoL/GoL_SAT_utils.py} )
+( \url{https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/CA/GoL/GoL_SAT_utils.py} )
 
-\lstinputlisting{\CURPATH/reverse1.py}
+\lstinputlisting[style=custompy]{\CURPATH/reverse1.py}
 
-( \url{.../reverse1.py} )
+( \url{https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/CA/GoL/reverse1.py} )
 
 Here is the result:
 
@@ -282,7 +282,7 @@ \subsubsection{Reversing back the state of ``Game of Life''}
 
 \end{lstlisting}
 
-( \url{.../GoL/reverse2.py} )
+( \url{https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/CA/GoL/reverse2.py} )
 
 Functions \TT{reflect\_vertically()}, \TT{reflect\_horizontally} and \TT{rotate\_squarearray()}
 are simple array manipulation routines.
@@ -486,9 +486,9 @@ \subsubsection{Finding ``still lives''}
 
 \end{lstlisting}
 
-\lstinputlisting{\CURPATH/SL1.py}
+\lstinputlisting[style=custompy]{\CURPATH/SL1.py}
 
-( \url{.../GoL/SL1.py} )
+( \url{https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/CA/GoL/SL1.py} )
 
 What we've got for $2 \cdot 2$?
 
@@ -591,7 +591,7 @@ \subsubsection{Finding ``still lives''}
 
 \end{lstlisting}
 
-( \url{.../GoL/SL2.py} )
+( \url{https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/CA/GoL/SL2.py} )
 
 Now we can see that $3 \cdot 3$ square has 3 possible ``still lives'':
 
@@ -761,7 +761,7 @@ \subsubsection{Finding ``still lives''}
 
 \end{lstlisting}
 
-( \url{.../GoL/SL3.py} )
+( \url{https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/CA/GoL/SL3.py} )
 
 This is indeed denser:
 
@@ -927,5 +927,5 @@ \subsubsection{Finding ``still lives''}
 
 \subsubsection{The source code}
 
-Source code and Wolfram Mathematica notebook: \url{...GoL}.
+Source code and Wolfram Mathematica notebook: \url{https://github.com/DennisYurichev/SAT_SMT_by_example/tree/master/CA/GoL}.
 

CRC/cracker/main_EN.tex

@@ -50,7 +50,7 @@ \subsection{Getting CRC polynomial and other CRC generator parameters}
 total results 11
 \end{lstlisting}
 
-The files: \url{https://github.com/DennisYurichev/yurichev.com/...}.
+The files: \url{https://github.com/DennisYurichev/SAT_SMT_by_example/tree/master/CRC/cracker}.
 
 The shortcoming: longer samples slows down everything significantly.
 I had luck with samples up to 4 bytes, but no larger.

CRC/explanation/main_EN.tex

@@ -64,7 +64,7 @@ \subsubsection{(Binary) long divison}
 
 The following piece of code I've copypasted from somewhere:
 
-\begin{lstlisting}
+\begin{lstlisting}[style=customc]
 unsigned int divide(unsigned int dividend, unsigned int divisor)
 {
         unsigned int tmp = dividend;
@@ -104,7 +104,7 @@ \subsubsection{(Binary) long divison}
 }
 \end{lstlisting}
 
-( \url{https://github.com/DennisYurichev/yurichev.com/...div.c} )
+( \url{https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/CRC/explanation/div.c} )
 
 Let's divide 1234567 by 813 and find remainder:
 
@@ -131,7 +131,7 @@ \subsubsection{(Binary) long division, version 2}
 
 What we can do: tmp value will be shifted at each iteration, while divisor is not:
 
-\begin{lstlisting}
+\begin{lstlisting}[style=customc]
 uint8_t *buf;
 int buf_pos;
 int buf_bit_pos;
@@ -184,7 +184,7 @@ \subsubsection{(Binary) long division, version 2}
 }
 \end{lstlisting}
 
-( \url{https://github.com/DennisYurichev/yurichev.com/.../div_both.c} )
+( \url{https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/CRC/explanation/div_both.c} )
 
 Let's divide 1234567 by 813 and find remainder:
 
@@ -229,7 +229,7 @@ \subsubsection{CRC32}
 
 Now we can take the binary division algorithm and change it a little:
 
-\begin{lstlisting}
+\begin{lstlisting}[style=customc]
 uint32_t remainder_GF2(uint32_t dividend, uint32_t divisor)
 {
 	// necessary bit shuffling/negation to make it compatible with other CRC32 implementations.
@@ -275,7 +275,7 @@ \subsubsection{CRC32}
 }
 \end{lstlisting}
 
-( \url{https://github.com/DennisYurichev/yurichev.com/.../div_both.c} )
+( \url{https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/CRC/explanation/div_both.c} )
 
 And voila, this is the function which computes CRC32 for the input 32-bit value.
 

CRC/factor/main_EN.tex

@@ -13,5 +13,5 @@ \subsection{Factorize GF(2)/CRC polynomials}
 
 Also, can be used for tests, online GF(2) polynomials factorization: \url{http://www.ee.unb.ca/cgi-bin/tervo/factor.pl?binary=101}.
 
-\lstinputlisting{CRC/factor/factor_GF2.py}
+\lstinputlisting[style=custompy]{CRC/factor/factor_GF2.py}
 

CRC/find_poly/main_EN.tex

@@ -6,7 +6,7 @@ \subsection{Finding (good) CRC polynomial}
 I just generate 32 random samples, all has size between 1 and 32 bytes.
 Then I flip 1..3 random bits and I add a constraint: CRC hash of the sample and hash of the modified sample (with 1..3 bits flipped) must differ.
 
-\lstinputlisting{CRC/find_poly/CRC_find_poly.py}
+\lstinputlisting[style=custompy]{CRC/find_poly/CRC_find_poly.py}
 
 Several polynomials for CRC8:
 

FOL/TAOCP_7_1_1_exercise_56/main_EN.tex

@@ -10,9 +10,9 @@ \subsection{Exercise 56 from TAOCP ``7.1.1 Boolean Basics'', solving it using Z3
 
 For exists/forall/forall:
 
-\lstinputlisting{FOL/TAOCP_7_1_1_exercise_56/KnuthEAA.smt}
+\lstinputlisting[style=customsmt]{FOL/TAOCP_7_1_1_exercise_56/KnuthEAA.smt}
 
-All the rest: \url{FIXME}.
+All the rest: \url{https://github.com/DennisYurichev/SAT_SMT_by_example/tree/master/FOL/TAOCP_7_1_1_exercise_56}.
 
 Results:
 

FOL/TAOCP_7_1_1_exercise_9/main_EN.tex

@@ -10,17 +10,17 @@ \subsection{Exercise 9 from TAOCP ``7.1.1 Boolean Basics'', solving it using Z3}
 
 For (a):
 
-\lstinputlisting{FOL/TAOCP_7_1_1_exercise_9/Knuth_a.smt}
+\lstinputlisting[style=customsmt]{FOL/TAOCP_7_1_1_exercise_9/Knuth_a.smt}
 
 For (b):
 
-\lstinputlisting{FOL/TAOCP_7_1_1_exercise_9/Knuth_b.smt}
+\lstinputlisting[style=customsmt]{FOL/TAOCP_7_1_1_exercise_9/Knuth_b.smt}
 
 For (c):
 
-\lstinputlisting{FOL/TAOCP_7_1_1_exercise_9/Knuth_c.smt}
+\lstinputlisting[style=customsmt]{FOL/TAOCP_7_1_1_exercise_9/Knuth_c.smt}
 
 Results:
 
-\lstinputlisting{FOL/TAOCP_7_1_1_exercise_9/results.txt}
+\lstinputlisting[style=customsmt]{FOL/TAOCP_7_1_1_exercise_9/results.txt}
 

KLEE/UNIXdatetime_EN.tex

@@ -10,7 +10,6 @@ \subsection{UNIX date/time}
 
 Let's try it:
 
-% FIXME:
 \begin{lstlisting}
 % clang -emit-llvm -c -g klee_time1.c
 ...
@@ -31,7 +30,6 @@ \subsection{UNIX date/time}
 Wow, assert() at line 83 has been triggered, why?
 Let's see a value of UNIX time which triggers it:
 
-% FIXME:
 \begin{lstlisting}
 % ls klee-last | grep err
 test000001.exec.err
@@ -48,7 +46,6 @@ \subsection{UNIX date/time}
 
 Let's decode this value using UNIX date utility:
 
-% FIXME:
 \begin{lstlisting}
 % date -u --date='@978278400'
 Sun Dec 31 16:00:00 UTC 2000
@@ -60,7 +57,6 @@ \subsection{UNIX date/time}
 
 Just interesting, what would be if I'll replace switch() to array of strings, like it usually happens in concise C/C++ code?
 
-% FIXME:
 \begin{lstlisting}
 	...
 
@@ -91,7 +87,6 @@ \subsection{UNIX date/time}
 
 KLEE detects attempt to read beyond array boundaries:
 
-% FIXME:
 \begin{lstlisting}
 % klee klee_time2.bc
 KLEE: output directory is "/home/klee/klee-out-108"
@@ -108,7 +103,6 @@ \subsection{UNIX date/time}
 
 This is the same UNIX time value we've already seen:
 
-% FIXME:
 \begin{lstlisting}
 % ls klee-last | grep err
 test000001.exec.err
@@ -131,7 +125,6 @@ \subsection{UNIX date/time}
 
 \lstinputlisting[numbers=left]{KLEE/klee_time3.c}
 
-% FIXME:
 \begin{lstlisting}
 % clang -emit-llvm -c -g klee_time3.c
 ...
@@ -167,7 +160,6 @@ \subsection{UNIX date/time}
 
 Let's add constraints to hours/minutes/seconds as well:
 
-% FIXME:
 \begin{lstlisting}
 	...
 
@@ -179,7 +171,6 @@ \subsection{UNIX date/time}
 
 Let's run it and check \dots
 
-% FIXME:
 \begin{lstlisting}
 % ktest-tool --write-ints klee-last/test000597.ktest
 ktest file : 'klee-last/test000597.ktest'

KLEE/UNIXdatetime_RU.tex

@@ -175,7 +175,6 @@ \subsection{Дата и время в UNIX}
 
 Запустим и проверим \dots
 
-% FIXME:
 \begin{lstlisting}
 % ktest-tool --write-ints klee-last/test000597.ktest
 ktest file : 'klee-last/test000597.ktest'

KLEE/calc_EN.tex

@@ -5,11 +5,10 @@ \subsection{Unit testing: simple expression evaluator (calculator)}
 Unfortunately, it has no bugs, so I've introduced one: a token buffer (\TT{buf[]} at line 31) is smaller than input buffer (\TT{input[]} at line 19).
 
 \lstinputlisting[numbers=left,style=customc]{KLEE/calc.c}
-( \url{https://github.com/DennisYurichev/SAT_SMT_article/blob/master/KLEE/calc.c} )
+( \url{https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/KLEE/calc.c} )
 
 KLEE found buffer overflow with little effort (65 zero digits + one tabulation symbol):
 
-% FIXME:
 \begin{lstlisting}
 % ktest-tool --write-ints klee-last/test000468.ktest
 ktest file : 'klee-last/test000468.ktest'
@@ -24,7 +23,6 @@ \subsection{Unit testing: simple expression evaluator (calculator)}
 \\
 KLEE also found two expression strings which leads to division error (``0/0'' and ``0\%0''):
 
-% FIXME:
 \begin{lstlisting}
 % ktest-tool --write-ints klee-last/test000326.ktest
 ktest file : 'klee-last/test000326.ktest'

KLEE/color_EN.tex

@@ -12,7 +12,6 @@ \subsection{Unit test: HTML/CSS color}
 There are 5 possible paths in function, and let's see, if KLEE could find them all?
 It's indeed so:
 
-% FIXME:
 \begin{lstlisting}
 % clang -emit-llvm -c -g color.c
 
@@ -35,7 +34,6 @@ \subsection{Unit test: HTML/CSS color}
 
 So there are exactly 5 paths:
 
-% FIXME:
 \begin{lstlisting}
 % ls klee-last
 assembly.ll   run.stats            test000003.ktest     test000005.ktest
@@ -46,7 +44,6 @@ \subsection{Unit test: HTML/CSS color}
 
 1st set of input variables will result in ``red'' string:
 
-% FIXME:
 \begin{lstlisting}
 % ktest-tool --write-ints klee-last/test000001.ktest
 ktest file : 'klee-last/test000001.ktest'
@@ -65,7 +62,6 @@ \subsection{Unit test: HTML/CSS color}
 
 2nd set of input variables will result in ``green'' string:
 
-% FIXME:
 \begin{lstlisting}
 % ktest-tool --write-ints klee-last/test000002.ktest
 ktest file : 'klee-last/test000002.ktest'
@@ -84,7 +80,6 @@ \subsection{Unit test: HTML/CSS color}
 
 3rd set of input variables will result in ``\#010000'' string:
 
-% FIXME:
 \begin{lstlisting}
 % ktest-tool --write-ints klee-last/test000003.ktest
 ktest file : 'klee-last/test000003.ktest'
@@ -103,7 +98,6 @@ \subsection{Unit test: HTML/CSS color}
 
 4th set of input variables will result in ``blue'' string:
 
-% FIXME:
 \begin{lstlisting}
 % ktest-tool --write-ints klee-last/test000004.ktest
 ktest file : 'klee-last/test000004.ktest'
@@ -122,7 +116,6 @@ \subsection{Unit test: HTML/CSS color}
 
 5th set of input variables will result in ``\#F01'' string:
 
-% FIXME:
 \begin{lstlisting}
 % ktest-tool --write-ints klee-last/test000005.ktest
 ktest file : 'klee-last/test000005.ktest'

KLEE/strtodx_EN.tex

@@ -5,7 +5,7 @@ \subsection{strtodx() from RetroBSD}
 It converts a string into floating point number for given radix.
 
 \lstinputlisting[numbers=left]{KLEE/strtodx.c}
-( \url{https://github.com/DennisYurichev/SAT_SMT_article/blob/master/KLEE/strtodx.c} )
+( \url{https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/KLEE/strtodx.c} )
 
 Interestinly, KLEE cannot handle floating-point arithmetic, but nevertheless, found something:
 

MaxSMT/GCD_LCM/GCD_EN.tex

@@ -148,5 +148,5 @@ \subsubsection{Explanation of the \ac{GCD}}
 
 In SMT-LIB form:
 
-\lstinputlisting{GCD_BV2.smt}
+\lstinputlisting[style=customsmt]{GCD_BV2.smt}
 

MaxSMT/TSP/main.tex

@@ -4,7 +4,7 @@ \subsection{Travelling salesman problem}
 
 This is it:
 
-\lstinputlisting{\CURPATH/TSP.py}
+\lstinputlisting[style=custompy]{\CURPATH/TSP.py}
 
 The result:
 

MaxSMT/assign_problem/main_EN.tex

@@ -50,7 +50,7 @@ \subsection{Assignment problem}
 \\
 The problem can also be stated in SMT-LIB 2.0 format, and solved using MK85:
 
-\lstinputlisting{MaxSMT/assign_problem/assign_problem.smt}
+\lstinputlisting[style=customsmt]{MaxSMT/assign_problem/assign_problem.smt}
 
 \lstinputlisting[caption=The result]{MaxSMT/assign_problem/assign_problem.correct}
 

MaxSMT/minimum/main_EN.tex

@@ -1,5 +1,5 @@
 \subsection{Finding function minimum}
 \label{func_minimum}
 
-\lstinputlisting{MaxSMT/minimum/1959_AHSME_Problem_8.smt}
+\lstinputlisting[style=customsmt]{MaxSMT/minimum/1959_AHSME_Problem_8.smt}
 

MaxSMT/set_cover/main_EN.tex

@@ -17,7 +17,7 @@ \subsection{Making smallest possible test suite using Z3}
 from Apple sources.
 Such routines are not easy to test.
 Here is my version of it:
-\url{https://github.com/DennisYurichev/SAT_SMT_article/blob/master/SMT/set_cover/compression.c}.
+\url{https://github.com/DennisYurichev/SAT_SMT_by_example/blob/master/MaxSMT/set_cover/compression.c}.
 I've added random generation of input data to be compressed.
 Random generation is dependent of some kind of input seed.
 Standard \TT{srand()}/\TT{rand()} are not recommended to be used, but for such simple task as ours, it's OK.
@@ -55,7 +55,7 @@ \subsection{Making smallest possible test suite using Z3}
 
 Now the Z3Py script, which will parse all these 1000 gcov results and produce minimal \textit{hitting set}:
 
-\lstinputlisting{MaxSMT/set_cover/set_cover.py}
+\lstinputlisting[style=custompy]{MaxSMT/set_cover/set_cover.py}
 
 And what it produces (\textasciitilde{}19s on my old Intel Quad-Core Xeon E3-1220 3.10GHz):
 
@@ -78,7 +78,7 @@ \subsection{Making smallest possible test suite using Z3}
 Also, the code gives incorrect results on Z3 4.4.1, but working correctly on Z3 4.5.0 (so please upgrade).
 This is relatively fresh feature in Z3, so probably it was not stable in previous versions?
 
-The files: \url{https://github.com/DennisYurichev/SAT_SMT_article/tree/master/SMT/set_cover}.
+The files: \url{https://github.com/DennisYurichev/SAT_SMT_by_example/tree/master/MaxSMT/set_cover}.
 
 Further reading:
 \url{https://en.wikipedia.org/wiki/Set_cover_problem},