Z3在C++中最大化

在Z3中，通過模型x = true和y = true，可以清楚地評估以下最大值爲2。Z3在C++中最大化

(declare-const x Bool) 
(declare-const y Bool) 
(declare-const z Bool) 
(assert(= z false)) 
(maximize(
    + 
    (ite (= x true) 1 0) 
    (ite (= y true) 1 0) 
    (ite (= z true) 1 0) 
) 
) 
(check-sat) 
(get-model)

我該如何使用C/C++ API實現這個功能？我試過用這個簡單解析：

Z3_ast parsed = Z3_parse_smtlib2_string(c,<The above Z3>,0,0,0,0,0,0); 
z3::expr simpleExample(c, parsed); 
s.add(simpleExample);

但它打印「unsupported \n ;maximize」。

我不介意手動構建表達式 - 而不是使用構造文件。我根本不知道哪些expr函數或運算符用於「maximize」。

附錄：鑑於最近的一些答案和討論，似乎很清楚，我所要求的並不是正常的功能。因此，我改變了這個問題，要求提供一個方法的具體細節，以便目前的工作成爲現實。

來源

2014-07-04 d' alar' cop

替代方法：MS是否提供Z3的源代碼？如果是這樣，你可以調試正確解析和評估的第一種方法。 – Samuel

我不確定他們這麼做。不過，我知道我的例子在他們的網站上運行。 –

http://z3.codeplex.com/SourceControl/latest#README – Samuel

感謝您指出這個問題。優化功能不是SMT-LIB2的一部分。他們是自定義擴展。此外，解析SMT-LIB2基準的函數沒有任何方法可以反映優化編譯指示。 API解析器無法識別這些擴展的原因是，優化功能未在該解析器中註冊（它們使用命令行解析器註冊）。當然，它們未在「unstable」分支中註冊爲解析器，並且它們也未在包含優化擴展的「opt」分支中的解析器中註冊。我幾乎試圖根據你的帖子「修復」這個，但我現在不確定爲什麼它很有用，因爲這個解析器沒有辦法使用這些擴展。 Z3還有其他擴展程序也未公開給SMT-LIB2分析程序。因此，目前我傾向於保持API暴露的解析器只接受正確的SMT-LIB2。

請注意，Christoph指出，優化功能只是「opt」分支的一部分。歡迎您嘗試一下，但它仍然在攪動很多。該API就我所知的「功能完備」（回答（1））而言。你可以在Python，Java和.NET中使用它。 OCaml集成正在等待OCaml API的其他更改。我沒有機會爲這些API提供任何豐富的文檔，但在http://rise4fun.com/Z3/tutorial/optimization上有一個關於SMT-LIB擴展的簡短教程。

來源

2014-07-06 15:26:42

Z3中的優化特性在`opt'分支中處於沉重構造之下，並未與不穩定或主分支集成在一起。很有可能並非所有功能都已添加到API中。又見尼古拉的這些問題的答案：

Encoding 「at-most-k/at-least-k booleans are true」 constraints in Z3

Simplex in z3 via for-all

來源

2014-07-04 10:36:49

謝謝。幾個問題。 1）你說「這很可能......」有什麼方法可以讓我們更確定這一點嗎？ 2）我們可以在家裏建立和使用這個'opt'分支嗎（順便說一下，最近的提交併不是最近的那些）？ 3）那麼有什麼方法可以使用任何語言或任何平臺（Windows/Linux）使問題中顯示的Z3輸入在使用網站之外運行？ Millionen Dank –

嗨，我剛剛下載並嘗試'opti'分支。命令行Z3仍然沒有選擇「最大化」條件。在代碼裏面，我看到一些看起來很神祕的函數，名字如「z3_check_opti」。我認爲這些都與這個問題有關，但我真的不太清楚如何利用這個問題。你有什麼想法？ –

1）是的。 2）是的。 3）是，但不方便。有些事情需要超過一週才能實施。 –

Z3在C++中最大化

回答

相關問題