给定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检查模型和断言之间的含义可能更适合某些用途。