Z3py是否支持線性時間邏輯LTL？

Question

Z3py支持線性時間邏輯LTL嗎？ 如果是，你能提供一個簡單解釋的例子。

Answer 1

Z3不支持LTL或其他時態或模態邏輯。 Z3接受的輸入是帶有理論的一階邏輯，如算術。