diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 94bd4f5e1..aa2b7b289 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -21,14 +21,12 @@ Notes: #include"ast_smt2_pp.h" #include"ast_pp.h" #include"model_smt2_pp.h" -#include"model_v2_pp.h" #include"array_decl_plugin.h" #include"pp.h" #include"cmd_util.h" #include"simplify_cmd.h" #include"eval_cmd.h" #include"gparams.h" -#include"model_params.hpp" #include"env_params.h" class help_cmd : public cmd { @@ -105,17 +103,7 @@ ATOMIC_CMD(get_model_cmd, "get-model", "retrieve model for the last check-sat co throw cmd_exception("model is not available"); model_ref m; ctx.get_check_sat_result()->get_model(m); - model_params p; - if (p.v1() || p.v2()) { - std::ostringstream buffer; - model_v2_pp(buffer, *m, p.partial()); - ctx.regular_stream() << "\"" << escaped(buffer.str().c_str(), true) << "\"" << std::endl; - } else { - ctx.regular_stream() << "(model " << std::endl; - model_smt2_pp(ctx.regular_stream(), ctx, *(m.get()), 2); - // m->display(ctx.regular_stream()); - ctx.regular_stream() << ")" << std::endl; - } + ctx.display_model(m); }); ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", { diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 3becba284..8fda13289 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -41,6 +41,8 @@ Notes: #include"scoped_timer.h" #include"interpolant_cmds.h" #include"model_smt2_pp.h" +#include"model_v2_pp.h" +#include"model_params.hpp" func_decls::func_decls(ast_manager & m, func_decl * f): m_decls(TAG(func_decl*, f, 0)) { @@ -1409,11 +1411,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions if (get_opt()->print_model()) { model_ref mdl; get_opt()->get_model(mdl); - if (mdl) { - regular_stream() << "(model " << std::endl; - model_smt2_pp(regular_stream(), *this, *(mdl.get()), 2); - regular_stream() << ")" << std::endl; - } + display_model(mdl); } r = get_opt()->optimize(); } @@ -1456,9 +1454,29 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions } display_sat_result(r); validate_check_sat_result(r); - if (r == l_true) + if (r == l_true) { validate_model(); + if (m_params.m_dump_models) { + model_ref md; + get_check_sat_result()->get_model(md); + display_model(md); + } + } +} +void cmd_context::display_model(model_ref& mdl) { + if (mdl) { + model_params p; + if (p.v1() || p.v2()) { + std::ostringstream buffer; + model_v2_pp(buffer, *mdl, p.partial()); + regular_stream() << "\"" << escaped(buffer.str().c_str(), true) << "\"" << std::endl; + } else { + regular_stream() << "(model " << std::endl; + model_smt2_pp(regular_stream(), *this, *mdl, 2); + regular_stream() << ")" << std::endl; + } + } } void cmd_context::display_sat_result(lbool r) { diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 81f819e3a..86563eb9b 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -325,6 +325,7 @@ public: check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); } check_sat_state cs_state() const; void validate_model(); + void display_model(model_ref& mdl); void register_plugin(symbol const & name, decl_plugin * p, bool install_names); bool is_func_decl(symbol const & s) const; diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index 8eee593d9..70f110c92 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -27,6 +27,7 @@ context_params::context_params() { m_unsat_core = false; m_model = true; m_model_validate = false; + m_dump_models = false; m_auto_config = true; m_proof = false; m_trace = false; @@ -79,6 +80,9 @@ void context_params::set(char const * param, char const * value) { else if (p == "model_validate") { set_bool(m_model_validate, param, value); } + else if (p == "dump_models") { + set_bool(m_dump_models, param, value); + } else if (p == "trace") { set_bool(m_trace, param, value); } @@ -116,6 +120,7 @@ void context_params::updt_params(params_ref const & p) { m_proof = p.get_bool("proof", m_proof); m_model = p.get_bool("model", m_model); m_model_validate = p.get_bool("model_validate", m_model_validate); + m_dump_models = p.get_bool("dump_models", m_dump_models); m_trace = p.get_bool("trace", m_trace); m_trace_file_name = p.get_str("trace_file_name", "z3.log"); m_unsat_core = p.get_bool("unsat_core", m_unsat_core); @@ -129,6 +134,7 @@ void context_params::collect_param_descrs(param_descrs & d) { d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true"); d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true"); d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "false"); + d.insert("dump_models", CPK_BOOL, "dump models whenever check-sat returns sat", "false"); d.insert("trace", CPK_BOOL, "trace generation for VCC", "false"); d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log"); d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false"); diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index eb250f486..bdd77fb1c 100644 --- a/src/cmd_context/context_params.h +++ b/src/cmd_context/context_params.h @@ -36,6 +36,7 @@ public: bool m_well_sorted_check; bool m_model; bool m_model_validate; + bool m_dump_models; bool m_unsat_core; bool m_smtlib2_compliant; // it must be here because it enable/disable the use of coercions in the ast_manager. unsigned m_timeout;