diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 8256fc0e2..1eed57b8c 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -21,6 +21,7 @@ Revision History: #include "util/scoped_ctrl_c.h" #include "util/file_path.h" #include "parsers/smt2/smt2parser.h" +#include "model/model_params.hpp" #include "opt/opt_context.h" #include "opt/opt_cmds.h" #include "opt/opt_parse.h" @@ -210,7 +211,8 @@ extern "C" { to_optimize_ptr(o)->get_model(_m); Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); if (_m) { - if (mk_c(c)->params().m_model_compress) _m->compress(); + model_params mp(to_optimize_ptr(o)->get_params()); + if (mp.compact()) _m->compress(); m_ref->m_model = _m; } else { diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index e67c7a215..8dc6f39e0 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -31,6 +31,7 @@ Revision History: #include "api/api_model.h" #include "api/api_stats.h" #include "api/api_ast_vector.h" +#include "model/model_params.hpp" #include "smt/smt_solver.h" #include "smt/smt_implied_equalities.h" #include "solver/smt_logics.h" @@ -618,7 +619,8 @@ extern "C" { RETURN_Z3(nullptr); } if (_m) { - if (mk_c(c)->params().m_model_compress) _m->compress(); + model_params mp(to_solver_ref(s)->get_params()); + if (mp.compact()) _m->compress(); } Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); m_ref->m_model = _m; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 8e844a406..ebf51c794 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1674,9 +1674,9 @@ void cmd_context::display_dimacs() { void cmd_context::display_model(model_ref& mdl) { if (mdl) { if (m_mc0) (*m_mc0)(mdl); - if (m_params.m_model_compress) mdl->compress(); - add_declared_functions(*mdl); model_params p; + if (p.compact()) mdl->compress(); + add_declared_functions(*mdl); if (p.v1() || p.v2()) { std::ostringstream buffer; model_v2_pp(buffer, *mdl, p.partial()); diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index 447718aa9..fd5892217 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -34,7 +34,6 @@ context_params::context_params() { m_debug_ref_count = false; m_smtlib2_compliant = false; m_well_sorted_check = false; - m_model_compress = true; m_timeout = UINT_MAX; m_rlimit = 0; m_statistics = false; @@ -104,9 +103,6 @@ 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 == "model_compress") { - set_bool(m_model_compress, param, value); - } else if (p == "dump_models") { set_bool(m_dump_models, param, value); } @@ -154,7 +150,6 @@ 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_model_compress = p.get_bool("model_compress", m_model_compress); 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"); @@ -172,7 +167,6 @@ 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("model_compress", CPK_BOOL, "compress models for easier consumption", "true"); 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"); diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index f00d39641..837381665 100644 --- a/src/cmd_context/context_params.h +++ b/src/cmd_context/context_params.h @@ -40,7 +40,6 @@ public: bool m_well_sorted_check; bool m_model; bool m_model_validate; - bool m_model_compress; 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. diff --git a/src/model/model_params.pyg b/src/model/model_params.pyg index c108d1f34..7e370cb3a 100644 --- a/src/model/model_params.pyg +++ b/src/model/model_params.pyg @@ -3,7 +3,7 @@ def_module_params('model', params=(('partial', BOOL, False, 'enable/disable partial function interpretations'), ('v1', BOOL, False, 'use Z3 version 1.x pretty printer'), ('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'), - ('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'), + ('compact', BOOL, True, 'try to compact function graph (i.e., function interpretations that are lookup tables)'), ('inline_def', BOOL, False, 'inline local function definitions ignoring possible expansion'), ('completion', BOOL, False, 'enable/disable model completion'), )) diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 89147165c..f89830aee 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -18,7 +18,6 @@ Revision History: --*/ #include "smt/params/smt_params.h" #include "smt/params/smt_params_helper.hpp" -#include "model/model_params.hpp" #include "util/gparams.h" void smt_params::updt_local_params(params_ref const & _p) { @@ -42,8 +41,6 @@ void smt_params::updt_local_params(params_ref const & _p) { m_core_validate = p.core_validate(); m_logic = _p.get_sym("logic", m_logic); m_string_solver = p.string_solver(); - model_params mp(_p); - m_model_compact = mp.compact(); if (_p.get_bool("arith.greatest_error_pivot", false)) m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR; else if (_p.get_bool("arith.least_error_pivot", false)) @@ -144,7 +141,6 @@ void smt_params::display(std::ostream & out) const { DISPLAY_PARAM(m_display_ll_bool_var2expr); DISPLAY_PARAM(m_model); - DISPLAY_PARAM(m_model_compact); DISPLAY_PARAM(m_model_on_timeout); DISPLAY_PARAM(m_model_on_final_check); diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 45f287f4f..0acbf164a 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -188,7 +188,6 @@ struct smt_params : public preprocessor_params, // // ----------------------------------- bool m_model; - bool m_model_compact; bool m_model_on_timeout; bool m_model_on_final_check; @@ -291,7 +290,6 @@ struct smt_params : public preprocessor_params, m_display_bool_var2expr(false), m_display_ll_bool_var2expr(false), m_model(true), - m_model_compact(false), m_model_on_timeout(false), m_model_on_final_check(false), m_progress_sampling_freq(0), diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index d47e8dde3..1c64901c3 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4387,8 +4387,6 @@ namespace smt { m_proto_model->complete_partial_funcs(false); TRACE("mbqi_bug", tout << "before cleanup:\n"; model_pp(tout, *m_proto_model);); m_proto_model->cleanup(); - if (m_fparams.m_model_compact) - m_proto_model->compress(); TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model);); IF_VERBOSE(11, model_pp(verbose_stream(), *m_proto_model);); } diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 36a0dd80c..5852be0d1 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -26,6 +26,7 @@ Notes: #include "solver/solver.h" #include "solver/solver_params.hpp" #include "model/model_evaluator.h" +#include "model/model_params.hpp" unsigned solver::get_num_assertions() const { @@ -228,6 +229,8 @@ void solver::assert_expr(expr* f, expr* t) { void solver::collect_param_descrs(param_descrs & r) { solver_params sp(m_params); sp.collect_param_descrs(r); + model_params mp(m_params); + mp.collect_param_descrs(r); insert_timeout(r); insert_rlimit(r); insert_max_memory(r);