mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-03 13:56:08 +00:00
Code Activity

Remove const_cast from smt_solver context access

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-06-12 06:15:29 +00:00 • committed by GitHub
parent a3f07ba9ab
commit 4b7e4cf08a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 17 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/smt_context.h
View file

@ -294,6 +294,10 @@ namespace smt {
return m_fparams; return m_fparams;
} }
smt_params const& get_fparams() const {
return m_fparams;
}
params_ref const & get_params() { params_ref const & get_params() {
return m_params; return m_params;
} }
@ -1921,4 +1925,3 @@ namespace smt {
std::ostream& operator<<(std::ostream& out, enode_pp const& p); std::ostream& operator<<(std::ostream& out, enode_pp const& p);
}; };

4
src/smt/smt_kernel.cpp
View file

@ -292,6 +292,10 @@ namespace smt {
return m_imp->m_kernel; return m_imp->m_kernel;
} }
context const& kernel::get_context() const {
return m_imp->m_kernel;
}
void kernel::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) { void kernel::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) {
m_imp->m_kernel.get_levels(vars, depth); m_imp->m_kernel.get_levels(vars, depth);
} }

2
src/smt/smt_kernel.h
View file

@ -344,6 +344,6 @@ namespace smt {
\warning This method should not be used in new code. \warning This method should not be used in new code.
*/ */
context & get_context(); context & get_context();
context const& get_context() const;
}; };
}; };

17
src/smt/smt_solver.cpp
View file

@ -221,7 +221,7 @@ namespace {
expr_ref_vector get_assigned_literals() override { expr_ref_vector get_assigned_literals() override {
expr_ref_vector result(m); expr_ref_vector result(m);
auto& ctx = const_cast<smt::kernel&>(m_context).get_context(); auto const& ctx = m_context.get_context();
for (auto lit : ctx.assigned_literals()) { for (auto lit : ctx.assigned_literals()) {
expr* atom = ctx.bool_var2expr(lit.var()); expr* atom = ctx.bool_var2expr(lit.var());
if (!atom) if (!atom)
@ -232,7 +232,7 @@ namespace {
} }
unsigned get_assign_level(expr* e) const override { unsigned get_assign_level(expr* e) const override {
auto& ctx = const_cast<smt::kernel&>(m_context).get_context(); auto const& ctx = m_context.get_context();
expr* atom = e; expr* atom = e;
get_manager().is_not(e, atom); get_manager().is_not(e, atom);
if (!ctx.b_internalized(atom)) if (!ctx.b_internalized(atom))
@ -241,18 +241,18 @@ namespace {
} }
bool is_relevant(expr* e) const override { bool is_relevant(expr* e) const override {
auto& ctx = const_cast<smt::kernel&>(m_context).get_context(); auto const& ctx = m_context.get_context();
expr* atom = e; expr* atom = e;
get_manager().is_not(e, atom); get_manager().is_not(e, atom);
return ctx.b_internalized(atom) && ctx.is_relevant(atom); return ctx.b_internalized(atom) && ctx.is_relevant(atom);
} }
unsigned get_num_bool_vars() const override { unsigned get_num_bool_vars() const override {
return const_cast<smt::kernel&>(m_context).get_context().get_num_bool_vars(); return m_context.get_context().get_num_bool_vars();
} }
sat::bool_var get_bool_var(expr* e) const override { sat::bool_var get_bool_var(expr* e) const override {
auto& ctx = const_cast<smt::kernel&>(m_context).get_context(); auto const& ctx = m_context.get_context();
expr* atom = e; expr* atom = e;
get_manager().is_not(e, atom); get_manager().is_not(e, atom);
return ctx.b_internalized(atom) ? ctx.get_bool_var(atom) : sat::null_bool_var; return ctx.b_internalized(atom) ? ctx.get_bool_var(atom) : sat::null_bool_var;
@ -263,7 +263,7 @@ namespace {
} }
void setup_for_parallel() override { void setup_for_parallel() override {
const_cast<smt::kernel&>(m_context).get_context().setup_for_parallel(); m_context.get_context().setup_for_parallel();
} }
void set_preprocess(bool f) override { void set_preprocess(bool f) override {
@ -271,12 +271,12 @@ namespace {
} }
void set_max_conflicts(unsigned max_conflicts) override { void set_max_conflicts(unsigned max_conflicts) override {
auto& ctx = const_cast<smt::kernel&>(m_context).get_context(); auto& ctx = m_context.get_context();
ctx.get_fparams().m_max_conflicts = max_conflicts; ctx.get_fparams().m_max_conflicts = max_conflicts;
} }
unsigned get_max_conflicts() const override { unsigned get_max_conflicts() const override {
return const_cast<smt::kernel&>(m_context).get_context().get_fparams().m_max_conflicts; return m_context.get_context().get_fparams().m_max_conflicts;
} }
void get_backbone_candidates(vector<solver::scored_literal>& candidates, unsigned max_num) override { void get_backbone_candidates(vector<solver::scored_literal>& candidates, unsigned max_num) override {
@ -676,4 +676,3 @@ public:
solver_factory * mk_smt_solver_factory() { solver_factory * mk_smt_solver_factory() {
return alloc(smt_solver_factory); return alloc(smt_solver_factory);
} }