From d634c945bfb85d876ee3d48c9b85bde90e4d5a3d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Dec 2012 13:44:39 -0800 Subject: [PATCH] renamed validate_model --> model_validate Signed-off-by: Leonardo de Moura --- src/api/z3_api.h | 2 +- src/cmd_context/cmd_context.cpp | 2 +- src/cmd_context/context_params.cpp | 8 ++++---- src/cmd_context/context_params.h | 2 +- src/smt/params/smt_params.cpp | 2 +- 5 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 16bf9193c..07748e0e1 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1312,7 +1312,7 @@ extern "C" { - well_sorted_check type checker - auto_config use heuristics to automatically select solver and configure it - model model generation for solvers, this parameter can be overwritten when creating a solver - - validate_model validate models produced by solvers + - model_validate validate models produced by solvers - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver \sa Z3_set_param_value diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 19fbdcd3c..c6bfeb663 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -393,7 +393,7 @@ bool cmd_context::well_sorted_check_enabled() const { } bool cmd_context::validate_model_enabled() const { - return m_params.m_validate_model; + return m_params.m_model_validate; } cmd_context::check_sat_state cmd_context::cs_state() const { diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp index c7efa0d8d..495f73b75 100644 --- a/src/cmd_context/context_params.cpp +++ b/src/cmd_context/context_params.cpp @@ -62,8 +62,8 @@ void context_params::set(char const * param, char const * value) { else if (p == "model") { set_bool(m_model, param, value); } - else if (p == "validate_model") { - set_bool(m_validate_model, param, value); + else if (p == "model_validate") { + set_bool(m_model_validate, param, value); } else if (p == "trace") { set_bool(m_trace, param, value); @@ -92,7 +92,7 @@ void context_params::updt_params(params_ref const & p) { m_auto_config = p.get_bool("auto_config", true); m_proof = p.get_bool("proof", false); m_model = p.get_bool("model", true); - m_validate_model = p.get_bool("validate_model", false); + m_model_validate = p.get_bool("model_validate", false); m_trace = p.get_bool("trace", false); m_trace_file_name = p.get_str("trace_file_name", "z3.log"); m_unsat_core = p.get_bool("unsat_core", false); @@ -106,7 +106,7 @@ void context_params::collect_param_descrs(param_descrs & d) { d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true"); d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false"); d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true"); - d.insert("validate_model", CPK_BOOL, "validate models produced by solvers", "false"); + d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "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("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false"); diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h index 0fe4da93e..6b42b5b50 100644 --- a/src/cmd_context/context_params.h +++ b/src/cmd_context/context_params.h @@ -33,7 +33,7 @@ public: std::string m_trace_file_name; bool m_well_sorted_check; bool m_model; - bool m_validate_model; + bool m_model_validate; bool m_unsat_core; unsigned m_timeout; diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 70f0ad811..fb5ada715 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -43,7 +43,7 @@ void smt_params::updt_params(context_params const & p) { m_auto_config = p.m_auto_config; m_soft_timeout = p.m_timeout; m_model = p.m_model; - m_model_validate = p.m_validate_model; + m_model_validate = p.m_model_validate; m_proof_mode = p.m_proof ? PGM_FINE : PGM_DISABLED; }