Z3py支持「字符串」和「序列」

Question

在Z3中，它支持字符串和序列。但Z3py是否也支持它們，或者我們必須使用Python中的字符串或列表？從最新版本看來，新版本確實支持String和Sequence的理論，但我不知道如何使用它。有人會給我一個關於序列的例子嗎？

Answer 1

是的，Z3支持字符串和序列，但在最後一次公開發布中只有基本的支持。您必須從源代碼編譯最新的主文件以獲取所有功能（其中包括Python API）。