(check-sat-using default) 或类似的? [英] (check-sat-using default) or similar?

问题描述

当Z3在没有指定逻辑的情况下运行，并且发出(check-sat)时，default_tactic.cpp 用于有条件地调用最佳"求解器.我想从 SMT-LIB 2 界面访问这个默认策略.

When Z3 is run with no logic specified, and (check-sat) is issued, the logic in default_tactic.cpp is used to conditionally invoke the "best" solver. I would like to access this default tactic from the SMT-LIB 2 interface.

我尝试将 default_tactic.cpp 中的逻辑翻译成 SMT-LIB，然后我想出了这个:

I tried translating the logic from default_tactic.cpp into SMT-LIB, and I came up with this:

(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))))))))))

这个几乎"有效，也就是说，如果你删除带有nra、lira和qffpa的行，那么Z3将执行这没有问题.Z3 4.4.1的SMT-LIB 2接口似乎没有暴露这三种策略.但是，另一个问题是，如果在 Z3 的未来版本中更新了默认策略，那么我上面写的任何硬编码策略都不会更新.

This "almost" works, in that, if you delete the lines with nra, lira, and qffpa, then Z3 will execute this without issue. It seems that those three tactics are not exposed with the SMT-LIB 2 interface of Z3 4.4.1. Another problem with this, though, is that if the default tactic is updated in a future revision of Z3, then any hard-coded strategy like what I wrote above would not be updated.

我真正想做的是发出类似 (check-sat-using default) 或类似命令，并获得与使用 (check-坐).这可能吗?

What I would really like to do is issue a command like (check-sat-using default), or something similar, and get the same result as as obtained with (check-sat). Is this possible?

推荐答案

您引用的文件很旧.Z3 已经转移到 GitHub 并且 default_tactic.cpp 的最新版本是 这里.

The file you refer to is very old. Z3 has since moved to GitHub and the latest version of default_tactic.cpp is here.

QF_FP 的默认策略现在称为 qffp，lira 策略也已导出，我也只导出了 nra(截至本次提交).

The default tactic for QF_FP is now called qffp, the lira tactic has since been exported as well and I just exported nra as well (as of this commit).

截至本次提交，default 策略也已导出，因此现在可以根据要求编写 (check-sat-using default).

As of this commit, the default tactic has also been exported, so it's now possible to write (check-sat-using default) as requested.

这篇关于(check-sat-using default) 或类似的?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！