mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Cache param descrs when modifying solver params (#6156)

Browse source
This commit is contained in:
Stefan Muenzel 2022-07-15 01:11:56 +07:00 • committed by GitHub
parent 4a192850f2
commit 2f5fef92b7
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/api/api_solver.cpp
View file

@ -391,9 +391,11 @@ extern "C" {
bool new_model = params.get_bool("model", true);
if (old_model != new_model)
to_solver_ref(s)->set_produce_models(new_model);
param_descrs r;
to_solver_ref(s)->collect_param_descrs(r);
context_params::collect_solver_param_descrs(r);
param_descrs& r = to_solver(s)->m_param_descrs;
if(r.size () == 0) {
to_solver_ref(s)->collect_param_descrs(r);
context_params::collect_solver_param_descrs(r);
}
params.validate(r);
to_solver_ref(s)->updt_params(params);
}

1
src/api/api_solver.h
View file

@ -42,6 +42,7 @@ struct Z3_solver_ref : public api::object {
scoped_ptr<solver_factory> m_solver_factory;
ref<solver> m_solver;
params_ref m_params;
param_descrs m_param_descrs;
symbol m_logic;
scoped_ptr<solver2smt2_pp> m_pp;
scoped_ptr<cmd_context> m_cmd_context;