Support for getting models when SAT (similar to --dump-models in CVC4)

Question

I have just started playing with Z3 solver, after it was open sourced.

I am using Z3 as a command line black box tool at present, and would like it to dump counterexamples if the model is SAT. I am mostly passing QF_NIA and QF_LIA queries. I noticed that an option equivalent to CVC4s --dump-models doesn't exist in Z3. I could write (dump-model) after (check-sat) in the SMT2lib file, but that errors out if the formula is actually unsat.

The language of SMT2 lib though looks lispish, is far from being a properly interpreted interactive language. For example, something like (cond (check-sat) (dump-model)) should work.

In any case, being new to the Z3 source code, I've hacked up something, and thought I'd share it with the dev team. I have inlined a patch (not knowing how to attach stuff in stackoverflow), which if incorporated in the mainline, that would be great. Let me know if there is a better way of doing the same thing.

Also, apologies if this is not the right forum for this type of discussion. Please let me know then the correct avenue.

I also have some Z3 performance related questions on seemingly simple queries, which CVC4 is able to solve easily, that I'll reserve for the future discussion.

Thanks,

Pankaj

Patch begins:

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;
             }

Patch ends

Answer 1

I added dump-models option to the unstable branch. commit 3d7785c..fc3e1af