Get the default value of a constant array. Otherwise build an AppNode.
(a: ExprRef)
| 4290 | |
| 4291 | |
| 4292 | def Default(a: ExprRef) -> ExprRef: |
| 4293 | """Get the default value of a constant array. Otherwise build an AppNode.""" |
| 4294 | if isinstance(a._ast, ConstArrayNode): |
| 4295 | # Return the value stored in the constant array |
| 4296 | sort = a._sort |
| 4297 | rng = sort.range() if isinstance(sort, ArraySortRef) else a._sort |
| 4298 | return ExprRef(a._ast.val, rng, a._vars) |
| 4299 | # Generic: build an application node |
| 4300 | return ExprRef(AppNode(_AstVar("default"), (a._ast,)), a._sort, a._vars) |
| 4301 | |
| 4302 | |
| 4303 | def Ext(a: ExprRef, b: ExprRef) -> ExprRef: |