main.tex

\documentclass{article}

%\usepackage{fontspec}
%\setmainfont{DejaVu Sans}
%\setmonofont{DejaVu Sans Mono}

\usepackage{polyglossia}

\ifdefined\ENGLISH
\setmainlanguage{english}
\setotherlanguage{russian}
\fi

\ifdefined\RUSSIAN
\setmainfont[Ligatures=TeX]{CMU Serif}
\newfontfamily{\cyrillicfonttt}{CMU Typewriter Text}

\setmainlanguage{russian}
\setotherlanguage{english}
%\newfontfamily{\cyrillicfonttt}{DejaVu Sans Mono}
\fi

\usepackage{cmap}
%\usepackage[russian,english]{babel}
%\usepackage[T2A]{fontenc}
%\usepackage[default]{sourcesanspro}

\usepackage{amsmath, amssymb, graphics, setspace}
\usepackage[table]{xcolor}% http://ctan.org/pkg/xcolor

\usepackage{listings}
\usepackage{longtable}
\usepackage{pmboxdraw}
\usepackage{url}
\usepackage[cm]{fullpage}
\usepackage{graphicx}
\usepackage{framed}
\usepackage{color}
\usepackage{float}
\usepackage{tikz}
%\usepackage[margin=0.5in,headheight=12.5pt]{geometry}
\usepackage[footnote,printonlyused,withpage]{acronym}
\usetikzlibrary{arrows}
\usepackage[nottoc]{tocbibind}
%\usepackage{esint}
%\usepackage{charter}
%\usepackage[charter]{mathdesign}
\usepackage[]{hyperref} % should be last

\definecolor{lstbgcolor}{rgb}{0.94,0.94,0.94}
\definecolor{light-gray}{gray}{0.87}

