From 7b182c9440b1e8d6626b88e4b32cbda62322d21f Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Sun, 25 Jan 2026 12:38:34 -0800
Subject: [PATCH] Refactor find_tactic_cmd to use std::optional<tactic_cmd*>
 (#8331)

* Initial plan

* Refactor find_tactic_cmd to use std::optional<tactic_cmd*>

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   |  3 ++-
 4 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp
index e0038d8b7..4ecec02c8 100644
--- a/src/api/api_tactic.cpp
+++ b/src/api/api_tactic.cpp
@@ -59,14 +59,14 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_tactic(c, name);
         RESET_ERROR_CODE();
-        tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name));
-        if (t == nullptr) {
+        auto t = mk_c(c)->find_tactic_cmd(symbol(name));
+        if (!t) {
             std::stringstream err;
             err << "unknown tactic " << name;
             SET_ERROR_CODE(Z3_INVALID_ARG, err.str());
             RETURN_Z3(nullptr);
         }
-        tactic * new_t = t->mk(mk_c(c)->m());
+        tactic * new_t = (*t)->mk(mk_c(c)->m());
         RETURN_TACTIC(new_t);
         Z3_CATCH_RETURN(nullptr);
     }
@@ -391,12 +391,12 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_tactic_get_descr(c, name);
         RESET_ERROR_CODE();
-        tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name));
-        if (t == nullptr) {
+        auto t = mk_c(c)->find_tactic_cmd(symbol(name));
+        if (!t) {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
             return "";
         }
-        return t->get_descr();
+        return (*t)->get_descr();
         Z3_CATCH_RETURN("");
     }
     
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index c183a816c..9f0b5d159 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -654,9 +654,9 @@ static tactic * mk_skip_if_failed(cmd_context & ctx, sexpr * n) {
 
 tactic * sexpr2tactic(cmd_context & ctx, sexpr * n) {
     if (n->is_symbol()) {
-        tactic_cmd * cmd = ctx.find_tactic_cmd(n->get_symbol());
-        if (cmd != nullptr)
-            return cmd->mk(ctx.m());
+        auto cmd = ctx.find_tactic_cmd(n->get_symbol());
+        if (cmd)
+            return (*cmd)->mk(ctx.m());
         sexpr * decl = ctx.find_user_tactic(n->get_symbol());
         if (decl != nullptr)
             return sexpr2tactic(ctx, decl);
diff --git a/src/cmd_context/tactic_manager.cpp b/src/cmd_context/tactic_manager.cpp
index 1691f5b45..d2dfe1c2c 100644
--- a/src/cmd_context/tactic_manager.cpp
+++ b/src/cmd_context/tactic_manager.cpp
@@ -57,10 +57,11 @@ void tactic_manager::insert(probe_info * p) {
     m_probes.push_back(p);
 }
 
-tactic_cmd * tactic_manager::find_tactic_cmd(symbol const & s) const {
+std::optional<tactic_cmd*> tactic_manager::find_tactic_cmd(symbol const & s) const {
     tactic_cmd * c = nullptr;
-    m_name2tactic.find(s, c);
-    return c;
+    if (m_name2tactic.find(s, c))
+        return c;
+    return std::nullopt;
 }
 
 simplifier_cmd * tactic_manager::find_simplifier_cmd(symbol const & s) const {
diff --git a/src/cmd_context/tactic_manager.h b/src/cmd_context/tactic_manager.h
index b1e48a5ed..e9f9d9569 100644
--- a/src/cmd_context/tactic_manager.h
+++ b/src/cmd_context/tactic_manager.h
@@ -20,6 +20,7 @@ Notes:
 #include "cmd_context/tactic_cmds.h"
 #include "cmd_context/simplifier_cmds.h"
 #include "util/dictionary.h"
+#include <optional>
 
 class tactic_manager {
 protected:
@@ -36,7 +37,7 @@ public:
     void insert(tactic_cmd * c);
     void insert(simplifier_cmd* c);
     void insert(probe_info * p);
-    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;     
     simplifier_cmd* find_simplifier_cmd(symbol const& s) const;