Array extensionality: return an index where a and b differ.
(a: ExprRef, b: ExprRef)
| 4301 | |
| 4302 | |
| 4303 | def Ext(a: ExprRef, b: ExprRef) -> ExprRef: |
| 4304 | """Array extensionality: return an index where a and b differ.""" |
| 4305 | sort = a._sort |
| 4306 | dom = sort.domain() if isinstance(sort, ArraySortRef) else IntSort() |
| 4307 | merged = _merge(a._vars, b._vars) |
| 4308 | return ExprRef(AppNode(_AstVar("ext"), (a._ast, b._ast)), dom, merged) |
| 4309 | |
| 4310 | |
| 4311 | # --------------------------------------------------------------------------- |