我想在设置特定逻辑时重复使用/激活的策略，但我需要避免使用set-logic。
所以有什么办法可以使Z3以可重用的形式显示其采用的策略/配置？
例如(get-tactics)会回答一些我可以用作apply或check-sat-using的参数的问题
否则，有什么可能的方法来推断作为set-logic指令的副作用而部署的策略？
我无法使用(set-logic QF_LIA)，因为这使我无法使用special-functions，例如偏序。但是，一旦我删除了set-logic，我以前曾经以fast（200毫秒）为单位的UNSAT查询就会变成“未知”，例如，除了QF_LIA以外不使用任何其他内容。
因此，我知道设置逻辑有助于配置求解器，但是由于我无法使用set-logic，因此现在我需要绕过此内置配置机制。
我已经尝试过一些check-sat-using，但没有设置逻辑，但结果复杂：
smt相当快400msqflia令人惊讶地与设置逻辑不同，它慢20s但找到答案default预期中的未知，我想（希望）它与基本的check-sat这些都不像设置QF_LIA（200 ms）一样好。
[以详细模式-v:10运行Z3时，我可以在较快的运行中使用nnf-cnf看到它，这显然有助于触发一些简化，而较慢的版本开始分支（在此示例中为UNSAT）。但是这些信息很难利用，我知道Z3可以针对内置的问题进行正确的设置，但是如何触发它们呢？
逻辑选择和策略只是松散相关：选择逻辑将指示范围内的名称。策略决定了如何实际解决问题。通常，这两者之间是不相关的。
但是我确实看到您的观点，如果z3列出了适用的策略，那将是很好的。恐怕您可以从详细输出中收集到的信息至少是暂时的，因为没有(get-tactics)或类似的命令。您当然可以在他们的问题跟踪器中要求它，也许他们可以指出您可以使用的其他电话。 （https://github.com/Z3Prover/z3/issues）