From 76d46ee48aa3896c4eec9649e472d7b551647221 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 26 Jan 2026 13:20:03 -0800
Subject: [PATCH] Revert "Refactor find_tactic_cmd to use
 std::optional<tactic_cmd*> (#8331)"

This reverts commit 7b182c9440b1e8d6626b88e4b32cbda62322d21f.
---
 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, 13 insertions(+), 15 deletions(-)

diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp
index 4ecec02c8..e0038d8b7 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();
-        auto t = mk_c(c)->find_tactic_cmd(symbol(name));
-        if (!t) {
+        tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name));
+        if (t == nullptr) {
             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();
-        auto t = mk_c(c)->find_tactic_cmd(symbol(name));
-        if (!t) {
+        tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name));
+        if (t == nullptr) {
             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 9f0b5d159..c183a816c 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()) {
-        auto cmd = ctx.find_tactic_cmd(n->get_symbol());
-        if (cmd)
-            return (*cmd)->mk(ctx.m());
+        tactic_cmd * cmd = ctx.find_tactic_cmd(n->get_symbol());
+        if (cmd != nullptr)
+            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 d2dfe1c2c..1691f5b45 100644
--- a/src/cmd_context/tactic_manager.cpp
+++ b/src/cmd_context/tactic_manager.cpp
@@ -57,11 +57,10 @@ void tactic_manager::insert(probe_info * p) {
     m_probes.push_back(p);
 }
 
-std::optional<tactic_cmd*> tactic_manager::find_tactic_cmd(symbol const & s) const {
+tactic_cmd * tactic_manager::find_tactic_cmd(symbol const & s) const {
     tactic_cmd * c = nullptr;
-    if (m_name2tactic.find(s, c))
-        return c;
-    return std::nullopt;
+    m_name2tactic.find(s, c);
+    return c;
 }
 
 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 e9f9d9569..b1e48a5ed 100644
--- a/src/cmd_context/tactic_manager.h
+++ b/src/cmd_context/tactic_manager.h
@@ -20,7 +20,6 @@ Notes:
 #include "cmd_context/tactic_cmds.h"
 #include "cmd_context/simplifier_cmds.h"
 #include "util/dictionary.h"
-#include <optional>
 
 class tactic_manager {
 protected:
@@ -37,7 +36,7 @@ public:
     void insert(tactic_cmd * c);
     void insert(simplifier_cmd* c);
     void insert(probe_info * p);
-    std::optional<tactic_cmd*> find_tactic_cmd(symbol const & s) const; 
+    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;