(check-sat) vs (check-sat-using smt)
(check-sat) vs (check-sat-using smt)
读了 Leo 的 strategies guide of Z3, and this answer 后，我认为 (check-sat) 和 (check-sat-using smt) 是等价的。但是，当 运行 Z3 4.3.2 对我们的测试套件（230 个 SMTLIB2 文件）执行三次时，(check-sat) 花费了 198s/192s/195s 秒，而 [=11= 花费了 275s/283s/270s ].我也试过 nightly build Z3 4.4.0 d3fb5f2a4cda，区别也差不多。
为什么会这样？
可能相关的更多信息：
- Windows 7 x64, Z3 x64
- 我们所有的测试都配置了
auto_config false 和 smt.mbqi false
- 全部使用量词和未解释的函数
- 一些使用（非线性）int and/or 实数算术
- 所有人都大量使用推弹块
编辑：我最终想做的是为一些 check-sat调用设置超时，但不是对所有人。 AFAIK，check-sat 本身是不可能的，但是 check-sat-using (using-params smt :soft_timeout $timeout) 应该可以。是吗？
我假设您在 SMT2 文件上 运行ning Z3？
Z3 具有在指定 none 时确定基准逻辑的工具（参见 default_tactic.cpp）。 smt 策略是当没有其他策略适用时的后备策略。当 Z3 是 运行 和 -v:10 时，它将显示哪个（子）策略是 运行。
最近，我们还遇到了一些配置参数无法进入 smt 内核的问题。我们已经修复了这些问题，但当然有可能某处仍然存在错误。
读了 Leo 的 strategies guide of Z3, and this answer 后，我认为 (check-sat) 和 (check-sat-using smt) 是等价的。但是，当 运行 Z3 4.3.2 对我们的测试套件（230 个 SMTLIB2 文件）执行三次时，(check-sat) 花费了 198s/192s/195s 秒，而 [=11= 花费了 275s/283s/270s ].我也试过 nightly build Z3 4.4.0 d3fb5f2a4cda，区别也差不多。
为什么会这样？
可能相关的更多信息：
- Windows 7 x64, Z3 x64
- 我们所有的测试都配置了
auto_config false和smt.mbqi false - 全部使用量词和未解释的函数
- 一些使用（非线性）int and/or 实数算术
- 所有人都大量使用推弹块
编辑：我最终想做的是为一些 check-sat调用设置超时，但不是对所有人。 AFAIK，check-sat 本身是不可能的，但是 check-sat-using (using-params smt :soft_timeout $timeout) 应该可以。是吗？
我假设您在 SMT2 文件上 运行ning Z3？
Z3 具有在指定 none 时确定基准逻辑的工具（参见 default_tactic.cpp）。 smt 策略是当没有其他策略适用时的后备策略。当 Z3 是 运行 和 -v:10 时，它将显示哪个（子）策略是 运行。
最近，我们还遇到了一些配置参数无法进入 smt 内核的问题。我们已经修复了这些问题，但当然有可能某处仍然存在错误。