\newcommand{\TT}[1]{\texttt{#1}}
%\newcommand*{\TT}[1]{\colorbox{light-gray}{\texttt{#1}}}

\EN{\newcommand{\TITLE}{SAT/SMT by example}}
\RU{\newcommand{\TITLE}{SAT/SMT в примерах}}
\EN{\newcommand{\AUTHOR}{Dennis Yurichev \TT{<dennis@yurichev.com>}}}
\RU{\newcommand{\AUTHOR}{Денис Юричев \TT{<dennis@yurichev.com>}}}

\definecolor{linkcolor}{RGB}{10,0,190}

\hypersetup{
    pdftex,
    colorlinks=true,
    allcolors=linkcolor,
    %allcolors=darkblue,
    pdfauthor={\AUTHOR},
    pdftitle={\TITLE},
    pdfpagemode=None
}

\lstset{
    %backgroundcolor=\color{lstbgcolor},
    %backgroundcolor=\color{light-gray},
    %basicstyle=\ttfamily\small, 
    basicstyle=\ttfamily\normalsize,
    %basicstyle=\ttfamily\large,
    %basicstyle=\ttfamily\footnotesize, 
    literate={~} {$\sim$}{1},
    breaklines=true,
    frame=single,
    %columns=fullflexible,keepspaces,
    columns=keepspaces,
    escapeinside=§§,
    inputencoding=utf8
}

\definecolor{digits}{RGB}{0,0,0}
\definecolor{colkw}{RGB}{0,0,0}

%\definecolor{colstr}{RGB}{80,80,80}
%\definecolor{colid}{RGB}{80,80,80}

\definecolor{colstr}{RGB}{0,0,0}
\definecolor{colid}{RGB}{0,0,0}

\definecolor{colcomment}{RGB}{130,130,130}
%\definecolor{colcomment}{RGB}{170,170,170}

\definecolor{colbg}{RGB}{255,255,255}

\lstdefinestyle{custompy}{
  language=Python,
  showstringspaces=false,
  backgroundcolor=\color{colbg},
  keywordstyle=\color{colkw},
  commentstyle=\color{colcomment},
  identifierstyle=\color{colid},
  stringstyle=\color{colstr}
}

\lstdefinestyle{customc}{
  language=C,
  showstringspaces=false,
  backgroundcolor=\color{colbg},
  keywordstyle=\color{colkw},
  commentstyle=\color{colcomment},
  identifierstyle=\color{colid},
  stringstyle=\color{colstr}
}

% FIXME: doesn't work:
\lstdefinestyle{customsmt}{
  morecomment=[l];%
  showstringspaces=false,
  backgroundcolor=\color{colbg},
  keywordstyle=\color{colkw},
  commentstyle=\color{colcomment},
  identifierstyle=\color{colid},
  stringstyle=\color{colstr}
}

% с fullflexible в русской версии "+-----+" выглядит длиннее! ХЗ, почему

\author{\AUTHOR}
\title{\TITLE}

\begin{document}

\maketitle

\tableofcontents

\newcommand{\CURPATH}{NOTHING}

% sections
\input{intro}
\input{basics/main}
\input{equations/main}
\input{proofs/main}
\input{regexp/main}
\input{gray_code/main}
\input{puzzles/main}
\input{color/main}
\input{knapsack/main}
\input{SGP/main}
\input{latin/main}
\input{CRC/main}
\input{MaxSMT/main}
\input{pgm_synth/main}
\input{logic_synth/main}
\input{toy_decompiler/main}
\input{symbolic/main}
\input{KLEE/main}
\input{crypto/main}
\input{FOL/main}
\input{CA/main}
\input{other/main}
\input{solvers/main}
\input{reading}
\input{apps}

\section{Acronyms used}

\begin{acronym}
\acro{GCD}{Greatest Common Divisor}
\acro{LCM}{Least Common Multiple}
\acro{CNF}{Conjunctive normal form}
\acro{DNF}{Disjunctive normal form}
\acro{DSL}{Domain-specific language}
\acro{CPRNG}{Cryptographically Secure Pseudorandom Number Generator}
\acro{SMT}{Satisfiability modulo theories}
\acro{SAT}{Boolean satisfiability problem}
\acro{LCG}{Linear congruential generator}
\acro{PL}{Programming Language}
\acro{OOP}{Object-oriented programming}
\acro{SSA}{Static single assignment form}
\acro{CPU}{Central processing unit}
\acro{FPU}{Floating-point unit}
\acro{PRNG}{Pseudorandom number generator}
\acro{CRT}{C runtime library}
\acro{CRC}{Cyclic redundancy check}
\acro{AST}{Abstract syntax tree}
\acro{AKA}{Also Known As}
\acro{CTF}{Capture the Flag}
\acro{ISA}{Instruction Set Architecture}
\acro{CSP}{Constraint satisfaction problem}
\acro{CS}{Computer science}
\acro{DAG}{Directed acyclic graph}
\acro{NOP}{No Operation}
\acro{JVM}{Java Virtual Machine}
\acro{VM}{Virtual Machine}
\acro{LZSS}{Lempel–Ziv–Storer–Szymanski}
\acro{RAM}{Random-access memory}
\acro{FPGA}{Field-programmable gate array}
\acro{EDA}{Electronic design automation}
\acro{MAC}{Message authentication code}
\acro{ECC}{Elliptic curve cryptography}
\acro{API}{Application programming interface}
\acro{NSA}{National Security Agency}
\acro{DPLL}{Davis–Putnam–Logemann–Loveland}
\acro{QF}{Quantifier Free}
\acro{LIA}{Linear Integer Arithmetic}
\acro{SGP}{Social Golfer Problem}
\acro{WBO}{Weighted Boolean Optimization}
\acro{PBO}{Pseudo-Boolean Optimization}
\acro{FSM}{Finite State Machine}
\acro{RE}{Regular Expression}
\acro{RSA}{Rivest–Shamir–Adleman cryptosystem}
\acro{ITE}{If-Then-Else}
\acro{DFA}{Deterministic finite automaton}
\acro{TAOCP}{The Art Of Computer Programming}
\acro{DES}{Data Encryption Standard}
\acro{ALU}{Arithmetic logic unit}
\acro{EE}{Electrical engineering}
\acro{PCB}{Printed circuit board}

\end{acronym}

\end{document}