什麼是Z3的默認解算器？

[新手]。根據http://rise4fun.com/Z3/tutorialcontent/strategies，'smt'是Z3的主要策略。但是，使用它明確地打破即使是微不足道的問題。如何在戰術序列中引用默認的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)

來源

2016-02-29 Cristian Petrescu-Prahova

相關：https://stackoverflow.com/q/34789949/1959808 –

默認情況下，Z3會考慮你的公式來確定哪些功能和需要的邏輯，然後它會調用合適的求解器/戰術。您可以提供一個（set-logic ...）命令來引導它，或者您可以直接使用其中一種默認策略。有關Z3具有自定義策略的SMT邏輯列表，請參閱default_tactic.cpp。如果它們中沒有一個匹配並且沒有選擇邏輯，則「smt」是將被執行的策略。

要查看運行哪些策略，請將-v:10添加到命令行，並且Z3將在執行時打印策略名稱和統計信息。

對於這種類型的非線性實數，「smt」策略不是很強，它會很快放棄並返回「未知」。但是，這不是這類問題的默認策略;相反（經過一些預處理），它是解決問題的「nlsat」策略，如通過QF_NRA的默認策略調用（請參閱qfnra.cpp）。

來源

2016-02-29 18:21:46

感謝您的迴應！我正在通過Java API運行Z3。有沒有一種方法可以問Z3'''ctx.mkTactic（select-best）'''，當問題被完全指定後，它將調用求解器的魔法選擇算法？這裏有一點雞雞蛋問題，因爲求解器必須在問題約束被添加之前建立。提前解決問題的綜合解決方案是否合理？ –

問題：如何從Java API指定''-v：10'''？ ''''ctx.mkParams（）'''似乎並不正確。 [感謝一個真棒工具，順便說一下！] –

是的，所有這些都是可能的。求解器類的構造函數需要參數，這些參數可以是用於邏輯聲明或策略的字符串。默認的mkSolver（）會爲你選擇一種策略，並且在所有的斷言被添加後它會這樣做。 –

什麼是Z3的默認解算器？

回答

相關問題