Map function f over finite set s.
(f: FuncDeclRef, s: ArrayRef)
| 3724 | |
| 3725 | |
| 3726 | def FiniteSetMap(f: FuncDeclRef, s: ArrayRef) -> ArrayRef: |
| 3727 | """Map function f over finite set s.""" |
| 3728 | sort = s._sort |
| 3729 | if not isinstance(sort, ArraySortRef): |
| 3730 | raise TypeError("FiniteSetMap requires set (array) argument") |
| 3731 | dom = sort.domain() |
| 3732 | i = Const("__fsm_i", f._range) |
| 3733 | x = Const("__fsm_x", dom) |
| 3734 | # {f(x) | x in s} == {y | exists x, x in s /\ f(x) == y} |
| 3735 | # Simplified: use Lambda over the range |
| 3736 | fx = f(x) |
| 3737 | mem = BoolRef(SelectNode(s._ast, x._ast), _merge(s._vars, x._vars)) |
| 3738 | body = And(mem, fx == i) |
| 3739 | exists_body = Exists([x], body) |
| 3740 | lam = Lambda(i, exists_body) |
| 3741 | result_sort = SetSort(f._range) |
| 3742 | return ArrayRef(lam._ast, result_sort, _merge(s._vars, frozenset([(f._name, f._ast_sort)]))) |
| 3743 | |
| 3744 | |
| 3745 | def FiniteSetFilter(f: FuncDeclRef, s: ArrayRef) -> ArrayRef: |