Z3 的默认求解器是什么？

Question

【新手】。根据http://rise4fun.com/Z3/tutorialcontent/strategies，“smt”是 Z3 的主要策略。但是，明确地使用它甚至可以解决微不足道的问题。如何在战术序列中引用默认的 Z3 求解器？

http://rise4fun.com/Z3/K8nn

(declare-fun var1 () Real)
(assert (= (* var1 var1) 9.0))
(assert (< var1 0.0))
; Works
;(check-sat)
;(get-model)
; Breaks
(check-sat-using smt)
(get-info :reason-unknown)

Answer 1

默认情况下，Z3 将查看您的公式以确定需要哪些功能和逻辑，然后它会调用合适的求解器/策略。您可以提供一个 (set-logic ...) 命令来控制它，或者您可以直接使用这些默认策略之一。有关 Z3 具有自定义策略的 SMT 逻辑列表，请参阅default_tactic.cpp。如果它们都不匹配并且没有选择逻辑，则“smt”是将执行的策略。

要查看运行了哪些策略，请添加-v:10到命令行，Z3 将在执行时打印策略名称和统计信息。

对于这种类型的非线性实数，“smt”策略不是很强，它会很快放弃并返回“unknown”。但是，这不是此类问题的默认策略；相反（经过一些预处理）它是解决问题的“nlsat”策略，如通过 QF_NRA 的默认策略调用的（参见qfnra.cpp）。