IsSubset creates a BoolRef.
(self)
| 2028 | assert isinstance(d, ExprRef) |
| 2029 | |
| 2030 | def test_is_subset(self): |
| 2031 | """IsSubset creates a BoolRef.""" |
| 2032 | from lean_py.z3 import BoolRef |
| 2033 | |
| 2034 | a = EmptySet(IntSort()) |
| 2035 | b = SetAdd(EmptySet(IntSort()), IntVal(1)) |
| 2036 | s = IsSubset(a, b) |
| 2037 | assert isinstance(s, BoolRef) |
| 2038 | |
| 2039 | |
| 2040 | # ------------------------------------------------------------------ |