我在http://research.microsoft.com/en-us/um/redmond/projects/z3/ml/Z3.html浏览 Z3 的 OCaml API寻找一种方法来访问满足简单命题公式的求解器返回的模型，即。仅使用 Z3 的 SAT 部分，而不是“T”部分，例如。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 false。一种方法是调用函数
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 等）并以相同的方式读出结果。