mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
add dump_models option per suggestion from Pankaj Chauhan
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
3d7785cc18
commit
fc3e1af4a9
|
@ -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", {
|
||||
|
|
|
@ -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) {
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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");
|
||||
|
|
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue