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

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

Browse source 
* 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>
This commit is contained in:
Copilot 2026-01-25 12:38:34 -08:00 • committed by Nikolaj Bjorner
parent 46af26e72c
commit e30c3b3656
4 changed files with 15 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/api/api_tactic.cpp
View file

@ -59,14 +59,14 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_tactic(c, name); LOG_Z3_mk_tactic(c, name);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name)); auto t = mk_c(c)->find_tactic_cmd(symbol(name));
if (t == nullptr) { if (!t) {
std::stringstream err; std::stringstream err;
err << "unknown tactic " << name; err << "unknown tactic " << name;
SET_ERROR_CODE(Z3_INVALID_ARG, err.str()); SET_ERROR_CODE(Z3_INVALID_ARG, err.str());
RETURN_Z3(nullptr); 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); RETURN_TACTIC(new_t);
Z3_CATCH_RETURN(nullptr); Z3_CATCH_RETURN(nullptr);
} }
@ -391,12 +391,12 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_tactic_get_descr(c, name); LOG_Z3_tactic_get_descr(c, name);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name)); auto t = mk_c(c)->find_tactic_cmd(symbol(name));
if (t == nullptr) { if (!t) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return ""; return "";
} }
return t->get_descr(); return (*t)->get_descr();
Z3_CATCH_RETURN(""); Z3_CATCH_RETURN("");
} }

6
src/cmd_context/tactic_cmds.cpp
View file

@ -654,9 +654,9 @@ static tactic * mk_skip_if_failed(cmd_context & ctx, sexpr * n) {
tactic * sexpr2tactic(cmd_context & ctx, sexpr * n) { tactic * sexpr2tactic(cmd_context & ctx, sexpr * n) {
if (n->is_symbol()) { if (n->is_symbol()) {
tactic_cmd * cmd = ctx.find_tactic_cmd(n->get_symbol()); auto cmd = ctx.find_tactic_cmd(n->get_symbol());
if (cmd != nullptr) if (cmd)
return cmd->mk(ctx.m()); return (*cmd)->mk(ctx.m());
sexpr * decl = ctx.find_user_tactic(n->get_symbol()); sexpr * decl = ctx.find_user_tactic(n->get_symbol());
if (decl != nullptr) if (decl != nullptr)
return sexpr2tactic(ctx, decl); return sexpr2tactic(ctx, decl);

7
src/cmd_context/tactic_manager.cpp
View file

@ -57,10 +57,11 @@ void tactic_manager::insert(probe_info * p) {
m_probes.push_back(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; tactic_cmd * c = nullptr;
m_name2tactic.find(s, c); if (m_name2tactic.find(s, c))
return c; return c;
return std::nullopt;
} }
simplifier_cmd * tactic_manager::find_simplifier_cmd(symbol const & s) const { simplifier_cmd * tactic_manager::find_simplifier_cmd(symbol const & s) const {

3
src/cmd_context/tactic_manager.h
View file

@ -20,6 +20,7 @@ Notes:
#include "cmd_context/tactic_cmds.h" #include "cmd_context/tactic_cmds.h"
#include "cmd_context/simplifier_cmds.h" #include "cmd_context/simplifier_cmds.h"
#include "util/dictionary.h" #include "util/dictionary.h"
#include <optional>
class tactic_manager { class tactic_manager {
protected: protected:
@ -36,7 +37,7 @@ public:
void insert(tactic_cmd * c); void insert(tactic_cmd * c);
void insert(simplifier_cmd* c); void insert(simplifier_cmd* c);
void insert(probe_info * p); 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; 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;