z3 - 如何在 Ubuntu 上使用 Z3 运行 smtLib 文件？

Question

例如，我有一个 smtLib 文件“encoding.smt”。现在我想通过 z3（独立 exe）在 Ubuntu 机器上使用给定的超时和内存分配运行这个文件。喜欢 ：

$./z3 encoding.smt 240(sec) 6(GB)

我已经从 Z3 下载页面下载了 ubuntu 32 位 zip 文件。我现在必须做什么？“bin”文件夹中有一个 z3 应用程序。我是否需要更改任何环境变量 - 如果我想在 Ubuntu 下编写任何 Z3py 脚本？

谁能给我两个步骤（通过独立的Z3运行.smt文件，给定超时和内存，从z3py脚本运行.smt文件，给定超时和内存）

谢谢你的建议

Answer 1

这些选项分别被调用timeout和memory_max_size。在python界面中，可以如下设置：

set_option(timeout='60')
set_option(memory_max_size='1000')

可以通过运行获得（全局和模块）选项列表z3 -p。这些选项也可以在命令行上设置，例如，

z3 encoding.smt2 timeout=60 memory_max_size=1000