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

Question

例如，我有一个smtLib文件'encoding.smt‘。现在，我想在Ubuntu机器上使用给定的超时和内存分配由z3 (独立执行程序)运行这个文件。比如：

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

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

谁能给我两个步骤(运行.smt文件 by ，独立Z3和给定的超时和内存，以及从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