def createSTP(self, stp_filename, parameters):
        wordsize = parameters["wordsize"]
        rounds = parameters["rounds"]
        weight = parameters["sweight"]

        with open(stp_filename, 'w') as stp_file:
            stp_file.write("% Input File for STP\n% Salsa w={}"
                           "rounds={}\n\n\n".format(wordsize, rounds))

            # Setup variables
            a = ["a{}r{}".format(j, i) for i in range(rounds + 1) for j in range(16)]
            b = ["b{}r{}".format(j, i) for i in range(rounds) for j in range(16)]
            w = ["w{}r{}".format(j, i) for i in range(rounds) for j in range(16)]

            stpcommands.setupVariables(stp_file, a, wordsize)
            stpcommands.setupVariables(stp_file, b, wordsize)
            stpcommands.setupVariables(stp_file, w, wordsize)

            # Ignore MSB
            stpcommands.setupWeightComputation(stp_file, weight, w, wordsize, 1)

            for rnd in range(rounds):
                if rnd % 2 != 0:
                    #Rowround
                    for row in range(4):
                        a_in = [a[(i + row) % 4 + 4 * row + 16 * rnd] for i in range(4)]
                        a_out = [a[(i + row) % 4 + 4 * row + 16 * (rnd + 1)] for i in range(4)]
                        tmp_b = [b[i + 4 * row + 16 * rnd] for i in range(4)]
                        tmp_w = [w[i + 4 * row + 16 * rnd] for i in range(4)]
                        self.setupQuarterRound(stp_file, a_in, tmp_b, a_out, tmp_w, wordsize)
                else:
                    #Columnround
                    for col in range(4): 
                        a_in = [a[(i * 4 + 4 * col + col) % 16 + 16 * rnd] for i in range(4)]
                        a_out = [a[(i * 4 + 4 * col + col) % 16 + 16 * (rnd + 1)] for i in range(4)]
                        tmp_b = [b[i * 4 + col + 16 * rnd] for i in range(4)]
                        tmp_w = [w[i * 4 + col + 16 * rnd] for i in range(4)]
                        self.setupQuarterRound(stp_file, a_in, tmp_b, a_out, tmp_w, wordsize)

            #stp_file.write("ASSERT(({}[31:31]) = 0b0);\n".format(a[0]))
            # No all zero characteristic
            stpcommands.assertNonZero(stp_file, a, wordsize)

            for key, value in parameters["fixedVariables"].items():
                stpcommands.assertVariableValue(stp_file, key, value)

            for char in parameters["blockedCharacteristics"]:
                stpcommands.blockCharacteristic(stp_file, char, wordsize)

            stpcommands.setupQuery(stp_file)

        return
Consume the ORDER BY clause.
dataset/ETHPy150Open kste/cryptosmt/ciphers/salsa.py/SalsaCipher.createSTP--crossover with--dataset/ETHPy150Open CollabQ/CollabQ/.google_appengine/google/appengine/ext/gql/__init__.py/GQL.__OrderBy