Declare a linear (total) order relation.
(name: str, ctx: Context | None = None)
| 4368 | |
| 4369 | |
| 4370 | def LinearOrder(name: str, ctx: Context | None = None) -> FuncDeclRef: |
| 4371 | """Declare a linear (total) order relation.""" |
| 4372 | s = DeclareSort(name) |
| 4373 | return FuncDeclRef(f"{name}_le", (s, s), BoolSort()) |
| 4374 | |
| 4375 | |
| 4376 | def TreeOrder(name: str, ctx: Context | None = None) -> FuncDeclRef: |
nothing calls this directly
no test coverage detected