有什么办法可以增加Z3中模型的内存空间吗？答案

【问题标题】：Is there any way to increase the memory space for a model in Z3?有什么办法可以增加Z3中模型的内存空间吗？
【发布时间】：2012-04-13 07:23:33
【问题描述】：

我使用 Z3 .Net API 开发了一个模型。程序运行良好。但是当我增加输入大小（即模型大小）时，程序会运行很长时间，然后它会结束并给出以下消息：

"Unhandled Exception: OutOfMemoryException."

我想知道有什么办法可以增加程序的内存大小。

【问题讨论】：

标签： .net z3

【解决方案1】：

如果您要编译到x86 平台，您将达到 32 位进程的 2GB 内存限制。如果您的目标是x64，还有2GB limit of .NET objects 是您无法绕过的。根据我的经验，这个 2GB 的限制在正常情况下就足够了。

您可以选择使用 .NET 和 redirecting output string 运行 Z3 可执行文件来自行处理。作为最后的手段，您可以使用 Z3 C API 重写程序中的内存关键部分以绕过上述限制，我认为您可能不想这样做。

【讨论】：

您能否解释一下“您可以选择使用 .NET 运行 Z3 可执行文件并重定向输出字符串以自行处理”？此外，我的一位研究员告诉我，“Yices”没有这种限制。是不是可以让 Z3 使用所有可用内存？
我的意思是使用 .NET 中的 Process 类将 Z3.exe 作为外部进程运行。这就是VCC/Boogie 使用 Z3 的方式。 Yices 没有这个问题，因为 Yices 在 .NET 平台上没有 API，这有固有的限制。