Z3 が解釈されない並べ替えを含むモデルを返す場合、たとえばQ、 の形式の定数を使用しますQ!val!0。
ただし、ゼロからクエリを作成し、このシンボルを の居住者として参照するとQ、Z3はそれQ!val!0が未知の定数であると文句を言います。
Q基本的に、以前に返されたモデルとは異なるモデルを提供するように Z3 に依頼することで、Z3 に のすべての住民を列挙させようとしています。したがって、以降の Z3 の呼び出しでは、これらの定数を参照する必要があります。
SMT-Lib2 インターフェイスを使用してこれを行う方法はありますか?