给定 Z3 中的一组约束（断言），我想知道检查我已经拥有的模型是否满足这些断言的最有效方法是什么。该模型是从类似的一组约束中获得的。我需要一个是/否的答案，而不是像为 Z3 指定初始模型值那样的软约束。
我正在使用 Z3 3.2 的 x64 版本在 Windows 7 x64 上使用 C# API 对位向量进行操作。我通过实例化多个 Z3Context对象来实现多线程，每个线程一个。由于缺乏对多线程的支持，我没有使用 Z3 4.0。
我目前的方法只是将模型断言为一组额外的约束Context.AssertCnstr(Term)，然后简单地调用Context.Check().
Z3 公开了一个名为“Z3_model_eval”或“Model.Eval”（来自 C#）的方法，它接受一个模型和一个表达式。如果表达式包含量词并且评估者无法确定量化公式模模型的真值，则评估可能会失败。如果模型评估成功，您可以检查返回值以确定模型是否强制断言为真。Z3_model_eval 的文档更详细地详细说明了合同：
http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86670c291a16640b932e7892176a9d1b
模型评估不会检测重言式，因此将模型序列化为公式并让 Z3 检查模型和断言之间的含义可能更适合某些用途。