mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

move parameter validation for when solver object is actually crated

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-15 09:58:54 -07:00
parent 92166eb5cb
commit 136b172b5a
1 changed files with 8 additions and 3 deletions

11
src/api/api_solver.cpp
View file

@ -40,6 +40,10 @@ extern "C" {
params_ref p = s->m_params;
mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled);
s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic);
param_descrs r;
s->m_solver->collect_param_descrs(r);
p.validate(r);
s->m_solver->updt_params(p);
}
@ -130,14 +134,15 @@ extern "C" {
Z3_TRY;
LOG_Z3_solver_set_params(c, s, p);
RESET_ERROR_CODE();
param_descrs r;
to_solver_ref(s)->collect_param_descrs(r);
to_param_ref(p).validate(r);
if (to_solver(s)->m_solver) {
bool old_model = to_solver(s)->m_params.get_bool("model", true);
bool new_model = to_param_ref(p).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);
to_param_ref(p).validate(r);
to_solver_ref(s)->updt_params(to_param_ref(p));
}
to_solver(s)->m_params = to_param_ref(p);