Set intersection via lambda.
(a: ArrayRef, b: ArrayRef, ctx: Context | None = None)
| 3651 | |
| 3652 | |
| 3653 | def SetIntersect(a: ArrayRef, b: ArrayRef, ctx: Context | None = None) -> ArrayRef: |
| 3654 | """Set intersection via lambda.""" |
| 3655 | sort = a._sort |
| 3656 | if not isinstance(sort, ArraySortRef): |
| 3657 | raise TypeError("SetIntersect requires set (array) arguments") |
| 3658 | dom = sort.domain() |
| 3659 | i = Const("__si_i", dom) |
| 3660 | a_i = BoolRef(SelectNode(a._ast, i._ast), _merge(a._vars, i._vars)) |
| 3661 | b_i = BoolRef(SelectNode(b._ast, i._ast), _merge(b._vars, i._vars)) |
| 3662 | body = And(a_i, b_i) |
| 3663 | lam = Lambda(i, body) |
| 3664 | merged = a._vars | b._vars |
| 3665 | return ArrayRef(lam._ast, sort, merged) |
| 3666 | |
| 3667 | |
| 3668 | def SetComplement(s: ArrayRef, ctx: Context | None = None) -> ArrayRef: |