Does Z3py support Linear Temporal logic LTL? If yes, can you provide an example of simple explain.

有帮助吗?

解决方案

Z3 does not support LTL or other temporal or modal logics. The input accepted by Z3 is first-order logic with theories, such as arithmetic.

许可以下: CC-BY-SA归因
不隶属于 StackOverflow
scroll top