mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

make sure parser context within solver object has its parameters updated

Browse source 
this is to enable use cases like:

```
from z3 import *

s = Solver()
OnClause(s, print)
s.set("solver.proof.check", False)
s.from_file("../satproof.smt2")
```

instead of setting global parameters before the proof replay is initialized.
This commit is contained in:
Nikolaj Bjorner 2022-11-23 07:55:49 +07:00
parent 477b90228e
commit 5c5673bc09
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/api/api_solver.cpp
View file

@ -406,7 +406,11 @@ extern "C" {
params.validate(r); params.validate(r);
to_solver_ref(s)->updt_params(params); to_solver_ref(s)->updt_params(params);
} }
to_solver(s)->m_params.append(params); auto& solver = *to_solver(s);
solver.m_params.append(params);
if (solver.m_cmd_context && solver.m_cmd_context->get_proof_cmds())
solver.m_cmd_context->get_proof_cmds()->updt_params(solver.m_params);
init_solver_log(c, s); init_solver_log(c, s);
@ -937,8 +941,10 @@ extern "C" {
install_proof_cmds(*solver.m_cmd_context); install_proof_cmds(*solver.m_cmd_context);
} }
if (!solver.m_cmd_context->get_proof_cmds()) if (!solver.m_cmd_context->get_proof_cmds()) {
init_proof_cmds(*solver.m_cmd_context); init_proof_cmds(*solver.m_cmd_context);
solver.m_cmd_context->get_proof_cmds()->updt_params(solver.m_params);
}
solver.m_cmd_context->get_proof_cmds()->register_on_clause(user_context, _on_clause); solver.m_cmd_context->get_proof_cmds()->register_on_clause(user_context, _on_clause);
Z3_CATCH; Z3_CATCH;
} }