（check-sat-using default）或类似的？

Question

当 Z3 为运行且未指定逻辑且发出 (check-sat) 时，default_tactic.cpp 中的逻辑用于有条件地调用 "best" 求解器。我想从 SMT-LIB 2 界面访问这个默认策略。

我尝试将逻辑从 default_tactic.cpp 翻译成 SMT-LIB，我想出了这个：

(check-sat-using (and-then simplify
    (cond is-qfbv qfbv
    (cond is-qflia qflia
    (cond is-qflra qflra
    (cond is-qfnra qfnra
    (cond is-qfnia qfnia
    (cond is-nra nra
    (cond is-lira lira
    (cond is-qffpabv qffpa
    smt))))))))))

此 "almost" 有效，因为如果您删除带有 nra、lira 和 qffpa 的行，则 Z3 将毫无问题地执行此操作。 Z3 4.4.1的SMT-LIB 2接口似乎没有暴露这三种策略。但是，另一个问题是，如果默认策略在 Z3 的未来版本中更新，那么任何像我上面写的那样的硬编码策略都不会更新。

我真正想做的是发出像 (check-sat-using default) 或类似的命令，并获得与 (check-sat) 相同的结果。这可能吗？

Answer 1

您引用的文件非常旧。 Z3 已移至 GitHub and the latest version of default_tactic.cpp is here。

QF_FP 的默认策略现在称为 qffp，lira 策略也已导出，我也刚刚导出 nra（截至this commit).

编辑： 自 this commit 起，default 策略也已导出，因此现在可以按要求编写 (check-sat-using default) .

（check-sat-using default）或类似的？

(check-sat-using default) or similar?

z3