SMT2 格式日志文件

Question

我正在尝试使用 JNI 接口 (Java) 将 Z3 日志文件的输出格式更改为 SMT2 格式。这个问题在 issue#867 中标记为已解决，但后来实现的方法发生了变化。

根据更改日志，现在应该可以（在 C 中）使用solver.smtlib2_log = file。但是，我无法在 Java 中设置此参数，因为 setParameter() 或任何其他 Solver Module 命令不存在该参数。我是否遗漏了什么，或者目前这仅在非 JNI 中才有可能？

感谢您的帮助。

Answer 1

对于任何想知道的人，smt2-logging 现在可以工作，您可以通过 2 种方式使用它：

1. 全球： set_param("solver.smtlib2_log", "log.smt2")

2. 仅限求解器： 求解器.set("smtlib2_log", "log.smt2")

使用“log.smt2”作为您的日志文件。