z3 - ソート Seq の定義

Question

sort Seq の定義を知りたいです。Z3 SMT 2.0 ガイドでその定義を見つけることができませんでした。Seq という名前のソートを定義しようとしたため、Seq が既に定義されていることに気付きました。Seq に関連するアサーションはありますか?

ありがとう！！

マキシ

Answer 1

はい、, Seq(RegEx正規表現) とFP(浮動小数点) は Z3 4.0 で「予約済み」です。これらはまだ実装されていませんが、将来のリリースで利用可能になる予定です。たとえば、Z3 にはseq-last、 、seq-concat、seq-lengthおよびその他の多くの組み込み関数があります。Z3 4.0 では、これらの並べ替えと関数は単なる「スタブ」であり、解釈されない並べ替えと関数のように動作します。そのため、それらのドキュメントはありません。