Set complement via lambda.
(s: ArrayRef, ctx: Context | None = None)
| 3666 | |
| 3667 | |
| 3668 | def SetComplement(s: ArrayRef, ctx: Context | None = None) -> ArrayRef: |
| 3669 | """Set complement via lambda.""" |
| 3670 | sort = s._sort |
| 3671 | if not isinstance(sort, ArraySortRef): |
| 3672 | raise TypeError("SetComplement requires set (array) argument") |
| 3673 | dom = sort.domain() |
| 3674 | i = Const("__sc_i", dom) |
| 3675 | s_i = BoolRef(SelectNode(s._ast, i._ast), _merge(s._vars, i._vars)) |
| 3676 | body = Not(s_i) |
| 3677 | lam = Lambda(i, body) |
| 3678 | return ArrayRef(lam._ast, sort, s._vars) |
| 3679 | |
| 3680 | |
| 3681 | def SetDifference(a: ArrayRef, b: ArrayRef, ctx: Context | None = None) -> ArrayRef: |