2
我剛剛開始使用Z3解算器，在它開源後。SAT支持獲取模型（類似於CVC4中的--dump-models）
我現在正在使用Z3作爲命令行黑盒工具，並且希望在模型爲SAT時傾倒反例。我主要是通過QF_NIA和QF_LIA查詢。我注意到Z3中不存在與CVC4s相同的選項--dump-models。我可以在SMT2lib文件（check-sat）之後寫入（dump-model），但是如果公式實際上不合格，則會出錯。
SMT2 lib的語言雖然看起來很清晰，但遠不是一個正確解釋的交互式語言。例如，像（cond（check-sat）（dump-model））應該可以工作。在任何情況下，作爲Z3源代碼的新手，我已經破解了一些東西，並認爲我會與開發團隊分享它。我已經插入了一個補丁（不知道如何在stackoverflow中添加東西），如果將其納入主線，這將非常棒。讓我知道是否有更好的方法來做同樣的事情。
此外，道歉，如果這不是這種類型的討論正確的論壇。請讓我知道，然後正確的大道。
對於看似簡單的查詢，我也有一些與Z3性能相關的問題，CVC4能夠輕鬆解決，我將爲未來的討論保留。
感謝，
潘卡
補丁開始：
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 7316085..c45f668 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -40,6 +40,8 @@ Notes:
#include"scoped_timer.h"
#include"interpolant_cmds.h"
+extern bool g_get_model_when_sat;
+
func_decls::func_decls(ast_manager & m, func_decl * f):
m_decls(TAG(func_decl*, f, 0)) {
m.inc_ref(f);
@@ -1355,8 +1357,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
m_solver->set_status(r);
display_sat_result(r);
validate_check_sat_result(r);
- if (r == l_true)
+ if (r == l_true) {
validate_model();
+ if (g_get_model_when_sat) {
+ symbol gm("get-model");
+ cmd *gm_cmd = find_cmd(gm);
+ gm_cmd->prepare(*this);
+ gm_cmd->execute(*this);
+ }
+ }
}
else {
// There is no solver installed in the command context.
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index 0eb612f..2fbd8ec 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -43,6 +43,7 @@ bool g_standard_input = false;
input_kind g_input_kind = IN_UNSPECIFIED;
bool g_display_statistics = false;
bool g_display_istatistics = false;
+bool g_get_model_when_sat = false;
void error(const char * msg) {
std::cerr << "Error: " << msg << "\n";
@@ -92,6 +93,7 @@ void display_usage() {
//
std::cout << "\nOutput:\n";
std::cout << " -st display statistics.\n";
+ std::cout << " -m Execute get-model after every check-sat, if model is available\n";
#if defined(Z3DEBUG) || defined(_TRACE)
std::cout << "\nDebugging support:\n";
#endif
@@ -174,6 +176,9 @@ void parse_cmd_line_args(int argc, char ** argv) {
else if (strcmp(opt_name, "st") == 0) {
g_display_statistics = true;
}
+ else if (strcmp(opt_name, "m") == 0) {
+ g_get_model_when_sat = true;
+ }
else if (strcmp(opt_name, "ist") == 0) {
g_display_istatistics = true;
}
補丁結束