z3' check() 能做什么？答案

【问题标题】：What can z3' check() do?z3' check() 能做什么？
【发布时间】：2021-04-06 04:01:40
【问题描述】：

我最近遇到了一个使用 z3 的 C# 项目。我发现当程序运行到check()时，会持续很长时间，以至于解决方案无法得到结果。更具体地说，这个项目至少有 40 个约束和至少 8 个变量。约束和变量的数量是与输入相关的倍数。只能在输入为1的情况下解决，但只要输入大于1，就会卡在check()中。然而，实际上，我的输入必须大于一。

我想问一下check()有什么用。如果有其他方法可以替换它，或者即使它可以删除。（我试过删了，奇怪的是当输入大于一的时候，可以很快得到结果。）

【问题讨论】：

这个问题似乎与 Visual Studio 应用程序无关。您确定要将其标记为[visual-studio]？
@Llama 该项目在visual studio上运行。
请查看tag description 以查看此标签是否适合您的问题：“如果您对 Visual Studio 特性和功能有特定的疑问，请使用此标签。请勿使用此标签关于恰好用 Visual Studio 编写的代码的问题。”
[visual-studio] 标记可能适用的时间示例：您的问题是关于您正在创建的 Visual Studio 扩展，您正在询问如何在 Visual Studio 中执行某些操作（例如“如何向项目中添加新类？”），您在使用 Visual Studio 时遇到了一些问题（例如“我无法在 VS 中创建 .NET Core 项目。”）。不合适的示例：“我的代码（用 C# 编写）由于错误而无法编译”、“C# 中的 int 和 Int32 有什么区别？”、“我的应用程序在这行代码上崩溃了”等。
visual-studio 标签确实是一个红鲱鱼。我正在删除它。

标签： c# z3

【解决方案1】：

对check 的调用确保给定的约束是可满足的。如果您不调用检查，那么显然z3 不会为您检查任何内容，因此速度更快也就不足为奇了。

关于是否可以删除对check的调用；好吧，你还没有告诉我们这个项目是什么，也没有告诉我们它使用 z3 做什么。但总的来说，没有；您无法删除对check 的呼叫。结果它将返回sat 或unsat（当然，它也可能无法终止或返回unknown，具体取决于断言的约束。）您将根据调用的结果继续。

我建议查看您的代码如何使用调用结果进行检查。或者首先联系开发者。

【讨论】：

感谢您的回答。我会根据您的建议进一步研究。