Check if a is a subset of b.
(a: ArrayRef, b: ArrayRef)
| 3684 | |
| 3685 | |
| 3686 | def IsSubset(a: ArrayRef, b: ArrayRef) -> BoolRef: |
| 3687 | """Check if a is a subset of b.""" |
| 3688 | sort = a._sort |
| 3689 | if not isinstance(sort, ArraySortRef): |
| 3690 | raise TypeError("IsSubset requires set (array) arguments") |
| 3691 | dom = sort.domain() |
| 3692 | i = Const("__iss_i", dom) |
| 3693 | a_i = BoolRef(SelectNode(a._ast, i._ast), _merge(a._vars, i._vars)) |
| 3694 | b_i = BoolRef(SelectNode(b._ast, i._ast), _merge(b._vars, i._vars)) |
| 3695 | return ForAll([i], Implies(a_i, b_i)) |
| 3696 | |
| 3697 | |
| 3698 | def SetHasSize(s: ArrayRef, n: int) -> BoolRef: |