z3 MaxSAT示例錯誤

我有興趣使用z3（Microsoft Research）網站上提供的MaxSAT/MaxSMT c示例（特別是maxsat.c）。使用Visual Studio 2010，我最終得到了編譯示例（使用全新安裝的z3 4.0）。但是，我無法使用我的（SMT 2.0）模型來運行它們。此外，我無法獲得發佈在this問題中的示例。z3 MaxSAT示例錯誤

在第一種情況下，當我編譯的程序試圖調用文件get_hard_constraints中的Z3_get_smtlib_num_formulas時崩潰。我不知道爲什麼，而是我得到標準的Windows 7「這個程序已停止工作」彈出。

在第二種情況下，它報告unsupported ;benchmark。

爲了幫助我完成這項工作，我在想如果（a）編譯此代碼時是否有人遇到過類似的問題？如果是的話，您是如何解決這些問題的？（b）如何調試文件的編譯（假設它是正確的）？也就是說，是否有人可以枚舉正確的庫（和庫版本 - 例如z3 4.0？）以包含在編譯器選項中以使此示例正常工作？

在任何一種情況下，第二種情況中報告的錯誤信息也將被讚賞：它究竟意味着什麼？關鍵字無效？ SMT輸入是錯誤的版本？或者是其他東西？

謝謝。

來源

2012-09-27 Jan Gorzny

MaxSAT示例尚未更新爲SMTLIB 2.0。它使用函數Z3_parse_smtlib_file來解析輸入，這意味着它目前僅支持SMTLIB 1.0。

本例與Z3一起發佈，即您應該收到Z3-4.0/examples/maxsat/的副本，其中也包含編譯和執行腳本。

通過在Visual Studio命令提示符下運行build.cmd或在Linux上運行build.sh，編譯應該很簡單。

來源

2012-09-27 18:46:46

感謝您的回答。這個例子也不起作用（我之前忘了提及這個），但我解決了這個問題（一些環境變量沒有設置）。你知道是否有可能用新的函數調用（也可能是其他任何特定於舊標準的函數調用），並讓它在SMTLIB 2.0上工作？ –

是的，還有一個SMT2函數，它被稱爲Z3_parse_smtlib2_file。該示例將需要進一步修改，因爲此函數僅返回單個表達式，而不是一組假設和一組公式。所以，目前還不清楚如何區分SMT2中的軟硬件限制（也許這可以通過註釋完成）。 –

z3 MaxSAT示例錯誤

回答

相關問題