from mythril.laser.smt.bitvec import BitVec
from mythril.laser.smt.expression import Expression
from mythril.laser.smt.bool import Bool

import z3


class SymbolFactory:
    @staticmethod
    def BitVecVal(value: int, size: int, annotations=None):
        raise NotImplementedError()

    @staticmethod
    def BitVecSym(name: str, size: int, annotations=None):
        raise NotImplementedError()


class SmtSymbolFactory(SymbolFactory):

    @staticmethod
    def BitVecVal(value: int, size: int, annotations=None):
        raw = z3.BitVecVal(value, size)
        return BitVec(raw, annotations)

    @staticmethod
    def BitVecSym(name: str, size: int, annotations=None):
        raw = z3.BitVec(name, size)
        return BitVec(raw, annotations)


class Z3SymbolFactory(SymbolFactory):
    @staticmethod
    def BitVecVal(value: int, size: int, annotations=None):
        return z3.BitVecVal(value, size)

    @staticmethod
    def BitVecSym(name: str, size: int, annotations=None):
        return z3.BitVec(name, size)


symbol_factory = Z3SymbolFactory()


@@ -171,195 +171,943 @@
     
-@staticmethod%0A    def BitVecVal(value: int, size: int, annotations=None):%0A        raise NotImplementedError()%0A%0A    @staticmethod%0A    def BitVecSym(name: str, size: int, annotations=None):
+%22%22%22%0A    A symbol factory provides a default interface for all the components of mythril to create symbols%0A    %22%22%22%0A%0A    @staticmethod%0A    def BitVecVal(value: int, size: int, annotations=None):%0A        %22%22%22%0A        Creates a new bit vector with a concrete value%0A        :param value: The concrete value to set the bit vector to%0A        :param size: The size of the bit vector%0A        :param annotations: The annotations to initialize the bit vector with%0A        :return: The freshly created bit vector%0A        %22%22%22%0A        raise NotImplementedError()%0A%0A    @staticmethod%0A    def BitVecSym(name: str, size: int, annotations=None):%0A        %22%22%22%0A        Creates a new bit vector with a symbolic value%0A        :param name: The name of the symbolic bit vector%0A        :param size: The size of the bit vector%0A        :param annotations: The annotations to initialize the bit vector with%0A        :return: The freshly created bit vector%0A        %22%22%22
 %0A   
@@ -1147,16 +1147,17 @@
 %0A%0Aclass 
+_
 SmtSymbo
@@ -1181,16 +1181,137 @@
 ctory):%0A
+    %22%22%22%0A    An implementation of a SymbolFactory that creates symbols using%0A    the classes in: mythril.laser.smt%0A    %22%22%22
 %0A    @st
@@ -1373,32 +1373,95 @@
 otations=None):%0A
+        %22%22%22 Creates a new bit vector with a concrete value %22%22%22%0A
         raw = z3
@@ -1594,32 +1594,95 @@
 otations=None):%0A
+        %22%22%22 Creates a new bit vector with a symbolic value %22%22%22%0A
         raw = z3
@@ -1749,16 +1749,17 @@
 %0A%0Aclass 
+_
 Z3Symbol
@@ -1778,24 +1778,118 @@
 olFactory):%0A
+    %22%22%22%0A    An implementation of a SymbolFactory that directly returns%0A    z3 symbols%0A    %22%22%22%0A
     @staticm
@@ -1946,32 +1946,95 @@
 otations=None):%0A
+        %22%22%22 Creates a new bit vector with a concrete value %22%22%22%0A
         return z
@@ -2148,38 +2148,163 @@
     
-return z3.BitVec(name, size)%0A%0A
+%22%22%22 Creates a new bit vector with a symbolic value %22%22%22%0A        return z3.BitVec(name, size)%0A%0A%0A# This is the instance that other parts of mythril should use
 %0Asym
@@ -2317,16 +2317,17 @@
 ctory = 
+_
 Z3Symbol

add documentation to symbol factory