From bcee8c045e93e0527bf5dad8a29631c3681929e1 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Wed, 5 Dec 2018 13:08:53 +0100
Subject: [PATCH] Create symbol factories and move bitvec constructors there

---
 mythril/laser/smt/__init__.py | 42 +++++++++++++++++++++++++++++++++++
 mythril/laser/smt/bitvec.py   |  9 --------
 2 files changed, 42 insertions(+), 9 deletions(-)

diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py
index e69de29b..fc65fd4e 100644
--- a/mythril/laser/smt/__init__.py
+++ b/mythril/laser/smt/__init__.py
@@ -0,0 +1,42 @@
+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()
+
diff --git a/mythril/laser/smt/bitvec.py b/mythril/laser/smt/bitvec.py
index 3f31268a..abfd9336 100644
--- a/mythril/laser/smt/bitvec.py
+++ b/mythril/laser/smt/bitvec.py
@@ -92,12 +92,3 @@ def UDiv(a: BitVec, b: BitVec) -> BitVec:
     union = a.annotations + b.annotations
     return BitVec(z3.UDiv(a.raw, b.raw), annotations=union)
 
-
-def BitVecVal(value, size, annotations=None):
-    raw = z3.BitVecVal(value, size)
-    return BitVec(raw, annotations)
-
-
-def BitVecSym(name, size, annotations=None):
-    raw = z3.BitVec(name, size)
-    return BitVec(raw, annotations)