Z3 の一連の制約 (アサーション) を考えると、私が既に持っているモデルがこれらのアサーションを満たしているかどうかを確認する最も効率的な方法は何か疑問に思っています。モデルは、同様の一連の制約から取得されました。Z3 の初期モデル値の指定 のような柔軟な制約ではなく、はい/いいえの答えが必要です。
Windows 7 x64 で C# API を使用して、Z3 3.2 の x64 バージョンを使用してビット ベクトルを操作しています。Contextスレッドごとに 1 つずつ、複数の Z3 オブジェクトをインスタンス化することでマルチスレッド化しています。マルチスレッドがサポートされていないため、Z3 4.0 は使用していません。
私の現在のアプローチは、 を使用Context.AssertCnstr(Term)して、単にモデルを追加の制約セットとしてアサートすることContext.Check()です。
Z3 は、モデルと式を取る "Z3_model_eval" または "Model.Eval" (C# から) と呼ばれるメソッドを公開します。式に量指定子が含まれていて、評価者がモデルを法として量化された式の真理値を判断できない場合、評価は失敗する可能性があります。モデルの評価が成功した場合は、返された値を調べて、モデルがアサーションを強制的に true にするかどうかを判断できます。Z3_model_eval のドキュメントでは、コントラクトについて詳しく説明しています。
http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86670c291a16640b932e7892176a9d1b
モデルの評価ではトートロジーが検出されないため、モデルを式としてシリアル化し、モデルとアサーションの間の含意を Z3 でチェックする方が、用途によってはより適切な場合があります。