mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-13 04:13:01 +00:00
Code Activity

Revert "Refactor find_tactic_cmd to use std::optional<tactic_cmd*> (#8331)"

Browse source 
This reverts commit 7b182c9440.
This commit is contained in:
Nikolaj Bjorner 2026-01-26 13:20:03 -08:00
parent 3f26d42215
commit 76d46ee48a
4 changed files with 13 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/cmd_context/tactic_manager.h
View file

@ -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;