From 49817bc2591ea31453ed55fd4af7a294da14a49f Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 25 Jan 2026 15:13:36 -0800 Subject: [PATCH] Refactor find_probe() to use std::optional (#8334) * Initial plan * Refactor find_probe() to use std::optional - Updated tactic_manager.h: Changed return type to std::optional - 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> --- src/api/api_tactic.cpp | 12 ++++++------ src/cmd_context/tactic_cmds.cpp | 6 +++--- src/cmd_context/tactic_manager.cpp | 7 ++++--- src/cmd_context/tactic_manager.h | 2 +- 4 files changed, 14 insertions(+), 13 deletions(-) diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 4ecec02c8..e6e879995 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -91,12 +91,12 @@ extern "C" { Z3_TRY; LOG_Z3_mk_probe(c, name); RESET_ERROR_CODE(); - probe_info * p = mk_c(c)->find_probe(symbol(name)); - if (p == nullptr) { + auto p = mk_c(c)->find_probe(symbol(name)); + if (!p) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } - probe * new_p = p->get(); + probe * new_p = (*p)->get(); RETURN_PROBE(new_p); Z3_CATCH_RETURN(nullptr); } @@ -404,12 +404,12 @@ extern "C" { Z3_TRY; LOG_Z3_probe_get_descr(c, name); RESET_ERROR_CODE(); - probe_info * p = mk_c(c)->find_probe(symbol(name)); - if (p == nullptr) { + auto p = mk_c(c)->find_probe(symbol(name)); + if (!p) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return ""; } - return p->get_descr(); + return (*p)->get_descr(); Z3_CATCH_RETURN(""); } diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 9f0b5d159..00abefeaa 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -767,9 +767,9 @@ MK_NARY_PROBE(mk_mul); probe * sexpr2probe(cmd_context & ctx, sexpr * n) { if (n->is_symbol()) { - probe_info * pinfo = ctx.find_probe(n->get_symbol()); - if (pinfo != nullptr) - return pinfo->get(); + auto pinfo = ctx.find_probe(n->get_symbol()); + if (pinfo) + return (*pinfo)->get(); throw cmd_exception("invalid probe, unknown builtin probe ", n->get_symbol(), n->get_line(), n->get_pos()); } else if (n->is_numeral()) { diff --git a/src/cmd_context/tactic_manager.cpp b/src/cmd_context/tactic_manager.cpp index d2dfe1c2c..f5dff041f 100644 --- a/src/cmd_context/tactic_manager.cpp +++ b/src/cmd_context/tactic_manager.cpp @@ -70,9 +70,10 @@ simplifier_cmd * tactic_manager::find_simplifier_cmd(symbol const & s) const { return c; } -probe_info * tactic_manager::find_probe(symbol const & s) const { +std::optional tactic_manager::find_probe(symbol const & s) const { probe_info * p = nullptr; - m_name2probe.find(s, p); - return p; + if (m_name2probe.find(s, p)) + return p; + return std::nullopt; } diff --git a/src/cmd_context/tactic_manager.h b/src/cmd_context/tactic_manager.h index e9f9d9569..cc0afe7e0 100644 --- a/src/cmd_context/tactic_manager.h +++ b/src/cmd_context/tactic_manager.h @@ -38,7 +38,7 @@ public: void insert(simplifier_cmd* c); void insert(probe_info * p); std::optional find_tactic_cmd(symbol const & s) const; - probe_info * find_probe(symbol const & s) const; + std::optional find_probe(symbol const & s) const; simplifier_cmd* find_simplifier_cmd(symbol const& s) const; unsigned num_tactics() const { return m_tactics.size(); }