Set union via lambda.
(a: ArrayRef, b: ArrayRef, ctx: Context | None = None)
| 3636 | |
| 3637 | |
| 3638 | def SetUnion(a: ArrayRef, b: ArrayRef, ctx: Context | None = None) -> ArrayRef: |
| 3639 | """Set union via lambda.""" |
| 3640 | sort = a._sort |
| 3641 | if not isinstance(sort, ArraySortRef): |
| 3642 | raise TypeError("SetUnion requires set (array) arguments") |
| 3643 | dom = sort.domain() |
| 3644 | i = Const("__su_i", dom) |
| 3645 | a_i = BoolRef(SelectNode(a._ast, i._ast), _merge(a._vars, i._vars)) |
| 3646 | b_i = BoolRef(SelectNode(b._ast, i._ast), _merge(b._vars, i._vars)) |
| 3647 | body = Or(a_i, b_i) |
| 3648 | lam = Lambda(i, body) |
| 3649 | merged = a._vars | b._vars |
| 3650 | return ArrayRef(lam._ast, sort, merged) |
| 3651 | |
| 3652 | |
| 3653 | def SetIntersect(a: ArrayRef, b: ArrayRef, ctx: Context | None = None) -> ArrayRef: |