# 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
        command += "ASSERT({} = ~{});\n".format(w[0],
            stpcommands.getStringEq(a[0], a[3], b[0]))


        # Second addition
        tmp_xor0 = "BVXOR({}, {})".format(rotl(b[0], 7, wordsize), a[1])
        command += "ASSERT({});\n".format(
            stpcommands.getStringAdd(a[0], tmp_xor0, b[1], wordsize))

        command += "ASSERT({} = ~{});\n".format(w[1],
            stpcommands.getStringEq(a[0], tmp_xor0, b[1]))


        # Third addition
        tmp_xor1 = "BVXOR({}, {})".format(rotl(b[1], 9, wordsize), a[2])
        command += "ASSERT({});\n".format(
            stpcommands.getStringAdd(tmp_xor0, tmp_xor1, b[2], wordsize))

        command += "ASSERT({} = ~{});\n".format(w[2],
            stpcommands.getStringEq(tmp_xor0, tmp_xor1, b[2]))

        # Fourth addition
        tmp_xor2 = "BVXOR({}, {})".format(rotl(b[2], 13, wordsize), a[3])
        command += "ASSERT({});\n".format(
            stpcommands.getStringAdd(tmp_xor1, tmp_xor2, b[3], wordsize))

        command += "ASSERT({} = ~{});\n".format(w[3],
            stpcommands.getStringEq(tmp_xor1, tmp_xor2, b[3]))

        # Outputs

# 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/salsa.py
from parser import stpcommands
from ciphers.cipher import AbstractCipher
from parser.stpcommands import getStringLeftRotate as rotl

        command += "ASSERT({} = ~{});\n".format(w[0],
            stpcommands.getStringEq(a[0], a[3], b[0]))


        # Second addition
        tmp_xor0 = "BVXOR({}, {})".format(rotl(b[0], 7, wordsize), a[1])
        command += "ASSERT({});\n".format(
            stpcommands.getStringAdd(a[0], tmp_xor0, b[1], wordsize))

        command += "ASSERT({} = ~{});\n".format(w[1],
            stpcommands.getStringEq(a[0], tmp_xor0, b[1]))


        # Third addition
        tmp_xor1 = "BVXOR({}, {})".format(rotl(b[1], 9, wordsize), a[2])
        command += "ASSERT({});\n".format(
            stpcommands.getStringAdd(tmp_xor0, tmp_xor1, b[2], wordsize))

        command += "ASSERT({} = ~{});\n".format(w[2],
            stpcommands.getStringEq(tmp_xor0, tmp_xor1, b[2]))

        # Fourth addition
        tmp_xor2 = "BVXOR({}, {})".format(rotl(b[2], 13, wordsize), a[3])
        command += "ASSERT({});\n".format(
            stpcommands.getStringAdd(tmp_xor1, tmp_xor2, b[3], wordsize))

        command += "ASSERT({} = ~{});\n".format(w[3],
            stpcommands.getStringEq(tmp_xor1, tmp_xor2, b[3]))

        # Outputs

        command += "ASSERT({} = BVXOR({}, {}));\n".format(c[0], a[0], rotl(b[3], 18, wordsize))