mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 11:26:21 +00:00
Code Activity

Refactor find_probe() to use std::optional (#8334)

Browse source 
* Initial plan

* Refactor find_probe() to use std::optional

- Updated tactic_manager.h: Changed return type to std::optional<probe_info*>
- Updated tactic_manager.cpp: Modified implementation to return std::nullopt or probe pointer
- Updated api_tactic.cpp: Changed 2 call sites to use optional checks and dereference
- Updated tactic_cmds.cpp: Changed 1 call site to use optional check and dereference
- Build verified successfully
- Probe functionality tested with Python bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-01-25 15:13:36 -08:00 • committed by GitHub
parent 2ac78b6def
commit 49817bc259
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 14 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/api/api_tactic.cpp
View file

@ -91,12 +91,12 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_probe(c, name); LOG_Z3_mk_probe(c, name);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
probe_info * p = mk_c(c)->find_probe(symbol(name)); auto p = mk_c(c)->find_probe(symbol(name));
if (p == nullptr) { if (!p) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
RETURN_Z3(nullptr); RETURN_Z3(nullptr);
} }
probe * new_p = p->get(); probe * new_p = (*p)->get();
RETURN_PROBE(new_p); RETURN_PROBE(new_p);
Z3_CATCH_RETURN(nullptr); Z3_CATCH_RETURN(nullptr);
} }
@ -404,12 +404,12 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_probe_get_descr(c, name); LOG_Z3_probe_get_descr(c, name);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
probe_info * p = mk_c(c)->find_probe(symbol(name)); auto p = mk_c(c)->find_probe(symbol(name));
if (p == nullptr) { if (!p) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return ""; return "";
} }
return p->get_descr(); return (*p)->get_descr();
Z3_CATCH_RETURN(""); Z3_CATCH_RETURN("");
} }

6
src/cmd_context/tactic_cmds.cpp
View file

@ -767,9 +767,9 @@ MK_NARY_PROBE(mk_mul);
probe * sexpr2probe(cmd_context & ctx, sexpr * n) { probe * sexpr2probe(cmd_context & ctx, sexpr * n) {
if (n->is_symbol()) { if (n->is_symbol()) {
probe_info * pinfo = ctx.find_probe(n->get_symbol()); auto pinfo = ctx.find_probe(n->get_symbol());
if (pinfo != nullptr) if (pinfo)
return pinfo->get(); return (*pinfo)->get();
throw cmd_exception("invalid probe, unknown builtin probe ", n->get_symbol(), n->get_line(), n->get_pos()); throw cmd_exception("invalid probe, unknown builtin probe ", n->get_symbol(), n->get_line(), n->get_pos());
} }
else if (n->is_numeral()) { else if (n->is_numeral()) {

7
src/cmd_context/tactic_manager.cpp
View file

@ -70,9 +70,10 @@ simplifier_cmd * tactic_manager::find_simplifier_cmd(symbol const & s) const {
return c; return c;
} }
probe_info * tactic_manager::find_probe(symbol const & s) const { std::optional<probe_info*> tactic_manager::find_probe(symbol const & s) const {
probe_info * p = nullptr; probe_info * p = nullptr;
m_name2probe.find(s, p); if (m_name2probe.find(s, p))
return p; return p;
return std::nullopt;
} }

2
src/cmd_context/tactic_manager.h
View file

@ -38,7 +38,7 @@ public:
void insert(simplifier_cmd* c); void insert(simplifier_cmd* c);
void insert(probe_info * p); void insert(probe_info * p);
std::optional<tactic_cmd*> find_tactic_cmd(symbol const & s) const; std::optional<tactic_cmd*> find_tactic_cmd(symbol const & s) const;
probe_info * find_probe(symbol const & s) const; std::optional<probe_info*> find_probe(symbol const & s) const;
simplifier_cmd* find_simplifier_cmd(symbol const& s) const; simplifier_cmd* find_simplifier_cmd(symbol const& s) const;
unsigned num_tactics() const { return m_tactics.size(); } unsigned num_tactics() const { return m_tactics.size(); }