java - 为什么从 z3 java API 获取查询结果比直接从 z3 获取查询结果慢？

Question

刚刚注意到，对于某些基准测试，通过 java API 从 z3 获取查询结果非常慢。但是，如果我只是将查询转储为 smt2 格式，然后直接在命令行中运行 z3，则需要不到一秒的时间。想知道为什么吗？

Answer 1

我注意到您的问题包含一个(push)命令，删除它会极大地改变性能。当 Z3 第一次看到(push)时，它会切换到支持增量的不同求解器，这会对性能产生巨大影响。通过 -v:15 将详细程度设置为 15，Z3s 输出的第一行会告诉您它正在使用哪个解算器，例如，当出现 push 命令时，它会显示

(combined-solver "using solver 2 (without a timeout)")

如果不是，那么它会说

(combined-solver "using solver 1")

对于给定的示例，求解器 2 的速度明显更快。