Z3 の OCaml API をhttp://research.microsoft.com/en-us/um/redmond/projects/z3/ml/Z3.htmlで閲覧していました。単純な命題式を満たすソルバーによって返されたモデルにアクセスする方法を探します。たとえば、「T」部分ではなく、Z3のSAT部分を使用するだけです。p または q は、モデル p=true、q=false を返す場合があります。私が見つけた最も近いものは、モデルを返す Solver_get_model でした。しかし、モデル タイプが不透明に見えるため、モデルにアクセスする方法が見つかりませんでした。関数シンボルに関連付けられた解釈を取得するための関数 (model_get_func_interp) を見ましたが、それは私が望むものとはまったく異なり、それでも返された情報 (func_interp) をどうするかわかりませんでした。不透明タイプ。私が見ることができる唯一の他の方法は、モデルを文字列に変換することでした。これが唯一の方法ですか？
ありがとう
(公正な警告: 私は自分で OCaml API を使用したことがないので、C API の経験からこれを部分的に推測しています。)
関数を見てみましょう：
val model_get_const_interp : context -> model -> func_decl -> ast
渡される値は明確である必要がcontextありmodelます。func_decl定数の値を実際に探しているのに、なぜ a を渡す必要があるのか疑問に思うかもしれません。問題は、一般にSMTの世界、特にZ3では、定数は引数のない関数のようなものです（したがってget_arity c a == 0、ドキュメントに示されている前提条件です）。
これは、(オプション タイプの) AST を返します。true次のステップは、その AST をorに対してチェックすることfalseです。これを行う 1 つの方法は、関数を呼び出すことです。
val get_decl_kind : context -> func_decl -> decl_kind
OP_TRUEその後、結果をとで比較できますOP_FALSE。
モデルをクエリする別の方法は、
val model_eval : context -> model -> ast -> bool -> ast option
この関数に任意の AST を渡すことができ (例: p ∧ ¬q など)、同じ方法で結果を読み取ることができます。