Z3pyは "文字列"と "シーケンス"をサポートしています

Question

Z3では、文字列とシーケンスをサポートしています。しかし、Z3pyもそれらをサポートしているのですか、あるいはPythonの文字列やリストを使用する必要がありますか？最新のリリースから、新しいバージョンはStringとSequenceの理論をサポートしていたようでしたが、私はそれをどのように使用するのか分かりません。誰かがシーケンスについての例を教えてくれますか？

Answer 1

はい、Z3は文字列とシーケンスをサポートしますが、最後の一般公開では初歩的なサポートしかありません。ソースから最新のマスターをコンパイルして、すべての機能（Python APIを含む）を取得する必要があります。