Z3で完全に評価された結果は？

Question

Z3は、しばしば、中間関数の束として定義されたモデルを返します。たとえば、次のようなことがよくあります（私の不適切な構文を許してください）。

(define-const myArray (Array Bool Int) (_ as-array f)) 
(define-fun f (x Bool) Int (f!10 (k!26 x))) 

...などです。

私は私のプログラム（ライブラリバインディングを使ってZ3を呼び出す）に取り込むことができ、結果を出力し、それらを実際に実行できる関数に解析することができるようにしたいと思います。お互いに定義された複数の関数ではなく、私が実行できる単一直線プログラムとしてモデル関数を得ることができれば、これははるかに簡単です。

これは可能ですか？私は有限ドメイン関数のみを扱っています。

Answer 1

可能であれば、中間機能を圧縮するために、将来のリリースでモデル構築を更新する予定です。ただし、同じ補助機能を複数のコンテキストで再利用できるため、指数オーバーヘッドが発生する可能性があります。これらのモデルでは、補助機能を拡張する意味がありません。したがって、モデルを後処理したい場合、ユーザーはそのような機能に対処しなければならなくなります。