refactor solvers to work based of * variable

mythril/laser/smt/independence_solver.py

@@ -1,7 +1,8 @@
 import z3
 
-from mythril.laser.smt import Model
-from typing import Set, List, Dict
+from mythril.laser.smt.model import Model
+from mythril.laser.smt.bool import Bool
+from typing import Set, List, Dict, Union
 
 
 def _get_expr_variables(expression: z3.ExprRef) -> List[z3.ExprRef]:
@@ -97,7 +98,7 @@ class IndependenceSolver:
         """
         self.raw.set(timeout=timeout)
 
-    def add(self, constraints: list) -> None:
+    def add(self, *constraints: List[Bool]) -> None:
         """Adds the constraints to this solver.
 
         :param constraints: constraints to add
@@ -105,7 +106,7 @@ class IndependenceSolver:
         constraints = [c.raw for c in constraints]
         self.constraints.extend(constraints)
 
-    def append(self, constraints: list) -> None:
+    def append(self, *constraints: List[Bool]) -> None:
         """Adds the constraints to this solver.
 
         :param constraints: constraints to add

mythril/laser/smt/solver.py

@@ -3,6 +3,9 @@ import z3
 
 from mythril.laser.smt.expression import Expression
 from mythril.laser.smt.model import Model
+from mythril.laser.smt.bool import Bool
+
+from typing import List
 
 
 class Solver:
@@ -20,27 +23,21 @@ class Solver:
         """
         self.raw.set(timeout=timeout)
 
-    def add(self, constraints: list) -> None:
+    def add(self, *constraints: List[Bool]) -> None:
         """Adds the constraints to this solver.
 
         :param constraints:
         :return:
         """
-        if not isinstance(constraints, list):
-            self.raw.add(constraints.raw)
-            return
         constraints = [c.raw for c in constraints]
         self.raw.add(constraints)
 
-    def append(self, constraints: list) -> None:
+    def append(self, *constraints: List[Bool]) -> None:
         """Adds the constraints to this solver.
 
         :param constraints:
         :return:
         """
-        if not isinstance(constraints, list):
-            self.raw.append(constraints.raw)
-            return
         constraints = [c.raw for c in constraints]
         self.raw.add(constraints)
 

tests/laser/smt/independece_solver_test.py

@@ -96,7 +96,7 @@ def test_Independence_solver_unsat():
     solver = IndependenceSolver()
 
     # Act
-    solver.add(conditions)
+    solver.add(*conditions)
     result = solver.check()
 
     # Assert
@@ -116,7 +116,7 @@ def test_independence_solver_unsat_in_second_bucket():
     solver = IndependenceSolver()
 
     # Act
-    solver.add(conditions)
+    solver.add(*conditions)
     result = solver.check()
 
     # Assert
@@ -136,7 +136,7 @@ def test_independence_solver_sat():
     solver = IndependenceSolver()
 
     # Act
-    solver.add(conditions)
+    solver.add(*conditions)
     result = solver.check()
 
     # Assert