mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

consolidate model.compact and model_compress #2704

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-15 11:06:59 -08:00
parent 1a9dfc5e80
commit cb600a9329
10 changed files with 12 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_opt.cpp
View file

@ -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 {

4
src/api/api_solver.cpp
View file

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

4
src/cmd_context/cmd_context.cpp
View file

@ -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());

6
src/cmd_context/context_params.cpp
View file

@ -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");

1
src/cmd_context/context_params.h
View file

@ -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.

2
src/model/model_params.pyg
View file

@ -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'),
))

4
src/smt/params/smt_params.cpp
View file

@ -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);

2
src/smt/params/smt_params.h
View file

@ -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),

2
src/smt/smt_context.cpp
View file

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

3
src/solver/solver.cpp
View file

@ -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);