# 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
        command += "ASSERT({} = {});\n".format(output[4], stpcommands.getStringXORn([input[0], input[4], input[12]]))
        command += "ASSERT({} = {});\n".format(output[5], stpcommands.getStringXORn([input[1], input[9], input[13]]))
        command += "ASSERT({} = {});\n".format(output[6], stpcommands.getStringXORn([input[6], input[10], input[14]]))
        command += "ASSERT({} = {});\n".format(output[7], stpcommands.getStringXORn([input[3], input[7], input[11]]))
        command += "ASSERT({} = {});\n".format(output[8], stpcommands.getStringXORn([input[0], input[8], input[12]]))
        command += "ASSERT({} = {});\n".format(output[9], stpcommands.getStringXORn([input[5], input[9], input[13]]))
        command += "ASSERT({} = {});\n".format(output[10], stpcommands.getStringXORn([input[2], input[6], input[10]]))
        command += "ASSERT({} = {});\n".format(output[11], stpcommands.getStringXORn([input[3], input[7], input[15]]))
        command += "ASSERT({} = {});\n".format(output[12], stpcommands.getStringXORn([input[4], input[8], input[12]]))
        command += "ASSERT({} = {});\n".format(output[13], stpcommands.getStringXORn([input[1], input[5], input[9]]))
        command += "ASSERT({} = {});\n".format(output[14], stpcommands.getStringXORn([input[2], input[6], input[14]]))
        command += "ASSERT({} = {});\n".format(output[15], stpcommands.getStringXORn([input[3], input[11], input[15]]))

        return command

    def princeMhat(self, input, output):
        # Add constraints for Prince M
        # input = (a0 a1 a2 a3 b0 b1 b2 b3 c0 c1 c2 c3 d0 d1 d2 d3)
        command = ""

        command += "ASSERT({} = {});\n".format(output[0], stpcommands.getStringXORn([input[0], input[4], input[12]]))
        command += "ASSERT({} = {});\n".format(output[1], stpcommands.getStringXORn([input[1], input[9], input[13]]))
        command += "ASSERT({} = {});\n".format(output[2], stpcommands.getStringXORn([input[6], input[10], input[14]]))
        command += "ASSERT({} = {});\n".format(output[3], stpcommands.getStringXORn([input[3], input[7], input[11]]))
        command += "ASSERT({} = {});\n".format(output[4], stpcommands.getStringXORn([input[0], input[8], input[12]]))
        command += "ASSERT({} = {});\n".format(output[5], stpcommands.getStringXORn([input[5], input[9], input[13]]))
        command += "ASSERT({} = {});\n".format(output[6], stpcommands.getStringXORn([input[2], input[6], input[10]]))
        command += "ASSERT({} = {});\n".format(output[7], stpcommands.getStringXORn([input[3], input[7], input[15]]))
        command += "ASSERT({} = {});\n".format(output[8], stpcommands.getStringXORn([input[4], input[8], input[12]]))
        command += "ASSERT({} = {});\n".format(output[9], stpcommands.getStringXORn([input[1], input[5], input[9]]))

# 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/prince.py
from parser import stpcommands
from ciphers.cipher import AbstractCipher

        command += "ASSERT({} = {});\n".format(output[4], stpcommands.getStringXORn([input[0], input[4], input[12]]))
        command += "ASSERT({} = {});\n".format(output[5], stpcommands.getStringXORn([input[1], input[9], input[13]]))
        command += "ASSERT({} = {});\n".format(output[6], stpcommands.getStringXORn([input[6], input[10], input[14]]))
        command += "ASSERT({} = {});\n".format(output[7], stpcommands.getStringXORn([input[3], input[7], input[11]]))
        command += "ASSERT({} = {});\n".format(output[8], stpcommands.getStringXORn([input[0], input[8], input[12]]))
        command += "ASSERT({} = {});\n".format(output[9], stpcommands.getStringXORn([input[5], input[9], input[13]]))
        command += "ASSERT({} = {});\n".format(output[10], stpcommands.getStringXORn([input[2], input[6], input[10]]))
        command += "ASSERT({} = {});\n".format(output[11], stpcommands.getStringXORn([input[3], input[7], input[15]]))
        command += "ASSERT({} = {});\n".format(output[12], stpcommands.getStringXORn([input[4], input[8], input[12]]))
        command += "ASSERT({} = {});\n".format(output[13], stpcommands.getStringXORn([input[1], input[5], input[9]]))
        command += "ASSERT({} = {});\n".format(output[14], stpcommands.getStringXORn([input[2], input[6], input[14]]))
        command += "ASSERT({} = {});\n".format(output[15], stpcommands.getStringXORn([input[3], input[11], input[15]]))

        return command

    def princeMhat(self, input, output):
        # Add constraints for Prince M
        # input = (a0 a1 a2 a3 b0 b1 b2 b3 c0 c1 c2 c3 d0 d1 d2 d3)
        command = ""

        command += "ASSERT({} = {});\n".format(output[0], stpcommands.getStringXORn([input[0], input[4], input[12]]))
        command += "ASSERT({} = {});\n".format(output[1], stpcommands.getStringXORn([input[1], input[9], input[13]]))
        command += "ASSERT({} = {});\n".format(output[2], stpcommands.getStringXORn([input[6], input[10], input[14]]))
        command += "ASSERT({} = {});\n".format(output[3], stpcommands.getStringXORn([input[3], input[7], input[11]]))
        command += "ASSERT({} = {});\n".format(output[4], stpcommands.getStringXORn([input[0], input[8], input[12]]))
        command += "ASSERT({} = {});\n".format(output[5], stpcommands.getStringXORn([input[5], input[9], input[13]]))
        command += "ASSERT({} = {});\n".format(output[6], stpcommands.getStringXORn([input[2], input[6], input[10]]))
        command += "ASSERT({} = {});\n".format(output[7], stpcommands.getStringXORn([input[3], input[7], input[15]]))
        command += "ASSERT({} = {});\n".format(output[8], stpcommands.getStringXORn([input[4], input[8], input[12]]))
        command += "ASSERT({} = {});\n".format(output[9], stpcommands.getStringXORn([input[1], input[5], input[9]]))

        command += "ASSERT({} = {});\n".format(output[10], stpcommands.getStringXORn([input[2], input[6], input[14]]))