mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

api: avoid copying param_refs whenever possible

Browse source
This commit is contained in:
Nuno Lopes 2020-11-06 10:51:51 +00:00
parent d0d06c288a
commit 30fd01b526
5 changed files with 15 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_ast.cpp
View file

@ -740,7 +740,7 @@ extern "C" {
RESET_ERROR_CODE(); RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m(); ast_manager & m = mk_c(c)->m();
expr * a = to_expr(_a); expr * a = to_expr(_a);
params_ref p = to_param_ref(_p); auto &p = to_param_ref(_p);
unsigned timeout = p.get_uint("timeout", mk_c(c)->get_timeout()); unsigned timeout = p.get_uint("timeout", mk_c(c)->get_timeout());
bool use_ctrl_c = p.get_bool("ctrl_c", false); bool use_ctrl_c = p.get_bool("ctrl_c", false);
th_rewriter m_rw(m, p); th_rewriter m_rw(m, p);

3
src/api/api_opt.cpp
View file

@ -230,8 +230,7 @@ extern "C" {
param_descrs descrs; param_descrs descrs;
to_optimize_ptr(o)->collect_param_descrs(descrs); to_optimize_ptr(o)->collect_param_descrs(descrs);
to_params(p)->m_params.validate(descrs); to_params(p)->m_params.validate(descrs);
params_ref pr = to_param_ref(p); to_optimize_ptr(o)->updt_params(to_param_ref(p));
to_optimize_ptr(o)->updt_params(pr);
Z3_CATCH; Z3_CATCH;
} }

11
src/api/api_solver.cpp
View file

@ -367,22 +367,23 @@ extern "C" {
LOG_Z3_solver_set_params(c, s, p); LOG_Z3_solver_set_params(c, s, p);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
symbol logic = to_param_ref(p).get_sym("smt.logic", symbol::null); auto &params = to_param_ref(p);
symbol logic = params.get_sym("smt.logic", symbol::null);
if (logic != symbol::null) { if (logic != symbol::null) {
to_solver(s)->m_logic = logic; to_solver(s)->m_logic = logic;
} }
if (to_solver(s)->m_solver) { if (to_solver(s)->m_solver) {
bool old_model = to_solver(s)->m_params.get_bool("model", true); bool old_model = to_solver(s)->m_params.get_bool("model", true);
bool new_model = to_param_ref(p).get_bool("model", true); bool new_model = params.get_bool("model", true);
if (old_model != new_model) if (old_model != new_model)
to_solver_ref(s)->set_produce_models(new_model); to_solver_ref(s)->set_produce_models(new_model);
param_descrs r; param_descrs r;
to_solver_ref(s)->collect_param_descrs(r); to_solver_ref(s)->collect_param_descrs(r);
context_params::collect_solver_param_descrs(r); context_params::collect_solver_param_descrs(r);
to_param_ref(p).validate(r); params.validate(r);
to_solver_ref(s)->updt_params(to_param_ref(p)); to_solver_ref(s)->updt_params(params);
} }
to_solver(s)->m_params.append(to_param_ref(p)); to_solver(s)->m_params.append(params);
init_solver_log(c, s); init_solver_log(c, s);

10
src/api/api_tactic.cpp
View file

@ -226,8 +226,9 @@ extern "C" {
RESET_ERROR_CODE(); RESET_ERROR_CODE();
param_descrs r; param_descrs r;
to_tactic_ref(t)->collect_param_descrs(r); to_tactic_ref(t)->collect_param_descrs(r);
to_param_ref(p).validate(r); auto &params = to_param_ref(p);
tactic * new_t = using_params(to_tactic_ref(t), to_param_ref(p)); params.validate(r);
tactic * new_t = using_params(to_tactic_ref(t), params);
RETURN_TACTIC(new_t); RETURN_TACTIC(new_t);
Z3_CATCH_RETURN(nullptr); Z3_CATCH_RETURN(nullptr);
} }
@ -456,8 +457,9 @@ extern "C" {
RESET_ERROR_CODE(); RESET_ERROR_CODE();
param_descrs pd; param_descrs pd;
to_tactic_ref(t)->collect_param_descrs(pd); to_tactic_ref(t)->collect_param_descrs(pd);
to_param_ref(p).validate(pd); auto &params = to_param_ref(p);
Z3_apply_result r = _tactic_apply(c, t, g, to_param_ref(p)); params.validate(pd);
Z3_apply_result r = _tactic_apply(c, t, g, params);
RETURN_Z3(r); RETURN_Z3(r);
Z3_CATCH_RETURN(nullptr); Z3_CATCH_RETURN(nullptr);
} }

2
src/api/api_util.h
View file

@ -92,7 +92,7 @@ struct Z3_params_ref : public api::object {
inline Z3_params_ref * to_params(Z3_params p) { return reinterpret_cast<Z3_params_ref *>(p); } inline Z3_params_ref * to_params(Z3_params p) { return reinterpret_cast<Z3_params_ref *>(p); }
inline Z3_params of_params(Z3_params_ref * p) { return reinterpret_cast<Z3_params>(p); } inline Z3_params of_params(Z3_params_ref * p) { return reinterpret_cast<Z3_params>(p); }
inline params_ref to_param_ref(Z3_params p) { return p == nullptr ? params_ref() : to_params(p)->m_params; } inline params_ref& to_param_ref(Z3_params p) { return p == nullptr ? const_cast<params_ref&>(params_ref::get_empty()) : to_params(p)->m_params; }
struct Z3_param_descrs_ref : public api::object { struct Z3_param_descrs_ref : public api::object {
param_descrs m_descrs; param_descrs m_descrs;