C# 中的 Z3，只得到 1 个结果

【问题标题】：Z3 in C#, Only getting 1 resultC# 中的 Z3，只得到 1 个结果
【发布时间】：2016-02-21 05:32:09
【问题描述】：

我在 Visual Studio 中使用 z3，我想用以下内容做一个简单的检查 x > 3 运行代码后，我的模型中只得到一个结果。为什么我只能得到一个结果，我将如何在 C# 中完成模型？

【问题讨论】：

【解决方案1】：

Z3 是一个可满足性求解器（SMT 中的 S），即它检查是否存在 1 个满足公式的赋值。它可以在某些特殊情况下计算解决方案集，如果问题设置正确，但没有更多细节，我无法判断这是否适用于您的问题。

当然，在获得一个令人满意的分配后，您可以添加一个新的约束，强制排除您刚刚获得的分配，然后再获得一个新的分配。

【讨论】：