smt2 文件的 Java API 推送和弹出

Question

我生成了一个 smt2 文件，该文件已被 Z3 (4.3) 通过 Z3 Java API 成功读取（解析）。现在我想知道如何让Z3开始解决多个范围内的公式（push和pop）。 smt2 文件包含 push 和 pop 命令的列表。

我知道您可以使用 solver.push() 和 solver.pop() 来做到这一点，但这里的问题是文件中已经生成了范围，我没有使用 Z3 内部 API 来制作这些公式和范围.我只需要将整个 smt2 文件提供给 Z3 并执行多个求解（只有这部分我需要 Z3 API）。通过简单地调用 solver.check() 方法，Z3 似乎完全忽略了 smt2 文件中间的所有范围，只给了我最后一个（check-sat）命令的模型。

那么有没有一种方法可以调用 Z3 API (Java) 来对现有 smt2 文件中定义的多个范围执行一系列求解？

任何具体的例子都将不胜感激。

Answer 1

不，没有办法做到这一点。解析器函数可以读取输入文件，但它们忽略所有 SMT 命令，即，输出总是只有一组断言，没有别的。

在您处理文件的用例中，推荐的过程是将文件通过管道传输到 Z3，方法是直接提供文件名或通过管道传输到标准输入。