Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems (Logical Methods in Computer Science, 2020)