|
10 | 10 | import lhsmdu
|
11 | 11 | from pandas import DataFrame
|
12 | 12 | from scipy.stats._distn_infrastructure import rv_generic
|
13 |
| -from z3 import Bool, BoolRef, Const, EnumSort, Int, RatNumRef, Real, String, DatatypeRef |
| 13 | +from z3 import Bool, BoolRef, Const, EnumSort, Int, RatNumRef, Real, String |
14 | 14 |
|
15 | 15 | # Declare type variable
|
16 | 16 | T = TypeVar("T")
|
@@ -76,7 +76,6 @@ def __init__(self, name: str, datatype: T, distribution: rv_generic = None):
|
76 | 76 | def __repr__(self):
|
77 | 77 | return f"{self.typestring()}: {self.name}::{self.datatype.__name__}"
|
78 | 78 |
|
79 |
| - # TODO: We're going to need to implement all the supported Z3 operations like this |
80 | 79 | def __ge__(self, other: Any) -> BoolRef:
|
81 | 80 | """Create the Z3 expression `other >= self`.
|
82 | 81 |
|
@@ -167,8 +166,6 @@ def cast(self, val: Any) -> T:
|
167 | 166 | return val.as_string()
|
168 | 167 | if (isinstance(val, (float, int, bool))) and (self.datatype in (float, int, bool)):
|
169 | 168 | return self.datatype(val)
|
170 |
| - if issubclass(self.datatype, Enum) and isinstance(val, DatatypeRef): |
171 |
| - return self.datatype(str(val)) |
172 | 169 | return self.datatype(str(val))
|
173 | 170 |
|
174 | 171 | def z3_val(self, z3_var, val: Any) -> T:
|
|
0 commit comments