# Path: parser/stpcommands.py
# def blockCharacteristic(stpfile, characteristic, wordsize):
# def setupQuery(stpfile):
# def setupVariables(stpfile, variables, wordsize):
# def assertVariableValue(stpfile, a, b):
# def getStringForVariables(variables, wordsize):
# def assertNonZero(stpfile, variables, wordsize):
# def getStringForNonZero(variables, wordsize):
# def limitWeight(stpfile, weight, p, wordsize, ignoreMSBs=0):
# def setupWeightComputationSum(stpfile, weight, p, wordsize, ignoreMSBs=0):
# def setupWeightComputation(stpfile, weight, p, wordsize, ignoreMSBs=0):
# def getWeightString(variables, wordsize, ignoreMSBs=0, weightVariable="weight"):
# def getStringEq(a, b, c):
# def getStringAdd(a, b, c, wordsize):
# def getStringForAndDifferential(a, b, c):
# def getStringLeftRotate(value, rotation, wordsize):
# def getStringRightRotate(value, rotation, wordsize):
# def add4bitSbox(sbox, variables):
#     DDT = [[0]*16 for i in range(16)]
# 
# Path: ciphers/cipher.py
# class AbstractCipher(object, metaclass=ABCMeta):
#     """
#     Abstract Class for Ciphers
#     """
# 
#     @abstractmethod
#     def createSTP(self, filename, cipherParameters):
#         """
#         Each cipher need to define how it creates an instance for the
#         SMT solver.
#         """
#         pass
# 
#     @abstractmethod
#     def getFormatString(self):
#         """
#         Each cipher needs to specify the format it should be printed.
#         """
#         pass


from parser import stpcommands
from ciphers.cipher import AbstractCipher
                                                                  mc[4*col + row],
                                                                  xorsum)

        stp_file.write(command)
        return

    def setupMantisMiddleRound(self, stp_file, sb_in, m_in, m_out, sb_out, wn, wn2, wordsize):
        """
        Middle round of Mantis.
        """

        command = ""

        # SubBytes
        mantis_sbox = [0xc, 0xa, 0xd, 0x3, 0xe, 0xb, 0xf, 0x7,
                       0x8, 0x9, 0x1, 0x5, 0x0, 0x2, 0x4, 0x6]

        for sbox in range(16):
            command += stpcommands.add4bitSboxNibbles(mantis_sbox, sb_in[sbox], m_in[sbox], wn[sbox])

        # MixColumns
        for col in range(4):
            xorsum = stpcommands.getStringXORn(m_in[4*col:(4*(col + 1))])  # Get One column
            for row in range(4):
                command += "ASSERT({} = BVXOR({}, {}));\n".format(m_out[4*col + row],
                                                                  m_in[4*col + row],
                                                                  xorsum)

        # SubBytes
        for sbox in range(16):

# Path: parser/stpcommands.py
# def blockCharacteristic(stpfile, characteristic, wordsize):
# def setupQuery(stpfile):
# def setupVariables(stpfile, variables, wordsize):
# def assertVariableValue(stpfile, a, b):
# def getStringForVariables(variables, wordsize):
# def assertNonZero(stpfile, variables, wordsize):
# def getStringForNonZero(variables, wordsize):
# def limitWeight(stpfile, weight, p, wordsize, ignoreMSBs=0):
# def setupWeightComputationSum(stpfile, weight, p, wordsize, ignoreMSBs=0):
# def setupWeightComputation(stpfile, weight, p, wordsize, ignoreMSBs=0):
# def getWeightString(variables, wordsize, ignoreMSBs=0, weightVariable="weight"):
# def getStringEq(a, b, c):
# def getStringAdd(a, b, c, wordsize):
# def getStringForAndDifferential(a, b, c):
# def getStringLeftRotate(value, rotation, wordsize):
# def getStringRightRotate(value, rotation, wordsize):
# def add4bitSbox(sbox, variables):
#     DDT = [[0]*16 for i in range(16)]
# 
# Path: ciphers/cipher.py
# class AbstractCipher(object, metaclass=ABCMeta):
#     """
#     Abstract Class for Ciphers
#     """
# 
#     @abstractmethod
#     def createSTP(self, filename, cipherParameters):
#         """
#         Each cipher need to define how it creates an instance for the
#         SMT solver.
#         """
#         pass
# 
#     @abstractmethod
#     def getFormatString(self):
#         """
#         Each cipher needs to specify the format it should be printed.
#         """
#         pass


# Path: ciphers/mantis.py
from parser import stpcommands
from ciphers.cipher import AbstractCipher

                                                                  mc[4*col + row],
                                                                  xorsum)

        stp_file.write(command)
        return

    def setupMantisMiddleRound(self, stp_file, sb_in, m_in, m_out, sb_out, wn, wn2, wordsize):
        """
        Middle round of Mantis.
        """

        command = ""

        # SubBytes
        mantis_sbox = [0xc, 0xa, 0xd, 0x3, 0xe, 0xb, 0xf, 0x7,
                       0x8, 0x9, 0x1, 0x5, 0x0, 0x2, 0x4, 0x6]

        for sbox in range(16):
            command += stpcommands.add4bitSboxNibbles(mantis_sbox, sb_in[sbox], m_in[sbox], wn[sbox])

        # MixColumns
        for col in range(4):
            xorsum = stpcommands.getStringXORn(m_in[4*col:(4*(col + 1))])  # Get One column
            for row in range(4):
                command += "ASSERT({} = BVXOR({}, {}));\n".format(m_out[4*col + row],
                                                                  m_in[4*col + row],
                                                                  xorsum)

        # SubBytes
        for sbox in range(16):

            command += stpcommands.add4bitSboxNibbles(mantis_sbox, m_out[sbox], sb_out[sbox], wn2[sbox])