z3 - 我想知道Z3是否支持输入文件包含另一个文件

Question

我有两个文件，一个是变量定义文件，另一个是公式文件。你能告诉我如何将变量定义文件插入公式文件吗？在 yices 中，我们可以使用 "(include "file")" 来完成。

Answer 1

Z3 没有include命令。但是，您可以使用cat和管道来做您想做的事情。例如，假设您有文件def.smt2和form.smt2. 然后，您可以使用以下命令连接然后调用 Z3。

  cat def.smt2 form.smt2 | z3 -in -smt2

该选项-in告诉 z3 使用标准输入，并且-smt2输入是 SMT 2.0 格式。