Write to array.
(a: ArrayRef, idx: ExprRef, val: ExprRef)
| 1186 | |
| 1187 | |
| 1188 | def Store(a: ArrayRef, idx: ExprRef, val: ExprRef) -> ArrayRef: |
| 1189 | """Write to array.""" |
| 1190 | sort = a._sort |
| 1191 | if not isinstance(sort, ArraySortRef): |
| 1192 | raise TypeError(f"Store requires ArrayRef, got {type(a)}") |
| 1193 | merged: frozenset[tuple[str, ASTSort]] = frozenset().union(a._vars, idx._vars, val._vars) |
| 1194 | return ArrayRef( |
| 1195 | StoreNode(a._ast, idx._ast, val._ast), |
| 1196 | sort, |
| 1197 | merged, |
| 1198 | ) |
| 1199 | |
| 1200 | |
| 1201 | def K(domain: SortRef, val: ExprRef) -> ArrayRef: |