def createSTP(self, stp_filename, parameters):

        wordsize = parameters["wordsize"]
        rounds = parameters["rounds"]
        weight = parameters["sweight"]

        # Replace with custom if set in parameters.
        if "rotationconstants" in parameters:
            self.rot_alpha = parameters["rotationconstants"][0] 
            self.rot_beta = parameters["rotationconstants"][1]
            self.rot_gamma = parameters["rotationconstants"][2]

        self.num_messages = parameters["nummessages"]

        with open(stp_filename, 'w') as stp_file:
            header = ("% Input File for STP\n% Simon w={} alpha={} beta={}"
                      " gamma={} rounds={}\n\n\n".format(wordsize,
                                                         self.rot_alpha,
                                                         self.rot_beta,
                                                         self.rot_gamma,
                                                         rounds))
            stp_file.write(header)

            # Setup key
            key = ["key{}".format(i) for i in range(rounds + 1)]
            tmp_key = ["tmpkey{}".format(i) for i in range(rounds + 1)]

            stpcommands.setupVariables(stp_file, key, wordsize)
            stpcommands.setupVariables(stp_file, tmp_key, wordsize)

            #TODO Add constant addition
            self.setupKeySchedule(stp_file, key, tmp_key, rounds, wordsize)

            # Setup variables
            # x = left, y = right
            for msg in range(self.num_messages):
                x = ["x{}r{}".format(msg, i) for i in range(rounds + 1)]
                y = ["y{}r{}".format(msg, i) for i in range(rounds + 1)]
                and_out = ["andout{}r{}".format(msg, i) for i in range(rounds + 1)]
                stpcommands.setupVariables(stp_file, x, wordsize)
                stpcommands.setupVariables(stp_file, y, wordsize)
                stpcommands.setupVariables(stp_file, and_out, wordsize)

                #Setup Rounds
                for i in range(rounds):
                    self.setupSimonRound(stp_file, x[i], y[i], x[i+1], y[i+1],
                                         and_out[i], key[i], wordsize)

            #Differences between x_0 and x_i
            for msg in range(1, self.num_messages):
                delta_x = ["dx{}r{}".format(msg, i) for i in range(rounds + 1)]
                delta_y = ["dy{}r{}".format(msg, i) for i in range(rounds + 1)]
                stpcommands.setupVariables(stp_file, delta_x, wordsize)
                stpcommands.setupVariables(stp_file, delta_y, wordsize)
                for i in range(rounds + 1):
                    stp_file.write("ASSERT({} = BVXOR({}, {}));\n".format(
                        delta_x[i], "x0r{}".format(i),
                        "x{}r{}".format(msg, i)))
                    stp_file.write("ASSERT({} = BVXOR({}, {}));\n".format(
                        delta_y[i], "y0r{}".format(i),
                        "y{}r{}".format(msg, i)))

            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
Creates an STP file for SIMON.
dataset/ETHPy150Open kste/cryptosmt/ciphers/simonkeyrc.py/SimonKeyRcCipher.createSTP