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

【问题标题】：How to run smtLib file using Z3 on Ubuntu?如何在 Ubuntu 上使用 Z3 运行 smtLib 文件？
【发布时间】：2013-11-27 19:24:33
【问题描述】：

例如，我有一个 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文件具有给定的超时和内存）

谢谢你的建议

【问题讨论】：

我使用帮助命令 $ ./z3 -h 获得了超时选项、z3 内存（可执行文件）。但是谁能告诉我如何在 Z3py 脚本中设置选项？像 -solver.set('timeout', 240) solver.set('memory', 6) !!我不知道如何设置这些选项。我看过一些关于超时的帖子，但是如何设置内存限制。谢谢

标签： z3 z3py

【解决方案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

【讨论】：