# 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: parser/stpcommands.py
# def getStringLeftRotate(value, rotation, wordsize):
#     if rotation % wordsize == 0:
#         return "{0}".format(value)
#     command = "((({0} << {1})[{2}:0]) | (({0} >> {3})[{2}:0]))".format(
#         value, (rotation % wordsize), wordsize - 1, (wordsize - rotation) % wordsize)
# 
#     return command


from parser import stpcommands
from ciphers.cipher import AbstractCipher
from parser.stpcommands import getStringLeftRotate as rotl
            y = (y xor x xor (x | z) << b) <<< e
            z = (y xor z xor (x & y) << c) <<< f
        """
        command = ""

        # Conditions for non-linear layer
        xnl = "({} & ~({}|{}))".format(xsb, yin, zin)
        ynl = "({} & ~({}|{}))".format(ysb, xin, zin)
        znl = "({} & ~({}|{}))".format(zsb, xin, yin)

        command += "ASSERT(({} | {} | {}) = 0x{});\n".format(xnl, ynl, znl, "0" * (wordsize // 4))

        # Dependency between bits
        # (x & y & ~z) & ~(xout ^ yout)
        xcond = "(({} & {} & ~{}) & ~(BVXOR({}, {})))".format(xin, yin, zin, xsb, ysb)
        # (x & ~y & z) & (xout ^ zout)
        ycond = "(({} & ~{} & {}) & (BVXOR({}, {})))".format(xin, yin, zin, xsb, zsb)
        # (~x & y & z) & ~(yout ^ zout)
        zcond = "((~{} & {} & {}) & ~(BVXOR({}, {})))".format(xin, yin, zin, ysb, zsb)
        # (x & y & z) & (~(xout ^ yout ^ zout))
        fcond = "(({} & {} & {}) & ~(BVXOR(BVXOR({}, {}), {})))".format(xin, yin, zin, xsb, ysb, zsb)
        command += "ASSERT(({} | {} | {} | {}) = 0x{});\n".format(xcond, ycond, zcond, fcond, "0" * (wordsize // 4))

        xshift = "BVXOR({0}, BVXOR(({1} << 1)[{4}:0], ({2} << {3})[{4}:0]))".format(xin, zin, xsb, self.a, wordsize - 1)
        command += "ASSERT({} = {});\n".format(zout, rotl(xshift, self.d, wordsize))

        yshift = "BVXOR({}, BVXOR({}, ({} << {})[{}:0]))".format(yin, xin, ysb, self.b, wordsize - 1)
        command += "ASSERT({} = {});\n".format(yout, rotl(yshift, self.e, wordsize))

        zshift = "BVXOR({}, BVXOR({}, ({} << {})[{}:0]))".format(zin, yin, zsb, self.c, wordsize - 1)

# 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: parser/stpcommands.py
# def getStringLeftRotate(value, rotation, wordsize):
#     if rotation % wordsize == 0:
#         return "{0}".format(value)
#     command = "((({0} << {1})[{2}:0]) | (({0} >> {3})[{2}:0]))".format(
#         value, (rotation % wordsize), wordsize - 1, (wordsize - rotation) % wordsize)
# 
#     return command


# Path: ciphers/gimli.py
from parser import stpcommands
from ciphers.cipher import AbstractCipher
from parser.stpcommands import getStringLeftRotate as rotl

            y = (y xor x xor (x | z) << b) <<< e
            z = (y xor z xor (x & y) << c) <<< f
        """
        command = ""

        # Conditions for non-linear layer
        xnl = "({} & ~({}|{}))".format(xsb, yin, zin)
        ynl = "({} & ~({}|{}))".format(ysb, xin, zin)
        znl = "({} & ~({}|{}))".format(zsb, xin, yin)

        command += "ASSERT(({} | {} | {}) = 0x{});\n".format(xnl, ynl, znl, "0" * (wordsize // 4))

        # Dependency between bits
        # (x & y & ~z) & ~(xout ^ yout)
        xcond = "(({} & {} & ~{}) & ~(BVXOR({}, {})))".format(xin, yin, zin, xsb, ysb)
        # (x & ~y & z) & (xout ^ zout)
        ycond = "(({} & ~{} & {}) & (BVXOR({}, {})))".format(xin, yin, zin, xsb, zsb)
        # (~x & y & z) & ~(yout ^ zout)
        zcond = "((~{} & {} & {}) & ~(BVXOR({}, {})))".format(xin, yin, zin, ysb, zsb)
        # (x & y & z) & (~(xout ^ yout ^ zout))
        fcond = "(({} & {} & {}) & ~(BVXOR(BVXOR({}, {}), {})))".format(xin, yin, zin, xsb, ysb, zsb)
        command += "ASSERT(({} | {} | {} | {}) = 0x{});\n".format(xcond, ycond, zcond, fcond, "0" * (wordsize // 4))

        xshift = "BVXOR({0}, BVXOR(({1} << 1)[{4}:0], ({2} << {3})[{4}:0]))".format(xin, zin, xsb, self.a, wordsize - 1)
        command += "ASSERT({} = {});\n".format(zout, rotl(xshift, self.d, wordsize))

        yshift = "BVXOR({}, BVXOR({}, ({} << {})[{}:0]))".format(yin, xin, ysb, self.b, wordsize - 1)
        command += "ASSERT({} = {});\n".format(yout, rotl(yshift, self.e, wordsize))

        zshift = "BVXOR({}, BVXOR({}, ({} << {})[{}:0]))".format(zin, yin, zsb, self.c, wordsize - 1)

        command += "ASSERT({} = {});\n".format(xout, rotl(zshift, self.f, wordsize))